一句话：提出Taype语言，将安全策略与程序逻辑解耦，并首次实现不经意代数数据类型与磁带语义。
安全多方计算（MPC）允许对多个实体的私有数据进行联合计算，但现有高级MPC编程语言通常要求开发者将安全策略嵌入程序逻辑，导致更新安全需求或试验不同策略变得困难。本文设计并实现了Taype，一种允许将安全关注点与程序逻辑解耦的语言。为此，Taype提供了不经意代数数据类型和磁带语义的首个实现，这两个语言特性最近由用于不经意计算的核心演算λ OADT+提出。作者在一系列基准测试上评估了Taype的实现，展示了其能够为丰富的数据类型编码多种安全策略。
Secure multiparty computation (MPC) allows for joint computation over private data from multiple entities, usually backed by powerful cryptographic techniques that protect sensitive data. Several high-level programming languages have been proposed to make writing MPC applications accessible to non-experts. These languages typically require developers to enforce security policies within the logic of the secure application itself, making it difficult to update security requirements, or to experiment with different policies. This paper presents the design and implementation of Taype, a language that permits security concerns to be decoupled from the program logic. To do so, Taype provides the first implementation of oblivious algebraic data types and tape semantics, two language features recently proposed by a core calculus for oblivious computation, λ OADT + . We evaluate our implementation of Taype on a range of benchmarks, demonstrating its ability to encode a range of security polices for a rich class of data types.
@article{paperbot1980,
title = {Taype: A Policy-Agnostic Language for Oblivious Computation},
author = {Qianchuan Ye and Benjamin Delaware},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591261}
}