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

SaTC：核心：小：指定和验证 C 代码到标记硬件的安全编译

基本信息

批准号：
2048499
负责人：
Andrew Tolmach
金额：
$ 49.98万
依托单位：
Portland State University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-04-01 至 2025-03-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2048499&HistoricalAwards=false
关键词：
SaTC CORE Small Specifying Verifying

项目摘要

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.

软件漏洞是对个人，关键基础设施和国家安全的重大威胁。这些漏洞中有许多源于C编程语言的广泛使用，该语言几乎没有保护对常见程序员错误的影响。新的硬件监视体系结构可以检测到此类错误并限制其安全性影响，但是这些保护只有在正确部署时才起作用。该项目旨在构建一个可证明的安全平台，用于在受监视的硬件上执行C代码，并使用正式规范来定义其所需的行为和正式验证，以确认其已正确实施。证明这个高保险平台的可行性将使工程师充满信心地采用受监控的硬件系统，最终的目的是减少对我们世界的基础系统的网络安全威胁。该项目将正式指定和验证COMPILER基础结构，以基于标签的基于标签的硬件结构设置，以支持基于标签的硬件体系结构，从而支持灵活的安全性和有效的安全性。特定的项目贡献包括（1）一种新颖的规范语言，用于以简单且灵活的方式描述C级安全性属性；（2）用于验证C程序及其与标记增强机器代码相关的安全性属性的通用技术；（3）一种新的C内存模型，该模型捕获了证明编译器保留程序行为所需的最低内存安全要求；（4）将编译器框架应用于正式指定和验证的广泛记忆安全策略的实现；（5）该框架的应用在具有控制记忆共享的情况下实施新的政策，以划分计划。该奖项反映了NSF的法定任务，并使用基金会的智力优点和更广泛的审查标准，认为值得通过评估来获得支持。