SaTC: CORE: Small: verifying security for data non-interference

SaTC：核心：小：验证数据互不干扰的安全性

• 批准号: 1812522
• 负责人: Nickolai Zeldovich
• 金额: $ 50万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-09-01 至 2022-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1812522&HistoricalAwards=false
• 关键词: SaTC; CORE; Small; verifying; security

Many security problems today stem from bugs in software. Although there has been significant effort in reducing bugs through better testing, fuzzing, model checking, and so on, subtle bugs remain and continue to be exploited. This proposal explores the use of formal verification to prove security of a file system implementation along with an example application in the form of a mail server. Machine-checked verification is a powerful approach that can eliminate a large class of bugs in software by proving that an implementation meets a precise specification. As long as the specification rules out a certain class of bugs, the machine-checked proof will ensure no such bugs can exist in the implementation. This project develops techniques for proving security of sophisticated applications, such as proving that a mail server will not inappropriately disclose confidential email messages. At the high level, the impact of this work will be a more secure software infrastructure.The key technical challenge that this project focuses on is data confidentiality. The project explores approaches for specifying confidentiality of systems software, including a mail server and a POSIX file system, as well as a framework for implementation and machine-checked verification of confidentiality properties for these applications. The project also develops common infrastructure that such applications depend on, including a formal security specification for a POSIX file system and verified implementations of a mail server and a file system with proofs of security, which will be useful to the broader community. Finally, part of the project involves developing course modules focused on machine-checked proofs of correctness and security for systems software.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.

今天的许多安全问题都源于软件中的错误。尽管在通过更好的测试、模糊、模型检查等减少错误方面已经做出了很大努力，但仍然存在并继续利用微妙的错误。该提案探讨了如何使用正式验证来证明文件系统实现的安全性，以及一个邮件服务器形式的示例应用程序。机器检查验证是一种强大的方法，它可以通过证明实现满足精确的规范来消除软件中的一大类错误。只要规范排除了某一类错误，机器检查的证明将确保在实现中不存在这样的错误。该项目开发了用于证明复杂应用程序的安全性的技术，例如证明邮件服务器不会不适当地泄露机密电子邮件消息。在高层次上，这项工作的影响将是一个更安全的软件基础设施。这个项目关注的关键技术挑战是数据保密性。该项目探讨了规定系统软件机密性的方法，包括邮件服务器和POSIX文件系统，以及这些应用程序机密性属性的实施和机检核查框架。该项目还开发了此类应用程序所依赖的公共基础设施，包括POSIX文件系统的正式安全规范，以及具有安全证明的邮件服务器和文件系统的经过验证的实现，这将对更广泛的社区有用。最后，该项目的一部分涉及开发课程模块，重点是系统软件的正确性和安全性的机器检查证明。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Notary: a device for secure transaction approval

• DOI: 10.1145/3341301.3359661
• 发表时间: 2019-10
• 期刊: Proceedings of the 27th ACM Symposium on Operating Systems Principles
• 作者: Anish Athalye;A. Belay;M. Kaashoek;R. Morris;Nickolai Zeldovich

Verifying Hardware Security Modules with Information-Preserving Refinement

• 发表时间: 2022
• 作者: Anish Athalye;M. Kaashoek;Nickolai Zeldovich

Proving confidentiality in a file system using DISKSEC

使用 DISKSEC 证明文件系统的机密性

• 发表时间: 2018
• 期刊: Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation (OSDI
• 作者: Ileri, Atalay;Chajed, Tej;Chlipala, Adam;Kaashoek, Frans;Zeldovich, Nickolai
• 通讯作者: Zeldovich, Nickolai