Formal Verification Of Security Policy And Visualization Realized

Safe execution of untrusted mobile code is one of the key problems in mobile code security. Model-carrying code (MCC) provides a systematic, complete and effective solution to the problem from the viewpoints of both the producer and t he consumer of mobile code. MCC mainly includes t he specification of security policies, the generation and verification of the security-related behavior model, and the enforcement of security policies.Based on the framework of model-carrying code, we make several improvements: we use the extended pushdown automaton (EPDA) as the program behavior model to avoid impossible paths, and reduce ambiguity in regular expressions over events (REE) that express security policies as extended finite state automata(EFSA). Consequently, we propose a new verification algorithm according to above significant improvements, which is based on a formal proof we demonstrate of the equivalence between defined automata.finally, In Mobile development platform(J2ME) study of mobile code security behavior detection formal verification and support tools development.