用密码学证明执行器纯净性,确保认知工作流不可绕过治理。
Certified Purity for Cognitive Workflow Executors: From Static Analysis to Cryptographic Attestation
- 通过无副作用指令的WebAssembly编译,从结构上保证执行器纯净。
- 验证延迟仅39–42微秒,全程低于400微秒,性能开销不足0.4%。
- 支持跨组织验证,适合高安全要求的工作流系统设计者。
我们提出一种认证纯净性架构,将认知工作流系统的治理强制从运行时约定转变为结构性能力边界。先前的三层治理架构在纯模块约束下可证明治理完整性、溯源完整性和不可规避效应的存在,但该约束依赖模块导入图分析,在BEAM虚拟机上易被恶意绕过。本文通过四项机制填补此漏洞:(1)采用移除副作用指令的受限WebAssembly编译目标;(2)生成加密签名的纯净证书,绑定执行器二进制与其导入分类;(3)运行时验证门禁,拒绝未认证执行器进入治理流程;(4)通过远程认证实现可移植的治理凭证,支持跨组织验证。我们证明了四个定理:构造性纯净性、对五类BEAM绕过方式的消除、证书完整性及门禁完备性。该保障基于显式可信计算基。在四个实现的执行器上评估显示,验证延迟为39–42微秒,完整计划周期低于400微秒,运行时开销低于100毫秒HTTP请求的0.4%,重复调用间无确定性偏差。
原文摘要 · Abstract (English)
We present a certified purity architecture that converts governance enforcement in cognitive workflow systems from a runtime convention into a structural capability boundary. A prior three-layer governance architecture proves governance completeness, provenance completeness, and the impossibility of ungoverned effects, conditional on the pure module constraint: that step executors cannot perform effects. That constraint was enforced by module import graph analysis, which is insufficient against adversarial bypass on the BEAM virtual machine. This paper closes the gap through four mechanisms: (1) a restricted WebAssembly compilation target where effect-producing instructions are structurally absent; (2) purity certificates, cryptographically signed proofs binding executor binaries to their import classifications; (3) a runtime verification gate that rejects uncertified executors before they enter the governance pipeline; and (4) portable governance credentials via remote attestation for cross-organizational verification. We prove four theorems: structural purity by construction, bypass elimination for all five BEAM bypass classes, certificate integrity, and gate completeness. The guarantee holds relative to an explicit Trusted Computing Base. Evaluation on four implemented executors shows verification latency of 39--42 us, full plan cycle under 400 us, runtime overhead under 0.4% of a 100 ms HTTP request, and zero determinism divergences across repeated invocations.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。