形式化验证（Formal Verification）

OpenClaw 使用 TLA+/TLC 对最高风险路径进行机器检查的安全模型验证。

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

当前状态：可执行的、攻击者驱动的安全回归套件，每个声明都有有限状态空间上的可运行模型检查，以及配对的负面模型（产生反例 trace）。

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

模型仓库

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models
# 需要 Java 11+（TLC 运行在 JVM 上）
make <target>

声明：绑定到非 loopback 且无认证会增加远程妥协风险；token/password 阻断未认证攻击者。

make gateway-exposure-v2          # 绿色（通过）
make gateway-exposure-v2-negative # 红色（预期反例）

声明：exec host=node 需要节点命令 allowlist + 声明命令 + 实时审批（配置时）；审批令牌化防止重放。

make nodes-pipeline          # 绿色
make approvals-token         # 绿色
make nodes-pipeline-negative # 红色（预期）

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

make pairing      # 绿色
make pairing-cap  # 绿色

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

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