Document Open Access Logo

Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model

Authors Andrew Tolmach , Chris Chhak, Sean Anderson

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.36.pdf
  • Filesize: 0.84 MB
  • 20 pages

Document Identifiers

Author Details

Andrew Tolmach
  • Portland State University, OR, USA
Chris Chhak
  • Portland State University, OR, USA
Sean Anderson
  • Portland State University, OR, USA

Funding

Work supported by the National Science Foundation under Grant No. 2048499.

Cite AsGet BibTex

Andrew Tolmach, Chris Chhak, and Sean Anderson. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.36

Abstract

We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Software and its engineering → Compilers
  • Software and its engineering → Semantics
Keywords
  • Compiler verification
  • C language semantics
  • Coq proof assistant

Metrics

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

Supplementary Materials

References

  1. Arthur Azevedo de Amorim, Maxime Dénès, Nick Giannarakis, Catalin Hritcu, Benjamin C. Pierce, Antal Spector-Zabusky, and Andrew Tolmach. Micro-policies: Formally verified, tag-based security monitors. In 2015 IEEE Symposium on Security and Privacy, pages 813-830, 2015. URL: https://doi.org/10.1109/SP.2015.55.
  2. Sean Anderson, Allison Naaktgeboren, and Andrew Tolmach. Flexible runtime security enforcement with tagged C. In Panagiotis Katsaros and Laura Nenzi, editors, Runtime Verification - 23rd International Conference, RV 2023, Thessaloniki, Greece, October 3-6, 2023, Proceedings, volume 14245 of Lecture Notes in Computer Science, pages 231-250. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-44267-4_12.
  3. ARM. Armv8.5-a memory tagging extension white paper. URL: https://developer.arm.com/-/media/ Arm%20Developer%20Community/PDF/ Arm_Memory_Tagging_Extension_Whitepaper.pdf.
  4. Daniel J. Bernstein. boringcc. Boring crypto google group post, 2015. URL: https://groups.google.com/g/boring-crypto/c/48qa1kWignU/m/ o8GGp2K1DAAJ.
  5. Frédéric Besson, Sandrine Blazy, and Pierre Wilke. CompCertS: A Memory-Aware Verified C Compiler using a Pointer as Integer Semantics. Journal of Automated Reasoning, 63(2):369-392, August 2019. URL: https://doi.org/10.1007/s10817-018-9496-y.
  6. Frédéric Besson, Sandrine Blazy, and Pierre Wilke. A verified compcert front-end for a memory model supporting pointer arithmetic and uninitialised data. J. Autom. Reasoning, 62(4):433-480, 2019. URL: https://doi.org/10.1007/s10817-017-9439-z.
  7. Frédéric Besson, Sandrine Blazy, Alexandre Dang, Thomas P. Jensen, and Pierre Wilke. Compiling sandboxes: Formally verified software fault isolation. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 499-524. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_18.
  8. Quentin Carbonneaux, Jan Hoffmann, Tahina Ramananandro, and Zhong Shao. End-to-end verification of stack-space bounds for C programs. In Michael F. P. O'Boyle and Keshav Pingali, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09 - 11, 2014, pages 270-281. ACM, 2014. URL: https://doi.org/10.1145/2594291.2594301.
  9. CHR Chhak, Andrew Tolmach, and Sean Anderson. Towards formally verified compilation of tag-based policy enforcement. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, pages 137-151, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3437992.3439929.
  10. Coq Development Team. The Coq Reference Manual, version 8.18.0, September 2023. URL: https://coq.inria.fr/doc/V8.18.0/refman/.
  11. Crispin Cowan, Calton Pu, Dave Maier, Heather Hintony, Jonathan Walpole, Peat Bakke, Steve Beattie, Aaron Grier, Perry Wagle, and Qian Zhang. Stackguard: Automatic adaptive detection and prevention of buffer-overflow attacks. In Proceedings of the 7th Conference on USENIX Security Symposium - Volume 7, SSYM’98, page 5, USA, 1998. USENIX Association. URL: https://static.usenix.org/publications/library/proceedings/sec98/full_papers/cowan/cowan.pdf.
  12. Joe Devietti, Colin Blundell, Milo M. K. Martin, and Steve Zdancewic. HardBound: Architectural support for spatial safety of the C programming language. In 13th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 103-114, 2008. URL: http://acg.cis.upenn.edu/papers/asplos08_hardbound.pdf.
  13. Udit Dhawan, Catalin Hritcu, Raphael Rubin, Nikos Vasilakis, Silviu Chiricescu, Jonathan M. Smith, Thomas F. Knight, Jr., Benjamin C. Pierce, and Andre DeHon. Architectural support for software-defined metadata processing. In Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '15, pages 487-502, New York, NY, USA, 2015. ACM. URL: https://doi.org/10.1145/2694344.2694383.
  14. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and J. F. Bastien. Bringing the web up to speed with WebAssembly. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 185-200, 2017. URL: https://doi.org/10.1145/3062341.3062363.
  15. Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis. A formal C memory model supporting integer-pointer casts. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pages 326-335, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2737924.2738005.
  16. Robbert Krebbers. The C Standard Formalized in Coq. PhD thesis, Radboud University Nijmegen, December 2015. URL: http://robbertkrebbers.nl/research/thesis.pdf.
  17. Joshua Kroll, Gordon Stewart, and Andrew Appel. Portable software fault isolation. In 27th IEEE Computer Security Foundations Symposium. IEEE, 2014. URL: http://www.cs.princeton.edu/~appel/papers/psfi.pdf.
  18. Volodymyr Kuznetsov, Laszlo Szekeres, Mathias Payer, George Candea, R. Sekar, and Dawn Song. Code-pointer integrity. In Jason Flinn and Hank Levy, editors, 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14, Broomfield, CO, USA, October 6-8, 2014, pages 147-163. USENIX Association, 2014. URL: https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-kuznetsov.pdf.
  19. Juneyoung Lee, Chung-Kil Hur, Ralf Jung, Zhengyang Liu, John Regehr, and Nuno P. Lopes. Reconciling high-level optimizations and low-level code in LLVM. Proc. ACM Program. Lang., 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276495.
  20. Xavier Leroy. A Formally Verified Compiler Back-End. J. Autom. Reason., 43(4):363-446, December 2009. URL: https://doi.org/10.1007/s10817-009-9155-4.
  21. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  22. Xavier Leroy and Sandrine Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1-31, 2008. URL: http://xavierleroy.org/publi/memory-model-journal.pdf.
  23. Xavier Leroy et al. Compcert 3.10. URL: https://github.com/AbsInt/CompCert/releases/tag/v3.10.
  24. Hans Liljestrand, Carlos Chinea Perez, Rémi Denis-Courmont, Jan-Erik Ekberg, and N. Asokan. Color my world: Deterministic tagging for memory safety. CoRR, abs/2204.03781, 2022. URL: https://doi.org/10.48550/arXiv.2204.03781.
  25. John Lu and Keith D. Cooper. Register promotion in C programs. In Proceedings of the ACM SIGPLAN 1997 Conference on Programming Language Design and Implementation, PLDI '97, pages 308-319, New York, NY, USA, 1997. Association for Computing Machinery. URL: https://doi.org/10.1145/258915.258943.
  26. Kayvan Memarian. The Cerberus C Semantics. PhD thesis, University of Cambridge, 2023. URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-981.pdf.
  27. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. Exploring C semantics and pointer provenance. Proceedings of the ACM on Programming Languages, 3, 2019. URL: https://dl.acm.org/citation.cfm?id=3290380.
  28. Eric Mullen, Daryl Zuniga, Zachary Tatlock, and Dan Grossman. Verified peephole optimizations for CompCert. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, pages 448-461, 2016. URL: https://doi.org/10.1145/2908080.2908109.
  29. Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic. SoftBound: highly compatible and complete spatial memory safety for C. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 245-258. ACM, 2009. URL: http://repository.upenn.edu/cgi/viewcontent.cgi? article=1941&context=cis_reports.
  30. Santosh Nagarakatte, Jianzhou Zhao, Milo M.K. Martin, and Steve Zdancewic. CETS: Compiler enforced temporal safety for C. SIGPLAN Not., 45(8):31-40, June 2010. URL: https://doi.org/10.1145/1837855.1806657.
  31. Michael Norrish. C formalised in HOL. PhD thesis, University of Cambridge, 1998. URL: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf.
  32. Marco Patrignani, Amal Ahmed, and Dave Clarke. Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv., 51(6), February 2019. URL: https://doi.org/10.1145/3280984.
  33. Alexander L. Richardson. Complete Spatial Safety for C and C++ using CHERI capabilities. PhD thesis, University of Cambridge, October 2019. URL: https://www.repository.cam.ac.uk/bitstream/handle/1810/ 307454/thesis-hardbound.pdf.
  34. Kostya Serebryany. ARM memory tagging extension and how it improves C/C++ memory safety. login Usenix Mag., 44(2), 2019. URL: https://www.usenix.org/publications/login/summer2019/ serebryany.
  35. Jaroslav Sevcík, Viktor Vafeiadis, Francesco Zappa Nardelli, Suresh Jagannathan, and Peter Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. Journal of the ACM, 60(3):22, 2013. URL: https://doi.org/10.1145/2487241.2487248.
  36. Laurent Simon, David Chisnall, and Ross J. Anderson. What you get is what you C: Controlling side effects in mainstream C compilers. In IEEE European Symposium on Security and Privacy (EuroS&P), pages 1-15. IEEE, 2018. URL: https://doi.org/10.1109/EuroSP.2018.00009.
  37. Laszlo Szekeres, Mathias Payer, Tao Wei, and Dawn Song. SoK: Eternal war in memory. In IEEE Symposium on Security and Privacy, pages 48-62. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/SP.2013.13.
  38. Harvey Tuch. Formal verification of C systems code. J. Autom. Reasoning, 42:125-187, April 2009. URL: https://doi.org/10.1007/s10817-009-9120-2.
  39. Harvey Tuch, Gerwin Klein, and Michael Norrish. Types, bytes, and separation logic. SIGPLAN Not., 42(1):97-108, January 2007. URL: https://doi.org/10.1145/1190215.1190234.
  40. Robert Wahbe, Steven Lucco, Thomas E. Anderson, and Susan L. Graham. Efficient software-based fault isolation. In Proceedings of the Symposium on Operating Systems Principles, SOSP, pages 203-216, 1993. URL: http://www.eecs.harvard.edu/~greg/cs255sp2004/ wahbe93efficient.pdf.
  41. Yuting Wang, Pierre Wilke, and Zhong Shao. An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290375.
  42. Robert N.M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. CHERI: A hybrid capability-system architecture for scalable software compartmentalization. In Proceedings - IEEE Symposium on Security and Privacy, 2015. URL: https://doi.org/10.1109/SP.2015.9.
  43. Jianhao Xu, Kangjie Lu, Zhengjie Du, Zhu Ding, Linke Li, Qiushi Wu, Mathias Payer, and Bing Mao. Silent bugs matter: A study of compiler-introduced security bugs. In 32nd USENIX Security Symposium (USENIX Security 23), pages 3655-3672, Anaheim, CA, August 2023. USENIX Association. URL: https://www.usenix.org/conference/usenixsecurity23/ presentation/xu-jianhao.
  44. Bennet Yee, David Sehr, Gregory Dardyk, J. Bradley Chen, Robert Muth, Tavis Ormandy, Shiki Okasaka, Neha Narula, and Nicholas Fullagar. Native Client: A sandbox for portable, untrusted x86 native code. Communications of the ACM, 53(1):91-99, 2010. URL: https://doi.org/10.1145/1629175.1629203.
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