去密政策与受控释放

形式陈述

允许公开哪一种区别

沿用信息流类型系统的固定变量整数IMP与L/H标签。所有变量初始有值，表达式全定义，没有别名、外部I/O、异常和并发。观察只包含两次正常结束后的低变量值，不含终止与耗时。

政策是一张批准清单 $\Pi=\{p\mapsto e_p\}$ ：p是释放站点名， $e_p$ 是只读初始变量名、常量和全定义运算的纯表达式。程序可在表达式中写 $\operatorname{release}_p(e)$ ；检查器要求p在清单中，且e与批准表达式语法完全相同，不允许嵌套release。执行时release仍计算当前状态中的e，不主动修改数值；检查时它的结果可视为L。

政策允许的输入关系定义为

\sigma_1\equiv_{L,\Pi}\sigma_2 \iff \sigma_1\equiv_L\sigma_2\quad\land\quad \forall p\in\Pi,\;\llbracket e_p\rrbracket\sigma_1=\llbracket e_p\rrbracket\sigma_2.

安全合同要求：从这个关系中的两个初态出发，若程序在两侧都正常结束，则终态低等价。它允许区分批准表达式值不同的秘密，禁止额外区分表达式值相同的秘密。全部清单表达式都进入关系，即使某次运行不经过相应站点；这是事先批准的信息范围。[1, §3]

为什么还需要更新效应

同一个表达式语法，在变量被改写后可能计算完全不同的秘密函数。所以只检查站点和表达式名称还不够。为表达式返回 $(\ell,D)$ ： $\ell$ 是结果标签，D是所有release内部读到的变量名。普通常量/变量的D为空，二元运算合并子D； $\operatorname{release}_p(e_p)$ 给 $(L,FV(e_p))$ 。

为命令返回 $(U,D)$ ：U是可能赋值的变量集合，D是该命令所有释放表达式的来源名字。普通pc赋值条件仍然生效，因而release结果为L也不能在高pc下写L目标。效应规则如下：

命令	效应与附加条件
skip	U、D都为空
$x:=e$	$U=\{x\}$ ，D取e的释放依赖；满足原pc赋值条件
$c_1;c_2$	要求 $U_1\cap D_2=\varnothing$ ，然后分别合并U和D
if e then $c_1$ else $c_2$	两支pc提升到 $pc\sqcup\ell_e$ ，U合并两支，D再加入守卫的D
while e do c	身体用提升后的pc；要求 $U_c\cap(D_e\cup D_c)=\varnothing$ ，输出 $(U_c,D_e\cup D_c)$

顺序条件是有方向的：前段不能改写后段将释放的来源。循环条件保证身体不会破坏下一轮守卫或身体里的释放来源。U/D按语法保守地覆盖两支，不因某个测试恰好不执行便忽略。[1, §4，Figure 2]

可靠性：批准站点匹配且上述效应类型检查通过，便满足该终止不敏感的受控释放合同。清单可包含程序没有用到的表达式；这样只会收紧所比较的输入对，仍有可靠性，但授权范围可能比实际所需更宽。

直觉

批准“总和”不等于批准它背后的两个数

若允许公开两个私密数字a和b的和，初始(2,5)与(3,4)都属于公开总和7的同一类。程序可以输出7，不能再输出a来区分这两种情况。

把b先改成a，再运行字面上仍叫“a+b”的批准表达式，输出却变成2a。释放站点没有改名，真正释放的函数已经被前面的更新改变。U/D规则把这种跨语句联系变成可以直接检查的集合交集。

例子与边界

两组同和秘密的手算

设a、b为H，out为L，批准清单只含sum ↦ a+b。

text

out := release_sum(a + b)

赋值在pc=L，release结果标签L，目标out为L。U= $\{out\}$ ，D= $\{a,b\}$ ，检查通过。初态(2,5)与(3,4)都输出7。

现在在前面添加b:=a。该赋值自身是合法高写入，但 $U_1=\{b\}$ 与后段 $D_2=\{a,b\}$ 相交，因此顺序规则拒绝。若绕过检查运行，第一组变成(2,2)输出4，第二组变成(3,3)输出6，确实违反初始同和政策。问题在更新顺序，不在加法是否正确。

批准初始总和7，合法释放两侧都为7；先改写b后输出4与6，更新效应与释放来源相交

修改发生在释放之后

