处理器微处理架构安全攻击技术建模

处理器的推测执行、乱序执行等性能优化机制可能留下可被侧信道利用的状态，引发微架构信息泄露。此类漏洞的检测与分析往往依赖人工构造测试程序，且复现结果易受处理器型号和运行配置影响，难以开展系统化比较。针对这些问题，本项目以推测合约为统一的安全规范，设计并实现自动化微架构漏洞检测系统，通过比较合约模型与真实硬件的可观测行为识别超出模型预期的泄露，并结合复现与最小化分析定位触发机制。最终，本项目在多款真实商业处理器平台上开展验证，形成可复现的漏洞样例与测试基础，为微架构漏洞机理分析和防御措施评估提供理论和技术支撑。

基于推测合约的自动化微架构漏洞检测方法

推测合约从攻击者视角定义可观察的信息边界，由观察子句与执行子句组成。前者规定模型记录哪些信息，如访存地址、控制流或数据值；后者描述允许考虑的执行行为，如条件分支误预测、存储旁路和异常延迟处理。研究人员可以组合两类子句，为不同泄露机制建立可执行的参考模型，而不必考虑处理器全部的内部实现细节。

图1 基于推测合约的自动化检测系统架构

系统由模糊测试器统一调度，支持随机生成和模板引导两种测试方式。随机模式探索不同指令和输入的组合，模板模式则围绕条件分支、除法异常或存储依赖等机制构造测试框架。同一程序和输入分别交给合约模型与真实处理器执行，得到合约痕迹ctrace和硬件痕迹htrace。测试输入包括寄存器初始值和内存数据，因此分析不仅针对程序执行路径，也能够追踪输入差异如何影响泄露。

硬件执行端通过Linux内核模块构建沙箱，在受控条件下运行测试程序，并利用Prime+Probe等微架构侧信道采集状态变化。合约模型端按选定语义模拟执行，记录模型允许暴露的信息。两条执行路径提供了不同层次的观察结果：一条来自安全规范，另一条来自实际硬件。测量窗口覆盖测试代码执行前后的缓存准备与探测，使错误推测或异常回滚后仍然保留的访问痕迹能够被记录。如果同一程序的两个输入产生相同的合约痕迹，却在硬件上留下可稳定区分的缓存痕迹，系统便报告合约违规。这意味着硬件暴露了当前模型未区分的信息，后续仍需分析其来源和安全含义。

图2 由合约等价输入的硬件痕迹差异识别合约违规

对于初步筛出的可疑结果，系统增加重复测量，并统一初始微架构状态，以降低噪声造成的误报。确认能够复现后，再删除无关指令、简化程序和输入差异，保留仍能触发违规的短序列。最小化将复杂的随机程序转化为便于人工分析的样例，帮助定位触发指令、输入来源与缓存编码路径。研究人员据此判断差异来自已知推测行为、模型尚未覆盖的机制，还是需要进一步排查的测量因素，并决定是否补充合约。

八款处理器上的实验验证

实验覆盖Intel第9至14代的六款处理器，以及采用Zen 4、Zen 5架构的两款AMD处理器，共八款型号。由于两款 Intel 处理器通过同一主机更换CPU开展测试，实际使用七台实验主机。测试设置涵盖十四类模式，包括Spectre、Meltdown、MDS、瞬态存储地址和除法相关行为；这些模式在不同平台上的检测结果不尽相同。

图3 AMD Ryzen 7 9800X3D 实验平台

成果总结

项目围绕处理器微架构安全攻击技术建模问题，完成了从形式化建模、自动化检测到真实硬件验证的完整研究工作。项目以推测合约为核心，将微架构泄露行为抽象为观察子句与执行子句的组合，并在此基础上构建了能够生成测试用例、采集硬件痕迹、模拟合约痕迹并进行违规检测的自动化工具链。实验结果表明，该方法能够有效发现多类典型微架构漏洞中的合约违规现象，并通过最小化分析定位核心触发指令和泄露路径。总体来看，实现了对处理器微架构安全漏洞的系统化描述和自动化表征，形成了可复现的漏洞样例与测试基础，为后续开展未知漏洞发现、漏洞机理分析和防御措施评估提供了较好的工具支撑和研究基础。