AI 中文总结
针对非格状析取信息流策略，构建流敏感类型系统族，发现通用类型对象分裂问题，在不同自由对象上分析精度差异，提出通过推迟特化恢复精度的方案。
AI 中文摘要
析取策略允许值依赖于两个秘密中的至多一个，而绝不会同时依赖于两者：分析师可以查阅一个客户的文件或另一个客户的文件，拆分秘密的一个份额可以被发布但不能发布其对应的份额。此类策略并非格状结构，Hunt 和 Sands 引入了信息的 quantale（量子群）以赋予其语义，却留下了实施层未解决。我们构建了该 quantale 所要求的流敏感类型系统族，并表明使此类系统族有用的对象——每个成员都从中特化出的通用类型对象——会分裂为二，这对实施产生了影响。在程序变量上的自由交换 quantale 中，整个机制对每个策略都成立：单调重命名、规范推导、主类型、内部完备性。在具有幂等生成元的自由对象上，经认证的界限严格更精确且仍保持合理，因为它记录了对同一源的两次读取符合一个析取项。该间隙无法从独立属性族内部闭合：其形状的任何标记映射支持单调重命名的机制，都无法认证出比第一个更精确的界限，且在生成元精确同态特化下的主类型方面，两者是一致的。在伦理墙和秘密共享标记下，因此对析取源的第二次读取会使此类证书失去所有保证，满足策略的程序会被拒绝。格时代对象的字面转写也无法逃脱：它是进一步的商，丢失了分支析取。通过将特化推迟到判断级别来恢复精度，所得的读出映射是最合理的保并映射。
英文摘要
A disjunctive policy allows a value to depend on at most one of two secrets and never on both: an analyst may consult one client's file or the other's, a share of a split secret may be released but not its sibling. Such policies are not lattice-shaped, and Hunt and Sands introduced the quantale of information to give them a semantics, leaving the enforcement layer open. We build the flow-sensitive type system family that the quantale calls for, and show that the object which makes such families useful, the universal type object from which every member specialises, splits in two, with a consequence for enforcement. Over the free commutative quantale on the program variables the whole mechanism survives for every policy: monotone renaming, canonical derivations, principal typings, internal completeness. Over the free object with idempotent generators the certified bound is strictly more precise and still sound, because it records that two reads of one source honour one disjunct. The gap cannot be closed from inside the independent-attribute family: no mechanism of that shape whose labelling maps support monotone renaming certifies a bound more precise than the first, and for principal typings under generator-exact homomorphic specialisation the two coincide. Under the ethical-wall and secret-sharing labels the second read of a disjunctive source therefore drives every such certificate to no guarantee, and programs that satisfy the policy are rejected. The literal transcription of the lattice-era object is no escape either: it is a further quotient that loses branch disjunction. Precision is recovered by deferring specialisation to the judgement level, and the resulting read-out map is the least sound join-preserving one.
Comments13 pages, 3 figures, 1 table. Under review
