
NSF Org: |
CNS Division Of Computer and Network Systems |
Recipient: |
|
Initial Amendment Date: | March 26, 2021 |
Latest Amendment Date: | May 20, 2021 |
Award Number: | 2048499 |
Award Instrument: | Standard Grant |
Program Manager: |
Selcuk Uluagac
suluagac@nsf.gov (703)292-4540 CNS Division Of Computer and Network Systems CSE Directorate for Computer and Information Science and Engineering |
Start Date: | April 1, 2021 |
End Date: | March 31, 2025 (Estimated) |
Total Intended Award Amount: | $499,838.00 |
Total Awarded Amount to Date: | $499,838.00 |
Funds Obligated to Date: |
|
History of Investigator: |
|
Recipient Sponsored Research Office: |
1600 SW 4TH AVE PORTLAND OR US 97201-5508 (503)725-9900 |
Sponsor Congressional District: |
|
Primary Place of Performance: |
1600 SW 4th Ave Portland OR US 97207-0751 |
Primary Place of
Performance Congressional District: |
|
Unique Entity Identifier (UEI): |
|
Parent UEI: |
|
NSF Program(s): | Secure &Trustworthy Cyberspace |
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 vulnerabilities are a significant and ongoing threat to the security of individuals, critical infrastructure, and the nation. Many of these vulnerabilities arise from the widespread use of the C programming language, which provides little protection against the effects of common programmer mistakes. New hardware monitoring architectures can detect such errors and limit their security impact, but these protections only work when they are deployed correctly. This project aims to build a provably secure platform for executing C code on monitored hardware, using formal specification to define its desired behavior and formal verification to confirm that it is correctly implemented. Demonstrating the feasibility of this high-assurance platform will make it possible for engineers to adopt monitored hardware systems with confidence, with the ultimate goal of reducing cybersecurity threats to the systems that underpin our world.
The project will formally specify and verify C compiler infrastructure that targets emergent tag-based hardware architectures which support flexible and efficient security monitoring. Specific project contributions include (1) a novel specification language for describing C-level security properties in simple and flexible ways; (2) generic techniques for verified compilation of C programs and their associated security properties to tag-enhanced machine code; (3) a new C memory model which captures the minimum memory safety requirements needed to prove that the compiler preserves program behavior; (4) application of the compiler framework to implement formally specified and verified implementations of a broad spectrum of C memory safety policies; and (5) application of the framework to implement novel policies for compartmentalizing programs with controlled memory sharing.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
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.
Much of the legacy software that supports critical computing infrastructure is written in the C programming language, which
notoriously lacks protection against common programmer errors that
often lead to exploitable security flaws. One way to mitigate the
risks of using C is to run code in a monitored environment that can
detect potentially dangerous program behaviors. Monitoring can be
suitable both in fielded systems and in testing environments. It can
be implemented using different combinations of hardware and software
support, with different cost/performance trade-offs. A useful
monitoring system should be flexible, so that it can be targeted at
many different kinds of bugs, and highly reliable, so that the system
provides strong guarantees does not itself introduce new security
concerns.
In this project we developed Tagged C, a novel formalism for
specifying and enforcing security policies via monitors. In Tagged C,
policies are expressed in terms of metadata tags that are conceptually
attached to all values flowing through the program. Tagged C is
equipped with a formal semantics that extends ordinary C behavior by
propagating and checking tags at each program point. We built two
software-based implementations for Tagged C: an interpreter based on
the CompCert verified C compiler (and provably faithful to the
semantics), and a source-to-source transformation that inserts
monitoring instrumentation. Ultimately, we intend Tagged C to be
compiled to machine code for hardware with built-in tag support; a
realistic verified compiler remains future work, but we have formally
verified (in the Rocq proof assistant) correctness of memory behavior
for a simplified compiler. We have successfully used Tagged C to
define a variety of security policies, including memory safety,
compartmentalization, and information flow. Finally, we have
integrated Tagged C into an automated testing ("fuzzing") framework,
and have begun to explore how to use specialized policies to make
fuzzing results more precise and actionable.
Overall, we have demonstrated the feasibility of using C-level tag-based
security policies to detect important classes of errors in C programs.
We expect Tagged C to be a useful tool in future attempts to tame the
bad behaviors of C programs. In addition, this project trained
several PhD students to work in formal specification and verification.
Last Modified: 06/23/2025
Modified by: Andrew P Tolmach
Please report errors in award information by writing to: awardsearch@nsf.gov.