1. A type system for extracting functional specifications from memory-safe imperative programs
- Author
-
Adam Wick, Matthew Yacavone, Paul He, Aaron Tomb, Chris Phifer, Steve Zdancewic, Karl Smeltzer, Andrei Ştefănescu, Eddy Westbrook, Valentin Robert, and Brent Carmer
- Subjects
Functional specification ,Programming language ,Computer science ,020207 software engineering ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,01 natural sciences ,Index (publishing) ,010201 computation theory & mathematics ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,0202 electrical engineering, electronic engineering, information engineering ,Key (cryptography) ,Array data structure ,Purely functional ,State (computer science) ,Safety, Risk, Reliability and Quality ,computer ,Memory safety ,Software - Abstract
Verifying imperative programs is hard. A key difficulty is that the specification of what an imperative program does is often intertwined with details about pointers and imperative state. Although there are a number of powerful separation logics that allow the details of imperative state to be captured and managed, these details are complicated and reasoning about them requires significant time and expertise. In this paper, we take a different approach: a memory-safe type system that, as part of type-checking, extracts functional specifications from imperative programs. This disentangles imperative state, which is handled by the type system, from functional specifications, which can be verified without reference to pointers. A key difficulty is that sometimes memory safety depends crucially on the functional specification of a program; e.g., an array index is only memory-safe if the index is in bounds. To handle this case, our specification extraction inserts dynamic checks into the specification. Verification then requires the additional proof that none of these checks fail. However, these checks are in a purely functional language, and so this proof also requires no reasoning about pointers.
- Published
- 2021