Document Open Access Logo

Verifying an HTTP Key-Value Server with Interaction Trees and VST

Authors Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, Steve Zdancewic

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.32.pdf
  • Filesize: 0.73 MB
  • 19 pages

Document Identifiers

Author Details

Hengchu Zhang
  • University of Pennsylvania, Philadelphia, PA, USA
Wolf Honoré
  • Yale University, New Haven, CT, USA
Nicolas Koh
  • Princeton University, NJ, USA
Yao Li
  • University of Pennsylvania, Philadelphia, PA, USA
Yishuai Li
  • University of Pennsylvania, Philadelphia, PA, USA
Li-Yao Xia
  • University of Pennsylvania, Philadelphia, PA, USA
Lennart Beringer
  • Princeton University, New Haven, NJ, USA
William Mansky
  • University of Illinois at Chicago, IL, USA
Benjamin Pierce
  • University of Pennsylvania, Philadelphia, PA, USA
Steve Zdancewic
  • University of Pennsylvania, Philadelphia, PA, USA

Funding

This work is supported by the National Science Foundation’s Expedition in Computing The Science of Deep Specification under the awards 1521602 (Appel), 1521539 (Weirich, Zdancewic, Pierce), and 1521523 (Shao). Additional support is provided by the NSF projects Verified High Performance Data Structure Implementations, award 1005849 (Beringer, Mansky), Random Testing for Language Design, award 1421243 (Pierce), and by the ONR projects N00014-18-2618 and N00014-17-1-2930.

Acknowledgements

We thank all members of the DeepSpec project for their collaboration and feedback, and we greatly appreciate the reviewers' comments and suggestions.

Cite AsGet BibTex

Hengchu Zhang, Wolf Honoré, Nicolas Koh, Yao Li, Yishuai Li, Li-Yao Xia, Lennart Beringer, William Mansky, Benjamin Pierce, and Steve Zdancewic. Verifying an HTTP Key-Value Server with Interaction Trees and VST. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.32

Abstract

We present a networked key-value server, implemented in C and formally verified in Coq. The server interacts with clients using a subset of the HTTP/1.1 protocol and is specified and verified using interaction trees and the Verified Software Toolchain. The codebase includes a reusable and fully verified C string library that provides 17 standard POSIX string functions and 17 general purpose non-POSIX string functions. For the KVServer socket system calls, we establish a refinement relation between specifications at user-space level and at CertiKOS kernel-space level.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program specifications
  • Theory of computation → Program verification
  • Theory of computation → Separation logic
