スケーラブルで透明性の高い
ソフトウェアセキュリティのためのパス代数

1 はじめに

1.1 根本的な課題: 実行の振る舞いのソフトな無限

タスク固有（解析か、変換か、検証か）および言語固有の数多くのソフトウェアの課題に取り組んできた結果、我々は、スケーラビリティの根本的な課題は実行の振る舞いのソフトな無限に根ざしていると考えている。ソフトな無限という用語は、どれほど高速なコンピュータであっても列挙できないほど大きな数（例えば、宇宙に存在すると推定される原子の数）を意味する。ノードが 100 個、エッジが 200 本しかなくても、有向非巡回グラフ（DAG）のパスの数はソフトな無限になり得る。実行の振る舞いのソフトな無限は、プログラムのループ（すべてのループが停止すると仮定しても）と手続き間の実行のために、DAG のパスの数をはるかに超えて増大する。実行の振る舞いのソフトな無限は、プログラミング言語にかかわらず、またソース形式かバイナリ形式かにかかわらず存在し続ける。これは、良いプログラミング慣行によって取り除くことのできない障壁である。

1.2 新しいアプローチ: パス代数

我々は 1996 年から大規模ソフトウェアの保守と進化に取り組んできた。この 15 年間は、大規模ソフトウェア（例えば 2,500 万行のコードを持つ Linux カーネル）を解析、修正、検証するためのスケーラブルで透明性の高い技術を目指して努力してきた。

最近、我々は実行の振る舞いをモデル化するための新しい非可換環 [1] を開発し、これをパス代数と呼んでいる。実行の振る舞いのソフトな無限のコンパクトな表現を提供することで、パス代数はスケーラブルなソフトウェアの解析、修正、検証を可能にする。また、ソフトウェアとその制御フローグラフとの直接的な対応を保つことで、透明性（すなわち理解しやすさ）を提供することもできる。

パス代数は、すべての主要な自動車、アビオニクス、防衛企業を含む世界中のお客様や、いくつかの DARPA サイバーセキュリティプロジェクトとの取り組みの中で直面したスケーラビリティと透明性の問題を解決するための、この 15 年間の実験から発展してきたものである。大規模ソフトウェアを対象とした自明でない実験を高速に繰り返せるよう、我々は C、C++、Java、Simulink、Java バイトコード、バイナリのソフトウェアを解析・修正するツールを構築するための高度なプラットフォーム Atlas [2, 3, 4] を構築した。Atlas は、eXtensible Common Software Graph（XCSG）スキーマ [5]、XCSG を操作するための eDSL、プログラム理解を助ける豊富な可視化、そして大規模ソフトウェアに対する eDSL の高速な実行を支えるグラフデータベースを実装している。パス代数は、ソフトな無限に対処するために我々が試してきた他のいくつかの技術の限界に対処することを目的としている。

2 動機となる問題

パス代数の数学的な説明とその実践での使用に入る前に、BLAST モデル検査器 [6] を用いた Linux 検証実験で我々が直面したスケーラビリティと透明性の限界について、短い話をしておく必要がある。

この実験では、ミューテックスの LOCK の後には必ずミューテックスの UNLOCK が続くという安全性プロパティの検証を目指した。実験には 66609 件の LOCK インスタンスが含まれていた。我々が直面した限界は次のとおりである。

• モデル検査器のスケーラビリティの限界: モデル検査器は、LOCK インスタンスの 34% について検証を完了できなかった。検証を完了しないまま実行し続けたのである。

• モデル検査器の透明性の限界: ここでは透明性の限界が 2 つの形で現れた。

  • モデル検査器は、一部の LOCK インスタンスについて検証を完了できなかった理由を何も説明しなかった。スケーラビリティの失敗について明確な理由が示されなければ、スケーラビリティの改善は困難になる。
  • モデル検査器が安全（すべての実行の振る舞いについて安全性プロパティが成り立つ）と判定したインスタンスについて、モデル検査器は、人間が答えの妥当性を容易に照合し再確認するために使える情報を何も提供しなかった。

