7th International Conference on Collaborative Computing: Networking, Applications and Worksharing

Research Article

Static Analysis Based Invariant Detection for Commodity Operating Systems

Download638 downloads
  • @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
Jinpeng Wei1,*, Feng Zhu1, Yasushi Shinjo2
  • 1: Florida International University
  • 2: University of Tsukuba
*Contact email: weijp@cs.fiu.edu

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%).