缓存侧信道自由性的符号验证
软件工程
2018-07-23 v1 密码学与安全
摘要
缓存时序攻击允许第三方观察者从程序执行中检索敏感信息。但是，是否可能自动检查程序针对缓存时序攻击的脆弱性，并随后在程序执行中自动屏蔽这些攻击？对于给定的程序、缓存配置和攻击模型，我们的 CACHEFIX 框架要么验证程序的缓存侧信道自由性，要么合成一系列补丁以确保程序执行期间的缓存侧信道自由性。我们框架的核心是一种基于缓存语义自动抽象精化的新颖符号验证技术。该框架的优势在于能够对反例轨迹进行符号推理，并将其与运行时监控相结合，从而在程序执行中消除缓存侧信道。我们使用来自 OpenSSL、libfixedtimefixedpoint、GDK 和 FourQlib 库的例程进行评估，结果显示我们的 CACHEFIX 方法在平均 75 秒内（不）证明缓存侧信道自由性。此外，除一例之外，CACHEFIX 在 20 分钟内合成所有补丁，以确保各例程在执行期间的缓存侧信道自由性。
引用
@article{arxiv.1807.04701,
title = {Symbolic Verification of Cache Side-channel Freedom},
author = {Sudipta Chattopadhyay and Abhik Roychoudhury},
journal= {arXiv preprint arXiv:1807.04701},
year = {2018}
}