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

软件漏洞是对个人、关键基础设施和国家安全的重大且持续的威胁。这些漏洞中有许多是由于C编程语言的广泛使用而产生的，而C编程语言几乎没有提供针对常见程序员错误影响的保护。新的硬件监控架构可以检测到此类错误并限制其安全影响，但这些保护只有在正确部署时才能发挥作用。该项目旨在构建一个可证明安全的平台，用于在受监控的硬件上执行C代码，使用形式化规范来定义其期望的行为，并使用形式化验证来确认其正确实现。通过展示这一高保证平台的可行性，工程师将能够放心地采用受监控的硬件系统，最终目标是减少对支撑我们世界的系统的网络安全威胁。该项目将正式指定和验证C编译器基础设施，该基础设施针对基于标签的紧急硬件架构，支持灵活高效的安全监控。具体的项目贡献包括：（1）一种新的规范语言，用于以简单灵活的方式描述C级安全特性;（2）用于验证C程序编译及其相关安全特性以生成标记增强机器码的通用技术;（3）一种新的C内存模型，该模型捕获了证明编译器保留程序行为所需的最低内存安全要求;（4）应用编译器框架来实现广泛的C存储器安全策略的正式指定和验证的实现;以及（5）该奖项反映了NSF的法定使命，并通过使用基金会的智力价值进行评估，被认为值得支持和更广泛的影响审查标准。

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.