NSF Award Search: Award # 1512611 - SHF: Medium: Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem Prover

National Science Foundation

Award Abstract # 1512611

SHF: Medium: Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem Prover

NSF Org:	CCF Division of Computing and Communication Foundations
Awardee:	MASSACHUSETTS INSTITUTE OF TECHNOLOGY
Initial Amendment Date:	June 11, 2015
Latest Amendment Date:	July 5, 2016
Award Number:	1512611
Award Instrument:	Standard Grant
Program Manager:	Anindya Banerjee abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Direct For Computer & Info Scie & Enginr
Start Date:	September 1, 2015
End Date:	August 31, 2020 (Estimated)
Total Intended Award Amount:	$800,000.00
Total Awarded Amount to Date:	$816,016.00
Funds Obligated to Date:	FY 2015 = $800,000.00 FY 2016 = $16,016.00
History of Investigator:	Adam Chlipala (Principal Investigator) adamc@csail.mit.edu
Awardee Sponsored Research Office:	Massachusetts Institute of Technology 77 MASSACHUSETTS AVE Cambridge MA US 02139-4301 (617)253-1000
Sponsor Congressional District:	07
Primary Place of Performance:	Massachusetts Institute of Technology 77 Massachusetts Avenue Cambridge MA US 02139-4307
Primary Place of Performance Congressional District:	07
Unique Entity Identifier (UEI):
Parent UEI:
NSF Program(s):	Software & Hardware Foundation
Primary Program Source:	040100 NSF RESEARCH & RELATED ACTIVIT 040100 NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s):	7924, 7943, 9251
Program Element Code(s):	7798
Award Agency Code:	4900
Fund Agency Code:	4900
Assistance Listing Number(s):	47.070

ABSTRACT

Title: SHF: Medium: Fiat: Correct-by-Construction and Mostly Automated Derivation of Programs with an Interactive Theorem Prover

To scale to ambitious software-development tasks, programming languages must provide features for abstraction and modularity. Large advances in programming productivity have often come via new features of that kind. This project investigates new program-structuring ideas based fundamentally on machine-checked mathematical proofs. More specifically, through the design of a prototype system Fiat within the Coq proof assistant, the project studies how to derive efficient programs automatically from logical specifications. Programmers may package new notations and associated styles of automation as libraries, and a single program may mix notations, automatically benefiting from the combination of all of their associated automation for deriving efficient programs. In this way, Fiat makes it possible to split a program into parts for functionality and performance, with strong guarantees that bugs in the performance parts can never violate the requirements in the functionality parts. The intellectual merits are widely applicable new ideas in modular program structuring, with strong formal guarantees of correctness. The project's broader significance and importance are based on the potential to improve programmer productivity dramatically, for software projects in a wide variety of contexts; and the project also studies how the idea of mostly automated refinement from specifications can be integrated into introductory programming and discrete-math classes, to drive home the value of logical notation in programming.

The primary case-study domain in the project is practical Internet servers, such as for domain-name lookup or delivery of electronic mail. The goal is to develop Fiat versions of these key services, deriving efficient executable code automatically. Past work on deriving data layers from specifications in the style of SQL is being extended, in addition to exploration of other domains for specification and automated derivation, such as synthesis of parsers from grammars, to use for the protocols that servers speak, the configuration files that they read, etc. Beyond studying how such new libraries may be constructed and composed, the project also investigates how to push the synthesis process to lower abstraction levels than in our prototype implementation, which generates functional programs. The improved Fiat system will derive assembly programs, enabling choice of more effective optimizations thanks to more direct control of machine resources, integrating with the Bedrock Coq library for verified multilanguage programming.

PUBLICATIONS PRODUCED AS A RESULT OF THIS RESEARCH

Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher. Some full text articles may not yet be available without a charge during the embargo (administrative interval).

Some links on this page may take you to non-federal websites. Their policies may differ from this site.

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit--Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye "The End of History? Using a Proof Assistant to Replace Language Design with Library Design" SNAPL , 2017

Jason Gross, Andres Erbsen, Adam Chlipala "Reification by Parametricity: Fast Setup for Proof by Reflection, in Two Lines of Ltac" ITP , 2018

Peng Wang, Di Wang, Adam Chlipala "TiML: A Functional Language for Practical Complexity Analysis with Invariants" OOPSLA , 2017

Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala "Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises" IEEE Security and Privacy , 2019

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala "Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats" ICFP , 2019

Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye "The End of History? Using a Proof Assistant to Replace Language Design with Library Design" Proceedings of the The 2nd Summit oN Advances in Programming Languages (SNAPL'17) , 2017

Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, Adam Chlipala "Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises" Proceedings of the IEEE Symposium on Security & Privacy 2019 (S&P'19) , 2019

Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, Adam Chlipala "Narcissus: Correct-By-Construction Derivation of Decoders and Encoders from Binary Formats" Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP'19) , 2019

Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross, Adam Chlipala "Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs" Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR'20) , 2020

PROJECT OUTCOMES REPORT

Disclaimer

This Project Outcomes Report for the General Public is displayed verbatim as submitted by the Principal Investigator (PI) for this award. Any opinions, findings, and conclusions or recommendations expressed in this Report are those of the PI and do not necessarily reflect the views of the National Science Foundation; NSF has not approved or endorsed its content.

This project studied how to use computer-theorem-proving tools to write software automatically from mathematical specifications, also automatically producing proof that the software behaves correctly. One of the first programming domains we studied was relational querying and updating, in the style of SQL, a popular database language. In the course of this grant, we upgraded our support within that domain, with automatic selection of data structures by analysis of access patterns in specifications. We also added Narcissus, a domain for parsing and generation of binary network-packet formats, starting from nondeterministic generators of bitstrings from high-level representations, as specifications. A further domain was network-firewall rules, where efficient specialized software can be constructed from naive specifications that analyze complete histories of packets so far.
We also studied a cross-cutting feature: generating efficient imperative code (e.g., not relying on garbage collection) automatically from purely functional code. Our solution is extensible, in the form of a compiler that can be taught new tricks for generating imperative code along with its proof of correctness. Each new trick must come with a proof (or a proof generator) of correctness. Combining these pieces (also using the Bedrock framework for program verification and verified compilation), we produced the first pipeline to go automatically from relational specifications to efficient assembly code with proof of correctness.
One offshoot of the project, which was combined with our DeepSpec Expedition effort, is Fiat Cryptography, which generates high-performance cryptography routines automatically with proof. Specifically, we targeted finite-field arithmetic for elliptic-curve cryptography, where the previous state of practice was to rewrite code manually in C or assembly for each different elliptic curve and each family of hardware architectures (principally 32-bit vs. 64-bit). We showed that these algorithms could be generalized into high-level templates that can be proved once-and-for-all, then specialized to parameters and compiled to lean code by a verified compiler. The result is a domain-specific compiler that can be invoked as easily as standard tools like GCC. It has been adopted in a number of high-profile open-source projects, including parts of TLS code for both Chrome and Firefox, so that today a majority of secure web connections made by browsers run TLS code generated by our formally verified Fiat Cryptography compiler.

Last Modified: 12/30/2020
Modified by: Adam J Chlipala

Please report errors in award information by writing to: awardsearch@nsf.gov.