モデル検査器による検証は、自動検証のために低レベルのブール論理の抽象を用いる SAT ソルビングに基づいている。問題を表す膨大なブール論理の表現は、透明性になじまない。

透明性が欠けていたため、我々は別のアプローチを採用した。モデル検査器で検証できなかった 34% の LOCK インスタンスについて、制御フローグラフ（CFG）とコールグラフ（CG）を解析したのである。これらのグラフは非常に大きく複雑であることが多い。グラフに基づく解析を簡略化しスケールさせるため、我々は CFG に対するグラフの支配関係に基づく簡略化である射影制御フローグラフ（PCG）[7] を開発し、スケーラビリティを実現するためにマッチングペアグラフ（MPG）[8] の技術を考案した。PCG と MPG に基づくグラフ解析ツールの構築には Atlas プラットフォームを使用した。この解析から新しいグラフベースのソフトウェア検証技術が生まれ、我々はそれを用いて Linux の検証を完了した [6]。Linux の検証結果は Web サイト [9] で公開されている。我々が提供する裏付けの証拠によって、我々の自動検証は各インスタンスについて手作業で容易に照合できる。

3 パス代数

前述のとおり、我々はこの 15 年間、ソフトウェアを解析、修正、検証するためのスケーラブルで透明性の高い技術を求めて実験を行ってきた。パス代数は、これらの実験を通じて得られた洞察から生まれたものである。

3.1 数学を用いた無限への対処

我々の目標は、実行の振る舞いのソフトな無限によって生じる複雑さを管理することで、ソフトウェアの抽象に対する効率的な解析と変換を可能にすることである。

数学には、強力な概念によって無限に対処してきた長い歴史があり、それらの概念は大きな科学的進歩をもたらしてきた（例えば、無限べき級数に基づくニュートンの微積分や、ある一点で無限大に近づくディラックのデルタ関数）。適切な概念は、一見ソフトな無限の演算を必要とするように見える問題を解くための計算量を劇的に削減する鍵となり得る。例えば、2¹⁰⁰ 番目のフィボナッチ数は、黄金比を用いれば（意外にも）100 回の算術演算で計算できる。

3.2 新しい代数の定義

抽象代数は、さまざまな種類の問題を解くために作られる新しい代数系の基礎となるテンプレートとして、「群」「環」「体」の三つ組を提供している。パス代数は、実行の振る舞いをモデル化するための、非可換環に基づく新しい代数である。パス代数では、実行パスは変数の積として現れる。加算は分岐を表す。ループは除算として簡潔に現れ、ループ本体は一度だけ表される。

この新しい代数の仕組みは SymPy [10] を用いて構築され、Atlas [2] のプラグインモジュールとして組み込まれている。我々の実装は、Linux カーネルのような大規模ソフトウェアを処理できるほど堅牢であり、複数のプログラミング言語をサポートしている。以下では、パス代数を説明する例を示し、続いてパス代数を用いて得られた新しい知見のいくつかを紹介する。

図 1 は、安全性プロパティ（すべての制御パスで LOCK の後に UNLOCK が続かなければならない）を検証するためにパス代数をどのように使えるかを示している。この例では、関連する振る舞いを抽出するための準同型の使用も示している。図 1 のソースコードは、我々が Linux カーネルで発見した LOCK-UNLOCK のバグの例をモデル化したものである [6]。

図 2 にまとめた重要な点のいくつかを説明しよう。

1. 実行の振る舞いの代数的表現:
   • 実行の振る舞いの全体は、代数的な振る舞いのコンパクト表現（CRB）によって表される: B 2(3(T)4 5(F)8(10(T)11 + 10(F)13))^*(3(T)4 5(T)6 + 3(F))E。ここでは行番号をプログラムの文の ID として用いている。条件文については、T と F が True または False を表す。この式は、3(T) の後に 4 が続き、3(F) の後に E（すなわちプログラムの終了）が続くことを示している。
   • CRB のコンパクトさは代数的な因数分解によるものである。展開すると多数の単項式が得られ、それぞれが 1 つの実行の振る舞いに対応する。例えば、単項式 2(3(T)4 5(F)8 10(T)11)^*3(T)4 5(T)6 がそうである。これは、while ループがすべての反復で 5(F) と 10(T) をとって反復し、その後 break が続く場合の振る舞いである。
   • ループによる実行の振る舞いは、部分式によって表される振る舞いの反復を示す * 演算子を上付きにした部分式によって与えられる。
