超性质

安全性可以取决于两次执行之间的差异 ​

单独看输出 5，无法断言秘密泄漏了。它可能是公开输入要求的结果，也可能编码了秘密。非干扰固定公开输入，改变秘密输入，再比较输出：若观察者能从输出变化辨别秘密变化，程序就违反了这个合同。

“同一输入运行两次得到相同输出”只检验确定性。非干扰的两次运行允许 $h_1\ne h_2$，要求相同的只是 $l$。秘密也不是完全不能参与计算；它可以出现在内部算式中，只要最后公开结果不随它改变。

为什么不能逐条检查轨迹来表达 NI ​

取两条公开输入相同、公开输出不同的轨迹 $t_1,t_2$。单元素集合 $\{t_1\}$ 与 $\{t_2\}$ 都属于 $\mathrm{NI}$，因为各自内部不存在冲突的两条轨迹；它们的并集却不属于 $\mathrm{NI}$。

假设存在某个轨迹性质 $P$，对所有 $T\subseteq Tr$ 都有

两个单元素集合满足 NI，迫使 $t_1,t_2\in P$，于是 $\{t_1,t_2\}\subseteq P$，按假设它也应满足 NI，矛盾。问题不是某种单轨迹逻辑还不够强，而是固定的逐轨迹允许集无法表达这项跨轨迹约束。

这个证明比较一般的轨迹集合；其中的单元素集合不必来自一个覆盖全部整数输入域的程序。具体程序 $F$ 的验证仍使用上一节给定的完整 $T_F$。

秘密参与计算与秘密影响输出 ​

比较两个程序，内部变量 $z$ 不可观察：

安全候选 P                  泄漏程序 Q
z := l + h                  y := l + h
y := z - h                  output y
output y

固定 $l=3$，选择两个秘密输入：

对 $P$，代数化简给出 $F_P(l,h)=(l+h)-h=l$，所以对任意 $l,h_1,h_2$ 输出都相等。表格展示了一组实例，代数恒等式才覆盖全部输入。对 $Q$，表中的两条运行已经构成反例：同一公开输入 3 对应公开输出 5 和 10。

本例观察接口只保留最终 $y$。若在赋值后公开 $z$，安全候选也会泄漏；若观察运行时间或控制路径，则需要把那些信息加入轨迹重新验证。终止在本模型中已对所有输入作出保证，因此没有留下秘密依赖的终止差异。

有限非确定模型：先保留秘密输入的索引 ​

现在换一个明确有限的模型。公开输入域 $L$、秘密域 $H$ 都有限且非空，输出域 $Y$ 有限；程序总是终止，每个 $(l,h)$ 对应一个非空有限完整运行集 $\mathrm{Runs}(l,h)$，且能穷尽枚举，例如有限无环控制图上的程序。运行 $\rho =(l,h,c,y)$ 保留输入、完整内部选择记录 $c$ 与最终输出。公开观察仍只有 $(l,y)$，但规格量词在保留 $h$ 的完整运行域上解释。

定义

允许公开非确定性的一项合同为

它等价于固定 $l$ 时所有 $\mathrm{Out}(l,h)$ 相等。若 (M) 成立，任取第一集合的一个输出，选产生它的运行，再取匹配运行，便得到集合包含；交换有序输入对 $h_1,h_2$ 得到反向包含。反之，若集合相等，$y_1$ 属于第二集合，按定义就有一条输出它的完整运行。这是两个方向都可直接复核的等价证明。

将 $\mathrm{\exists }{\rho }_2$ 换成 $\mathrm{\forall }{\rho }_2$ 得到更强的全对相等条件。它推出 (M)，因为第二运行集非空；反向不成立。信息流文献也以交替轨迹量词允许选择匹配行为，[1, §2.3; 3, §3] 但这里证明的只是明确规定初始输入与最终输出的有限合同，并未把所有时序版本合并成同一个性质。

四条运行给出匹配，三个结果暴露缺口 ​

取 $L=\{0\}$、$H=Y=\{0,1\}$。程序 $P$ 非确定地选择位 $r$，输出 $y=r\mathrm{xor}h$；$Q$ 在 $h=0$ 时可输出两个位，在 $h=1$ 时只输出零。

对 $P$，两个输出集合都是 $\{0,1\}$。给定第一条运行的 $r_1,h_1$ 和目标秘密 $h_2$，取

就有 $r_2\mathrm{xor}{h}_2=r_1\mathrm{xor}{h}_1$，构成显式匹配函数。但它不满足全对相等：即使 $h_1=h_2=0$，$r_1=0,r_2=1$ 也产生不同输出。

对 $Q$，$\mathrm{Out}(0,0)=\{0,1\}$ 而 $\mathrm{Out}(0,1)=\{0\}$。取第一条运行 $h_1=0,y_1=1$，目标秘密 $h_2=1$ 没有匹配。这次不能靠“另一条运行输出不同”就断言无匹配；关键是已经穷尽了目标秘密下的全部运行。

若提前删除秘密标签，把两程序都压成公开轨迹集合，两者恰好都是 $\{(0,0),(0,1)\}$，却只有 $P$ 满足 (M)。所以不存在仅查看这个已遗忘 $h$ 的集合便区分二者的合同；必须先在完整运行集合上陈述 (M)，再通过公开投影定义匹配关系。此处与前面的确定性 NI 模型保留信息的需求不同。

自组合：把双运行关系变成单程序断言 ​

