《Electronics》：Zero-Override Architecture: Formally Verified Process Flow Integrity for Security Control Enforcement in Payment Systems
编辑推荐：
金融信息系统在人工覆盖（override）绕过安全控制时，仍面临流程完整性（process flow integrity）被突破的脆弱性，此类突破利用身份认证与工作流执行之间的间隙。研究人员提出零覆盖架构（Zero-Override Architecture,
金融信息系统在人工覆盖（override）绕过安全控制时，仍面临流程完整性（process flow integrity）被突破的脆弱性，此类突破利用身份认证与工作流执行之间的间隙。研究人员提出零覆盖架构（Zero-Override Architecture, ZOA），一种从结构上阻止验证机制被绕过的框架。通过形式化威胁建模分析既有架构弱点，识别合规缺口，推导防篡改支付处理的设计需求。所提架构实现密码学 attested 验证链，每个处理组件在推进交易前须出示所有前置控制已执行的证明。状态转移模型（含异常处理工作流）在 TLA+ 中形式化，其完备性、不可绕过性、重放抵抗性与失效安全（fail-secure）性质由 TLC 模型检查器针对能绕开组件与重放 attestation 的显式敌手穷举验证。两个刻意弱化的基线（含人工覆盖能力与以异常审批替代控制执行）被机械导出的绕过反例驳斥。组件消融（ablation）识别出性质所依赖的验证组件。本研究区分流程完整性与软件级控制流完整性（Control-Flow Integrity, CFI），将其确立为独立安全属性，提供带形式化状态转移规范的参考架构，通过显式控制到需求映射建立监管需求可追溯性，并给出跨金融信息系统的评估框架。
研究背景与动机
现代银行依赖金融信息系统协调操作并满足扩张的监管要求，但交易处理路径仍可被特权用户或恶意内部人员通过人工覆盖绕过反洗钱/打击恐怖主义融资（AML/CTF）筛查、交易监控与欺诈检测等强制控制，造成监管违规与非法交易处理。既有缓解手段如基于角色的访问控制（RBAC）、强客户认证（SCA）与检测型方案只治标不治本：RBAC不约束流程顺序与完备性，SCA不保证已认证用户走完所有步骤，检测方案无法在结构上预防。PSD2、GDPR、数字运营韧性法案（DORA）等设定了基线却未规定如何架构性地强制执行工作流完备性。与此同时，流程完整性不同于 Abadi 等人提出的二进制级控制流完整性（CFI），前者处在业务过程与系统架构层。现有供应链安全中的 in-toto 等 attested 步链机制未被移植到连续、失效安全、受监管绑定的交易处理场景。论文发表于《Electronics》，定位于填补上述研究空白。
关键技术方法
研究人员采用复合方法论：以 STRIDE 威胁建模识别四类流程完整性威胁（管理特权滥用、组件绕行、状态篡改、证据操纵）；用攻击树分析层次化攻击路径并依 NIST SP 800-30 定性评险；将状态转移模型形式化为六组件架构（安全交易发起器 STI、控制编排引擎 COE、合规验证模块 CVM、交易处理引擎 TPE、安全支付连接器 SPC、不可变审计子系统 IAS），在 TLA+ 中以配置模型（状态向量、attestation 映射、可用性映射）刻画，并用 TLC 模型检查器在含显式敌手（可直投下游组件、跨交易重放真实 attestation、令组件永久不可用）的有界模型上穷举验证完备性、不可绕过性、排序不变式、失效安全与重放抵抗性；设两个弱化负对照（信任路由状态+人工覆盖、异常审批替代控制执行）以证性质可判别；做组件级消融移除各组件验证以定位负载点；以专家判定将架构控制映射到 PSD2/GDPR/DORA/AML 要求。无生物试剂与样本队列，故不涉及。
研究结果
引言部分界定流程完整性并列为独立于 CFI 的属性，列出来源问题。
相关工作中比对 BIAN、微服务迁移、Van der Aalst 工作流 soundness、Ly 等 LTL 运行时合规、Abadi 的 CFI、in-toto 供应链布局+attestation+终端验证三差异（连续验证、失效安全异常语义、控制布局绑定监管），指出区块链方案不防初始处理绕过。
所提方法章给出设计原则（纵深防御、最小特权、职责分离、不可抵赖、失效安全、完全中介），形式需求 FR/NFR/CR，STRIDE 威胁类别，信任模型含可信计算基（组件可执行完整性、attestation 密钥留 HSM、COE 规则集签名多方可控、IAS 追加仅附），敌手可绕路由不可伪签；部署前提（凭证仅 SPC 持、出网仅 SPC、遗留接口退役、运维工具经 STI）为边界义务非架构内性质。
架构框架章描六组件与四交互模式（验证链、双层授权、异常工作流替代覆盖、状态转移控制），形式化元组与配置模型，给出性质1完备性（Completed 态 attestation 集合按类型与交易绑定计数等于强制控制数）、性质2不可绕过性、性质3失效安全（组件不可用则无推进转移，弱公平超时达终态）、性质4重放抵抗（attestation 绑交易标识、时间戳、组件身份、信封签名），另列排序安全不变式与异常健全性。
模型验证章中攻击树三目标（覆盖 AML/制裁、直连支付网、无痕篡改）显示参考数操纵为最高残险；STRIDE 表残留 Tampering 于组件间流、Spoofing/EoP 于信任边界；复合风险表 CVM 最高因参考数经合法管理渠道；控制有效性表验证链与密码 attestation 为 High。形式验证 R1 两交易 17391 态全量保性质，R2 启故障 1107072 态保失效安全，R5/R6 扩模型保异常健全；R3 基线十步反例（步骤6 ManualOverride 跳 CVM 无 attestation 至步骤10 Completed）驳斥；R7/R8 证异常审批替执行仅在信任路由基线可破 ZOA 不可破；消融表显去除 CVM/TPE/SPC 验证两转移内违序或破完备，去 STI 验证在扩敌手后两转移内违序，COE 与异常审查者验证非负载点。证明草图以 Inv(t) 归纳证排序与完备不依赖并发数，活性依赖超时弱公平，消息丢失/重投被吸收，局部部分提交不在模型。
讨论与结论翻译
讨论指出 ZOA 将覆盖问题从程序性要求升为架构强制，参考数操纵为最高残险提示流程完整性须涵盖控制所依数据完整性；局限含未做实现级渗透、不覆盖基础设施攻击、密钥托管假设、参考数完整性缺口、无经验性能数、定性评险单作者、可追溯非合规、部署前提为外部义务、attestation 未绑规则集版本。未来工作指向参考实现测代价、参考数密码绑外部源、attestation 绑规则集版本、TLA+ 证明系统化归纳、模型到实现精化、跨域移植、FIDO2/WebAuthn 接入 STI。
结论部分译文：本文提出零覆盖架构（ZOA），一种通过结构上阻止强制控制被绕过以保障金融信息系统流程完整性的框架：每个处理组件须呈验所有前置控制已执行的密码学证明方可推进交易。研究人员通过形式化威胁建模、TLA+ 状态转移规范与 TLC 穷举验证（含显式敌手与弱化负对照反例）表明，该架构在可达状态空间内满足完备性、不可绕过性、重放抵抗性与失效安全，并将流程完整性确立为异于二进制级 CFI 的独立安全属性。组件消融进一步定位 CVM、TPE 与 SPC 验证为负载点。控制到 PSD2/GDPR/DORA/AML 的显式映射提供监管可追溯性。该研究为支付系统给出可机械验证的参考架构与评估框架。
