Sequential Information Flow
summary
Introduces Hypertrace Logic, a first-order array-style logic with explicit trace vs time quantifiers and shows that HyperLTL (trace-prefix fragment) cannot express most natural sequential information-flow variants — notably any version with asynchronous transitions or point-based independence. Proofs build indistinguishable families of trace sets (Pn versus Qn) and use equivalences between trace-sets to give inexpressiveness results; one synchronous, segment-based hidden-phase variant is expressible, many others are provably not.
AI-written summary · about
chapters (10)
- 0:00Start
- 1:26Information Flow
- 9:35Combinational Properties
- 10:12Combinational Hyperproperties
- 12:25Sequential Properties
- 13:58Sequential Hyperproperties
- 19:45Combinational Independence
- 21:43Point-based Sequential independence
- 23:12Trace-based Sequential Independence General Noninterference
- 43:58Conclusion
related talks
21mHyper Separation Logic
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
15mStructural Information Flow: A Fresh Look at Types for Non-Interference
19mMechanized Logical Relations for Termination-Insensitive Noninterference
47mInformation Flow Types, Runtime Monitors, and Gradual Typing
26mType-directed Program Transformation for Constant-Time Enforcement
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations
32mSubstructural Information Flow via Polymorphism