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

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

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.