Thu 19 Jan 2023 14:20 - 14:45 at Avenue34 - Resource Analysis Chair(s): Robert Harper

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

13:30 - 14:45
Resource AnalysisPOPL at Avenue34
Chair(s): Robert Harper Carnegie Mellon University
13:30
25m
Talk
Probabilistic Resource-Aware Session Types
POPL
Ankush Das Amazon, Di Wang Peking University, Jan Hoffmann Carnegie Mellon University
DOI
13:55
25m
Talk
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
25m
Talk
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