Bit level types for high level reasoning

ABSTRACT

Bitwise operations are commonly used in low-level systems code to access multiple data fields that have been packed into a single word. Program analysis tools that reason about such programs must model the semantics of bitwise operations precisely in order to capture program control and data flow through these operations. We present a type system for subword data structures that explitictly tracks the flow of bit values in the program and identifies consecutive sections of bits as logical entities manipulated atomically by the programmer. Our type inference algorithm tags each integer value of the program with a bitvector type that identifies the data layout at the subword level. These types are used in a translation phase to remove bitwise operations from the program, thereby allowing verification engines to avoid the expensive low-level reasoning required for analyzing bitvector operations. We have used a software model checker to check properties of translated versions of a Linux device driver and a memory protection system. The resulting verification runs could prove many more properties than the naive model checker that did not reason about bitvectors, and could prove properties much faster than a model checker that did reason about bitvectors. We have also applied our bitvector type inference algorithm to generate program documentation for a virtual memory subsystem of an OS kernel. While we have applied the type system mainly for program understanding and verification, bitvector types also have applications to better variable ordering heuristics in boolean model checking and memory optimizations in compilers for embedded software.

REFERENCES

• 1: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 2: Clark W. Barrett , David L. Dill , Jeremy R. Levitt, A decision procedure for bit-vector arithmetic, Proceedings of the 35th annual conference on Design automation, p.522-527, June 15-19, 1998, San Francisco, California, United States [doi>10.1145/277044.277186]
• 3: E.M. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS 04: Tools and Algorithms for the construction and analysis of systems, LNCS 2988, pages 168--176. Springer, 2004.
• 4: J. Corbet, G. Kroah-Hartman, and A. Rubini. Linux device drivers, 3rd edition. O'Reilly, 2005.
• 5: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 6: David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005 [doi>10.1145/1066100.1066102]
• 7: Cormac Flanagan, Hybrid type checking, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.245-256, January 11-13, 2006, Charleston, South Carolina, USA
• 8: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: Rajiv Gupta , Eduard Mehofer , Youtao Zhang, A Representation for Bit Section Based Analysis and Optimization, Proceedings of the 11th International Conference on Compiler Construction, p.62-77, April 08-12, 2002
• 10: 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
• 11: R. Jhala and K.L. McMillan. Interpolant-based transition relation approximation. In CAV 05: Computer-Aided Verification, LNCS 3576, pages 39--51. Springer, 2005.
• 12: JOS. Jos: An operating system kernel. http://pdos.csail.mit.edu/6.828/2005/overview.html.
• 13: R. Komondoor, G. Ramalingam, J. Field, and S. Chandra. Dependent types for program understanding. In TACAS 05: Tools and Algorithms for the Construction and Analysis of Systems, LNCS 3440, pages 157--173. Springer, 2005.
• 14: Daniel Kroening and Natasha Sharygina. Approximating predicate images for bit-vector logic. In TACAS, pages 242--256, 2006.
• 15: Chunho Lee , Miodrag Potkonjak , William H. Mangione-Smith, MediaBench: a tool for evaluating and synthesizing multimedia and communicatons systems, Proceedings of the 30th annual ACM/IEEE international symposium on Microarchitecture, p.330-335, December 01-03, 1997, Research Triangle Park, North Carolina, United States
• 16: Bengu Li , Rajiv Gupta, Bit section instruction set extension of ARM for embedded applications, Proceedings of the 2002 international conference on Compilers, architecture, and synthesis for embedded systems, October 08-11, 2002, Grenoble, France [doi>10.1145/581630.581642]
• 17: M. Oliver Möller , Harald Rueß, Solving Bit-Vector Equations, Proceedings of the Second International Conference on Formal Methods in Computer-Aided Design, p.36-48, November 04-06, 1998
• 18: Robert O'Callahan , Daniel Jackson, Lackwit: a program understanding tool based on type inference, Proceedings of the 19th international conference on Software engineering, p.338-348, May 17-23, 1997, Boston, Massachusetts, United States [doi>10.1145/253228.253351]
• 19: G. Ramalingam , John Field , Frank Tip, Aggregate structure identification and its application to program analysis, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.119-132, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292553]
• 20: Aaron Stump , Clark W. Barrett , David L. Dill, CVC: A Cooperating Validity Checker, Proceedings of the 14th International Conference on Computer Aided Verification, p.500-504, July 27-31, 2002
• 21: Sriraman Tallam , Rajiv Gupta, Bitwidth aware global register allocation, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-96, January 15-17, 2003, New Orleans, Louisiana, USA
• 22: Emmett Witchel , Josh Cates , Krste Asanović, Mondrian memory protection, Proceedings of the 10th international conference on Architectural support for programming languages and operating systems, October 05-09, 2002, San Jose, California
• 23: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA

INDEX TERMS

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

General Terms:
Languages, Reliability, Verification

Keywords:
bit vectors, model checking, type inference