交付一份信息流政策与执行证书 ​

信息流政策与可执行检查路线的终点是一份逐步可核对的报告。它应同时回答三个问题：程序实际算出了什么，检查器批准或阻断了哪一步，以及被证明的观察究竟包含什么。

下载标准库解释器与核验器。运行python foundation-information-flow-check.py，它输出JSON，不读取文件、不联网。普通模式与python -O均使用显式检查，结果应一致。代码提供AST构造函数、static_check、run与独立低接口sme_low，方便替换程序后复算；它不是可直接部署的安全沙箱。

一、先写清观察和共同模型 ​

固定有限变量，所有初态名字都有数学整数值。使用常量、变量、加减、==、<、<=，以及skip、赋值、顺序、if、while。比较返回0或1，条件以0为假。没有堆、别名、异常、溢出、外部I/O和并发。

基本低观察是正常结束后指定out变量的一个值。中间状态、动态标签、拒绝原因、命令步数和整体终止都不在观察中。解释器返回的state、labels、events是教学诊断，不得把它们一起发给低侧后继续引用只保护out的定理。

REJECT表示监测失败或sink不允许；UNKNOWN表示命令预算耗尽。两者都不提供低值。UNKNOWN不能证明发散，有限输入全部通过也不能证明一般整数程序的NI。静态和动态监测页的普通可靠性只比较两次都正常结束且sink接受的运行。

二、用同一对秘密区分几种检查 ​

初态h为H，y、z为L且均为0，最终sink为z。分别让h=0和h=1，公开初态保持相同。表中“拒绝”指该次动态运行没有可释放结果；静态结论针对整段程序，而不是单个输入。

请补一列原始计算值。显式复制和异值分支在两侧分别为0、1；后三行均为0。于是可以同时看到：类型检查会保守拒绝某些安全程序，数据标签为空仍可能有控制泄漏，而相同数学结果仍可能保留执行来源标签。

SME的默认高输入是0，只有默认副本提供低结果。它不运行类型或动态标签准入，也不以真实副本的结果替换公开答案。下载JSON里raw与sme_low的sink_label为null，表示这些路径不使用运行时标签作放行条件；不能把null读成一份额外安全证明。

三、逐行拆开两层隐式流 ​

执行：

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

h=0时，第一支跳过，y仍为1ᴸ；第二支在低pc写z=0ᴸ。h=1时，朴素pc并集把y写成0ᴴ，第二支不执行，z仍是1ᴸ。两侧最终标签都为L，却泄漏了h。

NSU在h=1的第一处y写入拒绝；PU把y写成P，在第二个守卫拒绝。按下载执行器计数，前两赋值各一步，if测试各一步，被选中的skip也一步：朴素两侧均执行6步，NSU在h=1的第4步拒绝，PU在第5步拒绝。步骤编号只用于复算，不属于基本低观察。另报dispatches，统计包括seq容器在内的全部命令栈分派；循环会反复经过这些容器，实际解释成本用分派数K和表达式访问数计算，不能只按steps估算。

结构迁移一：把最后一个条件改成无条件z:=y。PU在h=1时可以复制P，但最终sink拒绝；阻断点从条件变成了输出。结构迁移二：再加无条件z:=0，PU两侧都能公开0。NSU此前已经拒绝的运行不会因为后来存在清除语句而恢复。

另将原公开覆盖程序的REJECT变成可见回复“拒绝”。h=0得到0，h=1得到“拒绝”，观察者便可区分秘密。报告要指出新观察包含了拒绝事件，原“双侧均接受”的合同没有比较这对运行；不能写成定理已经覆盖而实现偶然失效。

四、用来源事件图独立核污点 ​

指定a=3携带来源A，b=4携带来源B，其他名字初态为空来源。执行：

t := a + b
u := t - a
t := 0
out := u

验收值为out=4，标签为{A,B}。请画每个赋值产生的新值节点：u引用旧t与a，后来覆盖t不会回头改写u的来源。以图上的反向可达来源重新求集合，结果必须等于运行时并集传播。

