Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2019: Formal Methods – The Next 30 Years pp 573–590Cite as

Abstraction and Subsumption in Modular Verification of C Programs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Abstract

Representation predicates enable data abstraction in separation logic, but when the same concrete implementation may need to be abstracted in different ways, one needs a notion of subsumption. We demonstrate function-specification subtyping, analogous to subtyping, with a subsumption rule: if \(\phi \) is a of \(\psi \), that is \(\phi <:\psi \), then \(x:\phi \) implies \(x:\psi \), meaning that any function satisfying specification \(\phi \) can be used wherever a function satisfying \(\psi \) is demanded. We extend previous notions of Hoare-logic sub-specification, which already included parameter adaption, to include framing (necessary for separation logic) and impredicative bifunctors (necessary for higher-order functions, i.e. function pointers). We show intersection specifications, with the expected relation to subtyping. We show how this enables compositional modular verification of the functional correctness of C programs, in Coq, with foundational machine-checked proofs of soundness.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    A clause  p asserts that the current value of C local variable is the Coq value p. If n is a mathematical integer, then  n is its projection into 32-bit machine integers, and projects machine integers into the type of scalar C-language values.

  2. 2.

    Existentially abstracting over the internal representation predicates would further emphasize the uniformity between and —a detailed treatment of this is beyond the scope of the present article.

  3. 3.

    For example: in our proof of HMAC-DRBG [24], before VST had function-spec subsumption, we had two different proofs of the function , one with respect to a more concrete specification and one with respect to a more abstract specification . The latter proof was 202 lines of Coq, at line 37 of VST/hmacdrbg/drbg_protocol_proofs.v in commit 3e61d2991e3d70f5935ae69c88d7172cf639b9bc of https://github.com/PrincetonUniversity/VST. Now, instead of reproving the function-body a second time, we have a funspec_sub proof that is only 60 lines of Coq (at line 42 of the same file in commit c2fc3d830e15f4c70bc45376632c2323743858ef).

  4. 4.

    We give Kleymann’s rule for total correctness here. VST is a logic for partial correctness, but its preconditions also guarantee safety; Kleymann’s partial-correctness adaptation rule cannot guarantee safety.

  5. 5.

    Bifunctor function-specs in VST were the work of Qinxiang Cao, Robert Dockins, and Aquinas Hobor.

  6. 6.

    See file veric/semax_lemmas.v in the VST repo.

References

  1. America, P., Rutten, J.: Solving reflexive domain equations in a category of complete metric spaces. J. Comput. Syst. Sci. 39(3), 343–375 (1989)

    Article  MathSciNet  Google Scholar 

  2. Appel, A.W.: Verification of a cryptographic primitive: SHA-256. ACM Trans. on Program. Lang. Syst. 37(2), 7:1–7:31 (2015)

    Article  Google Scholar 

  3. Appel, A.W., Beringer, L., Cao, Q., Dodds, J.: Verifiable C: applying the verified software toolchain to C programs (2019). https://vst.cs.princeton.edu/download/VC.pdf

  4. Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)

    Book  Google Scholar 

  5. Beringer, L.: Relational decomposition. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 39–54. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22863-6_6

    Chapter  Google Scholar 

  6. Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: 24th USENIX Security Symposium, pp. 207–221. USENIX Assocation, August 2015

    Google Scholar 

  7. Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1–4), 367–422 (2018)

    Article  MathSciNet  Google Scholar 

  8. Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2

    Chapter  Google Scholar 

  9. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4

    Chapter  Google Scholar 

  10. Jung, R., Krebbers, R., Jourdan, J.-H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)

    Google Scholar 

  11. Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573–609 (2015)

    Article  MathSciNet  Google Scholar 

  12. Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11(5), 541–566 (1999)

    Article  Google Scholar 

  13. Koh, N., et al.: From C to interaction trees: specifying, verifying, and testing a networked server. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 234–248. ACM (2019)

    Google Scholar 

  14. Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. ACM Trans. Program. Lang. Syst. 37(4), 13:1–13:88 (2015)

    Article  Google Scholar 

  15. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  16. Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)

    Article  Google Scholar 

  17. Mansky, W., Appel, A.W., Nogin, A.: A verified messaging system. In: Proceedings of the 2017 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2017. ACM (2017)

    Google Scholar 

  18. Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. Program. Lang. Syst. 10(3), 470–502 (1988)

    Article  Google Scholar 

  19. Naumann, D.A.: Deriving sharp rules of adaptation for Hoare logics. Technical report 9906, Department of Computer Science, Stevens Institute of Technology (1999)

    Google Scholar 

  20. Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J. (ed.) CSL 2002. LNCS, vol. 2471, pp. 103–119. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45793-3_8

    Chapter  Google Scholar 

  21. Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2005), pp. 247–258 (2005)

    Google Scholar 

  22. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  23. Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theor. Comput. Sci. 343(3), 413–442 (2005)

    Article  MathSciNet  Google Scholar 

  24. Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedTLS HMAC-DRBG. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS 2017). ACM (2017)

    Google Scholar 

Download references

Acknowlegdements

This work was funded by the National Science Foundation under the awards 1005849 (Verified High Performance Data Structure Implementations, Beringer) and 1521602 Expedition in Computing: The Science of Deep Specification, Appel). We are grateful to the members of both projects for their feedback, and we greatly appreciate the reviewers’ comments and suggestions.

Author information

Authors and Affiliations

  1. Princeton University, Princeton, NJ, 08544, USA

    Lennart Beringer & Andrew W. Appel

Authors
  1. Lennart Beringer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew W. Appel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lennart Beringer .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Appendix: Fully General funspec_sub

Appendix: Fully General funspec_sub

as introduced in Sect. 4 specializes the “real” subtype relation \(\phi <:\psi \) in two regards: first, it only applies if \(\phi \) and \(\psi \) are of the form, i.e. the types of their WITH-lists (“witnesses”) are trivial bifunctors as they do not contain co- or contravariant occurrences of . Second, it fails to exploit step-indexing and is hence unnecessarily strong.

The technical report (www.cs.princeton.edu/~eberinge/funspec_sub.pdf) contains a brief appendix presenting the fully general .

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Beringer, L., Appel, A.W. (2019). Abstraction and Subsumption in Modular Verification of C Programs. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_34

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation