Proof-carrying code (PCC) is a framework for mechanically verifying the safety of machine language programs. A program that is successfully verified by a PCC system is guaranteed to be safe to execute, but this safety guarantee is contingent upon the correctness of various trusted components. For instance, in traditional PCC systems the trusted computing base includes a large set of low-level typing rules. Foundational PCC systems seek to minimize the size of the trusted computing base. In particular, they eliminate the need to trust complex, low-level type systems by providing machine-checkable proofs of type soundness for real machine languages.
In this thesis, I demonstrate the use of logical relations for proving the soundness of type systems for mutable state. Specifically, I focus on type systems that ensure the safe allocation, update, and reuse of memory. For each type in the language, I define logical relations that explain the meaning of the type in terms of the operational semantics of the language. Using this model of types, I prove each typing rule as a lemma.
The major contribution is a model of System F with general references—that is, mutable cells that can hold values of any closed type including other references, functions, recursive types, and impredicative quantified types. The model is based on ideas from both possible worlds and the indexed model of Appel and McAllester.
I show how the model of mutable references is encoded in higher-order logic. I also show how to construct an indexed possible-worlds model for a von Neumann machine. The latter is used in the Princeton Foundational PCC system to prove type safety for a full-fledged low-level typed assembly language. Finally, I present a semantic model for a region calculus that supports type-invariant references as well as memory reuse.
Cited By
- Jacobs J, Hinrichsen J and Krebbers R (2024). Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing, Proceedings of the ACM on Programming Languages, 8:POPL, (1385-1417), Online publication date: 5-Jan-2024.
- Devriese D, Patrignani M and Piessens F (2022). Two Parametricities Versus Three Universal Types, ACM Transactions on Programming Languages and Systems, 44:4, (1-43), Online publication date: 31-Dec-2022.
- van der Rest C, Poulsen C, Rouvoet A, Visser E and Mosses P (2022). Intrinsically-typed definitional interpreters à la carte, Proceedings of the ACM on Programming Languages, 6:OOPSLA2, (1903-1932), Online publication date: 31-Oct-2022.
- Patterson D, Mushtak N, Wagner A and Ahmed A Semantic soundness for language interoperability Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (609-624)
- Georges A, Trieu A and Birkedal L (2022). Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities, Proceedings of the ACM on Programming Languages, 6:OOPSLA1, (1-30), Online publication date: 29-Apr-2022.
- Labrada E, Toro M, Tanter É and Devriese D (2022). Plausible sealing for gradual parametricity, Proceedings of the ACM on Programming Languages, 6:OOPSLA1, (1-28), Online publication date: 29-Apr-2022.
- Spies S, Gäher L, Gratzer D, Tassarotti J, Krebbers R, Dreyer D and Birkedal L Transfinite Iris: resolving an existential dilemma of step-indexed separation logic Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (80-95)
- Jung R, Jourdan J, Krebbers R and Dreyer D (2021). Safe systems programming in Rust, Communications of the ACM, 64:4, (144-152), Online publication date: 1-Apr-2021.
- Sullivan Z, Downen P and Ariola Z Strictly capturing non-strict closures Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, (74-89)
- Hinrichsen J, Louwrink D, Krebbers R and Bengtson J Machine-checked semantic session typing Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, (178-198)
- Rajani V, Gaboardi M, Garg D and Hoffmann J (2021). A unifying type-theory for higher-order (amortized) cost analysis, Proceedings of the ACM on Programming Languages, 5:POPL, (1-28), Online publication date: 4-Jan-2021.
- Spies S, Krishnaswami N and Dreyer D (2021). Transfinite step-indexing for termination, Proceedings of the ACM on Programming Languages, 5:POPL, (1-29), Online publication date: 4-Jan-2021.
- Gregersen S, Bay J, Timany A and Birkedal L (2021). Mechanized logical relations for termination-insensitive noninterference, Proceedings of the ACM on Programming Languages, 5:POPL, (1-29), Online publication date: 4-Jan-2021.
- Georges A, Guéneau A, Van Strydonck T, Timany A, Trieu A, Huyghebaert S, Devriese D and Birkedal L (2021). Efficient and provable local capability revocation using uninitialized capabilities, Proceedings of the ACM on Programming Languages, 5:POPL, (1-30), Online publication date: 4-Jan-2021.
- Charguéraud A (2020). Separation logic for sequential programs (functional pearl), Proceedings of the ACM on Programming Languages, 4:ICFP, (1-34), Online publication date: 2-Aug-2020.
- Giarrusso P, Stefanesco L, Timany A, Birkedal L and Krebbers R (2020). Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris, Proceedings of the ACM on Programming Languages, 4:ICFP, (1-29), Online publication date: 2-Aug-2020.
- Skorstengaard L, Devriese D and Birkedal L (2019). Reasoning about a Machine with Local Capabilities, ACM Transactions on Programming Languages and Systems, 42:1, (1-53), Online publication date: 31-Mar-2020.
- Xia L, Zakowski Y, He P, Hur C, Malecha G, Pierce B and Zdancewic S (2019). Interaction trees: representing recursive and impure programs in Coq, Proceedings of the ACM on Programming Languages, 4:POPL, (1-32), Online publication date: 1-Jan-2020.
- Timany A and Birkedal L (2019). Mechanized relational verification of concurrent programs with continuations, Proceedings of the ACM on Programming Languages, 3:ICFP, (1-28), Online publication date: 26-Jul-2019.
- Qu W, Gaboardi M and Garg D (2019). Relational cost analysis for functional-imperative programs, Proceedings of the ACM on Programming Languages, 3:ICFP, (1-29), Online publication date: 26-Jul-2019.
- Toro M, Garcia R and Tanter É (2018). Type-Driven Gradual Security with References, ACM Transactions on Programming Languages and Systems, 40:4, (1-55), Online publication date: 31-Dec-2019.
- Frumin D, Krebbers R and Birkedal L ReLoC Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (442-451)
- Jung R, Jourdan J, Krebbers R and Dreyer D (2017). RustBelt: securing the foundations of the Rust programming language, Proceedings of the ACM on Programming Languages, 2:POPL, (1-34), Online publication date: 1-Jan-2018.
- Timany A, Stefanesco L, Krogh-Jespersen M and Birkedal L (2017). A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST, Proceedings of the ACM on Programming Languages, 2:POPL, (1-28), Online publication date: 1-Jan-2018.
- Patterson D, Perconti J, Dimoulas C and Ahmed A (2017). FunTAL: reasonably mixing a functional language with assembly, ACM SIGPLAN Notices, 52:6, (495-509), Online publication date: 14-Sep-2017.
- Kammar O, Levy P, Moss S and Staton S A monad for full ground reference cells Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, (1-12)
- Patterson D, Perconti J, Dimoulas C and Ahmed A FunTAL: reasonably mixing a functional language with assembly Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, (495-509)
- Amin N and Rompf T (2017). Type soundness proofs with definitional interpreters, ACM SIGPLAN Notices, 52:1, (666-679), Online publication date: 11-May-2017.
- Krebbers R, Timany A and Birkedal L (2017). Interactive proofs in higher-order concurrent separation logic, ACM SIGPLAN Notices, 52:1, (205-217), Online publication date: 11-May-2017.
- Amin N and Rompf T Type soundness proofs with definitional interpreters Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (666-679)
- Krebbers R, Timany A and Birkedal L Interactive proofs in higher-order concurrent separation logic Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (205-217)
- Jaber G and Tzevelekos N Trace semantics for polymorphic references Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, (585-594)
- Jacob-Rao R, Cave A and Pientka B Mechanizing Proofs about Mendler-style Recursion Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, (1-9)
- Svendsen K, Sieczkowski F and Birkedal L Transfinite Step-Indexing Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632, (727-751)
- Bach Poulsen C, Mosses P and Torrini P Imperative Polymorphism by Store-Based Types as Abstract Interpretations Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation, (3-8)
- Krishnaswami N, Turon A, Dreyer D and Garg D (2012). Superficially substructural types, ACM SIGPLAN Notices, 47:9, (41-54), Online publication date: 15-Oct-2012.
- Krishnaswami N, Turon A, Dreyer D and Garg D Superficially substructural types Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, (41-54)
- Dockins R and Hobor A (2012). Time Bounds for General Function Pointers, Electronic Notes in Theoretical Computer Science (ENTCS), 286, (139-155), Online publication date: 1-Sep-2012.
- Hur C, Dreyer D, Neis G and Vafeiadis V The marriage of bisimulations and Kripke logical relations Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (59-72)
- Hur C, Dreyer D, Neis G and Vafeiadis V (2012). The marriage of bisimulations and Kripke logical relations, ACM SIGPLAN Notices, 47:1, (59-72), Online publication date: 18-Jan-2012.
- Thamsborg J and Birkedal L A kripke logical relation for effect-based program transformations Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, (445-456)
- Thamsborg J and Birkedal L (2011). A kripke logical relation for effect-based program transformations, ACM SIGPLAN Notices, 46:9, (445-456), Online publication date: 18-Sep-2011.
- Appel A Verified software toolchain Proceedings of the 20th European conference on Programming languages and systems: part of the joint European conferences on theory and practice of software, (1-17)
- Stewart G and Appel A Local actions for a curry-style operational semantics Proceedings of the 5th ACM workshop on Programming languages meets program verification, (31-42)
- Pottier F A typed store-passing translation for general references Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (147-158)
- Birkedal L, Reus B, Schwinghammer J, Støvring K, Thamsborg J and Yang H Step-indexed kripke models over recursive worlds Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (119-132)
- Pottier F (2011). A typed store-passing translation for general references, ACM SIGPLAN Notices, 46:1, (147-158), Online publication date: 26-Jan-2011.
- Birkedal L, Reus B, Schwinghammer J, Støvring K, Thamsborg J and Yang H (2011). Step-indexed kripke models over recursive worlds, ACM SIGPLAN Notices, 46:1, (119-132), Online publication date: 26-Jan-2011.
- Hobor A, Dockins R and Appel A A logical mix of approximation and separation Proceedings of the 8th Asian conference on Programming languages and systems, (439-454)
- Dreyer D, Neis G and Birkedal L (2010). The impact of higher-order state and control effects on local relational reasoning, ACM SIGPLAN Notices, 45:9, (143-156), Online publication date: 27-Sep-2010.
- Dreyer D, Neis G and Birkedal L The impact of higher-order state and control effects on local relational reasoning Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, (143-156)
- Ahmed A, Appel A, Richards C, Swadi K, Tan G and Wang D (2010). Semantic foundations for typed assembly languages, ACM Transactions on Programming Languages and Systems, 32:3, (1-67), Online publication date: 1-Mar-2010.
- Hobor A, Dockins R and Appel A A theory of indirection via approximation Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (171-184)
- Hobor A, Dockins R and Appel A (2010). A theory of indirection via approximation, ACM SIGPLAN Notices, 45:1, (171-184), Online publication date: 2-Jan-2010.
- Neis G, Dreyer D and Rossberg A (2009). Non-parametric parametricity, ACM SIGPLAN Notices, 44:9, (135-148), Online publication date: 31-Aug-2009.
- Neis G, Dreyer D and Rossberg A Non-parametric parametricity Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, (135-148)
- Birkedal L, StØvring K and Thamsborg J Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures - Volume 5504, (456-470)
- Benton N and Tabareau N Compiling functional types to relational specifications for low level imperative code Proceedings of the 4th international workshop on Types in language design and implementation, (3-14)
- Benton N and Zarfaty U Formalizing and verifying semantic type soundness of a simple compiler Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming, (1-12)
- Appel A, Melliès P, Richards C and Vouillon J A very modal model of a modern, major, general type system Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (109-122)
- Appel A, Melliès P, Richards C and Vouillon J (2007). A very modal model of a modern, major, general type system, ACM SIGPLAN Notices, 42:1, (109-122), Online publication date: 17-Jan-2007.
- Feng X, Ni Z, Shao Z and Guo Y An open framework for foundational proof-carrying code Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, (67-78)
- Ahmed A Step-Indexed syntactic logical relations for recursive and quantified types Proceedings of the 15th European conference on Programming Languages and Systems, (69-83)
- Ni Z and Shao Z (2006). Certified assembly programming with embedded code pointers, ACM SIGPLAN Notices, 41:1, (320-333), Online publication date: 12-Jan-2006.
- Ni Z and Shao Z Certified assembly programming with embedded code pointers Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (320-333)
- Benton N A typed, compositional logic for a stack-based abstract machine Proceedings of the Third Asian conference on Programming Languages and Systems, (364-380)
- Ahmed A, Fluet M and Morrisett G A step-indexed model of substructural state Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, (78-91)
- Ahmed A, Fluet M and Morrisett G (2005). A step-indexed model of substructural state, ACM SIGPLAN Notices, 40:9, (78-91), Online publication date: 12-Sep-2005.
Index Terms
- Semantics of types for mutable state
Recommendations
Types with semantics: soundness proof assistant
MERLIN '05: Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable bindingWe present a parametric Hoare-like logic for computer-aided reasoning about typeable properties of functional programs. The logic is based on the concept of a specialised assertion, which is a predicate expressing the semantics of a typing judgment in a ...
Rely-guarantee references for refinement types over aliased mutable data
PLDI '13Reasoning about side effects and aliasing is the heart of verifying imperative programs. Unrestricted side effects through one reference can invalidate assumptions about an alias. We present a new type system approach to reasoning about safe assumptions ...
Mutable WadlerFest DOT
FTFJP'17: Proceedings of the 19th Workshop on Formal Techniques for Java-like ProgramsThe Dependent Object Types (DOT) calculus aims to model the essence of Scala, with a focus on abstract type members, path-dependent types, and subtyping. Other Scala features could be defined by translation to DOT.
Mutation is a fundamental feature of ...