动态信息流监测

一次高分支没有告诉你另一侧发生了什么 ​

秘密分支更新了y，当前执行能给y打H标签；另一种秘密可能完全跳过这次赋值，使y仍是L。随后若按y决定是否修改别的低变量，两个运行会用不同的标签和控制来走路。朴素并集只描述当前被执行的写入，漏掉了这种跨运行的不对称。

NSU在不对称刚出现时拦住写入。PU允许它暂时存在，用P提醒后续执行：“这个值在另一运行中可能仍公开，不能直接拿它控制动作。”若后来无条件用公开常量覆盖它，不对称已经被消除，程序就可以继续。

两层条件击穿朴素升级 ​

h为H，y、z开始为L，执行：

y := 1; z := 1
if h then y := 0
if y then z := 0

h=0时，第一支不写y，它仍为$1^L$；第二支在低pc下把z写成$0^L$。h=1时，朴素策略把y写成$0^H$；第二个条件为假，z保留$1^L$。两侧都能通过低sink，却分别公开0和1。

NSU在h=1的第一次y写入处拒绝。PU先把y标为$0^P$，到第二次条件读取P守卫时拒绝。这两种策略都阻止了“两个不同值均被接受”的反例，但其中一侧拒绝、另一侧成功仍可形成拒绝通道。

数据流污点跟踪理路动态污点跟踪Dynamic taint tracking · Data-flow taint propagation在一次执行中传播来源集合，精确说明它追踪的数据依赖，以及与语义依赖和隐式信息流的差别。只传播右端来源时，这个例子的常量写入全部为空标签，也会漏掉两层控制泄漏。加入pc有必要，正确处理敏感升级同样有必要。

公开覆盖让PU继续执行 ​

if h then z := 1
z := 0

z初始为$0^L$。h=1时，NSU在第一支写z就拒绝；PU暂存$1^P$，退出分支恢复pc=L，下一句用$0^L$覆盖，最后公开0。h=0时PU也输出0。两侧都通过，原始程序的低结果被保留。

若将最后一句移入秘密分支，pc不再恢复为L，第二次写z仍得到P，不能公开。关键是无条件的公开覆盖，而非某个特定常量的数值。

为什么P不能随意当作H ​

定义两个标记值兼容：两个L值必须数值相同；两个H值总兼容；任一侧是P时也兼容。其余H/L组合不兼容。状态逐名字兼容。这个关系不是传递的：$0^L$兼容$9^P$，$9^P$兼容$1^L$，但$0^L$不兼容$1^L$。

因此证明不能随意串联兼容关系。先定义高pc下允许的“演变”：保持原值，或H变H，或新标签变P。PU赋值表保证高pc执行的每个名字都只作这种演变。另证一侧兼容状态发生这种演变后，仍与原来的另一侧兼容；对称方向也成立。这是处理一侧执行秘密分支、另一侧跳过它的工具。[1, §4，Lemmas 1–2]

再按两次正常执行推导作归纳。公开条件在两侧有相同L值，选择同一支；私密条件可能不同，使用高pc演变约束；P条件不能出现在正常完成的推导中。赋值按lift表逐格保持兼容，循环沿有限推导处理。最终两个sink都为L，兼容便迫使数值相同。NSU正常执行不产生P，且其通过的每步也被PU允许，因此得到相同的低结果保证。[1, Theorems 1–2]

把P在单次运行中直接改为H会丢掉“另一侧可能是L”的事实，使上面的不变量失效。若语言允许显式隐私升级，必须固定在两侧一致的程序位置和规则下执行；本页执行器不包含升级注解自动推断。

执行、成本与观察边界 ​

下载解释器用显式命令栈保存外层pc，因此分支退出和循环重测都恢复到正确控制范围。一次常数标签连接、比较或lift查询需常数时间。令A为源程序语法大小，v为名字数，T为守卫/赋值/skip的语义步数，K为包括seq容器在内的实际命令栈分派次数，E为表达式节点总访问量；包含语法验证和初态复制，总时间$O(A+v+K+E)$，不含大整数算术位成本。当前状态与解释栈最坏$O(A+v)$，trace=True的额外日志按T条事件计。下载结果同时报告steps和dispatches；深层seq包装可以在循环中被反复经过，因此K不能直接用T或源语法大小A替代。

若把REJECT当成网络回复、让攻击者看超时，或在最终sink之前就输出中间值，观察模型已经改变。终点以公开覆盖例展示NSU的成功/拒绝差异，要求明确指出TINI前提在哪一侧不满足，而不是把拒绝包装成“没有任何泄漏”。

结构迁移 ​

在两层条件例中，把最后一句改为无条件z:=y。h=0时得到$1^L$并可公开；h=1时NSU仍在第一次写入拒绝，PU复制$0^P$，直到最终sink才拒绝。现在阻断点由P守卫改成P输出。再追加无条件z:=0，PU两侧都可完成；NSU仍不会越过它已经拒绝的早期写入。验收应列出每次旧标签、pc、右端标签和新标签。