基于最小信任基的可信系统构建与验证方法研究

Nowadays, we are suffering serious threats and attacks on computer and securities in national security, powering, financing, medical services, etc. We are facing three main security problems among them: the system platform tends to be compromised, software design is easy to leak bugs, and remote nodes are hard to be trusted. This project plans to construct and verify the trusted system based on minimal trusted computing base (TCB). It lies in 4 aspects: 1) we study how to measure and protect the system data based on dynamic root of trust, to prevent from tampering or stealing, to minimize the size of TCB to reduce the possibility of potential attacks, and to provide enough interfaces for upper application; 2) we study how to formally model, refine and prove the data security, to prevent from design bugs in system software and applications; 3) we study how to design remote attestation to enhance trustworthy and efficiency; 4) we study how to formally verify remote attestation based on Pi-calculus, to ensure the security of remote protocols and reduce the difficulty and complexity of formal verifying. The purpose of the project is to provide a minimal trusted base system, to solve the problem of platform integrity, correctness of software design and trustworthiness of remote nodes, to promote the development in the research field of system security.

现如今，我们的国防、能源、金融、医疗正遭受着严重的计算机系统和网络安全威胁与攻击。其中，我们面临三个重要系统安全问题：系统平台易被篡改、软件设计易出漏洞、远程结点难以信任。本课题拟研究基于最小信任基的可信系统构建与验证技术：研究基于动态可信根的系统数据完整性度量与保护技术，防止敌方恶意篡改或窃取数据，缩小信任基体积以减少设计漏洞的可能，同时尽可能提供丰富上层接口以降低应用软件的设计难度；研究基于Event-B的数据安全形式化建模、精化与证明技术，更细粒度地确保底层系统及应用软件不存在设计漏洞；研究基于TPM2.0的远程身份及平台可信性证明技术，提高远程证明的可信性及高效性；研究基于Pi演算的可信认证协议形式化验证技术，确保远程协议的设计安全，并减少协议的验证难度及工作量。本课题的目的就是提供一种最小信任基系统，解决平台完整性、设计可靠性、远程可证明性问题，为推进系统安全研究发展作出贡献。

计算机系统与网络安全面临三个研究难题：平台完整性、设计可靠性、远程可信性问题。最小信任基技术已成为解决上述问题的热门研究方法。然而，这些研究存在诸多不完善的地方，以致于其技术仍未商用及广泛运用。其中，最重要的两个研究挑战在于：(1)如何权衡可信基的系统体积与安全风险，使用两者均达到令人满意的程度；(2)如何设计有效的形式化验证方法，以方便地证明每一个最小信任基以及整个系统的安全。为此，本课题研究上述三个难题、两个挑战，为推进系统安全研究发展作出贡献。.我们的项目主要贡献如下：.(1) 提出一套安全协议通用全自动形式化验证平台.我们提出一套安全协议通用全自动形式化验证平台SmartVerif。我们采取深度学习与形式化验证技术相结合的方法，研究基于动态策略的安全协议形式化自动验证技术，以突破并解决传统形式化自动验证中的状态空间爆炸问题，并实现对主流网络安全协议的自动化证明。SmartVerif可以挖掘给定目标的安全协议与软件的所有安全漏洞，确保网络安全协议不会被攻击者攻破。该成果已被信息安全领域国际顶级学术会议USENIX Security 2020接收。.(2) 提出一套保护系统状态连续性形式化建模与验证框架.我们针对保护系统状态连续性解决方案提出了一个形式化建模与验证框架，该框架使用精化策略将抽象动作具体化为某个具体状态连续性解决方案的防护行为。我们在Coq证明工具中实现了该框架，并证明了一个称为Memior的状态连续性解决方案保证了受保护模块的状态连续性。.(3) 提出一套屏蔽系统形式化建模与验证的通用框架.我们提出了一个屏蔽系统形式化建模与验证的通用框架，该框架支持分析基于不同技术的屏蔽系统，通过逐步精化减少了对新屏蔽系统的形式验证的复杂性。我们在Coq验证工具中实现了该框架，并在发现了在使用屏蔽系统时的潜在安全威胁。.在项目执行阶段，发表26篇论文，其中包括CCF A类论文6篇（期刊论文2篇，会议论文4篇），以及获得14项国内专利，完成预期研究计划。