Higher-order probabilistic adversarial computations: categorical semantics and program logics
Higher-order probabilistic adversarial computations: categorical semantics and program logics
复制标题
高阶概率对抗性计算：分类语义和程序逻辑
DOI：
10.1145/3473598
复制
发表时间：
2021
影响因子：
--
通讯作者：
Sato, Tetsuya
中科院分区：
文献类型：
--
作者：
Aguirre, Alejandro;Barthe, Gilles;Gaboardi, Marco;Garg, Deepak;Katsumata, Shin-ya;Sato, Tetsuya
对抗性计算是一类被广泛研究的计算，其中资源有限的概率对手可以访问oracle，即具有私有状态的概率过程。这些计算经常出现在几个领域，包括安全、隐私和机器学习。在本文中，我们发展了高阶环境下对抗性计算推理的程序逻辑。我们的逻辑是建立在一个简单类型的λ微积分上的，扩展了一个概率和状态的分级单子。分级用于建模和限制计算的内存占用和成本（就oracle调用而言）。在这种观点下，对手是一个高阶表达式，它期望将其预言机的代码作为参数。我们开发了一元程序逻辑来推理错误概率和期望值，以及关系逻辑来推理基于耦合的属性。所有逻辑都具有对抗性计算的规则，并产生对满足固定资源策略的所有对手有效的保证。我们利用一般的分级谓词提升概念证明了拟borel空间范畴中逻辑的稳健性，并利用分级谓词提升上的逻辑关系建立了对手证明规则的稳健性。我们用简单但说明性的例子来说明我们的逻辑的工作原理。
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with private state. These computations arise routinely in several domains, including security, privacy and machine learning.In this paper, we develop program logics for reasoning about adversarial computations in a higher-order setting. Our logics are built on top of a simply typed λ-calculus extended with a graded monad for probabilities and state. The grading is used to model and restrict the memory footprint and the cost (in terms of oracle calls) of computations. Under this view, an adversary is a higher-order expression that expects as arguments the code of its oracles. We develop unary program logics for reasoning about error probabilities and expected values, and a relational logic for reasoning about coupling-based properties. All logics feature rules for adversarial computations, and yield guarantees that are valid for all adversaries that satisfy a fixed resource policy. We prove the soundness of the logics in the category of quasi-Borel spaces, using a general notion of graded predicate liftings, and we use logical relations over graded predicate liftings to establish the soundness of proof rules for adversaries. We illustrate the working of our logics with simple but illustrative examples.
登录
查看更多内容
功能空间的 Borel 结构
影响因子：
0.6
作者：
R. Aumann
通讯作者：
R. Aumann
代数效应的合理且完整的逻辑
DOI：
10.1007/978-3-030-17127-8_22
发表时间：
2019
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
C. Matache;S. Staton
通讯作者：
S. Staton
DOI：
10.1109/lics.2017.8005137
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Heunen C
通讯作者：
Heunen C
影响因子：
--
作者：
Benton, Nick;Hofmann, Martin;Nigam, Vivek
通讯作者：
Nigam, Vivek
计算不可区分性逻辑
DOI：
--
发表时间：
2010
期刊：
Conference on Computer and Communications Security
影响因子：
--
作者：
G. Barthe;M. Daubignard;B. M. Kapron;Y. Lakhnech
通讯作者：
Y. Lakhnech