| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | February 6, 2013 |
| Latest Amendment Date: | May 29, 2017 |
| Award Number: | 1253229 |
| Award Instrument: | Continuing Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | June 1, 2013 |
| End Date: | May 31, 2018 (Estimated) |
| Total Intended Award Amount: | $520,000.00 |
| Total Awarded Amount to Date: | $520,000.00 |
| Funds Obligated to Date: |
FY 2015 = $100,000.00 FY 2016 = $100,000.00 FY 2017 = $100,000.00 |
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
77 MASSACHUSETTS AVE CAMBRIDGE MA US 02139-4301 (617)253-1000 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
77 Massachusetts Avenue Cambridge MA US 02139-4307 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): |
Software & Hardware Foundation, PROGRAMMING LANGUAGES, SOFTWARE ENG & FORMAL METHODS |
| Primary Program Source: |
01001516DB NSF RESEARCH & RELATED ACTIVIT 01001617DB NSF RESEARCH & RELATED ACTIVIT 01001718DB NSF RESEARCH & RELATED ACTIVIT |
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Billions of people depend daily on software systems built on top of slowly changing operating systems, programming languages, and library interfaces. A unifying theme of this infrastructure, from operating systems to Web browsers, is the use of nested sandboxes, involving multiple levels of abstraction, with complete mediation of resource accesses within and across levels. That is, as a program runs, several layers of abstraction are checking all resource accesses for conformance to security and isolation policies. This run-time checking imposes substantial overhead and is also quite inflexible. Often some sandbox layer is fundamentally incompatible with a new programming technique that could bring improved performance, security, etc. We will study how the Bedrock system may be used to replace restrictive run-time policy enforcement with open-ended compile-time policy enforcement, by requiring programmers to distribute code with formal mathematical proofs of policy conformance. As a concrete case study, we will implement a platform to replace today's common combinations of cloud hosting and Web browsers, providing a similar application experience to end users while giving programmers much more flexibility. To educate the future users of our tools, we will also develop an online tutor program suitable for use in introductory discrete math and logic classes, giving students instant feedback on the validity of their rigorous proofs.
The theoretical foundation of Bedrock, a Coq library, is higher-order separation logic for assembly languages. Several past projects have demonstrated how proofs in such logics may be carried out using proof assistants. Bedrock is distinguished by providing tools for mostly automated proofs, where the programmer provides help to the verifier through loop invariants and a few other types of annotation. We will continue improving this automation support to lower the human cost of verification further, while also investigating ways to broaden Bedrock's domain, such as to multi-core programs. We also intend to investigate the new semantic idea of phantom monitors, which allow Bedrock programs to spawn arbitrary automata (defined with their transition relations in Coq) that watch all program behavior and may veto actions that violate some policy. This is a compile time-only feature to support effective specifications, and we hope to use it as a unifying framework for specifying the interfaces between components in our proof-of-concept distributed application platform.
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 grant supported work investigating a particular approach to programming with strong mathematical guarantees of correctness. The unusual features relate to use of proof assistant software, which checks mathematical proofs, which may be about complex computer systems. Work explored how to do programming inside a proof assistant (in particular, the Coq system), so that one integrated environment supports coding, writing down specifications capturing what is correct behavior, writing proofs establishing correctness, and compiling code into executable form.
The initial project plan centered on the Bedrock framework, for producing low-level software through the use of multiple high-level languages. Key demonstrations with Bedrock included verification of a multithreaded web server. There were also crucial technological contributions in proof automation and in structuring of large proofs so that they are broken into manageable pieces, for instance mirroring the decomposition of a program across libraries or languages.
Partly through collaborations with faculty in other research areas, the Bedrock approach was also extended fruitfully to other domains, not envisioned when the original project plan was written. In the Kami project, we support development, proof, and compilation of digital hardware components like processors and memory systems. In the FSCQ project, we support a similar model for creating proved file systems that integrate with real OS kernels. In the Fiat Cryptography project, we support generation of low-level code for fast cryptographic primitives. And two other projects demonstrated how this approach applies to distributed systems, specifically key-value stores and scientific stencil computations.
Broader impacts have included development of a new graduate course with an associated textbook, Formal Reasoning About Programs. There has also been a significant amount of technology transfer to industry. Most notably, Fiat Cryptography has been adopted by Google to generate elliptic-curve arithmetic code for Chrome, Android, and servers (e.g., for the main search engine); so now a majority of secure web connections opened by browsers use code generated and proved with our methods and tools. Two startup companies are also applying our results, in consultation with the PI. BedRock Systems is applying the latest Bedrock library to verification of operating systems for safety-critical applications like in the automotive industry. SiFive, Inc. is piloting use of the Kami framework to prove correctness of key hardware components that factor into their business model of helping customers put together custom hardware solutions via component reuse.
Last Modified: 10/01/2018
Modified by: Adam J Chlipala
Please report errors in award information by writing to: awardsearch@nsf.gov.
