SaTC: CORE: Small: Specifying and Verifying Secure Compilation of C Code to Tagged Hardware

点击翻译按钮获取中文摘要

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.