答えは「ノー」だ。本当の問いは、代わりに何を証明できるかである。

静的解析は、飛行機が墜落しないことを証明することはできない。しかし、高度計の制御ループが決してゼロ除算を起こさないこと、配列の範囲外を決して参照しないこと、固定小数点アキュムレータが決してオーバーフローしないことは証明できる。この区別が重要なのは、一方は物理、空気力学、そして応力下のアルミニウムに関する主張であり、他方は飛行機が離陸する前に検証できるコードに関する主張だからである。

これが抽象解釈の約束である。全知ではない。あらゆる可能な実行において、特定のカテゴリの壊滅的なソフトウェア障害が不可能であるという、厳密な証明こそがそれである。

百万のシナリオをテストしても、なお不安が残る理由

典型的な飛行制御システムは数十万行のC言語で構成されている。入力空間は、センサー読み取り値、パイロットの操作、環境条件、内部状態変数の直積である。宇宙の熱的死までシミュレータ上で実行し続けても、すべての経路を網羅することはできない。

テストはバグを発見する。不在を証明するわけではない。合格したテストはあくまでデータポイントである。保証ではない。

抽象解釈はこのアプローチを逆転させる。特定の入力でプログラムを実行するのではなく、可能な値の集合を表す抽象ドメイン上でプログラムを実行する。抽象解析がある特定のエラー状態が到達不可能だと示せば、そのエラーはあらゆる具体入力に対して到達不可能である。証明は網羅的であり、なぜなら一度の実行で入力空間全体をカバーするからである。

具体値はコストが高すぎる。代わりに「形」を使おう。

単純な変数 x を考えてみよう。具体実行では、x は 42 である可能性がある。抽象解釈では、x は「0から255までの任意の整数」である可能性がある。これを区間抽象と呼ぶ。

解析器はこれらの区間をすべての操作を通じて追跡する。x が [0, 100] で y が [1, 10] なら、x / y は [0, 100] である。除数の区間にゼロが含まれていないため、解析器は除算が安全だと判断する。

しかし、y が [-5, 5] であれば、解析器は潜在的なゼロ除算を警告する。具体実行がゼロに到達するかどうかはわからない。ただ、ゼロが可能な範囲の内側にあることを知っている。それだけで警報を発するに足る。

1976年にPatrick CousotとRadhia Cousotが示した核心的洞察は、抽象ドメインは具体意味論の健全な過大近似でなければならないということである。すべての具体的振る舞いは抽象化の中で表現可能でなければならない。抽象化が安全なら、具体プログラムも安全である。抽象化が警告を発すれば、具体プログラムは問題ない可能性もある。しかし、そうでない可能性もある。

Pythonでおもちゃの区間解析器を作る

以下は動作する区間抽象ドメインの実装である。素朴なものだが、その仕組みを示している。

from dataclasses import dataclass
from typing import Optional

