Unifying type checking and property checking for low-level code

ABSTRACT

We present a unified approach to type checking and property checking for low-level code. Type checking for low-level code is challenging because type safety often depends on complex, program-specific invariants that are difficult for traditional type checkers to express. Conversely, property checking for low-level code is challenging because it is difficult to write concise specifications that distinguish between locations in an untyped program's heap. We address both problems simultaneously by implementing a type checker for low-level code as part of our property checker.

We present a low-level formalization of a C program's heap and its types that can be checked with an SMT solver, and we provide a decision procedure for checking type safety. Our type system is flexible enough to support a combination of nominal and structural subtyping for C, on a per-structure basis. We discuss several case studies that demonstrate the ability of this tool to express and check complex type invariants in low-level C code, including several small Windows device drivers.

REFERENCES

• 1: The Coq proof assistant. http://coq.inria.fr/.
• 2: The HAVOC property checker. http://research.microsoft.com/projects/havoc/.
• 3: Amal J. Ahmed , Andrew W. Appel , Roberto Virga, A Stratified Semantics of General References A Stratified Semantics of General References, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.75, July 22-25, 2002
• 4: Andrew W. Appel, Foundational Proof-Carrying Code, Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, p.247, June 16-19, 2001
• 5: Andrew W. Appel , Amy P. Felty, A semantic model of types and machine instructions for proof-carrying code, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.243-253, January 19-21, 2000, Boston, MA, USA [doi>10.1145/325694.325727]
• 6: Andrew W. Appel , David McAllester, An indexed model of recursive types for foundational proof-carrying code, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.5, p.657-683, September 2001 [doi>10.1145/504709.504712]
• 7: T. Ball, B. Hackett, S. K. Lahiri, and S. Qadeer. Annotation-based property checking for systems software. Technical Report MSR-TR-2008-82, Microsoft Research, 2008.
• 8: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, v.36 n.5, p.203-213, May 2001
• 9: M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO), 2005.
• 10: M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), 2004.
• 11: Mike Barnett , K. Rustan M. Leino, Weakest-precondition of unstructured programs, Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, September 05-06, 2005, Lisbon, Portugal
• 12: Richard Bornat, Proving Pointer Programs in Hoare Logic, Proceedings of the 5th International Conference on Mathematics of Program Construction, p.102-126, July 03-05, 2000
• 13: C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In Static Analysis Symposium (SAS), 2006.
• 14: Bor-Yuh Evan Chang , Adam Chlipala , George C. Necula , Robert R. Schneck, The open verifier framework for foundational verifiers, Proceedings of the 2005 ACM SIGPLAN international workshop on Types in languages design and implementation, p.1-12, January 10-10, 2005, Long Beach, California, USA [doi>10.1145/1040294.1040295]
• 15: S. Chatterjee, S. K. Lahiri, S. Qadeer, and Z. Rakamaric. A reachability predicate for analyzing low-level software. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
• 16: Brian Chin , Shane Markstrum , Todd Millstein, Semantic type qualifiers, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 17: J. Condit, M. Harren, Z. Anderson, D. Gay, and G. Necula. Dependent types for low-level programming. In European Symposium on Programmig (ESOP), 2007.
• 18: Karl Crary , Joseph C. Vanderwaart, An expressive, scalable type theory for certified code, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.191-205, October 04-06, 2002, Pittsburgh, PA, USA
• 19: L. de Moura and N. Bjorner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
• 20: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 21: Xinyu Feng , Zhaozhong Ni , Zhong Shao , Yu Guo, An open framework for foundational proof-carrying code, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190325]
• 22: J.-C. Filliatre and C. Marche. The Why/Krakatoa/Caduceus platform for deductive program verification. In Computer Aided Verification (CAV), 2007.
• 23: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 24: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 25: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track of the annual conference on USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 26: Shuvendu Lahiri , Shaz Qadeer, Back to the future: revisiting precise program verification using SMT solvers, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 27: Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
• 28: Microsoft. Windows driver kit. http://www.microsoft.com/whdc/devtools/wdk/default.mspx.
• 29: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.3, p.527-568, May 1999 [doi>10.1145/319301.319345]
• 30: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 31: George C. Necula , Jeremy Condit , Matthew Harren , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy software, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.3, p.477-526, May 2005 [doi>10.1145/1065887.1065892]
• 32: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
• 33: Greg Nelson , Derek C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems (TOPLAS), v.1 n.2, p.245-257, Oct. 1979 [doi>10.1145/357073.357079]
• 34: Yann Régis-Gianas , François Pottier, A Hoare Logic for Call-by-Value Functional Programs, Proceedings of the 9th international conference on Mathematics of Program Construction, p.305-335, July 15-18, 2008, Marseille, France [doi>10.1007/978-3-540-70594-9_17]
• 35: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 36: Satisfiability Modulo Theories Library (SMT-LIB). Available at http://goedel.cs.uiowa.edu/smtlib/.
• 37: W. Schulte, S. Xia, J. Smans, and F. Piessens. A glimpse of a verifying C compiler. In C/C++ Verification Workshop, 2007.
• 38: Hongwei Xi, Imperative Programming with Dependent Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.375, June 26-29, 2000
• 39: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 40: Hongseok Yang , Oukseh Lee , Josh Berdine , Cristiano Calcagno , Byron Cook , Dino Distefano , Peter O'Hearn, Scalable Shape Analysis for Systems Code, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_36]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Verification

Keywords:
assertion checking, decision procedure, low-level code, property checking, smt solver, type checking