Binsec/Rel：用于安全的符号二进制分析器及其在恒定时间和秘密擦除中的应用
Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure
摘要：
本文处理的问题，设计有效的二进制级验证的一个子集的信息流属性，包括恒定时间和秘密擦除。这些属性对于加密实现是至关重要的，但编译器通常不保留这些属性。我们的建议建立在关系符号执行的基础上，通过专门用于信息流和二进制级别分析的新优化来增强，从而比以前基于符号执行的工作有了显着的改进。我们实现了一个原型，Binsec/Rel，用于恒定时间和秘密擦除的错误查找和有界验证，并在一组338个加密实现上进行了广泛的实验，证明了我们的方法的好处。使用Binsec/Rel，我们还自动化两个先前的手动研究保存常数时间和秘密擦除编译器的4148和1156二进制文件。有趣的是，我们的分析突出了不正确的使用volatile数据指针的秘密擦除，并表明基于volatile函数指针的擦洗机制可以引入额外的寄存器溢出，这可能会破坏秘密擦除。我们还发现，gcc -O 0和clang的后端通道在以前被LLVM级别的最先进的恒定时间验证工具视为安全的实现中引入了恒定时间的违规行为，这表明了二进制级别推理的重要性。
英文摘要：
This paper tackles the problem of designing efficient binary-level verification for a subset of information flow properties encompassing constant-time and secret-erasure. These properties are crucial for cryptographic implementations, but are generally not preserved by compilers. Our proposal builds on relational symbolic execution enhanced with new optimizations dedicated to information flow and binary-level analysis, yielding a dramatic improvement over prior work based on symbolic execution. We implement a prototype, Binsec/Rel, for bug-finding and bounded-verification of constant-time and secret-erasure, and perform extensive experiments on a set of 338 cryptographic implementations, demonstrating the benefits of our approach. Using Binsec/Rel, we also automate two prior manual studies on preservation of constant-time and secret-erasure by compilers for a total of 4148 and 1156 binaries respectively. Interestingly, our analysis highlights incorrect usages of volatile data pointer for secret erasure and shows that scrubbing mechanisms based on volatile function pointers can introduce additional register spilling which might break secret-erasure. We also discovered that gcc -O0 and backend passes of clang introduce violations of constant-time in implementations that were previously deemed secure by a state-of-the-art constant-time verification tool operating at LLVM level, showing the importance of reasoning at binary-level.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
