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

The authors propose a light-weight approach for certification of monitor inlining for sequential Java bytecode using proof-carrying code. The goal is to enable the use of monitoring for quality assurance at development time, while minimizing the need for post-shipping code rewrites as well as changes to the end-host TCB. Standard automaton-based security policies express constraints on allowed API call/return sequences. Proofs are represented as JML-style program annotations. This is adequate in the case as all proofs generated in the framework are recognized in time polynomial in the size of the program.