Binsec/Rel：面向安全的符号二进制分析器及其在恒定时间与秘密擦除中的应用
密码学与安全
2022-09-05 v1
摘要
本文致力于为涵盖恒定时间与秘密擦除的信息流属性子集设计高效的二进制级验证。这些属性对密码学实现至关重要，但通常不被编译器保持。我们的方案构建于关系符号执行之上，并增强了专用于信息流与二进制级分析的新优化，相较基于符号执行的已有工作取得显著改进。我们实现了原型 Binsec/Rel，用于恒定时间与秘密擦除的缺陷查找与有界验证，并在一组 338 个密码学实现上进行了大量实验，展示了我们方法的优势。利用 Binsec/Rel，我们还自动化了两项先前关于编译器对恒定时间与秘密擦除保持性的手动研究，分别对应 4148 与 1156 个二进制文件。有趣的是，我们的分析凸显了针对秘密擦除的 volatile 数据指针的错误用法，并表明基于 volatile 函数指针的擦除机制可能引入额外的寄存器溢出，从而破坏秘密擦除。我们还发现，gcc -O0 与 clang 后端通路在先前被最先进 LLVM 级恒定时间验证工具判定为安全的实现中引入了恒定时间违例，显示了在二进制级进行推理的重要性。
引用
@article{arxiv.2209.01129,
title = {Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure},
author = {Lesly-Ann Daniel and Sébastien Bardin and Tamara Rezk},
journal= {arXiv preprint arXiv:2209.01129},
year = {2022}
}
备注
Technical report, corresponding paper accepted to Transactions on Privacy and Security 2022 (TOPS), 54 pages. arXiv admin note: substantial text overlap with arXiv:1912.08788