A formal specification of Java (TM) class leading

The Java Virtual Machine (JVM) has a novel and powerful mechanism to suppor t lazy, dynamic class loading according to user-definable policies. Class l oading directly impacts type safety, on which the security of Java applicat ions is based. Conceptual bugs in the loading mechanism were found in earli er versions of the JVM that lead to type violations. A deeper understanding of the class loading mechanism, through such means as formal analysis, wil l improve our confidence that no additional bugs are present. The work presented in this paper provides a formal specification of (the re levant aspects of) class loading in the JVM and proves its type safety. Our approach to proving type safety is different from the usual ones since cla sses are dynamically loaded and full type information may not be statically available. In addition, we propose an improvement in the interaction betwe en class loading and bytecode verification, which is cleaner and enables la zier loading.