Sciweavers

Share
CORR
2010
Springer

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

8 years 6 months ago
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...
Mads Dam, Andreas Lundblad
Added 01 Mar 2011
Updated 01 Mar 2011
Type Journal
Year 2010
Where CORR
Authors Mads Dam, Andreas Lundblad
Comments (0)
books