Towards Formalizing the Java Security Architecture of JDK 1.2

The Java security architecture in the Java Development Kit 1.2 expands the current Java sandbox model, allowing finer-grained, configurable access control for Java code. This new security architecture permits more precise, yet flexible, protection for both remote code loaded across a network connection and local code residing on the same machine running the Java Virtual Machine developed using the Java programming 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 context 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 effects of static and dynamic security policies for a given Java Virtual Machine.