Reconciling Progress-Intensive Noninterference and Declassification
summary
Proposes a concrete security condition that dials between progress-insensitive noninterference and progress-sensitive policies by tagging code regions with TV statements that mark where termination/trace length leaks are allowed and by bounding attacker and progress knowledge on those tags. Formalizes traces, attacker projection, and progress knowledge, implements dynamic enforcement in the language true (runtime PC raises on branches, lowers on declassification), and reports a case study and classroom use showing the mechanism is implementable and usable though enforced naively at runtime.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:39Progress Insensitive NI PIN
- 3:25Outline for the rest of the
- 3:40While-language with pini staten
- 5:20Trace semantics
- 10:13An observation about PIN
- 11:56PC declassification
- 14:50Room booking example nevis
- 15:26Insights from implementatid
- 19:58The actual definition
related talks
16mReconciling Optimization With Secure Compilation
19mDecompiling for Constant-Time Analysis
22mQuest Complete: The Holy Grail of Gradual Security
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
08mShort Talk: Generalising secure compilation criteria
18mCompiling countermeasures against fault attacks with “Tracing LLVM”
26mType-directed Program Transformation for Constant-Time Enforcement
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations