基于超属性语义分析的 SemPat：生成微架构攻击模式

软件的微架构安全验证出现了两种主要方法。第一种基于语义安全属性（例如非干涉），对给定程序和指定的硬件微架构抽象模型进行验证。第二种基于攻击模式，如果在程序执行中发现该模式，即表示存在漏洞利用。虽然前者使用形式规范能够捕获针对同一漏洞的多个 gadget 变体，但受限于验证的可扩展性。而模式虽然更可扩展，但必须手动构建，因为其作用范围较窄，对 gadget 特定结构敏感。本工作开发了一种技术，给定基于非干涉的语义安全超属性，自动生成复杂度参数（称为骨架大小）的攻击模式。因此，我们结合了两种方法的优势：安全可由捕获多个 gadget 变体的超属性进行指定，而自动生成的模式可用于可扩展验证。我们实现了该技术并演示了能够生成新模式（例如针对 SpectreV1、SpectreV4）以及使用生成的模式相对于基于超属性的验证实现的更好可扩展性。