Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art countermeasures. To defend against Spectre, developers of verification tools and compiler-based mitigations are forced to reason about microarchitectural details such as speculative execution. In order to aid developers with these attacks in a principled way, the research community has sought formal foundations for speculative execution upon which to rebuild provable security guarantees. This paper systematizes the community's current knowledge about software verification and mitigation for Spectre. We study state-of-the-art software defenses, both with and without associated formal models, and use a cohesive framework to compare the security properties each defense provides. We explore a wide variety of tradeoffs in the complexity of formal frameworks, the performance of defense tools, and the resulting security guarantees. As a result of our analysis, we suggest practical choices for developers of analysis and mitigation tools, and we identify several open problems in this area to guide future work on grounded software defenses.


翻译:光谱脆弱性违反了我们对建筑抽象学的基本假设,使攻击者可以窃取敏感数据,尽管此前是最先进的反措施。为了防御光谱,核查工具的开发者和基于编译者的缓解措施被迫解释微观建筑细节,例如投机性执行。为了以原则方式帮助开发者应对这些攻击,研究界为投机性执行寻求正式基础,以此重建可证实的安全保障。本文将社区目前关于软件核查和减轻监视器影响的知识系统化。我们研究的是最新的软件防御,无论是否相关的正式模型,并使用一个统一框架来比较每一项防御所提供的安全特性。我们探索了形式框架的复杂性、国防工具的性能以及由此产生的安全保障。我们的分析的结果是,我们为分析和缓解工具的开发者提出了切实可行的选择,我们找出了这方面的一些公开问题,以指导今后关于基础软件防御的工作。

0
下载
关闭预览

相关内容

这个新版本的工具会议系列恢复了从1989年到2012年的50个会议的传统。工具最初是“面向对象语言和系统的技术”,后来发展到包括软件技术的所有创新方面。今天许多最重要的软件概念都是在这里首次引入的。2019年TOOLS 50+1在俄罗斯喀山附近举行,以同样的创新精神、对所有与软件相关的事物的热情、科学稳健性和行业适用性的结合以及欢迎该领域所有趋势和社区的开放态度,延续了该系列。 官网链接:http://tools2019.innopolis.ru/
专知会员服务
33+阅读 · 2020年12月28日
【2020新书】Web应用安全,331页pdf
专知会员服务
23+阅读 · 2020年10月24日
专知会员服务
52+阅读 · 2020年9月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
人工智能 | ISAIR 2019诚邀稿件(推荐SCI期刊)
Call4Papers
6+阅读 · 2019年4月1日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
IEEE | DSC 2019诚邀稿件 (EI检索)
Call4Papers
10+阅读 · 2019年2月25日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Arxiv
38+阅读 · 2020年3月10日
Deflecting Adversarial Attacks
Arxiv
8+阅读 · 2020年2月18日
VIP会员
相关VIP内容
专知会员服务
33+阅读 · 2020年12月28日
【2020新书】Web应用安全,331页pdf
专知会员服务
23+阅读 · 2020年10月24日
专知会员服务
52+阅读 · 2020年9月7日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
151+阅读 · 2019年10月12日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
相关资讯
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
CCF推荐 | 国际会议信息8条
Call4Papers
9+阅读 · 2019年5月23日
CCF C类 | DSAA 2019 诚邀稿件
Call4Papers
6+阅读 · 2019年5月13日
计算机 | CCF推荐期刊专刊信息5条
Call4Papers
3+阅读 · 2019年4月10日
人工智能 | ISAIR 2019诚邀稿件(推荐SCI期刊)
Call4Papers
6+阅读 · 2019年4月1日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
IEEE | DSC 2019诚邀稿件 (EI检索)
Call4Papers
10+阅读 · 2019年2月25日
大数据 | 顶级SCI期刊专刊/国际会议信息7条
Call4Papers
10+阅读 · 2018年12月29日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
Top
微信扫码咨询专知VIP会员