2. 関連する実行の振る舞いのための準同型:
   • 準同型は抽象代数における強力な道具である。ここでは、LOCK（#4 行目）の後に常に UNLOCK（#8 行目）が続くかどうかを検査するために関連する実行の振る舞いを抽出するのに用いられる。
   • 準同型によって抽出される実行の振る舞いは次のように与えられる: (3(T)4 5(F)8 )^*(3(T)4 5(T) + 3(F))。
3. 準同型を用いたソフトウェア検証:
   • 抽出された 2 つの振る舞いのうち、LOCK（#4 行目）の後に UNLOCK（#8 行目）が続かないものが 1 つある: (3(T)4 5(F)8 )^*3(T)4 5(T)
4. ループの実行の振る舞いの代数的表現:
   • この代数式は、ループの 3 種類の振る舞いを表している。すなわち、ループからの通常の脱出を伴う反復的な振る舞い（この例では 3(F)）、ループからの脱出をもたらす終端的な振る舞い（この例では 5(T)）、そしてループがスキップされる場合の振る舞い（* は 0 回の反復でもよい）である。
   • 興味深いことに、パス代数はループを除算演算によって捉え、その結果得られる分数は、ループの反復に関連付けられる無限等比級数の閉形式の式であることが分かる。代数的な導出では、部分式 s に関連付けられたループの実行の振る舞いについて、分数 1​1 − S が得られる。
   • * 演算子は反復を表すために一般的に使われる表記であるため、代数式を示す際には 1​1 − S の代わりに s^* と書く。

3.3 振る舞いのコンパクト表現（CRB）の導出

有向グラフ G が与えられたとき、代数式は、G を一意に捉える線形連立方程式 S を立てることによって導出される。パス代数はエッジ上で定義され、乗算はパスの連結を、+ はパスの和集合を表す。G の各ノード i には変数 X_i が割り当てられる。線形方程式の係数はエッジの識別子である。方程式を解くと、各 X_i の値として部分式が得られる。その部分式は、ルート（#1 ノード）からノード i へのパスの集合を与える。

図 2 は、ループを持つ単純なグラフ、それに対応する線形連立方程式、そして連立方程式を解いて得られる答えを示している。まず、部分式がエッジの積として得られることに注意されたい。エッジは後続関係 [11] を表すため、この部分式は後続によるコンパクト表現（CRS）と呼ばれる。CRS は、各エッジをその始点ノードに写像することで CRB に変換される。前述のとおり、ループは除算演算によって捉えられる。

4 パス代数の利点

4.1 ソフトウェアセキュリティのためのスケーラビリティ

パス代数の最も重要な利点は、ソフトウェアセキュリティを確保するために提供されるスケーラビリティである。セキュリティプロパティは、すべての実行の振る舞いについて検査しなければならない。実行の振る舞いのソフトな無限のため、振る舞いを列挙して検査することは多くの場合不可能である。LOCK の後に常に UNLOCK が続くかどうかを検査するためにパス代数を用いた先の説明を思い出してほしい。すべての実行の振る舞いに対するコンパクトな表現を提供し、関連する振る舞いを容易に抽出するために準同型を用いることで、パス代数は振る舞いを列挙することなくすべての実行の振る舞いを検査することを可能にし、ソフトウェアのセキュリティプロパティを検査するための計算量を大幅に削減する。

4.2 ソフトウェアセキュリティのための透明性

Linux 検証実験で述べたように、モデル検査器はモデル検査のステップを説明しはする。しかしそれらのステップには、人間の理解になじまない低レベルの抽象と膨大な詳細が含まれる。De Millo、Lipton、Perlis（最初のチューリング賞受賞者）は、画期的な論文 [12] において、自動ソフトウェア検証は、人間が理解できる証明を作り出すという数学が示した手本に従うべきであると論じている。

