为不透明调用构建授权证据：一个故障封闭的重写授权边界
Build-Authorized Evidence for Opaque Calls: A Fail-Closed Rewrite-Authority Boundary
浏览论文内容
中文总结 AI 辅助
研究不透明本地提供程序重写权限问题，提出构建授权的路径效应接口，通过故障封闭授权和链接收据强化边界，经Rocq模型证明相关特性，用Toka实例化生产，展示了对不透明调用等的处理效果及贡献。
中文摘要 AI 辅助
关于不透明本地提供程序的分离语义事实本身并不能证明编译器重写的合理性：重写权限必须局限于已接受的事实、选定的提供程序和构建、调用者、回调环境、观察结果和运行时目标。我们提出了一个构建授权的路径效应接口，通过故障封闭授权和链接收据来强化这个边界。该设计分离了收据封闭、回调环境封闭和投影标识，并通过一个狭窄的内部API将已接受的事实传递给LLVM。我们使用单跳拓扑负载重用作为权限的最小可观察见证，而不是作为优化目标。Rocq模型在显式效应、别名、编译器/ABI和目标解析前提条件下证明了条件细化和权限非放大。我们用Toka实例化了经过检查的生产：一个源摘要门发出精确的LLVM IR，一个单独的IR检查器只接受有界的拓扑保留子集，只有被接受的IR才被编译成收据绑定的提供程序对象。一个有界的静态Darwin/arm64配置文件也会检查最终的直接分支目标。在跨发行者声明的readv、recvmsg和Cairo边界上，授权的IR保留每个不透明调用，将相关负载从两个减少到一个，并保留观察结果；不匹配的提供程序、构建、回调、投影和不支持的IR保持中立。一个libjpeg案例被拒绝，因为其回调环境是开放的，而一个绑定的回调单例展示了支持的封闭规则。贡献是一个经过检查的部署编译器边界，具有明确的信任和适用性边界，而不是一种独特的表达效应编码或一种新的负载消除算法。
英文摘要
Detached semantic facts about opaque native providers do not by themselves justify compiler rewrites: rewrite authority must be confined to the accepted fact, selected provider and build, caller, callback environment, observation, and runtime target. We present a build-authorized path-effect interface that enforces this boundary through fail-closed authorization and link receipts. The design separates receipt closure, callback-environment closure, and projection identity, and passes accepted facts to LLVM through a narrow internal API. We use one-hop topology-load reuse as a minimal observable witness of authority, not as the optimization target. A conservative LLVM consumer reuses a pointer observation only from a noalias root or one constant nonzero projection. Rocq models prove conditional refinement and authority non-amplification under explicit effect, alias, compiler/ABI, and target-resolution premises. We instantiate checked production with Toka: a source-summary gate emits exact LLVM IR, a separate IR checker accepts only a bounded topology-preserving subset, and only accepted IR is compiled into the receipt-bound provider object. A bounded static Darwin/arm64 profile also checks the final direct branch target. Across issuer-declared readv, recvmsg, and Cairo boundaries, authorized IR retains each opaque call, reduces the relevant loads from two to one, and preserves observed results; mismatched providers, builds, callbacks, projections, and unsupported IR remain neutral. A libjpeg case is rejected because its callback environment is open, while a bound callback singleton demonstrates the supported closure rule. The contribution is a checked deployment-compiler boundary with an explicit trust and applicability frontier, not a uniquely expressive effect encoding or a new load-elimination algorithm.
