Since the advent of Spectre attacks, researchers and practitioners have developed a range of hardware and software measures to counter transient execution attacks. A prime example of such mitigation is speculative load hardening in LLVM, which protects against leaks by tracking the speculation state and masking values during misspeculation. LLVM relies on static analysis to harden programs using slh that often results in over-protection, which incurs performance overhead. We extended an existing side-channel model validation framework, Scam-V, to check the vulnerability of programs to Spectre-PHT attacks and optimize the protection of programs using the slh approach. We illustrate the efficacy of Scam-V by first demonstrating that it can automatically identify Spectre vulnerabilities in real programs, e.g., fragments of crypto-libraries. We then develop an optimization mechanism that validates the necessity of slh hardening w.r.t. the target platform. Our experiments showed that hardening introduced by LLVM in most cases could be significantly improved when the underlying microarchitecture properties are considered.

翻译：自幽灵攻击出现以来，研究者和实践者已开发出一系列硬件与软件措施来应对瞬态执行攻击。此类缓解措施的典型代表是LLVM中的推测加载强化技术，它通过追踪推测状态并在错误推测期间对值进行掩码来防止信息泄露。LLVM依赖静态分析使用slh强化程序，往往导致过度防护并引发性能开销。我们扩展了现有侧信道模型验证框架Scam-V，用于检测程序对Spectre-PHT攻击的脆弱性，并基于slh方法优化程序防护。通过首先展示其能自动识别真实程序（如密码库片段）中的幽灵漏洞，我们验证了Scam-V的有效性。继而开发了一种优化机制，用以验证针对目标平台的slh强化必要性。实验表明，当考虑底层微架构特性时，LLVM引入的强化在多数情况下可得到显著优化。