文档
形式化验证（安全模型）

形式化验证（安全模型）

形式化验证（安全模型）

本页面跟踪 Moltbot 的形式化安全模型（今天是 TLA+/TLC；根据需要添加更多）。

注意：一些较旧的链接可能指的是以前的项目名称。

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

这是什么（今天）：一个可执行的、攻击者驱动的安全回归套件：

  • 每个声明都在有限状态空间上有一个可运行的模型检查。
  • 许多声明都有一个配对的负面模型，它为现实的错误类生成反例跟踪。

**这不是什么（尚未）：**证明"Moltbot 在所有方面都是安全的"或完整的 TypeScript 实现是正确的。

模型所在位置

模型在一个单独的仓库中维护：vignesh07/moltbot-formal-models。

重要警告

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

复现结果

今天，通过在本地克隆模型仓库并运行 TLC 来复现结果（见下文）。未来的迭代可以提供：

  • CI 运行模型与公共工件（反例跟踪、运行日志）
  • 托管的"运行此模型"工作流程用于小型、有界检查

入门：

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

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

make <target>

Gateway 暴露和开放网关错误配置

**声明：**绑定到环回之外而没有身份验证可能会使远程妥协成为可能/增加暴露；令牌/密码阻止未经身份验证的攻击者（根据模型假设）。

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

配对存储（私信门控）

**声明：**配对请求尊重 TTL 和待处理请求上限。

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

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

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

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

路由/会话密钥隔离

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

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

v1++：附加有界模型（并发、重试、跟踪正确性）

这些是后续模型，它们围绕真实故障模式（非原子更新、重试和消息扇出）收紧保真度。

配对存储并发/幂等性

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

这意味着：

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

  • 对于相同的 (频道, 发送者) 的重复请求/刷新不应创建重复的活动待处理行。

  • 绿色运行：

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

  • 红色（预期）：

    • make pairing-race-negative（非原子开始/提交上限竞争）
    • 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
消息