パス代数は、人間が容易に結び付けて考えられる実行パスと直接対応するコンパクトな表現を提供する。代数的な準同型は、関連する振る舞いに焦点を当てることを可能にすることで、人間の理解をさらに高める。図 1 の例を再び取り上げて例示しよう。安全性プロパティに違反する実行の振る舞いの準同型による式は (3(T)4 5(F)8 )^*(3(T)4 5(T) + 3(F)) である。安全性プロパティの違反は、3 行目と 5 行目の条件が True のときにちょうど発生し、その結果、UNLOCK が決して続かない LOCK が生じることは容易に分かる。この情報があれば、人間は多数の実行の振る舞いに惑わされることなく、検証を容易に照合できる。

5 パス代数の広範な洞察と適用可能性

図 3 は、GOTO 文を含むコード片の制御フローグラフを示している。これには LOCK（L）と UNLOCK（U）が含まれる。すべての実行パスで L の後に U が続くだろうか。グラフの複雑さに注目されたい。これをスパゲッティコードと呼ぶ人もいるだろう。パス代数はスパゲッティコードの複雑さを特徴付けられるだろうか。パス代数はその複雑さを管理し、セキュリティプロパティのスケーラブルで透明性の高い解析を可能にできるだろうか。

図 3 の複雑さは、単なる理論上の好奇心の対象ではない。複雑な有限状態機械（FSM）の実装でこれに遭遇することは多く、その場合、その機械に奇妙な（意図しない）振る舞いがあるかどうかを知ることが重要になる。Linux カーネルには何千もの GOTO 文がある。それらはセキュリティプロパティを検証する障壁になるのだろうか。Linux は GOTO 文を取り除くように書き直されるべきなのだろうか。パス代数はコードの書き直しに役立つだろうか。Linus Torvalds はそのような書き直しに反対してきた [13]。なぜ GOTO 文を使うべきなのか、あるいは使うべきでないのかを理解するための洞察を、パス代数は提供できるだろうか。GOTO（ジャンプ）の複雑さを理解し管理することは、バイナリにとって不可欠である。

以下の順序で、パス代数の洞察と適用可能性を明らかにしていく。

A. パス代数は、GOTO による複雑さについて、驚くべき定量的な特徴付けを提供する。 コンピュータサイエンスの多くの著名人がこの問題に取り組み、その結果いわゆる構造化プログラミングが考案されたことに注意されたい。Knuth は “Structured Programming with GOTO Statements” と題した論文 [14] で、Dijkstra、Hoare らとの議論をまとめ、次のように結論付けている: 「誰もがそれ（構造化プログラム）が良いものだと知っているが、McCracken が言ったように、あえて定義を試みる人はほとんどいない。実際、単純な定義が今のところ存在するのかどうかも明らかではない。」Knuth と Floyd [15] は、正規表現に基づく特徴付けを定式化しようと試みた。我々は Knuth とのやり取りの中で、彼らの試みを復活させるうえでパス代数がいかに重要であるかについて議論した。

B. パス代数は、GOTO 文を除去するための標準変換をもたらす。 Manna は書籍 [16] “Introduction to Mathematical Theory of Computation” を著し、後にその理論を応用して GOTO 文を除去する体系的な方法を開発した [17]。パス代数は、Manna が提案した数学的理論よりもはるかに単純で洗練されている。

C. 実践において（例えば Linux の GOTO）、その複雑さはパス代数によって直接管理できる。 GOTO を除去すると別の複雑さが生じるため、構造化プログラミングによって負担が軽くなるわけではない。したがって、GOTO（ジャンプ）の除去という選択肢がないバイナリ解析にとって、パス代数は特に重要である。

5.1 構造化プログラムの代数的特徴付け