把程序改成先释放，再执行b:=a。前段U只有out，后段D为空，交集为空；两次输出仍为7，所以检查通过。该政策并不要求秘密变量终生只读。

若再接第二次out:=release_sum(a+b)，前缀U已经包含b，后一次D仍含b，于是拒绝。相同修改放在最后没有问题，放到未来释放之前就必须重新检查。

循环能把“最后一次修改”变成下一轮的前缀

令n为L，执行while n>0 do (out:=release_sum(a+b); b:=a; n:=n-1)。单轮内部先释放再修改，看似合法；但身体U含b，身体D也含b，循环规则拒绝。第二轮已不再释放原始总和。

删去b:=a后，U= $\{out,n\}$ ，D= $\{a,b\}$ ，循环规则通过。n可以正常递减，因为批准的表达式没有读取n。若政策改为释放a+n，n也进入D，当前循环便被保守拒绝。

推论与应用

可靠性的关键是保住释放表达式的解释

表达式低一致性现在有两种依据：普通L变量在两侧相等，release内部的批准表达式由初态关系保证相等。顺序组合时，后段需要的是中间状态上的释放表达式相等。 $U_1\cap D_2=\varnothing$ 保证前段没有修改它们读到的名字，所以其值从初态保留到中间状态；归纳前提由此成立。

循环对每轮重复同样的保护。秘密守卫仍由pc限制低写入；公开守卫或者批准释放后的守卫，在所比较两状态取相同值。两侧都终止时，原信息流类型证明加上释放表达式保持，就给出低结果一致。[1, 附录]

不带U/D而只把release标签强行降为L，上述顺序证明缺了关键前提；同和例已给出可执行反例。反过来，U/D可能拒绝语义上无害的更新，如把a写回同一个a，因为它追踪“可能修改名字”，不证明新旧数值恒等。

政策的表达能力和成本

下载器把检查和求值分成两个接口：static_check返回准入与U/D证据，run(policy=Π)按原始程序计算数值，只核清单格式而不自动执行效应准入。要发布结果，调用方必须先确认类型检查通过；对拒绝程序执行run只用于复算反例，不能把得到数值视为获得释放许可。

该关系把所有批准表达式都看作可以公开，因此不表达“本次只能在a、b中选择一个公开，不能两个都公开”的历史政策。把单射密码摘要列入允许结果还可能让输入等价类只剩单元素；信息论关系无法替代计算隐藏性，相关反例见常数时间泄漏合同。本页的执行器也没有签名验证、访问主体或审批流程，清单本身必须来自任务给定的授权政策。

令A包含程序与批准表达式清单的总语法大小，v为变量数， $b=1+\lceil v/w\rceil$ 。以位集计算FV、U、D，并用后序遍历和从左到右的顺序合并，保守时间界为 $O((A+v)b)$ ；显式语法栈与保存的效应摘要最坏 $O((A+v)b)$ 空间。站点/名字已编号，查表按常数时间计；下载Python散列表采用期望查找成本，整数值运算位成本另计。

结构迁移

批准a+b后，尝试把b:=a替换为b:=b。运行值不变，程序满足合同，但U/D仍拒绝；请指出这是语法效应的保守性。再把更新移到最后，检查通过。最后在末尾加第二个释放，拒绝恢复。三个程序的差别是更新相对释放的次序，验收须给出各处U/D及同和输入的实际输出。

终点同时核验未批准站点、同站点换表达式、嵌套release与循环重复来源，先区分格式/授权错误，再区分类型拒绝和运行结果。

参考资料

[1] Andrei Sabelfeld and Andrew C. Myers, “A Model for Delimited Information Release”, ISSS 2003，LNCS 3233，2004，pp.174–191，§3初始状态的delimited release及信息洗白反例，§4更新/释放效应规则，附录Theorem 1证明。本文采用两级、全定义整数表达式特例，外加显式站点清单作为教学检查输入；清单的权限管理不由该定理证明。

形式陈述 ​

允许公开哪一种区别 ​

为什么还需要更新效应 ​

批准“总和”不等于批准它背后的两个数 ​

两组同和秘密的手算 ​

修改发生在释放之后 ​

循环能把“最后一次修改”变成下一轮的前缀 ​

可靠性的关键是保住释放表达式的解释 ​

政策的表达能力和成本 ​

结构迁移 ​

反向链接