Binsec/Rel：面向二进制级恒定时间的有效关系符号执行
密码学与安全
2020-07-14 v2
摘要
恒定时间编程准则（CT）是针对时序侧信道攻击的一种有效对策，它要求控制流和内存访问独立于秘密。然而，编写 CT 代码具有挑战性，因为它需要对成对执行轨迹（2-超安全属性）进行推理，且通常不能被编译器保持，因此需要进行二进制级分析。遗憾的是，当前用于 CT 的验证工具要么在更高层级（C 或 LLVM）推理，要么牺牲缺陷查找或有界验证，要么无法扩展。我们致力于设计一个高效的二进制级 CT 验证工具，同时提供缺陷查找和有界验证。该技术构建于关系符号执行之上，并增强了专用于信息流和二进制级分析的新优化，相较先前基于符号执行的工作取得了显著改进。我们实现了原型系统 Binsec/Rel，并在一组 338 个密码学实现上进行了大量实验，证明了我们的方法在缺陷查找和有界验证两方面的优势。利用 Binsec/Rel，我们还自动化了先前一项关于编译器 CT 保持性的手动研究。有趣的是，我们发现 gcc -O0 和 clang 后端通路在先前被最先进的 LLVM 级 CT 验证工具认定为安全的实现中引入了 CT 违例，显示了在二进制级进行推理的重要性。
引用
@article{arxiv.1912.08788,
title = {Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level},
author = {Lesly-Ann Daniel and Sébastien Bardin and Tamara Rezk},
journal= {arXiv preprint arXiv:1912.08788},
year = {2020}
}
备注
18 pages, 7 figures, accepted at IEEE Symposium on Security and Privacy 2020