Towards Temporal Adversarial Logic
summary
Preliminary system embeds temporal reasoning into an under‑approximate adversarial program logic and defines a time footprint Δ per command plus left/right error tags, so reads/writes append input/output events annotated with execution time and synchronize attacker and target timelines. Claims: this exposes timing leaks (example reduces a 64‑bit brute force to 64‑bit→2×32‑bit by distinguishing slow log paths counted as 100 cycles), supports summaries for expensive operations, and is work‑in‑progress requiring instruction‑level semantics and an adversary synthesis backend.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:29Motivation for temporal adversarial logic
- 3:14Challenges with temporal logics
- 4:15Adversarial logic overview
- 5:17Arbiter logic model shift
- 7:05Case study: adversarial assertion
- 8:09Timing in adversarial triples
- 9:13Reads and writes in logic
- 10:59Timing behavior summary
- 11:40Synchronizing execution timelines
- 13:28Verification complexity and analysis
- 14:10Timing interactions algebra
- 15:15Future work and goals
- 16:43Time abstraction in logic
- 17:45Constant time and resource analysis
- 18:51Delta time footprint function
- 20:39Delta inference and parametric rules
- 21:20Question on adversary program generation
related talks
35mShowTime: CPU Timing Attacks With the Human Eye
15mTimelock Drive: Isolated Time-Based Defense for Storage Systems
25mRISC-V Zkt: Portable Timing Attack Resistance (via Dynamic Taint Analys...
50mTime Trial: Racing Towards Practical Timing Attacks
14mProtecting cryptography code from timing vulnerabilities
22mBi-abductive adversarial program synthesis
05mBuilding Privilege Access on Temporal
19mDecompiling for Constant-Time Analysis