When Obfuscations Preserve Cryptographic Constant-Time
summary
Proposes a sufficient condition and a per-program translation validation that statically checks whether an obfuscation preserves cryptographic constant-time (modeled as termination‑insensitive noninterference over memory ops and guard evaluations). Implements checks on examples: mixed boolean‑arithmetic rewrites (MBA) never introduce new memory operations so they pass, while Tigress control‑flow/data‑flow obfuscations can introduce new mops and fail the check; the approach accepts some Tigress-transformed programs case‑by‑case. Proof of soundness is unfinished and work remains to integrate with Tigress/LLVM.
AI-written summary · about
chapters (12)
- 0:00Obfuscation preserving constant-time
- 1:47Program transformations security
- 3:14Why obfuscate crypto code
- 5:05Constant-time definition
- 6:50Preserving constant-time
- 8:18Top-level expressions mapping
- 11:06Static check for constant-time
- 12:54MBA obfuscation example
- 13:17Tigress limitations
- 14:19Translation validation
- 15:26Safe obfuscation guidelines
- 16:30Q&A
related talks
32mVerifying Constant-Time Implementations
33mObfuscation with Constant Multiplicative Size Overhead
26mAn Effective Approach to Software Obfuscation
23mRobust Constant-Time Cryptography
28mType-directed Program Transformation for Constant-Time Enforcement
16mReconciling Optimization With Secure Compilation
52mIndistinguishability Obfuscation via Mathematical Proofs of Equivalence
18mPreservation of Speculative Constant-time by Compilation