SHF: Medium: Self-certifying Compilation and its Applications

SHF：Medium：自认证编译及其应用

• 批准号: 1564296
• 负责人: Lenore Zuck
• 金额: $ 85.45万
• 依托单位: University of Illinois at Chicago
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-08-01 至 2020-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1564296&HistoricalAwards=false
• 关键词: SHF; Medium; Self; certifying; Compilation

Software is embedded into our daily activities. Ensuring that the software is trustworthy - does what is intended - and secure - is not vulnerable to attack - is a prime concern. Much attention has been devoted to establishing the correctness of high-level programs. This project is focused on the important task of ensuring that the, often complex and opaque, transformations carried out by a compiler do not degrade the trustworthiness and security guarantees of its input program.The key innovation pursued in this project is self-certification which guarantees the correctness and security of compilation. A self-certifying compiler creates a tangible, independently-checkable proof, justifying the correctness of the compilation run. By linking in information from external analysis tools certificates can also aid in obtaining better machine code. In particular, they allow for automatic insertion of defensive measures, which protect the program from common security attacks. This work builds on existing theoretical ideas and compiler implementations, while extending them in new directions. The self-certifying compiler is implemented in the popular LLVM framework, making it suitable for immediate adoption by programmers, and its security benefits available to end users in a transparent fashion. Provable program correctness is a true "Grand Challenge" for computing. By developing both theory and implementation of a self-certifying compiler, this project is taking a significant step forward in meeting that challenge.

软件嵌入到我们的日常活动中。确保软件是值得信赖的-做什么是打算-和安全-是不容易受到攻击-是一个主要的关注。许多注意力已经投入到建立高级程序的正确性。该项目的重点是确保编译器执行的通常复杂和不透明的转换不会降低其输入程序的可信度和安全性保证的重要任务。该项目所追求的关键创新是保证编译正确性和安全性的自认证。自证明编译器创建一个有形的、可独立检查的证明，证明编译运行的正确性。通过链接来自外部分析工具的信息，证书也可以帮助获得更好的机器代码。特别是，它们允许自动插入防御措施，保护程序免受常见的安全攻击。这项工作建立在现有的理论思想和编译器实现，同时在新的方向上扩展它们。自认证编译器在流行的LLVM框架中实现，使其适合程序员立即采用，并以透明的方式向最终用户提供其安全优势。可证明的程序正确性是计算的一个真正的“大挑战”。通过开发自证明编译器的理论和实现，该项目在迎接这一挑战方面迈出了重要的一步。

项目成果

Exact quantitative probabilistic model checking through rational search

通过理性搜索精确定量概率模型检查

• DOI: 10.1007/s10703-020-00348-y
• 发表时间: 2020
• 期刊: Formal Methods in System Design
• 影响因子: 0.8
• 作者: Mathur, Umang;Bauer, Matthew S.;Chadha, Rohit;Sistla, A. Prasad;Viswanathan, Mahesh
• 通讯作者: Viswanathan, Mahesh