A Proof Carrying Code Framework for Inlined Reference Monitors in Java Bytecode

We propose a lightweight approach for certification of Java bytecode monitor inlining using proof-carrying code. The main purpose of such a framework is to enable development use of monitoring for quality assurance, while minimizing the runtime overhead of monitoring, minimizing the need for changes to the load- and runtime tcb, and eliminating the need for post-shipping code rewrites with the resulting loss of liability. Policies to be enforced are specified in the ConSpec policy specification language which, roughly, express regular sequences of method calls to some fixed API. Proofs are represented as Java class files augmented with logical assertion in Floyd/Hoare logic style: Assertions are associated to each program point as well as to method entry and (exceptional and normal) exit points using standard, JML-style pre- and post-conditions. Such a proof representation is adequate in our case, as all proofs generated in our framework can be recognized in time linear in the size of...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Mads Dam, Andreas Lundblad
• Keywords: ConSpec Policy Specification, CORR 2010, Education, Proof Generation Strategy, Simple Two-state Policy