ソフトウェアの脆弱性を数学で形式化する：∀x S(P(x)) から形式検証まで

「脆弱性がない」を数学の言葉で書く

「このソフトウェアには脆弱性がありません」という主張は、日常語のままだと検証できません。 どんな入力を想定しているのか、「安全」とは何を指すのかが曖昧だからです。そこで、 プログラムと入力と安全性を記号で定義し、主張を論理式として書き下します。 これが形式化(formalization)です。

まず記号を決めます。

Σ      : 入力に使える記号(バイト)の集合
Σ*     : Σ の記号を有限個並べた列すべての集合(=ありうる全入力)
P      : 検証対象のプログラム
P(x)   : 入力 x を与えたときの P の実行結果
S(·)   : 実行結果が「安全」であることを表す述語

すると「すべての入力に対して安全」は次のように書けます。

∀x ∈ Σ*,  S(P(x))

読み方は「Σ* に属するどんな入力 x を与えても、P(x) は安全である」。 ポイントは ∀(すべての)が無限集合 Σ* 全体にかかっていることです。 テストで何万件の入力を試しても、それは Σ* のごく一部を調べたにすぎません。

脆弱性の「存在」と「非存在」

脆弱性判定関数 V(P, x) を、入力 x によって P が危険な状態に陥るなら 1、 そうでなければ 0 を返すものとします。すると、2つの主張は次のように対になります。

脆弱性が存在する     :  ∃x  V(P, x) = 1
脆弱性が存在しない   :  ∀x  V(P, x) = 0

この2つは互いの否定です(¬∃x φ ≡ ∀x ¬φ)。しかし、示すための労力はまったく違います。

• 存在の証明は、条件を満たす x を1つ見つければ終わります。ファジングやペネトレーションテストが得意とするのはこちらです。
• 非存在の証明は、無限にある x のすべてについて成り立つことを示す必要があります。テストを積み重ねるだけでは原理的に到達できません。

「テストはバグの存在を示せるが、不在は示せない」というダイクストラの有名な指摘は、 まさにこの量化子の非対称性を言い表しています。

出力だけでなく「途中経過」も見る: 実行トレース

最終的な出力が正しくても、実行の途中でバッファの範囲外を読んだり、権限のない領域に 触れたりしていれば、それは脆弱性です。そこで、実行を状態の列(トレース)として扱います。

Traces(P, x) : 入力 x に対する P のありうる実行トレースの集合
τ = s₀ s₁ s₂ …  : トレース(状態の列)
Safe         : 安全な状態の集合

∀x ∀τ ∈ Traces(P, x) ∀s ∈ τ,  s ∈ Safe

「どの入力でも、どの実行経路でも、途中のどの状態も安全な状態に含まれる」という意味です。 Traces が集合になっているのは、スレッドのスケジューリングや外部からの割り込みなどで、 同じ入力でも実行経路が複数ありうるためです。このような「悪いことは決して起きない」型の性質は 安全性(safety)プロパティと呼ばれます。

攻撃者が探すもの: ∃x ¬Safe(P, x)

上の安全性の主張を否定すると、攻撃者(あるいは脆弱性診断者)が探しているものになります。

¬(∀x Safe(P, x))  ≡  ∃x ¬Safe(P, x)

つまり攻撃とは、安全性の反例を1つ見つけることです。防御側は ∀ を守り切る必要があり、 攻撃側は ∃ を1つ見つければよい。セキュリティが「攻撃側有利」と言われる構造が、 論理式の形そのものに現れています。逆に言えば、形式検証の道具が反例を返してきたとき、 それは「その入力が実際に危険な状態を引き起こす」という具体的な証拠になります。

形式化と証明は別物

ここまでで行ったのは形式化、つまり主張を曖昧さのない論理式に書き直すことです。 書けたからといって、その式が真であると証明できたわけではありません。

これは「形式検証は無意味」という意味ではありません。現実の手法は、この壁を次のいずれかの方法で迂回しています。

• 対象を有限の状態に制限する(有限状態なら全探索できる)
• 入力長やループ回数に上限を置く(有界検証)
• 近似を許す(「安全」と言えないものは警告として残す)
• 人間が証明の方針(ループ不変条件など)を与える

主要な手法

ホーア論理

プログラムの各部分について、実行前の条件と実行後の条件の関係を記述・証明する体系です。

{ Pre }  C  { Post }
「Pre が成り立つ状態で C を実行し、停止したなら、Post が成り立つ」

例: 配列アクセスの安全性
{ 0 ≤ i ∧ i < len(a) }  y := a[i]  { y = a[i] }

ループには「毎回の反復の前後で保たれる性質」(ループ不変条件)を人間が与える必要があり、 ここが自動化の難所になります。

モデル検査

システムを有限の状態遷移系 M としてモデル化し、性質 φ(時相論理で書く)を満たすかどうかを 状態空間の網羅探索で判定します。

M ⊨ □ Safe      (□ は「常に」: すべての到達可能な状態で Safe)

