Secure Java class loading

The class loading mechanism, central to Java, plays a key role in JDK 1.2 by enabling an improved security policy that is permission-based and extensible. The author concludes that JDK 1.2 has introduced a powerful and secure class loading mechanism. It not only enforces type safety and name space separation but also has a significant role in the new security architecture that supports fine grained, permission based access control. The new class loading mechanism´s flexibility-through its delegation scheme and the rich set of class loader classes-gives Java applications and applets greater freedom to customize and specify how, when, and from where classes are loaded. Because the class loading mechanism is central to both the correctness and the security of the Java runtime system, we would like to model and define this mechanism, perhaps in a formal verification system. We can then obtain a formal specification and prove (or disprove) that the mechanism as currently designed is sufficient for security