strategFTO: Untimed Control for Timed Opacity
summary
A prototype strategFTO prototype implements an algorithm that decides untimed control for timed opacity and shows the control problem is not harder than full timed opacity, with decidability proven. It uses IMITATOR and PolyOp to compute public/private execution-time sets via parameter synthesis, enumerates action subsets, and synthesizes controllers. The tool finds minimal and maximal controllers, applies to an ATM benchmark, and scales reasonably when searching minimum strategies, producing concrete disabling sets that achieve full timed opacity. finds minimal/maximal controllers
AI-written summary · about
chapters (9)
- 0:00Timed opacity research intro
- 1:44Timing attacks and execution time
- 3:55Formalizing timed opacity
- 8:10Coffee machine example
- 12:55Computing execution times
- 15:06Untimed control for opacity
- 20:50Tool demo and benchmarks
- 23:06Future perspectives
- 24:25Q&A
related talks
22mTowards Temporal Adversarial Logic
01h 04mProtective Optimization Technologies
35mShowTime: CPU Timing Attacks With the Human Eye
21mWhen Obfuscations Preserve Cryptographic Constant-Time
28mType-directed Program Transformation for Constant-Time Enforcement
40mOP-TEE: When Linux Loses Control
24mAutomated game-theoretic security analysis of blockchain protocols
17mEfficient Dependency Resolution in IFC-aware Decentralized Programming