Compositional Security Definitions for Higher-Order Where Declassification
summary
Defines a compositional security notion for where declassification in higher-order languages by building an indistinguishability logical relation that stops enforcing equivalence once a relevant declassification step occurs. Presents a stepwise (bisimulation-like) relation on executions that checks four criteria for relevance (actually releases data, observer can see it, observer can distinguish it, and it occurs inside a declassify), gives a type system that enforces the relation, and proves compositionality and strength over prior flow-style definitions.
AI-written summary · about
chapters (14)
- 0:00Welcome
- 0:24Research overview and goals
- 1:07Non-interference and limitations
- 2:12Where declassification
- 3:14Higher-order programming challenges
- 4:19Compositional security definitions
- 5:43Security definitions problems
- 6:04Logical relations for security
- 7:28Logical relations extended
- 10:17Indistinguishability with declassification
- 12:23Relevant declassification steps
- 13:49Paper details and proof
- 14:55Summary and impact
- 15:16Opening the floor for questions and discussion
related talks
25mComposing Secure Compilers
27mUniversally Composable Security for Program Partitioning
08mShort Talk: Generalising secure compilation criteria
22mGiving Semantics to Program-Counter Labels via Secure Effects
25mUniversal Composability is Secure Compilation
23mSecurity Reasoning via Substructural Dependency Tracking
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
19mMechanized Logical Relations for Termination-Insensitive Noninterference