Static Analysis Based Invariant Detection for Commodity Operating Systems
The recent interest in runtime attestation requires modeling of a program's runtime behavior to formulate its integrity properties. In this paper, the authors study the possibility of employing static source code analysis to derive integrity models of a commodity operating systems kernel. They develop a precise and static analysis-based global invariant detection tool that overcomes several technical challenges: field-sensitivity, array-sensitivity, pointer analysis, and handling of assembly code. They apply their tool to Linux kernel 2.4.32 and identify 141,279 global invariants that are critical to its runtime integrity.