Automated Derivation of Data Invariants for System Runtime Integrity Monitoring

The recent interest in runtime attestation requires modeling of a program’s runtime behavior to formulate its integrity properties. We propose scoped invariants as a primitive for analyzing a software system for its integrity properties, and we develop automated tools that can derive scoped invariants for any given program: the first is a dynamic analysis tool that runs the target program in the QEMU machine emulator and monitors memory writes and events generated by the target program [3], and the second is a static analysis based tool that is field-sensitive, array-sensitive, and capable of handling pointers [1, 2]. We have applied our tools to Xen [3], the Linux kernel [2], and the Windows Research Kernel [1], which shows 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%).

Static analysis based invariant derivation architecture

Papers:

  1. Feng Zhu, Jinpeng Wei. "Static Analysis Based Invariant Detection for Commodity Operating Systems". Computers & Security, Elsevier Ltd., Volume 43, pp. 49-63, June 2014. doi: 10.1016/j.cose.2014.02.008. Full paper (825 KB).
  2. Jinpeng Wei, Feng Zhu, and Yasushi Shinjo. "Static Analysis Based Invariant Detection for Commodity Operating Systems". 7th International Conference on Collaborative Computing (CollaborateCom 2011), Orlando, FL, October 15-18, 2011. Full paper (120 KB), Slides (275 KB).
  3. Jinpeng Wei, Calton Pu, Carlos V. Rozas, Anand Rajan, and Feng Zhu. "Modeling the Runtime Integrity of Cloud Servers: a Scoped Invariant Perspective". International Workshop on Cloud Privacy, Security, Risk and Trust (CPSRT 2010). In conjunction with the 2nd IEEE International Conference on Cloud Computing Technology and Science (CloudCom 2010), Indianapolis, IN, Nov. 30 - Dec. 3, 2010.Full paper (219 KB), Slides (145 KB). Best paper award.

Static analysis result download: we have applied the invariant analyzer above to a merged Linux kernel  2.4.32; you can click here to see a snippte of the generated analysis report, and here to download the entire report (905 KB).  Note that the report is very large after decompression, so if you try to open it in a browser, it may take a long time. We suggest that you save the report and then use a text editor to read it.