关键词: 携带模型代码 Java安全机制 安全行为模型 形式验证

Abstract:

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 the consumer of mobile code. MCC mainly includes the specification  of security policies, the generation and verification of the security-related behavior model, and the enforcement of security policies. The Java 2 platf orm is widely used currently. Through the analysis of its access-control-based security architecture, an approach to adding new security policies and the implementation of security-related model verification is presented through modifying and extending the Java 2 kernel classes. The approach can improveJava 2 in supporting security policies, and provides a feasible way to guarantee a more complete security mechanism by implementing MCC based on the Java 2 platform.

Key words: model carrying code;java security mechanism, security related behavior model, formal verification