Provably Correct Runtime Monitoring
2009 (English)In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 78, no 5, 304-339 p.Article in journal (Refereed) Published
Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual 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 annotation 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 a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.
Place, publisher, year, edition, pages
2009. Vol. 78, no 5, 304-339 p.
Runtime monitoring, Policy enforcement, Monitor inlining, Proof-carrying code
IdentifiersURN: urn:nbn:se:kth:diva-13473DOI: 10.1016/j.jlap.2008.12.002ISI: 000266671300004ScopusID: 2-s2.0-67349154073OAI: oai:DiVA.org:kth-13473DiVA: diva2:325502
QC 201006182010-06-182010-06-182012-03-19Bibliographically approved