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. T. Ball and S.K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL 02: Principles of Programming Languages, pages 1--3. ACM, 2002.
2. C. Barrett, D. Dill, and J. Levitt. A decision procedure for bit-vector arithmetic. In DAC 98: Design Automation Conference, pages 522--527, 1998.
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. M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI 02: Programming Language Design and Implementation, pages 57--68. ACM, 2002.
6. D. Detlefs, G. Nelson, and J.B. Saxe. Simplify: a theorem prover for program checking. J. ACM, 52(3):365--473, 2005.
7. C. Flanagan. Hybrid type checking. In POPL 06: Principles of Programming Languages, pages 245--256. ACM Press, 2006.
8. J.S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In PLDI 02: Programming Language Design and Implementation, pages 1--12. ACM, 2002.
9. R. Gupta, E. Mehofer, and Y. Zhang. A representation for bit section based analysis and optimization. In CC 02: Compiler Construction, LNCS 2304, pages 62--77. Springer, 2002.
10. T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL 02: Principles of Programming Languages, pages 58--70. ACM, 2002.
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. C. Lee, M. Potkonjak, and W.H. Mangione-Smith. Mediabench: A tool for evaluating and synthesizing multimedia and communicatons systems. In MICRO 97: IEEE/ACM Symposium on Microarchitecture, pages 330--335. IEEE, 1997.
16. B. Li and R. Gupta. Bit section instruction set extension of arm for embedded applications. In CASES 02, pages 69--78. ACM, 2002.
17. M.O. Möller and H. Ruess. Solving bit-vector equations. In FMCAD 98: Formal Methods in Computer-Aided Design, LNCS 1522, pages 36--48. Springer, 1998.
18. R. O'Callahan and D. Jackson. Lackwit: A program understanding tool based on type inference. In ICSE 97: International Conference on Software Engineering, pages 338--348. ACM, 1997.
19. G. Ramalingam, J. Field, and F. Tip. Aggregate structure identification and its application to program analysis. In POPL 99: Principles of Programming Languages, pages 119--132. ACM, 1999.
20. A. Stump, C.W. Barrett, and D.L. Dill. Cvc: A cooperating validity checker. In CAV 02: Computer-Aided Verification, LNCS 2404, pages 500--504. Springer, 2002.
21. S. Tallam and R. Gupta. Bitwidth aware global register allocation. In POPL 03: Principles of Programming Languages, pages 85--96. ACM, 2003.
22. E. Witchel, J. Cates, and K. Asanović. Mondrian memory protection. In ASPLOS 02. ACM, 2002.
23. Y. Xie and A. Aiken. Scalable error detection using boolean satisfiability. In POPL 05: Principles of Programming Languages, pages 351--363. ACM, 2005.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification