形式化验证（安全模型）

本页追踪 OpenClaw 的形式化安全模型（目前用 TLA+/TLC；有需要会扩展）。

注意：部分旧链接可能使用之前的项目名。

终极目标： 提供机器检查的论证，证明 OpenClaw 在显式假设下执行了预期的安全策略（授权、会话隔离、工具门控和错误配置安全）。

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

每个声明都有一个在有限状态空间上的可运行模型检查。
许多声明还配有一个反例模型，能为一类现实的 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 错误配置

声明： 在非 loopback 上绑定但没有认证会让远程攻击成为可能 / 增加暴露面；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) node 命令允许列表加声明的命令，以及 (b) 配置时需要实时审批；审批令牌化以防止重放（在模型中）。

绿色运行：
- 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

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

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

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

路由/会话键隔离

声明： 来自不同对等方的私聊不会合并到同一个会话中，除非显式链接/配置。

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

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

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

配对存储并发/幂等性

声明： 配对存储在交错执行下也应该执行 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

入口轨迹关联/幂等性

声明： 消息摄入应该在扇出过程中保持轨迹关联，并在提供商重试下保持幂等性。

含义：

当一个外部事件变成多条内部消息时，每个部分保持相同的轨迹/事件标识。
重试不应导致重复处理。
如果提供商事件 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

路由 dmScope 优先级 + identityLinks

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

含义：

频道特定的 dmScope 覆盖必须优先于全局默认值。
identityLinks 应该只在显式链接的组内合并，不跨无关对等方。
绿色：
- make routing-precedence
- make routing-identitylinks
红色（预期的）：
- make routing-precedence-negative
- make routing-identitylinks-negative