资源安全的系统编程语言

以下摘要由 AI 根据胶片自动生成。

本报告探讨如何为系统编程语言引入资源安全保障，目标是在类型系统层面静态保证算法复杂度符合预期、物理资源消耗满足约束、且不存在资源相关安全漏洞。技术路线涵盖基于势能均摊的静态复杂度分析（自动推导多项式上界）、资源制导符号执行（生成最坏情况输入），以及量化霍尔逻辑（将霍尔三元组推广为势函数）与分离逻辑的结合。以概率程序高阶矩分析（PLDI’21）为例，展示如何用方差上界和 Markov 不等式给出侧信道攻击成功概率的严格界，成功率可达 83% 以上。