D.: 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 specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file 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 efficiently by a weakest precondition annota-tion checker, thus allowing on-device checking of inlining correctness in a proof-carrying code setting.