Proof Linking: An Architecture for Modular Verification of Dynamically-Linked Mobile Code

Security flaws are routinely discovered in commercial implementations of mobile code systems such as the Java Virtual Machine (JVM). Typical architectures for such systems exhibit complex interdependencies between the loader, the verifier, and the linker, making them difficult to craft, validate, and maintain. This reveals a software engineering challenge that is common to all mobile code systems in which a static verification phase is introduced before dynamic linking. In such systems, one has to articulate how loading, verification, and linking interact with each other, and how the three processes should be organized to address various security issues. We propose a standard architecture for crafting mobile code verifiers, based on the concept of proof linking. This architecture modularizes the verification process and isolates the dependencies among the loader, verifier, and linker. We also formalize the process of proof linking and establish properties to which correct implementatio..