Research Article
Static Analysis Based Invariant Detection for Commodity Operating Systems
@INPROCEEDINGS{10.4108/icst.collaboratecom.2011.247087, author={Jinpeng Wei and Feng Zhu and Yasushi Shinjo}, title={Static Analysis Based Invariant Detection for Commodity Operating Systems}, proceedings={7th International Conference on Collaborative Computing: Networking, Applications and Worksharing}, publisher={IEEE}, proceedings_a={COLLABORATECOM}, year={2012}, month={4}, keywords={integrity modeling invariants detection static analysis tools}, doi={10.4108/icst.collaboratecom.2011.247087} }- Jinpeng Wei
Feng Zhu
Yasushi Shinjo
Year: 2012
Static Analysis Based Invariant Detection for Commodity Operating Systems
COLLABORATECOM
ICST
DOI: 10.4108/icst.collaboratecom.2011.247087
Abstract
The 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 global invariant detection tool that overcomes several technical challenges: field-sensitivity, array-sensitivity, pointer analysis, and handling of assembly code. We apply our tool to Linux kernel 2.4.32 and identify 141,279 global invariants that are critical to its runtime integrity. Furthermore, comparison with the result of a dynamic invariant detector reveals 17,182 variables that can cause false alarms for the dynamic detector. Our experience suggests that static analysis is a viable option for automated integrity property derivation, and it can have very low false positive rate (1 out of 141,280 in our Linux kernel case study) and very low false negative rate (about 0.013%).
