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

SaTC：核心：小型：复杂系统信息流安全的正式端到端验证

基本信息

批准号：
1715154
负责人：
Zhong Shao
金额：
$ 50万
依托单位：
Yale University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-08-01 至 2020-07-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1715154&HistoricalAwards=false
关键词：
SaTC CORE Small Formal End

项目摘要

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.

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

项目成果

期刊论文数量（14）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

CompCertELF: verified separate compilation of C programs into ELF object files

DOI：
10.1145/3428265
发表时间：
2020-11
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao
通讯作者：
Yuting Wang;Xiangzhe Xu;Pierre Wilke;Zhong Shao

Blinder: Partition-Oblivious Hierarchical Scheduling

Blinder：忽略分区的分层调度

DOI：
发表时间：
2021
期刊：
Proceedings of the 30th USENIX Security Symposium (USENIX Security 2021
影响因子：
0
作者：
Yoon, Man-Ki;Liu, Mengqi;Chen, Hao;Kim, Jung-Eun;Shao, Zhong
通讯作者：
Shao, Zhong

ADLP: Accountable Data Logging Protocol for Publish-Subscribe Communication Systems

DOI：
10.1109/icdcs.2019.00117
发表时间：
2019-07
期刊：
2019 IEEE 39th International Conference on Distributed Computing Systems (ICDCS)
影响因子：
0
作者：
Man-Ki Yoon;Zhong Shao
通讯作者：
Man-Ki Yoon;Zhong Shao

Refinement-Based Game Semantics and Certified Abstraction Layers

基于细化的游戏语义和经过认证的抽象层