| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | July 28, 2016 |
| Latest Amendment Date: | June 29, 2020 |
| Award Number: | 1563393 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Nina Amla
namla@nsf.gov (703)292-7991 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | August 1, 2016 |
| End Date: | August 31, 2020 (Estimated) |
| Total Intended Award Amount: | $145,500.00 |
| Total Awarded Amount to Date: | $145,500.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
600, MOUNTAIN AVENUE MURRAY HILL NJ US 07974-2008 (469)991-4503 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
600-700 Mountain Avenue Murray Hill NJ US 07974-0636 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
Software is embedded into our daily activities. Ensuring that the software is trustworthy - does what is intended - and secure - is not vulnerable to attack - is a prime concern. Much attention has been devoted to establishing the correctness of high-level programs. This project is focused on the important task of ensuring that the, often complex and opaque, transformations carried out by a compiler do not degrade the trustworthiness and security guarantees of its input program.
The key innovation pursued in this project is self-certification which guarantees the correctness and security of compilation. A self-certifying compiler creates a tangible, independently-checkable proof, justifying the correctness of the compilation run. By linking in information from external analysis tools certificates can also aid in obtaining better machine code. In particular, they allow for automatic insertion of defensive measures, which protect the program from common security attacks. This work builds on existing theoretical ideas and compiler implementations, while extending them in new directions. The self-certifying compiler is implemented in the popular LLVM framework, making it suitable for immediate adoption by programmers, and its security benefits available to end users in a transparent fashion. Provable program correctness is a true "Grand Challenge" for computing. By developing both theory and implementation of a self-certifying compiler, this project is taking a significant step forward in meeting that challenge.
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.
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.
During this project we enhanced the theory of verifiable certificates (also called witnesses) with which to establish the correctness of compiler optimizations.
We began with the approach of "semantic equivalence," that is, of showing that the code before and after compilation has equivalent behavior. The witnesses generated by a self-certifying compiler considerably simplify such proofs, by letting them to be carried out in small digestable chunks. We enhanced this method to use "syntactic" reasoning that is akin to rewriting or syntactic equality under renaming of variables. As far as we know, this is the first comprehensive approach to translation validation that combines the two, almost opposing, techniques of syntactic equality and semantic equivalence.
We implemented this combined approach to certify LLVM's interprocedural optimizations, obtaining significant speedups in the certification process. Furthermore, we have also implemented a self-certification infrastructure for WebAssembly, a new intermediate language that is supported by all major web browsers.
Preservation of semantics does not imply preservation of security. In fact, some known optimizations are semantic preserveing while making the code more vulnerable, as in exposing a secret for longer than necessary. We extended self-certification to security, showing how custom security certificates could be generated for a large class of useful security properties, guaranteeing their preservation across a chain of optimizations.
Last Modified: 09/04/2020
Modified by: Kedar S Namjoshi
Please report errors in award information by writing to: awardsearch@nsf.gov.