Böhm と Jacopini によって証明された定理 [18] は、IBM の Harlan Mills による構造化プログラミングの教義 [19] の礎となった。Dijkstra は、GOTO のないプログラムのクラスに対して構造化プログラムという用語を考案した [20]。我々は、Dijkstra によって定義されたクラスに対して構造化プログラムという用語を用いる。実行の振る舞いのコンパクト表現の 2 つの形式として CRB と CRS を導入したことを思い出してほしい。CRB は制御フローグラフのノードを用いた表現であり、CRS はエッジを用いた表現である。CRS を用いて「構造化」を定義できる。

プログラムが構造化されているのは、CRS にエッジ要素の繰り返しがない場合であり、かつその場合に限る。

図 3 の制御フローグラフに戻ると、CRS は次のとおりである。

繰り返し: e₅: 2, e₆: 4, e₈: 2, e₉: 4, e₁₃: 2, e₁₄: 2。繰り返しの数が非構造化の度合いを定量化する。

5.2 GOTO のないプログラムを導出する標準変換

Manna は書籍 [16] “Introduction to Mathematical Theory of Computation” を著し、後にその理論を応用して GOTO 文を除去する体系的な方法を開発した [17]。パス代数が、非構造化プログラムを構造化プログラムに変換するための単純で洗練された強力な枠組みをどのようにもたらすかを説明しよう。

図 4 は、非構造化プログラムの制御フローグラフ（CFG）と、その構造化変換の CFG を示している。Manna を含む以前の文献では、非構造化を、制御ブロックの入口の一意性または出口の一意性のいずれかへの違反として説明している。まず、パス代数によって明らかになる非構造化の双対性に注目されたい。同じ非構造化が、制御ブロック（網掛けのブロックとして示す）の選び方によって、複数の入口としても複数の出口としても現れる。この双対性は、エッジ要素の繰り返しを避けるための 2 通りの因数分解に対応する。そのような繰り返しが非構造化を特徴付けることを思い出してほしい。図 4 に示すように、実行の振る舞いを表す代数式 e₁e₂e₃ + e₁e₄e₅ + e₆e₅ は 2 通りに因数分解できる。(i) e₁ の繰り返し（これを接頭辞の繰り返しと呼ぶ）を避ける e₁(e₂e₃ + e₄e₅) + e₆e₅、または (ii) e₅ の繰り返し（これを接尾辞の繰り返しと呼ぶ）を避ける e₁e₂e₃ + (e₁e₄ + e₆)e₅ である。この双対性から、Transform-1 と Transform-2 として示す 2 つの標準変換が導かれる。どちらの変換も、繰り返されるエッジ要素を複製することで非構造化を除去しており、そのためにはコードの複製が必要になることに注意されたい。例えば Transform-1 では、コード A₄ が複製されて A₄₁ と A₄₂ として示され、それに対応するエッジ要素 e₅ の複製が e₅₁ と e₅₂ として示されている。

5.3 パス代数による GOTO の複雑さの管理

上で論じた変換を用いれば、GOTO 文を除去することはできる。しかし、GOTO の除去には支払うべきコストがある。この変換にはコードの複製が伴い、これはコードの再利用を提唱するソフトウェア工学の格言に反することに注意されたい。このように、代数は、構造化か非構造化かという問題が実際には複製か再利用かのトレードオフであることを明確に示している。アプリケーションのロジックが本質的に非構造化である場合（一部の FSM がそうであるように）もあり、構造化プログラムを書いてもその複雑さを取り除くことはできない。複雑さは複製という形で再び入り込むだけである。Linus は GOTO を使う理由を明確に述べてはいないが、パス代数は彼の立場を理解し支持するのに役立つ。

図 3 の例は複雑に見える。前述のとおり、CRS には繰り返しがある。GOTO を除去するとコードの複製が多数生じ、コードは冗長になるが、少しも理解しやすくはならない。それにもかかわらず、繰り返しがあっても CRS の導出と解析は変わらないため、この複雑さはパス代数によって直接扱うことができる。関連する振る舞いを導出するために準同型を適用することも、同じように簡単である。

図 3 に示すように、準同型は CRS を次のように写像する。

得られた代数式から、ループが振る舞い e₇e_Le₈e₉ または e₇e_Le₁₄e₆ で終わるときに L の後に U が続かないことが、非常に明確に分かる。パス代数の助けがあれば、答えを照合するにはざっと見るだけで済む。

