-
3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers
Authors:
Sarah Fakhoury,
Markus Kuppe,
Shuvendu K. Lahiri,
Tahina Ramananandro,
Nikhil Swamy
Abstract:
Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted. However, distilling inform…
▽ More
Improper parsing of attacker-controlled input is a leading source of software security vulnerabilities, especially when programmers transcribe informal format descriptions in RFCs into efficient parsing logic in low-level, memory unsafe languages. Several researchers have proposed formal specification languages for data formats from which efficient code can be extracted. However, distilling informal requirements into formal specifications is challenging and, despite their benefits, new, formal languages are hard for people to learn and use.
In this work, we present 3DGen, a framework that makes use of AI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications in a language called 3D. To support humans in understanding and trusting the generated specifications, 3DGen uses symbolic methods to also synthesize test inputs that can be validated against an external oracle. Symbolic test generation also helps in distinguishing multiple plausible solutions. Through a process of repeated refinement, 3DGen produces a 3D specification that conforms to a test suite, and which yields safe, efficient, provably correct, parsing code in C.
We have evaluated 3DGen on 20 Internet standard formats, demonstrating the potential for AI-agents to produce formally verified C code at a non-trivial scale. A key enabler is the use of a domain-specific language to limit AI outputs to a class for which automated, symbolic analysis is tractable.
△ Less
Submitted 6 May, 2024; v1 submitted 16 April, 2024;
originally announced April 2024.
-
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
Authors:
Guido Martínez,
Danel Ahman,
Victor Dumitrescu,
Nick Giannarakis,
Chris Hawblitzel,
Catalin Hritcu,
Monal Narasimhamurthy,
Zoe Paraskevopoulou,
Clément Pit-Claudel,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem Rastogi,
Nikhil Swamy
Abstract:
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to generate verified code automatically.
Meta-F* is implemented as an F* effect, which, given the p…
▽ More
We introduce Meta-F*, a tactics and metaprogramming framework for the F* program verifier. The main novelty of Meta-F* is allowing the use of tactics and metaprogramming to discharge assertions not solvable by SMT, or to just simplify them into well-behaved SMT fragments. Plus, Meta-F* can be used to generate verified code automatically.
Meta-F* is implemented as an F* effect, which, given the powerful effect system of F*, heavily increases code reuse and even enables the lightweight verification of metaprograms. Metaprograms can be either interpreted, or compiled to efficient native code that can be dynamically loaded into the F* type-checker and can interoperate with interpreted code. Evaluation on realistic case studies shows that Meta-F* provides substantial gains in proof development, efficiency, and robustness.
△ Less
Submitted 7 March, 2019; v1 submitted 17 March, 2018;
originally announced March 2018.
-
A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Authors:
Niklas Grimm,
Kenji Maillard,
Cédric Fournet,
Catalin Hritcu,
Matteo Maffei,
Jonathan Protzenko,
Tahina Ramananandro,
Aseem Rastogi,
Nikhil Swamy,
Santiago Zanella-Béguelin
Abstract:
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than develo** separate tools for special classes of effects and relational properties, we advocate using a general purpos…
▽ More
Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than develo** separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs.
We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and game-based cryptographic security. By relying on SMT-based automation, unary weakest preconditions, user-defined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer.
△ Less
Submitted 12 October, 2019; v1 submitted 28 February, 2017;
originally announced March 2017.
-
Verified Low-Level Programming Embedded in F*
Authors:
Jonathan Protzenko,
Jean-Karim Zinzindohoué,
Aseem Rastogi,
Tahina Ramananandro,
Peng Wang,
Santiago Zanella-Béguelin,
Antoine Delignat-Lavaud,
Catalin Hritcu,
Karthikeyan Bhargavan,
Cédric Fournet,
Nikhil Swamy
Abstract:
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it h…
▽ More
We present Low*, a language for low-level programming and verification, and its application to high-assurance optimized cryptographic libraries. Low* is a shallow embedding of a small, sequential, well-behaved subset of C in F*, a dependently-typed variant of ML aimed at program verification. Departing from ML, Low* does not involve any garbage collection or implicit heap allocation; instead, it has a structured memory model à la CompCert, and it provides the control required for writing efficient low-level security-critical code.
By virtue of ty**, any Low* program is memory safe. In addition, the programmer can make full use of the verification power of F* to write high-level specifications and verify the functional correctness of Low* code using a combination of SMT automation and sophisticated manual proofs. At extraction time, specifications and proofs are erased, and the remaining code enjoys a predictable translation to C. We prove that this translation preserves semantics and side-channel resistance.
We provide a new compiler back-end from Low* to C and, to evaluate our approach, we implement and verify various cryptographic algorithms, constructions, and tools for a total of about 28,000 lines of code, specification and proof. We show that our Low* code delivers performance competitive with existing (unverified) C cryptographic libraries, suggesting our approach may be applicable to larger-scale low-level software.
△ Less
Submitted 11 December, 2018; v1 submitted 28 February, 2017;
originally announced March 2017.
