形式化验证（安全模型）

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

注意：一些旧链接可能还在用之前的项目名。

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

现状（今天）： 一个可执行的、攻击者驱动的安全回归测试套件：

  • 每个声明都有一个可运行的模型检查，覆盖有限状态空间。
  • 许多声明都配有一个负面模型，能为真实的 bug 类型生成反例追踪。

这不是什么（暂时）： 不是证明”OpenClaw 在所有方面都安全”，也不是证明完整的 TypeScript 实现是正确的。

模型在哪里

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

重要说明

  • 这些是模型，不是完整的 TypeScript 实现。模型和代码之间可能存在偏差。
  • 结果受 TLC 探索的状态空间限制；“绿色”不代表超出模型假设和边界之外的安全性。
  • 有些声明依赖明确的环境假设（比如正确的部署、正确的配置输入）。

复现结果

目前，你可以通过克隆模型仓库到本地并运行 TLC 来复现结果（见下文）。未来可能会提供：

  • CI 运行的模型，带公开产物（反例追踪、运行日志）
  • 托管的”运行这个模型”工作流，用于小型、有界的检查

开始使用：

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

# 需要 Java 11+（TLC 运行在 JVM 上）。
# 仓库内置了固定版本的 `tla2tools.jar`（TLA+ 工具），并提供 `bin/tlc` + Make 目标。

make <target>

Gateway 暴露和开放 Gateway 误配置

声明： 绑定到非本地回环地址且没有认证，可能导致远程攻击 / 增加暴露面；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) 配置时的实时审批；审批被令牌化以防止重放（在模型中）。

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

Pairing 存储（DM 门控）

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

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

Ingress 门控（提及 + 控制命令绕过）

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

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

Routing/session-key 隔离

声明： 来自不同对等方的 DM 不会合并到同一个 Session，除非明确链接/配置。

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

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

这些是后续模型，围绕真实世界的故障模式（非原子更新、重试和消息扇出）提高保真度。

Pairing 存储并发 / 幂等性

声明： Pairing 存储应该在交错情况下强制执行 MaxPending 和幂等性（即”检查后写入”必须是原子的 / 加锁的；刷新不应创建重复项）。

这意味着：

  • 在并发请求下，你不能超过 Channel 的 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

Ingress 追踪关联 / 幂等性

声明： 摄入应该在扇出过程中保持追踪关联，并在提供商重试时保持幂等性。

这意味着：

  • 当一个外部事件变成多个内部消息时，每个部分都保持相同的追踪/事件身份。

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

  • 如果提供商事件 ID 缺失，去重会回退到安全键（比如追踪 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

Routing dmScope 优先级 + identityLinks

声明： Routing 必须默认保持 DM Session 隔离，只有在明确配置时才合并 Session（Channel 优先级 + 身份链接）。

这意味着：

  • Channel 特定的 dmScope 覆盖必须优先于全局默认值。

  • identityLinks 应该只在明确链接的组内合并，而不是跨不相关的对等方。

  • 绿色：

    • make routing-precedence
    • make routing-identitylinks

  • 红色（预期）：

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