Internalizing Indistinguishability with Dependent Types
summary
DCOI (Dependent Calculus of Indistinguishability) internalizes indistinguishability as definitional equality and adds an observer-indexed identity type so equality depends on observer levels; it supports conversion and propositional equality at arbitrary levels. The paper proves type soundness and noninterference and mechanizes those proofs (mechanized in Coq), and ships a prototype type checker (artifact available) that implements the level-aware conversion rules and checks when high-level parts can be ignored.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:08Dependent types with dependency tracking
- 2:10Dependency tracking in types
- 4:14Dependency tracking analogy
- 5:40Box types and information flow
- 7:25Indistinguishability in security
- 8:07Equational reasoning in dependent types
- 9:10Identity type with observer levels
- 9:52Decoy language overview
- 10:35Dependency tracking benefits
- 12:02Flexible relevance with observer levels
- 13:29Map function example
- 14:10Compile-time irrelevance semantics
- 14:54Summary of decoy’s contributions
- 15:17Comparison with modal dependent types
- 17:01Question and answer session
related talks
17mA Deductive System for Contract Satisfaction Proofs
34mThe Concrete Security of Two-Party Computation: Simple Definitions, and Tight Proofs for PSI and...
22mQuest Complete: The Holy Grail of Gradual Security
19mCompositional Security Definitions for Higher-Order Where Declassification
40mEnvironmental Dependencies as Coeffects
23mSecurity Reasoning via Substructural Dependency Tracking
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
19mMechanized Logical Relations for Termination-Insensitive Noninterference