Efficient Relational Symbolic Execution for Constant-Time at Binary-Level

Explore a 16-minute IEEE conference talk on Binsec/Rel, an efficient relational symbolic execution tool for verifying constant-time programming at the binary level. Learn about the challenges of writing constant-time code to prevent timing side-channel attacks and the importance of binary-level analysis. Discover how Binsec/Rel improves upon previous symbolic execution techniques with optimizations for information flow and binary-level analysis. Examine the tool's effectiveness in bug-finding and bounded-verification through extensive experiments on cryptographic implementations. Gain insights into the impact of compiler optimizations on constant-time preservation and understand why binary-level reasoning is crucial for ensuring security in cryptographic code.

Intro
Problem: Protecting Secrets against Timing Attacks
Solution: Constant-Time Programming (CT)
Constant-Time is Generally not Preserved by Compilers (1)
The Need for Automatic Analysis
Lots of Verification Tools for Constant-Time
Definition: Bug-Finding & Bounded-Verif for Constant-Time
Adapt SE for Constant-Time: Technical Key Insights
Contributions
Standard Approach eg (1.2 ): Symbolic Execution for Constant-Time via Self-Composition
Better Approach: Relational Symbolic Execution (1.2)
Dedicated Optimizations for Constant-Time Analysis
Binsec/Rel: Experimental Evaluation
Scalability: Comparison with RelSE (RQ2)
Effect of Compiler Optimizations on Constant-Time (RQ1/RQ3)
Conclusion