埃尔顿：用于推理对抗性概率程序的瓮资源
Elton: Urn Resources for Reasoning about Adversarial Probabilistic Programs
浏览论文内容
中文总结 AI 辅助
研究对抗性概率程序，提出埃尔顿这一高阶分离逻辑，利用语言层面延迟采样和逻辑层面瓮资源等工具，结合其他特性，能证明安全示例错误界限，且证明已机械化验证。
中文摘要 AI 辅助
概率程序在许多应用中都很重要。特别是对于安全应用，人们希望建立在任意对手（即未知代码片段）存在的情况下都成立的属性。我们提出了埃尔顿，一种用于推理使用未知对抗性代码的高阶概率程序的高阶分离逻辑。埃尔顿在语言层面纳入了用于通过延迟采样指定分布属性不变量的新颖逻辑工具，并在逻辑层面引入了一种名为瓮资源的新型分离逻辑谓词。我们证明了这些扩展是合理的，并且可以回退到标准的按值调用语义。结合其他特性，埃尔顿具有足够的表现力来证明广泛安全示例的错误界限，其中一些超出了先前技术的范围。所有证明都使用Rocq证明助手和Iris分离逻辑框架进行了机械化验证。
英文摘要
Probabilistic programs are important for many applications. For security applications in particular, one is interested in establishing properties that hold in the presence of arbitrary adversaries, i.e., unknown pieces of code. We present Elton, a higher-order separation logic for reasoning about higher-order probabilistic programs utilizing unknown adversarial code. Elton incorporates novel logical facilities for specifying invariants over distributional properties using delayed samplings at the language level, and a new kind of separation-logic predicate called urn resources at the logic level. We show that these extensions are sound and can be erased back to a standard call-by-value semantics. Combined with other features, e.g. invariants and ghost resources, Elton is expressive enough to prove error bounds on a wide range of security examples, some of which are beyond the scope of previous techniques. All proofs are mechanized with the Rocq proof assistant and the Iris separation logic framework.
