Efficient Runtime Invariant Checking: A Framework and Case Study
Michael Gorbovitski, Tom Rothamel, Yanhong A. Liu, and Scott D. Stoller

This paper describes a general and powerful framework for efficient runtime invariant checking. The framework supports (1) declarative specification of arbitrary invariants using high-level queries, with easy use of information from any data in the execution, (2) powerful analysis and transformations for automatic generation of instrumentation for efficient incremental checking of invariants, and (3) convenient mechanisms for reporting errors, debugging, and taking preventive or remedial actions, as well as recording history data for use in queries. We demonstrate the advantages and effectiveness of the framework through implementations and case studies with abstract syntax tree transformations, authentication in a SMB client, and implementation of the BitTorrent peer-to-peer file sharing communication protocol.