A low-level memory model and an accompanying reachability predicate | International Journal on Software Tools for Technology Transfer Skip to main content
Springer Nature Link
Log in

A low-level memory model and an accompanying reachability predicate

  • Special Section on TACAS07
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Reasoning about program heap, especially if it involves handling unbounded, dynamically heap-allocated data structures such as linked lists and arrays, is challenging. Furthermore, sound analysis that precisely models heap becomes significantly more challenging in the presence of low-level pointer manipulation that is prevalent in systems software. The reachability predicate has already proved to be useful for reasoning about the heap in type-safe languages where memory is manipulated by dereferencing object fields. In this paper, we present a memory model suitable for reasoning about low-level pointer operations that is accompanied by a formalization of the reachability predicate in the presence of internal pointers and pointer arithmetic. We have designed an annotation language for C programs that makes use of the new predicate. This language enables us to specify properties of many interesting data structures present in the Windows kernel. We present our experience with a prototype verifier on a set of illustrative C benchmarks.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Babić, D., Hu, A.J.: Calysto: scalable and precise extended static checking. In: International Conference on Software Engineering (ICSE’08), pp. 211–220 (2008)

  2. Balaban, I., Pnueli, A., Zuck, L.D.: Shape analysis by predicate abstraction. In: International Conference on Verification, Model checking, and Abstract Interpretation (VMCAI’05), pp. 164–180 (2005)

  3. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’01), pp. 203–213 (2001)

  4. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: International Symposium on Formal Methods for Objects and Components (FMCO’05), pp. 364–387 (2005)

  5. Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering (PASTE’05), pp. 82–87 (2005)

  6. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Construction and Analysis of Safe, Secure and Interoperable Smart Devices (CASSIS’05), pp. 49–69 (2005)

  7. Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W., Wies, T., Yang, H.: Shape analysis for composite data structures. In: International Conference on Computer Aided Verification (CAV’07), pp. 178–192 (2007)

  8. Bingham, J., Rakamarić, Z.: A logic and decision procedure for predicate abstraction of heap-manipulating programs. In: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’06), pp. 207–221 (2006)

  9. Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Static Analysis Symposium (SAS’06), pp. 182–203 (2006)

  10. Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’07), pp. 19–33 (2007)

  11. Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.R.: An empirical study of operating system errors. In: ACM Symposium on Operating Systems Principles (SOSP’01), pp. 73–88 (2001)

  12. Clarke E., Kroening D., Sharygina N., Yorav K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods Syst. Des. (FMSD) 25, 105–127 (2004)

    Article  MATH  Google Scholar 

  13. Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’02), pp. 57–68 (2002)

  14. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), pp. 337–340 (2008)

  15. DeLine, R., Leino, K.R.M.: BoogiePL: a typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)

  16. Detlefs D., Nelson G., Saxe J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)

    Article  MathSciNet  Google Scholar 

  17. Dijkstra E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18, 453–457 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  18. Distefano, D., O’Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’06), pp. 287–302 (2006)

  19. Filliâtre, J., Marché, C.: Multi-prover verification of C programs. In: International Conference on Formal Engineering Methods (ICFEM’04), pp. 15–29 (2004)

  20. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’02), pp. 234–245 (2002)

  21. Gotsman, A., Berdine, J., Cook, B.: Interprocedural shape analysis with separated heap abstractions. In: Static Analysis Symposium (SAS), pp. 240–260 (2006)

  22. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’02), pp. 58–70 (2002)

  23. Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06), pp. 115–126 (2006)

  24. Lahiri, S.K., Qadeer, S.: A decision procedure for well-founded reachability. Technical Report MSR-TR-2007-43, Microsoft Research, (2007)

  25. Lahiri, S.K., Qadeer, S.: Back to the future: Revisiting precise program verification using SMT solvers. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’08), pp. 171–182 (2008)

  26. Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, S., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. In: International Conference on Automated Deduction (CADE’05), pp. 99–115 (2005)

  27. Lev-Ami, T., Sagiv, S.: TVLA: A system for implementing static analyses. In: Static Analysis Symposium (SAS’00), pp. 280–301 (2000)

  28. Li, Z., Tan, L., Wang, X., Lu, S., Zhou, Y., Zhai, C.: Have things changed now? An empirical study of bug characteristics in modern open source software. In: 1st Workshop on Architectural and System Support for Improving Software Dependability (ASID’06), pp. 25–33 (2006)

  29. McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: International Conference on Computer Aided Verification (CAV’05), pp. 476–490 (2005)

  30. Nelson, G.: Verifying reachability invariants of linked structures. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’83), pp. 38–47 (1983)

  31. Nelson G., Oppen D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. (TOPLAS) 2(1), 245–257 (1979)

    Article  Google Scholar 

  32. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: International Workshop on Computer Science Logic (CSL’01), pp. 1–19 (2001)

  33. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Annual IEEE Symposium on Logic in Computer Science (LICS’02), pp. 55–74 (2002)

  34. Sagiv S., Reps T.W., Wilhelm R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst. (TOPLAS) 20(1), 1–50 (1998)

    Article  Google Scholar 

  35. Schulte, W., Xia, S., Smans, J., Piessens, F.: A glimpse of a verifying C compiler (extended abstract). In: C/C++ Verification Workshop (2007)

  36. Sullivan, M., Chillarege, R.: Software defects and their impact on system availability—a study of field failures in operating systems. In: International Symposium on Fault-Tolerant Computing (FTCS’91), pp. 2–9 (1991)

  37. Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05), pp. 351–363 (2005)

  38. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: International Conference on Computer Aided Verification (CAV’08), pp. 385–398 (2008)

Download references

Author information

Authors and Affiliations

  1. University of California, Berkeley, USA

    Shaunak Chatterjee

  2. Microsoft Research, Redmond, USA

    Shuvendu K. Lahiri & Shaz Qadeer

  3. University of British Columbia, Vancouver, Canada

    Zvonimir Rakamarić

Authors
  1. Shaunak Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Shuvendu K. Lahiri
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Shaz Qadeer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zvonimir Rakamarić
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zvonimir Rakamarić.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Chatterjee, S., Lahiri, S.K., Qadeer, S. et al. A low-level memory model and an accompanying reachability predicate. Int J Softw Tools Technol Transfer 11, 105–116 (2009). https://doi.org/10.1007/s10009-009-0098-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-009-0098-1

Keywords

Search

Navigation