Award Abstract # 2048499
SaTC: CORE: Small: Specifying and Verifying Secure Compilation of C Code to Tagged Hardware

NSF Org: CNS
Division Of Computer and Network Systems
Recipient: PORTLAND STATE UNIVERSITY
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: FY 2021 = $499,838.00
History of Investigator:
  • Andrew Tolmach (Principal Investigator)
Recipient Sponsored Research Office: Portland State University
1600 SW 4TH AVE
PORTLAND
OR  US  97201-5508
(503)725-9900
Sponsor Congressional District: 01
Primary Place of Performance: Portland State University
1600 SW 4th Ave
Portland
OR  US  97207-0751
Primary Place of Performance
Congressional District:
01
Unique Entity Identifier (UEI): H4CAHK2RD945
Parent UEI: WWUJS84WJ647
NSF Program(s): Secure &Trustworthy Cyberspace
Primary Program Source: 01002122DB NSF RESEARCH & RELATED ACTIVIT
Program Reference Code(s): 025Z, 7923
Program Element Code(s): 806000
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.

Anderson, Sean and Naaktgeboren, Allison and Tolmach, Andrew "Flexible Runtime Security Enforcement with Tagged C" Runtime Verification 23rd International Conference, RV 2023 , 2023 Citation Details
Anderson, Sean Noble and Blanco, Roberto and Lampropoulos, Leonidas and Pierce, Benjamin C. and Tolmach, Andrew "Formalizing Stack Safety as a Security Property" 2023 IEEE 36th Computer Security Foundations Symposium (CSF) , 2023 https://doi.org/10.1109/CSF57540.2023.00037 Citation Details
Thibault, Jérémy and Blanco, Roberto and Lee, Dongjae and Argo, Sven and Azevedo_de_Amorim, Arthur and Georges, Aïna Linn and Hricu, Ctlin and Tolmach, Andrew "SECOMP: Formally Secure Compilation of Compartmentalized C Programs" , 2024 https://doi.org/10.1145/3658644.3670288 Citation Details
Tolmach, Andrew and Chhak, Chris and Anderson, Sean "Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model" , v.309 , 2024 https://doi.org/10.4230/LIPICS.ITP.2024.36 Citation Details

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.

Print this page

Back to Top of page