Detecting Speculative Data Flow Vulnerabilities Using Weakest Precondition Reasoning

doi:10.1007/978-3-031-98208-8_19

2026-01-01

PRE

Graeme Smith *

DOI：10.1007/978-3-031-98208-8_19

原文链接

原文求助

摘要

En 中文

推测执行是一种硬件优化技术，其中处理器在等待某条指令所需计算完成的同时，基于待定计算的预测值继续执行后续指令。2018年，随着Spectre和Meltdown两种相关攻击的披露，推测执行成为安全研究的焦点。此后，已识别出许多类似的攻击。尽管已有大量研究使用形式化方法基于预测控制流来检测推测执行漏洞，但针对基于预测数据流的漏洞的研究则显著较少。在本文中，我们介绍了一种基于最弱前置条件推理来检测数据流漏洞的方法，即Spectre-STL和Spectre-PSF。我们通过一套用于验证文献中相关方法的litmus测试集来验证我们的方法。

Keyword:

Speculative Execution

Data Flow Vulnerabilities

Weakest Precondition Reasoning

Spectre Attacks

Formal Methods