Abstract
We give a formal specification of the dynamic loading of classes in the Java Virtual Machine (JVM) and of the visibility of mmbers of the loaded classes. This specification is obtained by abstracting out the part of the run-time state of the JVM that is relevant for dynamic loading and visibility, and consists of a set of inference rules defining abstract operations for loading, linking and verifying classes. The formalisation of visibility includes an axiomatisation of the rules for membership of a class under inheritance, and of accessibility of a member in th presence of accessibility modifiers such as private and protected. We believe this specification to be at the right level of abstraction to help reasoning about security properties in Java because it is precise enough to include the security critical features of the language (e.g. visibility rules, dynamic loading and class loaders) and abstract enough to avoid all the irrelevant details (w.r.t. security) of the computer sematics. The contribution of the formalisation is twofold. First, it provides a clear and concise description of the loading process and the rules for member visibility compared to the definitions of the Java language and the JVM. Second, it is sufficiently simple to allow calculations of the effects of load operations in JVM. We demonstrate the usability of this formalisation by applying it to an example, due to Saraswat, of how dynamic loading can affect th visibility in a way that leads to a security breach in the JVM.
Keywords
Java, formal specification, dynamic linking, visibility rules
