paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Declassification Policy for Program Complexity Analysis

面向程序复杂度分析的脱密策略
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 2/10 · 该论文属于程序语言与形式化方法中的类型系统/复杂度分析,虽与静态分析相关,但未涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心交叉方向。引用 1 inbox
Emmanuel Hainry, Bruce Kapron, Jean-Yves Marion, Romain Péchoux
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话:提出一种保持 FP 可靠性的脱密策略,放宽非干扰类型系统以接受更多多项式时间程序,并刻画 BFF。

自动复杂度分析中,基于非干扰的类型系统可通过可靠性保证良类型程序属于给定复杂度类(如 FP),但这类系统并非内涵完备,会拒绝一些多项式时间算法。为缓解表达力限制,本文借鉴安全领域的脱密机制,提出一种新的直观脱密策略,以安全可控的方式放宽非干扰条件。该策略保持 FP 可靠性,且严格捕获比现有非干扰系统更多的程序。作者还展示了方法的通用性:在带一阶过程调用的二阶命令式语言中,它给出二阶多项式时间可计算函数类 BFF 的新刻画。类型推断可在多项式时间内完成。

问题
如何在不牺牲可靠性的前提下,缓解基于非干扰的复杂度类型系统内涵不完备、拒绝部分多项式时间算法的问题。
方法
借鉴信息流安全中的脱密机制,定义一种安全可控地释放关键数据的脱密策略,并设计相应的复杂度类型系统与推断算法。
评估
通过可靠性证明说明系统只接受属于目标复杂度类的程序,通过表达力比较证明严格多于现有非干扰系统,并证明类型推断可在多项式时间内完成;还给出 BFF 的新刻画。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@inproceedings{abs-2401-14957,
  title = {Declassification Policy for Program Complexity Analysis},
  author = {Emmanuel Hainry and Bruce Kapron and Jean-Yves Marion and Romain Péchoux},
  booktitle = {LICS},
  year = {2024},
  doi = {10.1145/3661814.3662100}
}