Type-directed Program Transformation for Constant-Time Enforcement
summary
Claims a more permissive information‑flow type system that records indirect-of{p} dependencies and rejects only direct flows, then uses those types to drive a source-to-source transformation that produces semantically equivalent constant‑time code. Implements an upgraded delayed if-conversion plus scope‑increase and dynamic bounds checks, targets a language with arrays and for‑loops, and is added as an early pass to the Jasmin compiler. Prototype broadens the class Fact accepted but has no formal proof yet and currently omits returns; scope moves can still introduce tricky indirect flows.
AI-written summary · about
chapters (4)
related talks
28mType-directed Program Transformation for Constant-Time Enforcement
18mPreservation of speculative constant-time by compilation
18mPreservation of Speculative Constant-time by Compilation
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
21mWhen Obfuscations Preserve Cryptographic Constant-Time
19mScalable Language Agnostic Taint Tracking using Explicit Data Dependencies
32mSubstructural Information Flow via Polymorphism