A General Noninterference Policy for Polynomial Time
summary
New noninterference policy claims an exact characterization: programs that are stratified and strongly normalizing compute exactly FP, strictly extending safe-recursion style systems. It separates control-flow noninterference from layering that preserves polynomial bounds, proves the decision problem is Π^0_1-complete, and gives a conservative, decidable instantiation via shape-analysis instantiation (TVLA-style) with exponential worst-case checking that types examples like list reversal. It ships as a prototype complexity parser.
AI-written summary · about
chapters (16)
- 0:00Intro
- 0:19Program complexity analysis
- 1:35The ICC approach
- 3:11What about Noninterference (NI)?
- 6:45Illustrating toy examples
- 8:04Adaptation to 00: not like taking candy off a baby (1/2)
- 10:30A simple counterexample
- 11:53Stratification
- 13:29Illustrating example
- 14:32Characterization of Polytime
- 15:06In the arithmetical hierarchy
- 16:20A decidable instance based on shape-analysis
- 17:31A new type system: SA
- 18:58Conclusion
- 19:35A fruitful technique
- 20:46Type system for safety