Completed
Definition: Bug-Finding & Bounded-Verif for Constant-Time
Class Central Classrooms beta
YouTube videos curated by Class Central.
Classroom Contents
Efficient Relational Symbolic Execution for Constant-Time at Binary-Level
Automatically move to the next video in the Classroom when playback concludes
- 1 Intro
- 2 Problem: Protecting Secrets against Timing Attacks
- 3 Solution: Constant-Time Programming (CT)
- 4 Constant-Time is Generally not Preserved by Compilers (1)
- 5 The Need for Automatic Analysis
- 6 Lots of Verification Tools for Constant-Time
- 7 Definition: Bug-Finding & Bounded-Verif for Constant-Time
- 8 Adapt SE for Constant-Time: Technical Key Insights
- 9 Contributions
- 10 Standard Approach eg (1.2 ): Symbolic Execution for Constant-Time via Self-Composition
- 11 Better Approach: Relational Symbolic Execution (1.2)
- 12 Dedicated Optimizations for Constant-Time Analysis
- 13 Binsec/Rel: Experimental Evaluation
- 14 Scalability: Comparison with RelSE (RQ2)
- 15 Effect of Compiler Optimizations on Constant-Time (RQ1/RQ3)
- 16 Conclusion
