形式化验证（安全模型）
本页跟踪 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 之外可能使远程入侵成为可能 / 增加暴露；令牌/密码可以阻止未认证的攻击者（根据模型假设）。 ...