Type Safe Dynamic Linking for JVM Access Control

The Java JDK security model provides an access control mechanism for the JVM based on dynamic stack inspection. Previous results have shown how stack inspection can be enforced at compile time via whole-program type analysis, but features of the JVM present significant remaining technical challenges. For instance, dynamic dispatch at the bytecode level requires special consideration to ensure flexibility in typing. Even more problematic is dynamic class loading and linking, which disallow a purely static analysis in principle, though the intended applications of the JDK exploit these features.