| 引用本文： |
-
张士轩,王海霞,邱朋飞,吕勇强,尹凌峰,王鸿鹏,汪东升.基于模型检验的缓存侧信道形式化验证与攻击检测[J].信息安全学报,已采用 [点击复制]
- zhangshixuan,wanghaixia,qiupengfei,lvyongqiang,yinlingfeng,wanghongpeng,wangdongsheng.Formal Verification of Cache Side-channels and Attack Detection Based on Model Checking[J].Journal of Cyber Security,Accept [点击复制]
|
|
| 摘要: |
| 缓存侧信道攻击利用对共享缓存的访问延迟差异泄露私密数据,具有隐蔽性高,难以防御的特点，对计算机系统的安全性威胁越来越大。此外，瞬态执行类攻击的发现也证明了缓存也可以作为隐蔽信道传递瞬态窗口中的信息。因此,需要对处理器上的缓存设计进行全面的验证和安全性分析,以评估其是否容易受到潜在的侧信道攻击。现有的关于缓存的评估和验证工作只考虑了最基本的缓存模型,而忽视了缓存的非包含属性和缓存的一致性协议等细粒度特征。随着大量的利用缓存细粒度特征的侧信道攻击方式被发现，凸显了传统方法对于缓存侧信道的评估和验证的不足。本文提出一种基于模型检验技术的形式化验证框架,该框架可系统的验证缓存设计并自动检测其中的侧信道攻击。为描述缓存的行为模型,本文提出了一种基于有限状态机的缓存微架构建模方法。它详细的描述了对缓存相关操作指令和缓存特征进行抽象及约简的方法，使得模型的状态空间显著减小。本文还根据延迟差分比较的思想定义了免受侧信道攻击的缓存需要满足的全局安全属性,违反该安全规范的每条指令输入序列都是一个潜在的漏洞；此外,本文提出了一个基于模型检验的反例搜索算法,它能够穷尽地搜索缓存的状态机模型，并找到所有违反安全约束的反例。这使得验证框架具备批量验证并发现侧信道攻击的能力，并且让验证过程更加高效。本文使用所提出的验证框架对当前处理器中应用广泛的非包含缓存模型和考虑缓存一致性的多核缓存模型进行了验证,验证得到的反例能够覆盖现有的攻击方式,并发现9种新的攻击方式。新发现的攻击方式可以让攻击者绕过一些侧信道防御措施，也可以为受害者提供当前缓存设计中的脆弱点，以便进行针对性的防御。我们在真实处理器上进行了测试,结果证明了本文发现新攻击的有效性。 |
| 关键词: 硬件安全 形式化验证 缓存侧信道攻击 模型检验 |
| DOI： |
| 投稿时间：2023-12-11修订日期：2024-04-10 |
| 基金项目:国家自然科学基金项目（面上项目，重点项目，重大项目） |
|
| Formal Verification of Cache Side-channels and Attack Detection Based on Model Checking |
|
zhangshixuan1, wanghaixia2, qiupengfei3, lvyongqiang2, yinlingfeng2, wanghongpeng1, wangdongsheng2
|
| (1.Harbin Institute of Technology, Shenzhen;2.Tsinghua University;3.Beijing University of Posts and Telecommunications) |
| Abstract: |
| Cache side-channel attacks exploit differences in access delays to shared caches, revealing sensitive data with high stealth and resilience against defense mechanisms. Additionally, the discovery of transient execution attacks demonstrates that caches can serve as covert channels for transmitting information within transient windows. Therefore, comprehensive veri-fication and security analysis of cache designs on processors are necessary to assess their susceptibility to potential side-channel attacks. Existing evaluations and verification efforts concerning caches predominantly focus on basic cache models, neglecting finer-grained features such as non-inclusive properties and cache coherence protocols. As numerous side-channel attack techniques exploiting cache's finer-grained features have been unveiled, it underscores the inadequacy of traditional methods for evaluating and verifying cache side-channels. This paper introduces a formal verification frame-work based on model-checking techniques, systematically validating cache designs and automatically detecting potential side-channel attacks. To describe the behavioral model of the cache, we propose a finite-state machine-based modeling ap-proach for cache microarchitecture. This approach intricately outlines methods for abstracting and simplifying cache-related operation instructions and features, significantly reducing the model's state space. Moreover, following the idea of delay difference comparison, this paper defines the global safety properties that caches must satisfy to be immune to side-channel attacks. Violations of these safety specifications by any instruction input sequence indicate a potential vulnerability. Additionally, we present a model-checking-based counterexample search algorithm that exhaustively explores the cache's state machine model, uncovering all instances that breach safety constraints. This empowers the verification framework with the capability to batch verify and discover side-channel attacks efficiently. The proposed verification framework is applied to widely-used non-inclusive cache models on current processors and multi-core cache models considering cache coherence. The obtained counterexamples cover existing attack methods and reveal nine new attack methods. The newly discovered attack methods can enable attackers to bypass some side-channel defense measures and provide victims with insights into vulnerabilities in the current cache design for targeted defense. Real processor testing validates the effective-ness of discovering new attacks presented in this paper. |
| Key words: hardware security formal verification cache side-channel attacks model checking |
