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.

保护通过计算系统操纵的信息的机密性是当今网络安全社区面临的最重要挑战之一。许多复杂的系统，例如操作系统，管理程序，网络浏览器和分布式系统，都要求用户相信私人信息与其他用户正确隔离。现实世界中的系统充满了错误，因此这种信任的假设是不合理的。这项拟议的研究的目的是将正式方法应用于复杂的安全敏感系统，以便我们可以向用户保证这些系统确实值得信赖。不幸的是，实现这一目标的方式存在着许多艰巨的挑战。一个挑战是如何指定复杂系统的所需安全策略。在现实世界中，纯净的非干预太强大了，无法有用。至关重要的是要支持更宽松的安全策略，以允许用户之间的某些明确的信息流，例如明确的拆分。第二个挑战是，现实世界中的系统通常是用C和汇编等低级语言编写的，但是这些语言在传统上很难推论。第三个挑战是如何实际进行低级代码进行安全证明，然后将所有内容链接到系统范围的保证中。在这项工作中，PI建议设计和实施一套新的正式技术和工具，以克服所有这些挑战。首先，PI将开发一种新的方法，用于使用单个统一机制（称为“观察功能”）正式指定，证明和传播信息流安全策略。根据经典非干预的表达概括，使用一种通用方法来指定策略，该方法既包含了安全标签的证明和信息隐藏的证明，又可以使用一种特殊的模拟来跨抽象层传播，以保证保留安全性。其次，为了证明新方法的有效性，PI将在COQ证明助手中建立一个实际的端到端安全性证明，并在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

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