Provably correct runtime monitoring

Abstract. Runtime monitoring is an established technique for enforc-ing a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Vir-tual Machine. Monitors are security automata given in a special-purpose monitor specication language, ConSpec. The automata operate on nite or innite strings of calls to a xed API, allowing local dependencies on parameter values and heap content. We use a two-level class le annota-tion scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has an instance of the given monitor embedded into it, which yields state changes at prescribed points accord-ing to the monitor's transition function. As our main application of these results we describe a concrete inliner, and use the annotation scheme to characterize its correctness. For this inliner, correctness of the level II annotations can be decided eciently by a weakest precondition annota-tion checker, thus allowing on-device checking of inlining correctness in a proof-carrying code setting.