SaTC: CORE: Small: Formal End-to-End Verification of Information-Flow Security for Complex Systems

保护计算机系统操作信息的机密性是当今网络安全社区面临的最重要挑战之一。许多复杂的系统，如操作系统、虚拟机管理程序、Web浏览器和分布式系统，都要求用户相信私人信息与其他用户正确隔离。然而，现实世界的系统充满了错误，因此这种信任的假设是不合理的。 这项研究的目标是将形式化方法应用于复杂的安全敏感系统，这样我们就可以向用户保证这些系统确实是值得信赖的。不幸的是，在实现这一目标的道路上存在着许多令人望而却步的挑战。一个挑战是如何指定复杂系统所需的安全策略。在真实的世界中，纯粹的不干涉太强了，没有用。支持更宽松的安全策略是至关重要的，这些策略允许用户之间特定的信息流，例如显式解密。第二个挑战是，现实世界的系统通常是用低级语言编写的，比如C和汇编，但这些语言传统上很难推理。第三个挑战是如何在底层代码上进行安全性证明，然后将所有内容链接到系统范围内的保证中。在这方面，PI建议设计和实现一套新的正式技术和工具，以克服所有这些挑战。首先，PI将开发一种新的方法，使用一种称为“观察功能”的统一机制来正式指定、证明和传播信息流安全策略。“一个策略是根据经典不干涉的表达性概括来指定的，使用一种包含安全标签证明和信息隐藏证明的通用方法来证明，并使用一种特殊的模拟来保证保持安全性，并在抽象层之间传播。 其次，为了证明新方法的有效性，PI将构建一个实际的端到端的安全证明，完全形式化和机器检查的Coq证明助手，一个非平凡的并发操作系统内核。 第三，PI还将通过使用虚拟化时间特性扩展内核来演示该方法的通用性和可扩展性，该特性允许用户进程对自己的执行进行计时。我们的目标是证明用户进程不能利用虚拟时间作为信息通道。构建经过认证的安全系统软件的技术将大大提高世界关键基础设施中许多关键组件的可靠性和安全性。 它将推进人类在软件规范和理解方面的知识，并通过将正式方法的新课程推向现有的网络安全课程来促进美国大学的文化变革。

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. Many complex systems, such as operating systems, hypervisors, web browsers, and distributed systems, require a user to trust that private information is properly isolated from other users. Real-world systems are full of bugs, however, so this assumption of trust is not reasonable. The goal of this proposed research is to apply formal methods to complex security-sensitive systems, in such a way that we can guarantee to users that these systems really are trustworthy. Unfortunately, there are numerous prohibitive challenges standing in the way of achieving this goal. One challenge is how to specify the desired security policy of a complex system. In the real world, pure noninterference is too strong to be useful. It is crucial to support more lenient security policies that allow for certain well-specified information flows between users, such as explicit declassifications. A second challenge is that real-world systems are usually written in low-level languages like C and assembly, but these languages are traditionally difficult to reason about. A third challenge is how to actually go about conducting a security proof over low-level code and then link everything together into a system-wide guarantee.In this effort, the PI proposes to design and implement a new set of formal techniques and tools for overcoming all of these challenges. First, the PI will develop a new methodology for formally specifying, proving, and propagating information-flow security policies using a single unifying mechanism, called the "observation function." A policy is specified in terms of an expressive generalization of classical noninterference, proved using a general method that subsumes both security-label proofs and information-hiding proofs, and propagated across layers of abstraction using a special kind of simulation that is guaranteed to preserve security. Second, to demonstrate the effectiveness of the new methodology, the PI will build an actual end-to-end security proof, fully formalized and machine-checked in the Coq proof assistant, of a nontrivial concurrent operating system kernel. Third, the PI will also demonstrate the generality and extensibility of the methodology by extending the kernel with a virtualized time feature allowing user processes to time their own executions. The goal is to prove that user processes cannot exploit virtualized time as an information channel. The technology for building certified secure system software will dramatically improve the reliability and security of many key components in the world's critical infrastructure. It will advance human knowledge in the specification and understanding of software and catalyze a cultural change in U.S. universities by pushing new courses on formal methods into the existing cybersecurity curriculum.