复制程序 $P$，把它读写的全部变量换成新鲜变量，得到 $P^{\prime }$：$l,h,z,y$ 分别变成 $l^{\prime },h^{\prime },z^{\prime },y^{\prime }$。两份存储完全不相交，再顺序执行 $P;P^{\prime }$。因为所有输入都正常终止，每个组合执行都能完成两份计算。

把输出视为终态变量 $y$，使用Hoare 三元组公理库Hoare 三元组Hoare triple断言若前置条件成立且程序终止，则后置条件成立的 {P}C{Q} 形式。检验

前置条件不要求 $h=h^{\prime }$，否则只会比较相同输入，失去检测秘密影响的能力。完全换新也包括输入变量和临时变量，避免第二份程序覆盖第一份所依赖的状态。[2]

在此模型中，三元组有效与 $P$ 满足 NI 等价。证明的关键是组合运行与两次独立运行的对应：任取原程序的两组输入，可把它们放在两份不相交的初始存储里；第一份只读写未加撇变量，第二份只读写加撇变量，所以终态恰好同时保存这两次运行的输出。

从三元组到 NI。 任取 $l$ 相同、$h$ 可以不同的两次原运行，把初始存储合并。它满足 $l=l^{\prime }$，组合执行后由有效三元组得 $y=y^{\prime }$，因此原来的两个输出相同。

从 NI 到三元组。 任取满足 $l=l^{\prime }$ 的组合初态。其两个存储分量分别决定原程序的两次运行；由 NI，它们的输出相同。第二份运行不改变第一份的 $y$，所以组合终态满足 $y=y^{\prime }$。这覆盖了所有满足前置条件的初态，三元组有效。

全终止假设在此承担实际工作：若第一份可能发散，串行组合可能根本执行不到第二份；部分正确性的三元组也可能因没有终态而真空成立。当前等价证明因此是在明确的总程序模型上进行的。

对安全候选，执行结果分别为 $y=l$ 与 $y^{\prime }=l^{\prime }$，前置条件直接推出后置条件。对泄漏程序，取 $l=l^{\prime }=3,h=2,h^{\prime }=7$，组合终态为 $y=5,y^{\prime }=10$，后置条件失败。自组合使跨执行问题落到已有的程序断言验证工具上。

为非确定匹配建立有限证书 ​

穷尽枚举每个 $\mathrm{Runs}(l,h)$，构造表

每个键保留一条见证即可；但键集合必须来自完整枚举。对每个 $l$ 选一个基准秘密 $h_0$，逐一比较所有表与 $W_{l,h_0}$ 的键集合。全部相等便接受；否则，从两个不等集合的差集中选一个输出，并把有该键的一侧作为 $h_1$，缺键的一侧作为 $h_2$，输出 $(l,h_1,h_2,{\rho }_1)$ 与第二侧的完整枚举结果。

接受可靠性来自：任意第一运行的 $y_1$ 都在所有第二侧表中，查表就构造 ${\rho }_2$。完整性来自：若 (M) 成立，已证明所有键集合相等，检查不会拒绝。拒绝可靠性则使用目标表的穷尽性；它证明没有可能被遗漏的匹配运行。若总运行数为 $N$、输入对数为 $K$，输出有固定有限编号，则用 $K|Y|$ 个槽和 $O(N+K|Y|)$ 时间即可构表并比较，另计存储或验证完整运行记录的成本。

普通自组合的全称 Hoare 三元组会检查所有独立选择对，因此验证的是全对相等；它会拒绝上例 $P$。验证 (M) 必须允许第二侧根据第一侧的运行挑选见证。这里的存在见证可以依赖整条已完成运行，尚未要求一个只能看到前缀的在线策略，也没有加入公平性或任何概率分布。相同可能输出不意味着相同输出概率。

两条有限坏观察与 2-safety ​

超安全性使用有限组有限前缀见证违反。形式化地，令 $U$ 是有限轨迹前缀的集合，写

超性质 $\mathcal{H}$ 是 $k$-safety，若每个 $T\notin \mathcal{H}$ 都存在有限前缀集合 $U$，使

这一定义要求至多 $k$ 条有限观察，而且无论怎样延长、怎样添加其他轨迹，违反都无法修复。[1, §§3–4]

为与通常基于无限轨迹的表述一致，把本页每条终止轨迹接上无限终态停顿，公开输入和已经输出的值保持不变。这是完整有限执行的编码，不把尚未输出的普通前缀误当作终止结果。

若 $T$ 违反 NI，必有两条轨迹的公开输入相同、公开输出不同。分别截取到最终输出已经出现的有限前缀，组成 $U$；任何延长都保留两个冲突输出，任何包含这些延长的执行集仍违反 NI。因此该 NI 是 2-safety。前面的单元素集合论证又说明，一个单轨迹坏观察不足以表达这种冲突。

这个 2-safety 结论针对全称 NI。它不直接适用于 (M)：在四条异或运行中删去 $h=1,y=1$ 的见证，就得到仍对每个输入有运行、却缺少匹配的集合；把该见证加回来又能修复。只看到两条不相等的输出不能排除未来观察到匹配运行。有限完整枚举能证实“没有”，依赖的是模型已被穷尽，不能与任意扩展下都不可修复的正观察坏前缀混淆。[1, §3]

这种有限见证解释了为什么产品程序适合搜索全称 NI 的泄漏反例：验证器寻找的是两份执行共同到达 $y\ne y^{\prime }$ 的状态。跨版本等价、关系化程序验证等也采用类似双运行思想，但应按各自的输入关系、输出关系和执行模型重新给出断言。