@dataclass(frozen=True)
class Interval:
    lo: int
    hi: int

    def __post_init__(self):
        if self.lo > self.hi:
            raise ValueError("Empty interval")

    def add(self, other: "Interval") -> "Interval":
        return Interval(self.lo + other.lo, self.hi + other.hi)

    def div(self, other: "Interval") -> Optional["Interval"]:
        if other.lo <= 0 <= other.hi:
            return None  # Potential division by zero
        # Simplified: assumes positive divisor for demo
        return Interval(self.lo // other.hi, self.hi // other.lo)

    def intersect(self, other: "Interval") -> Optional["Interval"]:
        lo = max(self.lo, other.lo)
        hi = min(self.hi, other.hi)
        if lo > hi:
            return None
        return Interval(lo, hi)

    def __repr__(self):
        return f"[{self.lo}, {self.hi}]"


def analyze_division(a: Interval, b: Interval) -> None:
    result = a.div(b)
    if result is None:
        print(f"ALERT: {a} / {b} may divide by zero")
    else:
        print(f"SAFE: {a} / {b} = {result}")

いくつかのケースを実行してみよう：

analyze_division(Interval(10, 20), Interval(2, 5))   # SAFE
analyze_division(Interval(10, 20), Interval(-1, 1))  # ALERT
analyze_division(Interval(10, 20), Interval(0, 5))   # ALERT

最初のケースは安全である。なぜならすべての除数が正だからである。2番目は警告される。ゼロが [-1, 1] の内側にあるからである。3番目も警告される。ゼロが [0, 5] の内側にあるからである。

3番目のケースで何が起きたか注意してほしい。具体プログラムは実際には b = 0 で決して実行されない可能性がある。解析器はそれを知らない。設計上、保守的である。これが根本的なトレードオフである。

偽陽性の代償

健全な静的解析器はバグを見逃さない。クラッシュが可能なら、それを報告する。しかし、不可能なクラッシュも報告する。これらの偽陽性が、健全性の代償である。

実際には、このコストは高い。for (i = 0; i < n; i++) のようなループに対する素朴な区間解析は、n が上限付きであっても、i を [0, +∞] と結論付けることが多い。解析器は、2つの制御フロー経路が合流しその抽象状態を結合しなければならないマージポイントで精度を失う。

実際のツールはより洗練されたドメインを用いる。多面体、八角形、述語抽象は変数間の関係を追跡する。x < y は区間には見えないが、多面体ドメインはそれを記憶する。これらのドメインはより精度が高い。しかし、よりコストもかかる。多面体ドメインは最悪の場合、指数関数的な計算量を持つ。30万行のC言語による飛行制御システムに対して、素朴な実装では航空機が退役するまでに終了しないだろう。

AstréeがA380で実際に証明したこと

Astréeは、航空分野で抽象解釈を有名にした静的解析器である。2003年、AstréeはエアバスA380の主要飛行制御ソフトウェアに対して実行された。あらゆるランタイムエラーの不在を証明した。ゼロ除算なし。配列の範囲外アクセスなし。算術オーバーフローなし。クリティカルパス上の到達不能コードなし。

それは飛行機が墜落しないことを証明したわけではない。制御則が正しいことを証明したわけでもない。迎角計算が航空機の物理と一致することを証明したわけでもない。それらは別の問題であり、別のツールで解決される。

Astréeが証明したのは、ソフトウェアが自己崩壊しないことである。聞こえよりも狭い主張だが、多くの人が認識しているよりも価値がある。ソフトウェアの自己崩壊は航空事故の一般的な原因である。それが起こりえないことを証明する価値は、努力に値する。

このツールは、いくつかのドメイン固有の工夫を組み合わせることでこれを達成した。速度のためには非関係ドメインを、精度のためには関係ドメインを用いる。丸め誤差を考慮したモデルで浮動小数点演算を扱う。航空電子機器で用いられる特定のC言語サブセットを理解し、未定義動作をエラーとして扱う。エンジニアが出力を信頼できるほど偽陽性率を下げるには、何年ものチューニングが必要だった。

健全性は選択であり、デフォルトではない

すべての静的解析器が健全性を目指しているわけではない。Coverity、CodeQL、Inferのようなツールは、不在の証明よりも実際のバグ発見を優先する。状態空間を過小近似する。ゼロ除算を見逃す可能性はあるが、発見したものは通常本物である。

これは正当な工学的選択である。Webアプリケーションでは、数分で実行される90%精度のバグ発見ツールが、偽陽性の海に溺れる健全な解析器より優る。飛行制御システムでは、その逆である。ノイズを滤過しなければならなくても、証明が欲しいのである。

抽象解釈は、その証明を可能にする技術である。唯一の形式的手法ではない。SPINやTLA+のようなモデルチェッカは状態機械を検証する。CoqやIsabelleのような定理証明器は機能的正しさを検証する。抽象解釈は絶妙な位置を占めている：完全に自動的であり、大規模な codebases にスケールし、ランタイム動作について数学的保証を与える。

抽象解釈が破綻する場所

この手法には硬い限界がある。複雑なポインタ演算によって割り当てられたメモリについて推論できない。アルゴリズムが正しい値を計算することは検証できず、計算中にクラッシュしないことだけを検証できる。並行性、動的ディスパッチ、そして設計上未定義動作に依存するコードには苦労する。

また、コードが検証可能なスタイルで書かれていることを要請する。A380の飛行ソフトウェアは再帰を避け、動的メモリ割り当てを制限し、制御フローを単純に保つ。これらの制約は解析器の限界ではない。証明の前提条件である。モデル化には混沌としすぎたコードの性質を証明することはできない。

実際の関数から区間解析を始めよう

これらのアイデアを適用するためにAstréeは必要ない。codebase から単一の純粋関数を選べ。境界内に留まらなければならない変数を1つ特定する。単純な区間伝播スクリプトを書く。その変数をすべての分岐と操作を通じて追跡する。

使用地点での区間が安全範囲内であれば、その変数に対する手動の安全性証明を得たことになる。そうでなければ、バグか、あるいはあなたの推論が不完全だった場所を特定したことになる。いずれにせよ、ユニットテストでは見逃したかもしれない何かを学んだことになる。

抽象解釈は、あなたの飛行機が墜落しないことを証明しない。何もそれを証明できない。だが、あなたのソフトウェアがその原因にならないことは証明できる。

よくある質問

抽象解釈とは何か？

抽象解釈は、具体的なプログラム値を区間や形などの抽象表現で置き換える静的プログラム解析のための形式的手法である。解析器はこれらの抽象値上でプログラム実行をシミュレートする。抽象ドメイン内でエラーが到達不可能であれば、あらゆる可能な入力に対して具体プログラムでも到達不可能である。

抽象解釈はすべてのバグを発見できるか？

いいえ。抽象解釈は、ゼロ除算、バッファオーバーフロー、算術オーバーフローなどの特定のランタイムエラーの不在を証明する。アルゴリズムが正しい結果を出力することは検証できず、クラッシュしないことだけを検証できる。ハードウェア故障や物理システムの動作など、コード外の性質についても推論できない。

健全な静的解析と不健全な静的解析の違いは何か？

健全な解析器は、可能なプログラム振る舞いの集合を過大近似する。設計された検出対象のバグを決して見逃さないが、偽陽性を報告する可能性がある。不健全な解析器は過小近似する。バグを見逃す可能性はあるが、報告されたものは実際のものである可能性が高い。健全性は安全クリティカルシステムにとって不可欠である。不健全な解析は、一般的なソフトウェア開発でより速いフィードバックを得るために好まれることが多い。

抽象解釈は安全クリティカルソフトウェア専用か？

いいえ。そこで最も多用されるが、それだけではない。抽象解釈のアイデアは多くのコンパイラやオプティマイザに現れる。例えば、LLVMの範囲解析は、冗長な境界チェックを除去するために区間抽象を用いる。同じ区間推論は、組み込みファームウェアから高性能数値カーネルまで、境界の証明が重要なあらゆるコードに適用できる。