満たさない場合は、違反に至る具体的な実行列(反例)を出力してくれるのが大きな利点です。 一方で、変数が増えると状態数が爆発的に増える「状態爆発」が最大の課題です。

SAT / SMT ソルバ

プログラムの実行経路と「危険な状態に到達する」という条件を1つの論理式にまとめ、 それを満たす変数の割り当てがあるかをソルバに解かせます。

φ = Path(P, x) ∧ ¬Safe
φ が充足可能 (SAT)   → 充足する x が脆弱性を引き起こす入力
φ が充足不能 (UNSAT) → (調べた範囲で)その経路に脆弱性はない

SMT は SAT に整数・配列・ビットベクタなどの理論を加えたもので、記号実行や有界モデル検査の エンジンとして広く使われています。

定理証明

Coq(Rocq)・Isabelle・Lean などの証明支援系で、プログラムとその仕様を記述し、 ∀x S(P(x)) を人間と機械が協力して証明します。最も強い保証が得られる一方、 コストも最も大きい手法です。形式検証済み OS カーネル seL4 や、検証済み C コンパイラ CompCert が代表例です。

抽象解釈

具体的な値の代わりに、値の範囲や符号などの「抽象的な値」で計算し、ありうる状態をすべて 過大近似します。

具体的な到達状態 ⊆ 抽象的な到達状態 γ(A)
γ(A) ⊆ Safe  ならば  具体的な到達状態 ⊆ Safe  (健全)

過大近似なので「安全」と判定されたものは本当に安全(健全性)ですが、 実際には安全なのに警告が出る誤検知は避けられません。 停止性問題の壁に対して「必ず止まる代わりに正確さを一部手放す」という選択をした手法です。

脆弱性の種類ごとに式が変わる

「Safe」の中身は、どの種類の脆弱性を扱うかで大きく変わります。代表的なものを並べます。

メモリ安全性 (バッファオーバーフロー等)	∀ アクセス a[i] : 0 ≤ i < len(a) すべての配列・ポインタアクセスが確保した範囲内に収まる。トレース上の各状態の性質として書ける。
整数オーバーフロー	∀ 演算 a + b : MIN ≤ a + b ≤ MAX 数学上の整数とマシン上の固定幅整数の結果が一致する。
インジェクション (SQL・コマンド等)	∀x : parse(query(x)) の構造 = 開発者が意図した構造 入力が「データ」の位置にとどまり、「命令」の構造を変えない。テイント(汚染)解析で扱うことが多い。
情報漏洩 (機密性)	∀ s₁, s₂ : low(s₁) = low(s₂) ⇒ obs(P, s₁) = obs(P, s₂) 秘密の値だけが異なる2つの実行で、外から観測できる結果が同じ。2つの実行を比べるハイパープロパティで、単一のトレースの性質としては書けない。
サイドチャネル (タイミング等)	∀ secret₁, secret₂ : time(P, secret₁) = time(P, secret₂) 実行時間が秘密の値に依存しない(定数時間実装)。これもハイパープロパティ。
サービス妨害 (DoS)	∀x : cost(P, x) ≤ f(|x|) 計算量が入力長に対して想定内に収まる。悪いことが「いつか終わる」ことを求める活性(liveness)寄りの性質。
認可・アクセス制御	∀ 操作 op, 主体 u : perform(u, op) ⇒ allowed(u, op) 実行されたすべての操作が、ポリシー上許可されたものである。

同じ「脆弱性がない」でも、1回の実行の各状態を見れば済むもの、2回の実行を比べる必要があるもの、 無限の実行を考える必要があるものと、論理的な形がまったく違います。どの道具が使えるかは、 この形で決まります。

実務での使いどころ

• 暗号ライブラリ・カーネル・ハイパーバイザなど、小さく重要で長く使われる部品には定理証明や SMT による検証が見合う
• アプリケーション全体には、抽象解釈ベースの静的解析とファジングを組み合わせ、「健全な警告」と「具体的な反例」の両面から攻める
• プロトコルや状態機械(認証フローなど)はモデル検査と相性がよい
• まず「何を Safe と呼ぶか」を式で書くこと自体が、仕様の穴を見つける最も安価な手段になる

まとめ

• 「すべての入力で安全」は ∀x ∈ Σ*, S(P(x)) と形式化でき、途中経過まで含めるならトレースで書く
• 脆弱性の存在(∃)は反例1つで示せるが、非存在(∀)はテストだけでは示せない
• 攻撃とは ∃x ¬Safe(P, x) の x を探すこと
• 形式化と証明は別物で、一般の証明は停止性問題・ライスの定理により決定不能
• ホーア論理・モデル検査・SAT/SMT・定理証明・抽象解釈は、それぞれ別の方法でこの壁を迂回している
• 脆弱性の種類によって、安全性・ハイパープロパティ・活性と、式の形そのものが変わる

実在の有名な脆弱性が、ここで書いた式のどれに違反していたのかは 「CVEとは？Log4Shell・Heartbleed・EternalBlue・XZ Utilsで学ぶ」で解説しています。