Dissertation
Dissertation > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > General issues > Security and confidentiality > Computer equipment safety

Formal Verification of Security Policy and Visualization Realized

Author YangZhiCai
Tutor ZhengXiaoJuan
School Northeast Normal University
Course Computer Software and Theory
Keywords Mobile Code MCC Mobile development platform Formal verification
CLC TP309.1
Type Master's thesis
Year 2011
Downloads 16
Quotes 0
Download Dissertation

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.

Related Dissertations
More Dissertations