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.