6 新しい研究の方向性

多くのソフトウェアの抽象は、グラフとして自然に表現できる（例えば、データフローグラフ、制御フローグラフ、コールグラフ）。代数的アプローチは、さまざまなグラフベースの抽象に等しく広く適用できるため、多くの新しい研究の可能性につながる。

我々は、ある自動車会社のために、C ソースと PowerPC バイナリの間の制御フローに基づく等価性を検証するツールを開発した。その後、オープンソースのオペレーティングシステムを対象に同様の実験を行い、その結果を論文 [21] で報告した。この経験は、ビルドプロセスの健全性を検査するという新しい研究の方向性を示唆している。

パス代数は、さまざまなソフトウェアの抽象の調査に適用できる。例えば、状態空間の爆発に巻き込まれることのない、スケーラブルで正確なデータフロー解析である。

もう 1 つの興味深い研究は、SAT ソルバーのスケーラビリティと透明性の問題に対処するために代数を用いることを探ることであろう。予備的な実験から、我々は 3-SAT 問題に対するスケーラブルで透明性の高い解法の枠組みのための特別な代数を開発できると考えている。

7 付録: Atlas を用いた BLAST による Linux 解析の調査

前述のとおり、我々は Atlas を用いて、BLAST の検証結果で直面した透明性とスケーラビリティの問題を調査する実験を行い、後に BLAST では完了できなかった 34% の LOCK インスタンスについて Linux の検証を完了するのにも役立てた。

我々は、モデル検査器で完了できなかった LOCK インスタンスを分類した。分類のための ATLAS スクリプトの例を図 5 に示す。これは、LOCK と UNLOCK のインスタンスが異なる関数にあり、それらの関数がループ内で呼び出されるという複雑なカテゴリを特定するために、コンパクトな eDSL スクリプトをどのように書けるかを示している。図 5 は、関数呼び出しを含むすべてのループを取得するスクリプトの一部を示している。XCSG.Loop や XCSG.LoopChild といった XCSG のタグを使うことで、クエリを簡潔に保てる。図中のソースコードはおもちゃの例（foo と bar）である。しかし、同じクエリを何百万行ものコードを持つ大規模ソフトウェアに対して実行し、そのカテゴリに属するすべての LOCK インスタンスを素早く抽出できる。

次に、パス代数の実験を行うための Atlas の使用法を説明する。洞察を得るため、我々は小さなオペレーティングシステムである XINU [22] を対象にパス代数の実験を行った。XINU のすべての関数の制御フローグラフについてパス式を計算した。

図 6(a) は XINU の関数 blkcopy のソースコードを示している。図 6(b) は対応する制御フローグラフ（CFG）を示している。図 6(c) は CFG のエッジラベル e_i とノードラベル X_i を示している。線形連立方程式は e_i と X_i を用いて立てられる。図 6(d) は XCSG の eDSL クエリとその結果を示している。クエリ getEquations はラベル付けされた CFG の線形連立方程式を作成し、クエリ getCRS は方程式を解いて CRS を計算する。最初のクエリは、関数 blkcopy のノードを取得し、blkcopy という名前の変数に格納するものである。この変数は後続のクエリの入力として使われる。

Atlas はプログラム全体をUniversal Graphと呼ばれるグラフとして格納することに注意されたい。関数などのプログラムの成果物は XCSG 属性を持つノードとして格納され、プログラムの成果物間の関係は XCSG 属性を持つエッジとして格納される。いくつかのデータフローと制御フローの関係は Atlas によって事前に計算され、その結果はUniversal Graphに格納される。eDSL のクエリは Universal Graph にアクセスする。

eDSL は Java に埋め込まれた DSL である。図 6 に示したクエリを Java のループに埋め込むことで、XINU の 210 個の関数すべて、合計 11000 行の C コードについて CRS を計算できる。XINU のすべての関数の CRS は、ノートパソコン上で 1 分未満で計算できる。

7.1 Linux 検証実験

先に Linux 検証実験について論じた。図 7 の表に、実験結果の概要を示す。