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 |