| 摘要: |
| 长期以来,处理器为追求高性能目标在微架构设计中引入了众多优化机制。预测执行技术是一类应用较为广泛的处理器硬件优化机制,主要包括分支预测技术和值预测技术两种,其在微架构中由配套设计的分支预测单元、存储缓冲区等硬件组件实现。近年来,以Spectre、微架构数据采样(MDS)等漏洞为代表的处理器硬件相关安全问题频频出现,表明现代处理器的微架构预测机制存在重大安全隐患。然而处理器微架构设计复杂,传统的测试验证方法效率低下,难以覆盖所有漏洞,基于形式化方法的安全验证方法成为新的研究热点。本文通过分析分支预测类漏洞和微架构数据采样类漏洞的攻击原理,归纳了两类漏洞违反的安全属性,提出了一种对微架构单元建模验证的方法,该方法具有架构适应范围广、硬件单元适用种类多、验证效率高的优点。本文使用模型检测工具NuSMV对上述两类漏洞做了实验验证,实验结果表明,本文提出的预测类漏洞的验证方法能够有效验证现有的分支预测类漏洞和微架构数据采样类漏洞在特定微架构硬件单元上的存在情况。分支预测类漏洞验证实验发现的攻击序列能够覆盖现有的所有分支预测攻击类型,并在分支预测器模型上发现了一种新的利用分支历史缓冲区泄露分支历史信息的攻击方式。微架构数据采样类漏洞验证实验发现的攻击序列能够覆盖所有存在于存储缓冲区、行填充缓冲区的数据采样攻击类型,以及一类可以绕过微架构数据采样类漏洞防御措施的攻击类型。 |
| 关键词: 微架构安全 Spectre漏洞 MDS漏洞 模型检测 |
| DOI：10.19363/J.cnki.cn10-1380/tn.2025.07.08 |
| Received:August 24, 2023Revised:January 08, 2024 |
| 基金项目:本课题得到国家自然科学基金(No. 62372258)、国家自然科学基金区域创新发展联合基金重点项目(No. U24A20289)和北京市自然科学基金面上项目(No. 4242026)的资助。 |
|
| Research on Verification Method of Processor Prediction Vulnerabilities Based on Model Checking |
| YE Qingyu,KE Qian,WANG Haixia,QIU Pengfei,LIU Chang,WANG Dongsheng |
| Zhongguancun Laboratory, Beijing 100094, China;Key Laboratory of Trustworthy Distributed Computing and Service, Ministry of Education, Beijing University of Posts and Telecommunications, Beijing 100867, China;Beijing National Research Center for Information Science and Technology, Tsinghua University, Beijing 100084, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;Zhongguancun Laboratory, Beijing 100094, China;Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China |
| Abstract: |
| For a long time, processors have introduced many optimization mechanisms in microarchitecture design to achieve high performance goals. Predictive execution technology is a widely used hardware optimization mechanism in processors, mainly including branch prediction technology and value prediction technology, which are implemented in microarchitecture through hardware components such as branch prediction unit and store buffer. In recent years, hardware-related security issues of processors, represented by Spectre and microarchitecture data sampling (MDS) vulnerabilities, have frequently occurred, indicating significant security risks in the microarchitecture prediction mechanisms of modern processors. However, processor microarchitecture design is complex, and traditional testing and verification methods are inefficient and difficult to cover all vulnerabilities, leading to the emergence of new research hotspots based on formal methods for security verification. This article analyzes the attack principles of branch prediction and microarchitecture data sampling vulnerabilities, summarizes the security properties violated by the two types of vulnerabilities, and proposes a method for modeling and verifying microarchitecture units. This method has the advantages of a wide range of architectural adaptation, applicable to various hardware units, and high verification efficiency. The article uses the model checking tool NuSMV to experimentally verify the two types of vulnerabilities, and the results show that the proposed verification method for predictive vulnerabilities can effectively verify the existence of existing branch prediction and microarchitecture data sampling vulnerabilities on specific microarchitecture hardware units. The branch prediction vulnerability verification experiment found attack sequences that can cover all existing branch prediction attack types and discovered a new attack method that exploits the leakage of branch history information in the branch history buffer model. The microarchitecture data sampling vulnerability verification experiment found attack sequences that can cover all data sampling attack types existing in store buffer and line fill buffer, as well as a type of attack that can bypass microarchitecture data sampling vulnerability defense measures. |
| Key words: microarchitectural security Spectre vulnerabilities MDS vulnerabilities model checking |
