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.