一句话：提出面向对象语言中捕获多项式时间函数的通用非干涉策略，并用形状分析给出可判定保守实例。
本文研究如何在面向对象语言中刻画多项式时间可计算函数，并扩展基于安全递归的既有可处理刻画。作者提出一种通用非干涉策略，将控制流层面的标准非干涉技术与为保证每一安全层级保持多项式时间可靠性所需的分层性质清晰分离，从而使策略能捕获更广的程序类。作者证明该刻画是安全递归类刻画的一个真扩展。尽管该策略本身是 Π⁰₁-完全的，作者进一步利用形状分析技术将其实例化为一个可判定且保守的判定实例。
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 Π 1 0 -complete, we show that it can be instantiated to some decidable and conservative instance using shape analysis techniques.
@article{paperbot2061,
title = {A General Noninterference Policy for Polynomial Time},
author = {Emmanuel Hainry and Romain Péchoux},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571221}
}