「秘密が漏れない」を Lean で証明して CI ゲートにした Rust CLI のリリースパイプライン

「テストが緑」で満足できなかった理由

エージェントに本物の API キーを渡さずに動かす CLI ツールを開発している。守りたい性質はシンプルで、子プロセスに本物の鍵を渡さないこと。ここが崩れれば、このツールを使う意味はない。

ただ、テストが通っているだけでは確認として物足りなかった。テストが言えるのは「この入力では問題ない」までで、「どんな入力でも問題ない」ではない。鍵を扱う以上、その差は無視できない。

そこで Lean で証明を書き、CI でビルドするようにした。手間はかかるが、扱うものを考えれば妥当な投資だと思う。この記事では、そのときに組んだ CI/CD を抜粋して紹介する。プロジェクト固有の内部名は伏せ、設計と仕組みのところだけを残した。

数字で見た中身

地味だが効いているのが、sorry（証明の穴埋めサボり）と axiom（無証明の仮定）が両方とも 0 という点だ。核の不変条件を仮定でごまかさず最後まで証明している、ということで、これが CI を緑にする条件に入っている。

CI は三層に分けている

┌─────────────────────────────────────────────┐
│ 1. 形式検証（核）                              │
│    「子プロセスは本物の鍵を受け取らない」を     │
│    Lean で証明 — 定理28 / sorry・axiom 0       │
├─────────────────────────────────────────────┤
│ 2. 安全不変条件ゲート × 11                      │
│    deny-before-inject / DNS guard /          │
│    audit boundary / secret-type … を          │
│    1条件＝1ゲートで機械チェック                 │
├─────────────────────────────────────────────┤
│ 3. 汎用品質 + サプライチェーン                  │
│    fmt / clippy -D warnings / test /          │
│    cargo-deny（advisories, bans, sources）    │
└─────────────────────────────────────────────┘

1. 核は Lean で証明して、CI でビルドする

「子プロセスは本物の鍵を受け取らない」という核の性質は、formal/lean に証明として置いている。定理と補題で28本、うち sorry も axiom も無し。CI は毎回この証明をビルドして、サボりや無証明の仮定なしで通ることを確かめる。

たとえば核の定理はこんな形だ。「本物の秘密をサニタイズした結果が、子プロセスに渡る値になることはあり得ない」を型で言い切っている。

theorem real_secret_is_not_sanitized_to_child
    {secret : Secret} {child : ChildValue} :
    sanitizeValue (InternalValue.realSecret secret) ≠ some child := by
  intro impossible
  cases impossible

拒否側も同じように証明してある（denied_request_never_calls_injector。拒否した要求は injector を呼ばない、というやつだ）。テストが「この入力では大丈夫」しか言えないのに対して、こうした定理は「どの入力でも大丈夫」を言う。その一歩ぶんを CI に肩代わりさせている。

2. 残りは「1条件＝1ゲート」にする

証明まで持っていけない運用上の条件は、ひとつずつ独立した check スクリプトにして CI のステップに並べている。全部で11本。巨大なテストにまとめないのは、壊れたときにどの条件が落ちたのかをステップ名でそのまま読みたいからだ。

どれかの条件を崩す変更が入れば、その場で該当ゲートが赤くなる。

漏洩スモーク：出力に秘密が出てこないか確かめる

セキュリティツールで個人的に一番こわいのが、ログや診断出力からうっかり秘密が漏れる事故だ。なので、ダミーの秘密を環境変数に入れて診断コマンドを走らせ、その出力にダミー値が出てこないことを CI で確かめている。やっていることは泥臭いが、その分はっきりしている（変数名とツール名だけ一般化、ロジックは実物に近い）。

- name: doctor json smoke
  env:
    SECRET_KEY: ci-dummy-secret
  run: |
    output="$(mktemp)"
    cargo run --quiet --bin <tool> -- doctor --json > "$output"
    # 1) 出力にダミー秘密が現れたら即失敗
    if grep -q "ci-dummy-secret" "$output"; then
      echo "secret leaked into doctor output" >&2
      exit 1
    fi
    # 2) 診断の fail 件数が 0 であること
    test "$(jq '.summary.fail' "$output")" -eq 0

「秘密を入れて、出てこないことを見る」だけのテストだが、現実に起きうる漏れ方をひとつ確実に塞いでくれる。

サプライチェーンと多 OS

依存まわりは cargo-deny に任せていて、脆弱性 advisory・禁止クレート・ソースの素性をまとめて見ている。ビルドは Linux を主に回し、Windows と macOS のスモークは普段は走らせず、必要なときだけ workflow_dispatch で手動起動している。毎回フル matrix を回すほどではない、という割り切りだ。

リリース：5ターゲットを matrix で組んでチェックサムを付ける

リリースはタグ push（v*）で走る。Linux（x86_64 / aarch64）・macOS（x86_64 / aarch64）・Windows（x86_64）の5ターゲットを matrix でビルドする。Linux の aarch64 だけ cross でクロスコンパイルしていて、macOS の arm64 は通常ビルドだ。

ビルド後は Unix バイナリを strip し、出来たアーカイブ（tar.gz / zip）にバイナリとライセンスがちゃんと入っているかをスモークで確認する。最後に全ターゲットを集めて sha256sum で SHA256SUMS を作って添付する。配布物の中身を機械的に見てから出すので、ライセンスの入れ忘れや片方のプラットフォーム欠けに後から気づく、ということが起きにくい。

公開：確認フレーズを通さないと出ない

開発はプライベートリポジトリでやっていて、公開リポジトリへは専用の publish ワークフローを手で叩いたときだけ反映する。誤って出さないように、手順をこう縛っている。

1. 実行時に確認フレーズの入力を必須にする（合わなければそこで止まる）
2. 公開許可リスト（allowlist）に載ったファイルだけを staging tree へコピーする
3. staging の中で内部コメントを落とす（ドキュメントコメントは残す）
4. staging に対して Trivy とテストを走らせる
5. 通った staging tree だけを公開リポジトリへ反映する

「private で開発して、検査を通った部分だけ public に出す」をパイプライン側で強制している。これがあると、未公開のコードや内部メモがうっかり公開側に混ざる、という事故が仕組みで防げる。

まとめ

結局のところ、セキュリティツールの CI/CD は「動く」を見る場所というより、「壊れていないか」を毎回確かめる場所だと思っている。核の不変条件は Lean に任せ、それ以外の運用条件はゲートで一つずつ見る、という分担にした。

真似するなら、ここから

Lean の証明は正直そのまま真似するには敷居が高い。でも、効いている部分はもっと安く取り入れられる。

• 1条件＝1ゲート：守りたい条件をひとつずつ独立した check スクリプトにするだけ。落ちたときにどこが壊れたか分かる。
• 漏洩スモーク：ダミー秘密を入れて grep で出てこないことを見る、数行のテスト。Lean が無くても今日から足せる。

「テストが緑」の先に、「この条件が崩れたら CI を赤くする」を一つずつ積んでいく。それだけでも、パイプラインの安心感はだいぶ変わる。

形式検証を組み込んだ CI/CD の設計、サプライチェーン対策、Rust のリリースまわりの整備など、このあたりが要る案件があれば Services からどうぞ。