形式化验证（安全模型）

本页面跟踪 OpenClaw 的形式化安全模型（目前使用 TLA+/TLC，后续按需扩展）。

注意：部分旧链接可能引用旧版项目名称。

目标（北极星）： 提供一个机器验证的论证，证明 OpenClaw 在明确假设下执行其预期的安全策略（授权、会话隔离、工具门控和错误配置安全）。

当前状态： 一套可执行的、以攻击者视角驱动的安全回归测试套件：

• 每条声明都有一个在有限状态空间上可运行的模型验证。
• 许多声明配有反例模型，可为现实 bug 类别生成反例 trace。

尚未实现的： 证明"OpenClaw 在所有方面都是安全的"，或完整 TypeScript 实现的正确性证明。

模型存放位置

模型维护在独立仓库：vignesh07/openclaw-formal-models。

重要说明

• 这些是模型，不是完整的 TypeScript 实现。模型与代码之间可能存在偏差。
• 结果受限于 TLC 探索的状态空间；"绿灯"并不意味着超出建模假设和边界范围之外的安全性。
• 部分声明依赖于明确的环境假设（如正确的部署、正确的配置输入）。

复现结果

目前，在本地克隆模型仓库并运行 TLC 即可复现结果（见下文）。未来迭代可提供：

• 带公共构件的 CI 运行模型（反例 trace、运行日志）
• 针对小型有界检查的托管"运行此模型"工作流

快速开始：

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# 需要 Java 11+（TLC 运行在 JVM 上）
# 仓库内置了固定版本的 tla2tools.jar 和 bin/tlc + Make targets

make <target>

网关暴露与开放网关错误配置

声明： 绑定到非回环地址且无认证可能导致远程入侵/增大暴露面；token/密码可阻止未授权攻击者（基于模型假设）。

• 绿灯运行：
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• 红灯（预期）：
  • make gateway-exposure-v2-negative

另见模型仓库中的 docs/gateway-exposure-matrix.md。

Nodes.run 管道（最高风险能力）

声明： nodes.run 需要 (a) 节点命令白名单加上已声明的命令，以及 (b) 配置时的实时审批；审批通过 token 化防止重放（模型中）。

• 绿灯运行：
  • make nodes-pipeline
  • make approvals-token
• 红灯（预期）：
  • make nodes-pipeline-negative
  • make approvals-token-negative

配对存储（DM 门控）

声明： 配对请求遵守 TTL 和待处理请求上限。

• 绿灯运行：
  • make pairing
  • make pairing-cap
• 红灯（预期）：
  • make pairing-negative
  • make pairing-cap-negative

入口门控（@提及 + 控制命令绕过）

声明： 在需要 @提及 的群组上下文中，未授权的"控制命令"无法绕过提及门控。

• 绿灯：
  • make ingress-gating
• 红灯（预期）：
  • make ingress-gating-negative

路由/会话密钥隔离

声明： 不同对等方的 DM 不会合并为同一会话，除非明确链接/配置。

• 绿灯：
  • make routing-isolation
• 红灯（预期）：
  • make routing-isolation-negative

v1++：额外的有界模型（并发、重试、trace 正确性）

这些是跟进模型，围绕现实故障模式（非原子更新、重试和消息扇出）收紧仿真精度。

配对存储并发/幂等性

声明： 即使在交错操作下，配对存储也应强制执行 MaxPending 和幂等性（"检查-然后-写入"必须是原子/加锁的；刷新不应创建重复项）。

含义：

• 在并发请求下，同一频道不能超过 MaxPending。

• 对同一 (channel, sender) 的重复请求/刷新不应创建重复的待处理行。

• 绿灯运行：

  • make pairing-race（原子/加锁上限检查）
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• 红灯（预期）：

  • make pairing-race-negative（非原子的 begin/commit 上限竞争）
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

入口 trace 关联/幂等性

声明： 摄取应在扇出中保持 trace 关联，并在提供商重试时保持幂等性。

含义：

• 当一个外部事件变成多条内部消息时，每个部分保持相同的 trace/事件标识。

• 重试不会导致重复处理。

• 如果提供商事件 ID 缺失，去重回退到安全键（如 trace ID），避免丢弃不同事件。

• 绿灯：

  • make ingress-trace
  • make ingress-trace2
  • make ingress-idempotency
  • make ingress-dedupe-fallback

• 红灯（预期）：

  • make ingress-trace-negative
  • make ingress-trace2-negative
  • make ingress-idempotency-negative
  • make ingress-dedupe-fallback-negative

路由 dmScope 优先级 + identityLinks

声明： 路由必须默认保持 DM 会话隔离，仅在明确配置时才合并会话（频道优先级 + 身份链接）。

含义：

• 频道特定的 dmScope 覆盖必须胜过全局默认值。

• identityLinks 仅应在明确的链接组内折叠，而不应跨不相关的对等方。

• 绿灯：

  • make routing-precedence
  • make routing-identitylinks

• 红灯（预期）：

  • make routing-precedence-negative
  • make routing-identitylinks-negative