We introduce a new noninterference policy to capture the class of functions computable in polynomial time on an object-oriented programming language. This policy makes a clear separation between the standard noninterference techniques for the control flow and the layering properties required to ensure that each ``security'' level preserves polynomial time soundness, and is thus very powerful as for the class of programs it can capture. This new characterization is a proper extension of existing tractable characterizations of polynomial time based on safe recursion. Despite the fact that this noninterference policy is $\Pi^0_1$-complete, we show that it can be instantiated to some decidable and conservative instance using shape analysis techniques.
Thu 19 JanDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 14:45  | |||
13:30 25mTalk  | Probabilistic Resource-Aware Session Types POPL  DOI | ||
13:55 25mTalk  | A Calculus for Amortized Expected Runtimes POPL Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja DTU, Lena Verscht RWTH Aachen University  DOI | ||
14:20 25mTalk  | A General Noninterference Policy for Polynomial Time POPL Emmanuel Hainry Université de Lorraine; CNRS; Inria; LORIA, Romain Péchoux Université de Lorraine; CNRS; Inria; LORIA  DOI | ||