Towards formalizing the Java security architecture in JDK 1.2

Abstract. The Java security architecture in the Java Development Kit 1.2 expands the current Java sandbox model, allowing ner-grained, con-gurable access control for Java code. This new security architecture per-mits more precise, yet exible, protection for both remote code (loaded across a network connection) and local code (residing on the same ma-chine running the Java Virtual Machine) developed using the Java pro-gramming language. Our formal model and analysis is intended to: (1) allow designers and implementors to understand and correctly use the protection provided by these security controls, and (2) provide guidance to a JVM implementor wishing to support these security controls. Access control decisions in Java are made based on the current execution con-text using stack introspection. To model this, we employ a state-based model that uses multiple access control matrices to model the security controls in JDK 1.2. We also present a safety analysis and discuss the eects of static and dynamic security policies for a given Java Virtual Machine.