Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Depe
summary
A semi-automatic Eclipse-based refactoring tool rewrites a subset of C into semi-interleaved ladder code, using a backend written in Idris so dependent types encode and machine-checks the three ladder equations and generates the missing f. Search for rewrites uses a tabu search (breadth-first with depth and seen-list) to avoid loops. Applied to modular exponentiation and multiplication it produces C that yields constant timing across Hamming weights, eliminating the side-channel timing leak.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:07Sidechannel Attacks
- 3:23Semiinterleaved Ladder
- 6:01Refactoring
- 6:34Eclipse
- 7:29Arithmetic Expressions
- 7:57Semantics
- 8:52Abstract Interpretation
- 17:19Function Extraction
- 17:56Automatic Ladderisation
- 20:52Modular exponentiation
- 22:48Summary
- 24:16Future work
- 25:28Thank you
- 25:53Should we be worried
- 27:23How hard is it
related talks
58mFast Cryptographic Code via Partial Evaluation
14mCollapsing Towers for Side-Channel Security
54mLost and Found in Translation
01h 00mAI Safety through Programming?
19mDo You Even Lift? Strengthening Compiler Security Guarantees Against Spectre Attacks
29mSyntia: Synthesizing the Semantics of Obfuscated Code
21mFormal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
45m"Advanced Malware Threat: handling obfuscated code using..."