论文标题
BINSEC/REL：用于安全性的符号二进制分析仪，并应用于恒定时间和秘密搜索
Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-Erasure
论文作者
论文摘要
本文解决了设计有效的二元级验证的问题，以涉及恒定时间和秘密搜索的信息流属性的一部分。这些属性对于加密实现至关重要，但通常不保留编译器。我们的建议建立在关系符号执行的基础上，通过专门针对信息流和二进制级别分析的新优化增强了，从而基于符号执行对先前的工作产生了巨大的改进。我们实施了一个原型Binsec/rel，用于对恒定时间和秘密搜索的错误进行错误验证，并对一组338个加密实现进行广泛的实验，证明了我们方法的好处。使用BINSEC/REL，我们还对编译器保存恒定时间和秘密射击的两项先前的手动研究分别为4148和1156二进制文件。有趣的是，我们的分析强调了用于秘密擦除的挥发性数据指针的错误用法，并表明基于挥发性功能指针的擦洗机制可能会引入其他寄存器溢出，这可能会破坏秘密搜索。我们还发现，GCC -O0和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.