Keywords
  • formal verification
  • Coq
  • HTTP
  • deep specification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H Schmitt, and Mattias Ulbrich. Deductive Software Verification-The KeY Book, volume 10001 of Lecture Notes in Computer Science. Springer, 2016. Google Scholar
  2. Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, and Artem Starostin. The verisoft approach to systems verification. In Natarajan Shankar and Jim Woodcock, editors, Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, volume 5295 of Lecture Notes in Computer Science, pages 209-224. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87873-5_18.
  3. Andrew W. Appel, Lennart Beringer, Adam Chlipala, Benjamin C. Pierce, Zhong Shao, Stephanie Weirich, and Steve Zdancewic. Position paper: the science of deep specification. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, 375(2104), 2017. URL: https://doi.org/10.1098/rsta.2016.0331.
  4. Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. Program Logics for Certified Compilers. Cambridge University Press, USA, 2014. Google Scholar
  5. Andrew W. Appel and David A. Naumann. Verified sequential malloc/free. In Chen Ding and Martin Maas, editors, ISMM'20: 2020 ACM SIGPLAN International Symposium on Memory Management, pages 48-59. ACM, 2020. URL: https://doi.org/10.1145/3381898.3397211.
  6. Lennart Beringer. Verified software units. In Nobuko Yoshida, editor, Programming Languages and Systems, pages 118-147, Cham, 2021. Springer International Publishing. Google Scholar
  7. Lennart Beringer and Andrew W. Appel. Abstraction and subsumption in modular verification of C programs. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, volume 11800 of Lecture Notes in Computer Science, pages 573-590. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30942-8_34.
  8. Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. Engineering with logic: Rigorous test-oracle specification and validation for TCP/IP and the Sockets API. J. ACM, 66(1), 2018. URL: https://doi.org/10.1145/3243650.
  9. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview. Technical Report UCAM-CL-TR-624, Computer Laboratory, University of Cambridge, 2005. 88pp. URL: http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-624.html.
  10. Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, and Keith Wansbrough. TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 2: The specification. Technical Report UCAM-CL-TR-625, Computer Laboratory, University of Cambridge, March 2005. 386pp. URL: http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-625.html.
  11. Paul E. Black. Axiomatic Semantics Verification of a Secure Web Server. PhD thesis, Brigham Young University, Provo, UT, USA, 1998. AAI9820483. Google Scholar
  12. Tej Chajed, M. Frans Kaashoek, Butler W. Lampson, and Nickolai Zeldovich. Verifying concurrent software using movers in CSPEC. In Andrea C. Arpaci-Dusseau and Geoff Voelker, editors, 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018, pages 306-322. USENIX Association, 2018. URL: https://www.usenix.org/conference/osdi18/presentation/chajed.
  13. Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent, crash-safe systems with Perennial. In Tim Brecht and Carey Williamson, editors, Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019, pages 243-258. ACM, 2019. URL: https://doi.org/10.1145/3341301.3359632.
  14. Cristina Cifuentes and Bernhard Scholz. Parfait - designing a scalable bug checker. In Florian Martin, Hanne Riis Nielson, Claudio Riva, and Markus Schordan, editors, Scalable Program Analysis, 13.04. - 18.04.2008, volume 08161 of Dagstuhl Seminar Proceedings. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2008. URL: http://drops.dagstuhl.de/opus/volltexte/2008/1573/.
  15. Denis Efremov, Mikhail U. Mandrykin, and Alexey V. Khoroshilov. Deductive verification of unmodified Linux kernel library functions. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part II, volume 11245 of Lecture Notes in Computer Science, pages 216-234. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03421-4_15.
  16. Roy T. Fielding and Julian Reschke. Hypertext Transfer Protocol (HTTP/1.1): Message Syntax and Routing. RFC 7230, 2014. URL: https://doi.org/10.17487/RFC7230.
  17. Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (Newman) Wu, Shu-Chun Weng, Haozhong Zhang, and Yu Guo. Deep specifications and certified abstraction layers. In Sriram K. Rajamani and David Walker, editors, Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 595-608. ACM, 2015. URL: https://doi.org/10.1145/2676726.2676975.
  18. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In Kimberly Keeton and Timothy Roscoe, editors, 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2-4, 2016, pages 653-669. USENIX Association, 2016. URL: https://www.usenix.org/conference/osdi16/technical-sessions/presentation/gu.
  19. Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan (Newman) Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. Certified concurrent abstraction layers. In Jeffrey S. Foster and Dan Grossman, editors, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 646-661. ACM, 2018. URL: https://doi.org/10.1145/3192366.3192381.
  20. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. Ironfleet: proving practical distributed systems correct. In Ethan L. Miller and Steven Hand, editors, Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, October 4-7, 2015, pages 1-17. ACM, 2015. URL: https://doi.org/10.1145/2815400.2815428.
  21. Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst., 12(3):463-492, 1990. URL: https://doi.org/10.1145/78969.78972.
  22. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, and Frank Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In NASA Formal Methods Symposium, pages 41-55. Springer, 2011. Google Scholar
  23. Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A software analysis perspective. Formal Aspects Comput., 27(3):573-609, 2015. URL: https://doi.org/10.1007/s00165-014-0326-7.
  24. Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015, pages 94-105, 2015. URL: https://doi.org/10.1145/2804302.2804319.
  25. Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. 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, CPP 2019, page 234–248, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3293880.3294106.
  26. Adam Koprowski and Henri Binsztok. TRX: A formally verified parser interpreter. Log. Methods Comput. Sci., 7(2), 2011. URL: https://doi.org/10.2168/LMCS-7(2:18)2011.
  27. Dirk Leinenbach, Wolfgang J. Paul, and Elena Petrova. Towards the formal verification of a C0 compiler: Code generation and implementation correctnes. In Bernhard K. Aichernig and Bernhard Beckert, editors, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany, pages 2-12. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/SEFM.2005.51.
  28. K. Rustan M. Leino. Dafny: An automatic program verifier for functional correctness. In Edmund M. Clarke and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, volume 6355 of Lecture Notes in Computer Science, pages 348-370. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-17511-4_20.
  29. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  30. Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, and Guillaume Hiet. Modular verification of programs with effects and effect handlers in Coq. In Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, pages 338-354, 2018. URL: https://doi.org/10.1007/978-3-319-95582-7_20.
  31. Yishuai Li, Benjamin C. Pierce, and Steve Zdancewic. Model-based testing of networked applications. In ACM SIGSOFT International Symposium on Software Testing and Analysis, 2021. Google Scholar
  32. William Mansky, Wolf Honoré, and Andrew W. Appel. Connecting higher-order separation logic to a first-order outside world. In Peter Müller, editor, Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, volume 12075 of Lecture Notes in Computer Science, pages 428-455. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-44914-8_16.
  33. Conor McBride. Turing-completeness totally free. In Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings, pages 257-275, 2015. URL: https://doi.org/10.1007/978-3-319-19797-5_13.
  34. Yannick Moy and Claude Marché. Modular inference of subprogram contracts for safety checking. J. Symb. Comput., 45(11):1184-1211, 2010. URL: https://doi.org/10.1016/j.jsc.2010.06.004.
  35. Peter W. O'Hearn. Separation logic. Commun. ACM, 62(2):86-95, 2019. URL: https://doi.org/10.1145/3211968.
  36. Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. Everparse: Verified secure zero-copy parsers for authenticated message formats. In Nadia Heninger and Patrick Traynor, editors, 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14-16, 2019, pages 1465-1482. USENIX Association, 2019. URL: https://www.usenix.org/conference/usenixsecurity19/presentation/delignat-lavaud.
  37. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages 55-74. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029817.
  38. Thomas Ridge, Michael Norrish, and Peter Sewell. TCP, UDP, and Sockets: Volume 3: The Service-level Specification. Technical Report UCAM-CL-TR-742, University of Cambridge, Computer Laboratory, 2009. 305pp. Google Scholar
  39. Artem Starostin. Formal verification of a C-library for strings. Master’s thesis, Saarland University, Saarbrücken, Germany, 2006. Google Scholar
  40. Nikhil Swamy, Aseem Rastogi, Aymeric Fromherz, Denis Merigoux, Danel Ahman, and Guido Martínez. Steelcore: an extensible concurrent separation logic for effectful dependently typed programs. Proc. ACM Program. Lang., 4(ICFP):121:1-121:30, 2020. URL: https://doi.org/10.1145/3409003.
  41. Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. Planning for change in a formal verification of the Raft consensus protocol. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, page 154–165, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/2854065.2854081.
  42. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
  43. Fang Yu, Tevfik Bultan, and Ben Hardekopf. String abstractions for string verification. In Alex Groce and Madanlal Musuvathi, editors, Model Checking Software - 18th International SPIN Workshop, Snowbird, UT, USA, July 14-15, 2011. Proceedings, volume 6823 of Lecture Notes in Computer Science, pages 20-37. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22306-8_3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact