Static analysis based invariant detection for commodity operating systems

Recent interest in runtime attestation requires modeling of a program's runtime behavior to formulate its integrity properties. In this paper, we study the possibility of employing static source code analysis to derive integrity models of a commodity operating systems kernel. We develop a precise and static analysis-based data invariant detection tool that overcomes several technical challenges: field-sensitivity, array-sensitivity, and pointer analysis. We apply our tool to Linux kernel 2.4.32 and Windows Research Kernel (WRK). For Linux kernel 2.4.32, our tool identifies 284,471 data invariants that are critical to its runtime integrity, e.g., we use them to detect ten real-world Linux rootkits. Furthermore, comparison with the result of a dynamic invariant detector reveals 17,182 variables that can cause false alarms for the dynamic detector in the constant invariants category. Our tool also works successfully for WRK and reports 202,992 invariants, which we use to detect nine real-world Windows malware and one synthetic Windows malware. When compared with a dynamic invariant detector, we see similar results in terms of false alarms. Our experience suggests that static analysis is a viable option for automated integrity property derivation, and it can have very low false positive rate and very low false negative rate (e.g., for the constant invariants of WRK, the false positive rate is one out of 100,822 and the false negative rate is 0.007% or seven out of 100,822).