把u:=t-a改成u:=b，最终值仍为4，标签只剩B。再把最后一句改成if a then out:=u else out:=0，数据标签在两支分别为B与空集；控制选择仍未被这张数据图表示。一个只允许B的sink通过，并不能证明关于A的双运行不变性。

API的sources使用整数位掩码，例如A=1、B=2、并集=3，allowed_sources=2表示sink只允许B。未提供allowed_sources时，taint模式报告标签而不阻断任何来源；必须另声明sink政策才能解释接受/拒绝。

五、批准初始总和，并阻止更新后的洗白 ​

固定a、b为H，out、n为L。批准清单只有sum ↦ a+b，比较初态(a,b)=(2,5)与(3,4)，两者初始公开和都为7。

先调用static_check并确认accepted，才可将run的结果按政策发布。表中被拒绝程序仍列原始运行数值，是为了展示攻击反例；run本身不会替调用者执行U/D准入。

初始同和关系才是批准合同；最后两次释放都使用同一个站点名，并不自动授权新函数2a。下载器为清单精确匹配站点和表达式，未知站点、同站点换表达式、嵌套release或清单读取未知名字都会给输入错误，而不是放宽政策后继续运行。

循环迁移：while n>0 do (out:=release_sum(a+b); b:=a; n:=n-1)在n=2时第二轮已释放改写后的和。身体U含b，D也含b，循环规则拒绝；删去b:=a后，U只含out和n，不与{a,b}相交，循环通过，两次都输出7。

再把更新换成b:=b。程序数值不变、满足本政策，但语法U/D仍拒绝，这是保守更新摘要。把它移到最终释放之后可通过；若末尾再加释放又被拒绝。请交出这三次方向变化的集合计算，不能只把拒绝解释成实际攻击。

六、分别验收SME的安全和透明性 ​

先运行while 0<h do h:=h-1; z:=0。默认高输入0，真实h取0、1、3。低副本都用2步公开0，高副本分别用2、4、8步，合计4、6、10步。安全来自低副本完全相同，工作量账本来自两份真实轨迹，不是“复制两份所以恰好两倍”。

然后运行while h==0 do skip; z:=0。真实h=1时2步结束，默认副本不会改变h，数学语义中发散。预算20只能实际报告UNKNOWN；另用不变真守卫证明发散。原程序所有结束运行都输出0，仍满足TINI，所以单有TINI不能保证SME保留本次返回行为。

将默认值改为1。此时低副本2步结束，真实h=0的高副本发散也不阻止低答案。最后把接口改成“两个副本都结束才返回”：它重新让高侧终止决定低侧是否有结果。这个迁移改变发布依赖，虽未改变投影公式，仍越出了原接口证明。

函数sme_low只执行低副本。教学报告若另外调用run得到高轨迹，是审计工作，不是低接口等待高结果的实现。硬件缓存、CPU调度和内存资源失败没有纳入这个纯语言模型，语义步数一致不能替代机器恒时证书。

七、交付和反向检查 ​

提交程序AST、标签/来源/释放清单、初态对、静态推导或失败规则、动态逐步标签、sink决定、实际值和有限预算状态。每个安全结论注明它比较的输入关系以及观察；每个拒绝注明是授权格式、静态规则、敏感升级、P守卫还是sink失败。

核验器的1176个有限程序每个运行27个输入，共比较127008对同低输入；它保留静态与监测结果和SME低轨迹检查。这些是实现回归证据。一般可靠性分别由pc低一致/高约束证明、PU兼容与演变证明、去密U/D来源保持证明和SME投影相等证明负责。

最终报告至少保留四个结构性反例：空污点的隐式流、朴素pc并集的两层洗白、批准表达式之前的秘密改写、默认副本或高副本等待改变终止行为。它们分别检验传播边、跨运行标签、政策输入关系和发布接口，不能互相替代。