你甚至需要提升吗？加强编译器针对Spectre攻击的安全保证
编程语言
2025-03-06 v2
摘要
主流编译器实现了不同的对策来防止特定类别的推测执行攻击。不幸的是，这些对策要么缺乏形式化保证，要么其证明局限于仅捕捉现代CPU支持的推测机制子集的推测语义，从而限制了它们的实际适用性。理想情况下，这些安全证明应针对捕捉现代CPU实现的所有推测机制效果的推测语义。然而，这并不实际，并且需要新的安全编译证明来支持额外的推测机制。在本文中，我们通过提出一种新颖的安全编译框架来解决这个问题，该框架允许将Spectre对策提供的安全保证从较弱的推测语义（忽略某些推测机制）提升到较强的推测语义（考虑被忽略的机制），而无需新的安全编译证明。使用我们的提升框架，我们进行了迄今为止最全面的主流编译器中Spectre对策的安全分析。我们的分析涵盖了针对5类Spectre攻击的9种不同对策，我们证明了这些对策在考虑五种不同推测机制的推测语义下是安全的。
引用
@article{arxiv.2405.10089,
title = {Do You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks},
author = {Xaver Fabian and Marco Patrignani and Marco Guarnieri and Michael Backes},
journal= {arXiv preprint arXiv:2405.10089},
year = {2025}
}