信息流类型系统

常量也可能把秘密带出去 ​

赋值out:=h沿数据操作直接复制秘密。if h then out:=1 else out:=0没有在右端读取h，却用秘密决定哪一个常量到达out。pc记录的正是这种选择信息，所以赋值规则要同时检查右端标签和控制标签。

固定标签像每个变量的存放许可，而不是当前值的精确秘密程度。H变量可以接收L值；L变量不能接收H值，也不能在秘密选择的路径上被修改。这样无需运行程序就能检查全部分支，包括测试输入没有走到的那一支。

沿推导树找出拒绝的位置 ​

设$\mathrm{\Gamma }(h)=H$，$\mathrm{\Gamma }(out)=L$。检查if h then out:=1 else out:=0时，守卫标签H把两支pc提升到H。两次赋值右端都是L，但$H\bigsqcup L=H⋢L$，因此拒绝。h=0和h=1实际分别输出0和1，双运行反例也成立。

把两支都改成out:=0，类型判断仍拒绝。此时每次正常运行都输出0，程序其实满足所选NI合同；检查器没有比较两个分支的语义。可先证明两支等价并把整个条件改写成一次公开赋值，改写后的程序便能通过。这样的拒绝是保守近似的代价。

再看if h then secret:=1; out:=0，其中secret为H。秘密分支中的H写入合法，后面的out赋值恢复pc=L，也合法。若把out赋值移入秘密分支，则即使常量还是0，也再次触发高pc写低变量的禁令。

接受不等于隐藏终止 ​

while h == 0 do skip
out := 0

循环体不写低变量，随后out在外层pc=L下写常量，所以类型检查接受。h=1时两步完成；h=0时守卫永远为真，数学语义中不终止。TINI只比较两次都结束的结果，不能阻止观察者通过“有没有返回”区分这两个秘密。有限预算解释器在后者报告UNKNOWN；证明不终止靠的是守卫和状态永不改变，不是这个预算报告。

可靠性证明的两个支点 ​

先证低表达式一致：若表达式标签L，它读到的变量全是L；两个低等价状态经过相同的全定义运算，得到相同值。再证高pc约束：当$pc=H$时，赋值只能写H变量；故任何正常结束的高pc命令都保持低状态。

对两次终止执行作归纳。赋值若目标为L，规则迫使pc和右端都是L，故写入值相同；若目标为H，不影响低等价。顺序组合用前段结果作为后段前提。低守卫的条件走同一支；高守卫即便走不同支，两支都不能改低状态。

循环也分两种。低守卫在对应低等价状态取相同真假，每一对循环体结束后维持低等价；沿有限终止推导重复即可。高守卫可能让两侧迭代次数不同，但全部循环体都在高pc下，正常结束时低状态仍是进入循环时的低状态。这一步没有证明终止同步，恰好解释了定理的量词范围。

执行与成本 ​

后序遍历语法树，向下传pc，向上传接受/拒绝信息即可；不需要展开循环。设完整语法树有A个节点，环境有v个名字，以已编号名字的常数时间查表和两级标签运算计，基本判定需$O(A+v)$时间，栈空间受语法深度约束，最坏$O(A+v)$。

下载实现的static_check还统一返回去密检查理路去密政策与受控释放Declassification policy · Delimited release with update effects把允许释放的初始表达式写成明确政策，并用更新/释放依赖效应阻止改写秘密后的信息洗白。使用的U/D名字位集。该实现的保守位操作界是$O((A+v)(1+\lceil v/w\rceil ))$，w为位集机器字宽；它不应直接套用只返回布尔值的基本判定成本。记录每条赋值的规则证据另用$O(A)$条记录，名字字符串成本单独计算。

结构迁移 ​

把前面的高循环改成while n>0 do (secret:=h; n:=n-1); out:=n，其中n和out为L，secret为H。可用0<n表达守卫。此时循环pc=L，写secret和递减n都合法。两次低等价初态具有相同n，因而有限非负n时循环次数也相同。若再把守卫改成0<h，递减n就发生在pc=H下，首先被拒绝的是n的低写入。验收应画出pc传递和失败赋值，而不只给最后一个“拒绝”。

完整终点将这套静态准入与运行时标签、授权释放和输入投影放在同一程序上比较。