証明器と検証機の配置

以降の設計判断は、この前提のもとで初めて成立します。前提が変われば、要求水準も畳み方も変わります。まずここに合意してから読み進めてください。

想定する攻撃者

実行体を完全に奪取できる攻撃者。外部 API の応答やユーザー入力を細工でき、実行体上のプロセス・ファイル・メモリに任意のアクセス権を持つ。ネットワーク経路の盗聴・書換は前提しません（TLS が健全な範囲で成立）。

達成したい性質

過去に確定した実行結果と監査ログを、事後に 改竄・偽造・削除できないこと。改竄を防ぐのではなく、改竄を検知不能にはできないことを最低ラインとします。合わせて、隔離／仕様適合／再現性の3つを、それぞれ独立に検証可能な状態に保つこと。

対象外

HSM／TPM 自体の物理侵害、鍵保管者の共謀、サプライチェーン全域の敵対的改変（それらは別途のサプライチェーン施策の領分）。国家アクター相当の攻撃能力も想定しません。ここを守る必要がある構成では、以降の推奨は下限として読み、追加の層を積む前提になります。

台数を決める前に、それぞれがいつ効くのかを揃えて見ます。ここを混ぜると、マシンだけ増えて保証は増えないという典型的な失敗になります。

スペックはワークロードで動きます。以下は「どの桁を見ておけばいいか」の目安として読んでください。

入力を秘匿したまま、ログを見られない第三者に納得させる必要が実在するか？

4つ同時に立ち上げると高くつきます。効き目の順に積むなら、こうなります。

1. 署名機を切り出す 最も安く、最も効きます。鍵を実行体の外に出すだけで改ざん耐性が立ちます。同時に seq と ts を署名対象に組み込み、鍵ローテーション運用も初日から回すこと。後付けは面倒です。
2. 実行体を隔離する これが無いと他の3つの保証が全部無意味になる前提条件です。1 より効果が大きいわけではなく、1 の成立条件として要ります。
3. 再現検証を回す 実バグの検出率が一番高い層です。監査目的よりデバッグ目的で元が取れます。この段階で成果物署名（ダイジェスト固定）が要件になります。
4. 形式検証を、対象を絞って入れる 最後で構いません。軽層（プロパティテスト・ファジング）はここまでに常時回っている想定で、重層（SMT・定理証明）をコアに限定して足す段階です。範囲を絞らずに入れると、費用だけが先に立ちます。

• 実行体は自身の出力に署名できない
• 署名対象には seq（単調カウンタ）と ts（時刻）を含める
• 検証機と監査ログは、実行体から書き込み到達不能である
• 監査ログは追記のみ。削除・更新の口を持たない
• 再現用イメージは、実行体が改変できないレジストリからダイジェスト固定で引く
• 権威的な検証を行うコードは、実行体と同じデプロイ単位に入らない（予備検証は同居可）
• 署名機の健全性は、信頼領域の外から attestation 等で検証できる

この7つは装飾ではなく定義です。1つでも崩れると、対応する保証は「弱くなる」のではなく形式的に消えます。マシンを何台並べても復活しません。

verify_audit_chain／lens_verify／d8_verdict_*／constitutional_check は、すでに検証側の役割を持っています。問題は台数ではなく、これらがコネクタ実行と同じホスト上にあるなら分離が名目に留まる、という点です。機材を足す前に、次の5つを確認してください。

• 署名鍵は、実行体と同じプロセス・ホスト・権限のどれかを共有していないか？ 1つでも共有していれば、改ざん耐性は現時点で成立していません。ここが最初の一手です。
• 署名対象に seq と ts が入っているか？ 入っていなければ、実行体を取った相手は過去ハッシュを再署名させて任意時点の履歴を偽造できます。件数単位の署名では止められません。
• 監査ログに対して、実行体は追記以外の操作ができないか？ 削除・truncate・ローテーション設定の変更まで含めて確認してください。追記専用は設定ではなく権限で担保します。
• 再現用イメージの取得元を、実行体が変更できないか？ タグを動かせるだけでも再現性は失われます。ダイジェスト固定であることまで見ます。
• 署名機の健全性を、実行体の外から確認する経路があるか？ TPM attestation または HSM の外部監査ログを想定。無い場合、ルートの健全性は自己申告で、脅威モデルの想定攻撃者に対して防御が閉じません。