一句话:提出一种保持 FP 可靠性的脱密策略,放宽非干扰类型系统以接受更多多项式时间程序,并刻画 BFF。
自动复杂度分析中,基于非干扰的类型系统可通过可靠性保证良类型程序属于给定复杂度类(如 FP),但这类系统并非内涵完备,会拒绝一些多项式时间算法。为缓解表达力限制,本文借鉴安全领域的脱密机制,提出一种新的直观脱密策略,以安全可控的方式放宽非干扰条件。该策略保持 FP 可靠性,且严格捕获比现有非干扰系统更多的程序。作者还展示了方法的通用性:在带一阶过程调用的二阶命令式语言中,它给出二阶多项式时间可计算函数类 BFF 的新刻画。类型推断可在多项式时间内完成。
In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in polynomial time. These characterizations are also extensionally complete - they capture all functions - but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization. To circumvent this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving FP-soundness and capturing strictly more programs than existing noninterference-based systems. We show the versatility of the approach: it also provides a new characterization of the class BFF of second-order polynomial time computable functions in a second-order imperative language, with first-order procedure calls. Type inference is tractable: it can be done in polynomial time.