一句话：提出核心语言 Lambda Obliv，用子结构类型系统与「概率区域」静态保证概率程序的不经意性，并修复 ObliVM 的不健全性。
不经意计算要求程序不因可观测的执行差异（如时间、内存访问模式）而直接或间接泄漏信息。已有基于类型系统的工作主要针对确定性程序，而密码学等场景常需实现概率算法，其可观测事件的分布本身也可能泄漏信息。本文提出核心语言 Lambda Obliv，其类型系统强制不经意性：它采用子结构类型系统，并引入全新的「概率区域」概念来推理值之间的概率相关性与独立性，从而保证信息不会通过可见事件分布泄漏。概率区域的引入直接源自作者在 ObliVM（实现先进不经意算法的语言）类型系统中发现的一处不健全性。作者证明了 Lambda Obliv 的类型系统确实保证不经意性，并展示其表达力足以对先进的树形不经意 RAM（ORAM）进行类型检查。
An oblivious computation is one that is free of direct and indirect information leaks, e.g., due to observable differences in timing and memory access patterns. This paper presents Lambda Obliv, a core language whose type system enforces obliviousness. Prior work on type-enforced oblivious computation has focused on deterministic programs. Lambda Obliv is new in its consideration of programs that implement probabilistic algorithms, such as those involved in cryptography. Lambda Obliv employs a substructural type system and a novel notion of probability region to ensure that information is not leaked via the observed distribution of visible events. Probability regions support reasoning about probabilistic correlation and independence between values, and our use of probability regions is motivated by a source of unsoundness that we discovered in the type system of ObliVM, a language for implementing state of the art oblivious algorithms. We prove that Lambda Obliv's type system enforces obliviousness and show that it is expressive enough to typecheck advanced tree-based oblivious RAMs.
@article{paperbot556,
title = {A language for probabilistically oblivious computation},
author = {David Darais and Ian Sweet and Chang Liu and Michael Hicks},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371118}
}