← ENSOFT の研究
2019

ソフトウェアの数学的解析を
認証するための簡潔な視覚的証拠

Suresh Kothari1

Payas Awadhutkar1

Ahmed Tamrawi2

1Iowa State University
Ames, IA 50011, USA

2ENSOFT
Ames, IA 50010, USA

概要. 認証は、ソフトウェアの障害による高額な現場サポート、製品のリコール、法的措置を避けるために企業にとって極めて重要である。数学的解析が認証に役立ちうるのは当然である。実際に採用されるためには、数学的解析は認証のための裏付けとなる証拠を生成しなければならない。本論文は、この重要なニーズへの対処を扱う。本論文は、認証証拠のための新しいスキーマを示す。このスキーマは、ソフトウェアの安全性とセキュリティの性質を認証するために、コンパクトで理解しやすい証拠を伝えるよう設計されている。このスキーマは、数学的証明とソフトウェアの振る舞いとの対応を簡潔に反映する。本論文は、実世界のソフトウェアを認証するうえで、提案するスキーマの適用可能性と重要性を示す事例研究を示す。

キーワード: ソフトウェア認証, 数学的解析, 認証証拠

目次

1 はじめに

ソフトウェアの障害は、死亡、負傷、多額の経済的損失をもたらす重大な事故を引き起こしてきた。何も手を打たなければ、ますます広がるソフトウェアの利用は、より頻繁でより深刻な事故をもたらしうる。Software for Dependable Systems に関する National Academy of Sciences の報告書 [12] は、ソフトウェアのディペンダビリティを保証することを意図した既存の認証の仕組みの実績はまちまちであり、大部分が効果のないものもあれば、逆効果のものもあると指摘している。National Academy の報告書 [12] は、開発プロセスへの準拠とテストに基づく従来の認証手法では、極めて重要な安全性とセキュリティの性質へのソフトウェアの準拠を保証できないと述べている。

DO-178C [10] と UK Def Stan 00-56 [32] はよく知られた認証規格である。どちらの規格も、検証と妥当性確認の手法がなぜ、どのように認証の目標を達成するのかについて、根拠のある正当化を提出することを求める。既存のセーフティケースでは、安全性の論証は通常、自由記述の文章で伝えられる。例えば、UK Def Stan 00-56 におけるセーフティケースは次のように定義されている。「与えられた運用環境における与えられた用途についてシステムが安全であることを、説得力があり、理解でき、妥当な形で示す、一連の証拠に裏付けられた構造化された論証。」

テストの証拠が主役となる DO-178C とは異なり、UK Def Stan 00-56 は解析的な証拠を優先する。それでも、準拠のための主な手段として数学的解析を用いることを認めてもらうには、数学的手法に、根拠のある正当化のための裏付けとなる証拠を伴わせる必要がある。実際には、根拠のある正当化を生み出すための支配的な手法はテストである。すべてのテストケースは要求から生成される。テストの品質は、要求カバレッジと構造カバレッジという二つのカバレッジ指標で判断される。前者のカバレッジはどの要求がテストされなかったかを決定し、後者はテストケースがコードの構造をどれだけよく動かしたかを決定する。テストを別の技術で置き換えるための論証を構築する際にとるべき一般的な方針は、置き換える技術が生み出す証拠が、少なくともテストが生み出す証拠と同程度に説得力があると論じられることを示すことである [17]。

セキュリティの脆弱性は、ソフトウェアのディペンダビリティの性質について示された論拠を損ないうる。したがって、ディペンダビリティの性質は、その他の側面を損ないうるセキュリティのリスクを明示的に考慮しなければならない。また、セキュリティの認証が攻撃への耐性について意味のある保証を与えることを確かにすることも重要である。一般に、テストはソフトウェアのセキュリティを保証するには十分でない。通常用いられる最大規模のテストスイートでさえ、ソフトウェアに脆弱性がないという証拠を与えるのに十分なパスを動かさないからである。認証された製品やシステムに対するほとんどの攻撃が失敗するという確信を与えられる、新しいセキュリティ認証の体制が必要である。

本論文では、数学的解析が生成でき、認証に使える認証証拠（CE）の新しいグラフィカルな概念と、それに伴うスキーマを示す。本研究を実際に採用できるよう、DO-178C [10] と UK Def Stan 00-56 [32] の認証文書を調べ、業界で広く行われている慣行に沿える CE の適切な概念に到達した。また、新しい CE スキーマが実際にどのように適用できるかを示す、Linux カーネルとその他のソフトウェアの事例研究も示す。

研究の貢献のまとめ: (a) 認証を目的として、検証の証明を簡潔な視覚的形式で明確に表現するよう設計された新しい認証証拠（CE）スキーマ（第 2 節）、(b) CE の証拠の重要性と使いやすさを明らかにする Linux の事例研究（第 4.1 節）、(c) CE スキーマを用いることで安全性の論証の落とし穴をどのように避けられるかを示す、Bftpd ソフトウェア [4] のサービス拒否の脆弱性の事例研究（第 4.2 節）。

2 認証証拠のスキーマ

この節では、証明の理解と照合を容易にするために、検証の証明を簡潔な視覚的形式で正当化するよう設計された新しい認証証拠（CE）スキーマについて述べる。一般的なスキーマのさまざまな側面を具体的に説明するため、メモリリーク（ML）の問題を例として用いる。

ML の検証には、メモリ割り当てのインスタンスごとに証明が必要である。したがって、CE スキーマは各インスタンスについて検証の証拠を提供する役割を果たさなければならない。

2.1 CE スキーマで提供される証拠

CE スキーマは、次の証拠を提供するよう設計されている。

  • 関連する関数: 検証の証明に関連する関数の集合。この集合は一つ以上の関数を持ちうる。例えば、関数 f1 でのメモリ割り当ての後に、割り当てに続く実行可能な各制御フロー（CF）パスで f1 自身でのメモリ解放が続くなら、それは一つの関数だけである。しかし、f1 に別の関数 f2 がメモリを解放する実行可能な CF パスがあるなら、それは二つの関数 f1 と f2 になりうる。
  • 関連する関数の間の関係: 関連する関数の間のデータと制御の関係。例えば、制御とデータの関係は、それぞれ f1 が f2 を呼び出すこと、および f1 が割り当てられたメモリへのポインタを f2 に渡すことでありうる。
  • CF パスのカバレッジ: 証拠は、関連する各関数内のすべての CF パスのグループ分けを示す。グループ分けは簡潔な証明のためである。CF パスの数は指数的に増え、入れ子でない分岐条件が n 個あると 2n 個のパスになる。同じ推論が適用できるパスは一つのグループにまとめられる。例えば、f1 でのメモリ割り当てに続く CF パスには、三つのグループがありうる。(i) 解放のあるパス、(ii) 割り当てられたメモリへのポインタが f2 に渡されるパス、(iii) 解放がなく、ポインタが別の関数に渡されないパス。
  • パスの実行可能性と関連する条件: 証拠は、偽陽性を避けるためにパスの実行可能性の検証を考慮する。例えば、解放がなく、ポインタが別の関数に渡されないパスについては、実行可能性を検査しなければならない。これらのパスが実行可能でなければ、メモリリークではない。証拠には、パスの実行可能性を検査するのに関連する条件の集合が含まれる。

2.2 CE スキーマのグラフィカルな表記法

認証証拠を伝える簡潔な視覚的媒体として、グラフィカルな表記法を示す。最初の二つの区分の証拠（関連する関数と関連する関数の間の関係）にはマクロな証拠という用語を、最後の二つの区分の証拠（CF パスのカバレッジとパスの実行可能性）にはミクロな証拠という用語を用いる。

CE スキーマは、関連する関数をノードとして、関数の間の相互作用をエッジとして描く。相互作用が、関数 f が割り当てられたメモリへのポインタをパラメータとして別の関数 g に渡すことだとする。このとき、スキーマは関連するパラメータの受け渡しを表すラベル par を持つ、f から g へのエッジを持つ。

CE スキーマは、関数の間のさまざまなデータフローと制御フローの相互作用を記述できるほど広範である。関数の間でデータを伝える三つの方式すべてを組み込んでいる。(i) パラメータとして渡す、(ii) 戻り値として渡す、(iii) グローバル変数を通じて共有する。また、ある関数から別の関数へ制御を渡す三つの方式すべてを組み込んでいる。(a) ある関数が別の関数を名前で呼び出す、(b) ある関数が関数ポインタを用いて別の関数を呼び出す、(c) 二つの関数が非同期に動作し、コンテキストスイッチのために制御がある関数から別の関数へ移る。

マクロな証拠とミクロな証拠の統合: ミクロな証拠は、検証のために関数 f 内の制御フローパスがさまざまなグループに分けられることを示す。マクロな証拠は、検証のために f と他の関数との相互作用を示す。マクロな証拠とミクロな証拠の統合を必要とする次のシナリオを考える。メモリを割り当てる関数 f から始める。関数 f の制御フローパスは三つのグループに分かれる。解放を含む制御パスのグループ、割り当てられたメモリへのポインタを関数 g に渡す制御パスのグループ、そしてそのどちらも持たない、すなわち解放を含まず、割り当てられたメモリへのポインタを他のどの関数にも伝えない制御パスの第三のグループである。パスのグループ分け（ミクロな証拠）と関連するパラメータの受け渡し（マクロな証拠）を簡潔に表現する必要がある。

では、上のシナリオを伝えるためにミクロな証拠とマクロな証拠がどのように統合されるかを論じる。図 1 に示すように、関数 f と g はノードで表される。f から出る三つのエッジは、制御パスの三つのグループに対応する。ラベル par を持つ f から g へのエッジは、パスのグループに沿った関連するパラメータの受け渡しを表す。f から deallocation へのエッジは、パスのグループに沿った対応する解放を表す。ラベル PFC を持つ f からのエッジは、パスのグループに沿ってパスの実行可能性の検査（PFC）が行われることを表す。

ノード f は三つの出ていくエッジを持つ。一つは解放のノードへ、一つは par とラベル付けされてノード g へ、一つは PFC とラベル付けされている。
図 1. 関数 f: 制御フローパスは三つのグループに分かれる

2.3 CE スキーマを用いた実世界の例の証拠

この例は、約 10,000 行のコードからなる XINU オペレーティングシステム [8] から選んだ。XINU では、getbuf と freebuf がそれぞれメモリを割り当てる呼び出しと解放する呼び出しである。dgwrite のメモリは getbuf の呼び出しによって割り当てられる。CE スキーマを用いて、dgwrite におけるこの割り当てに続くすべての実行可能な CF パスに、対応する freebuf の呼び出しがあるという証拠を示す。

CE の証拠: 図 2 に示すように、問題は関数 dgwrite におけるメモリ割り当てのインスタンス（getbuf の呼び出し）から始まる。dgwrite のパスは二つのグループに分かれる。対応する freebuf のあるパスと、割り当てられたメモリへのポインタがパラメータとして関数 udpsend に渡されるパスである。パラメータの受け渡しは、エッジラベル par を持つ dgwrite から udpsend へのエッジで示される。

dgwrite の割り当ての認証証拠。ポインタは par エッジによって udpsend、ipsend、route、write、ethwrite、ethwstrt を通って移動し、freebuf の対応は dgwrite、route、ethinter に現れ、write は fpc エッジで ethwrite を呼び出し、ethwstrt と ethinter はグローバル変数 dcmptr を共有し、ethinter からは四つの PFC エッジが出ている。
図 2. dgwrite における割り当てのインスタンスに対する CE スキーマを用いた証拠

図 2 に示した CE の証拠によれば、検証は次の手順を経ている。

  1. udpsend のパスは一つのグループに分かれ、割り当てられたメモリへのポインタはパラメータとして udpsend から ipsend に渡される。
  2. ipsend のパスは一つのグループに分かれ、割り当てられたメモリへのポインタはパラメータとして ipsend から route に渡される。
  3. route のパスは二つのグループに分かれる。一方のグループのパスに沿って、割り当てられたメモリへのポインタはパラメータとして route から write に渡され、もう一方のグループのパスに沿って、対応する freebuf がある。
  4. write のパスは一つのグループに分かれ、割り当てられたメモリへのポインタはパラメータとして write から ethwrite に渡される。write は関数ポインタを用いて ethwrite を呼び出す。関数ポインタによる呼び出しは、エッジラベル fpc で表される。
  5. ethwrite のパスは一つのグループに分かれ、割り当てられたメモリへのポインタはパラメータとして ethwrite から ethwstrt に渡される。
  6. ethwstrt のパスは一つのグループに分かれ、割り当てられたメモリへのポインタはグローバル変数 dcmptr に代入される。関数 ethinter はそのグローバル変数を読む。
  7. ethinter のパスは五つのグループに分かれる。一つのグループのパスには対応する freebuf がある。他の四つのグループのパスには対応する freebuf がなく、割り当てられたメモリへのポインタは他のどの関数にも伝えられない。これら四つのグループのパスには、エッジラベル PFC で表されるように、パスの実行可能性の検査が必要である。

パスの実行可能性の検査: ミクロな証拠を捉える、コンパクトで理解しやすい抽象として、射影制御グラフ（PCG）[34] を用いることを提案する。PCG は、関連する振る舞いと、実行可能性の検査に関連する条件を捉える。制御フローグラフ（CFG）は、検証の目的からすると、無関係な多くの条件と、関連する振る舞いが同一の多数のパスを持ちうる。一方 PCG は、関連する振る舞いごとに一つのパスしか持たず、関連する条件だけを捉える。

ethinter の PCG を図 3(a) に示す。これはパスの六つのグループを示す。二つのグループのパスには対応する freebuf があり（図 2 では一つにまとめている）、実行可能性の検査が必要な他の四つのグループのパスには、図 3(a) で 1 から 4 の番号を付けている。パスの実行可能性の検査に関連する条件は PCG によって捉えられる。表形式の表記法を用いたパスの実行可能性の条件の等価な表現を、図 3(b) に示す。四つのグループのパスはいずれも実行可能性の検査が必要だが、対応する関連する条件が同じではなく、したがって実行可能性の検査が実際には異なるので、別々のパスとして保たれている。

分岐条件 C1 から C5 と、二つの freebuf の呼び出しを含む結果のパス 1 から 4 を持つ ethinter の射影制御グラフと、関連する振る舞いごとにそれらの条件の T、F、星印の値を示す表。
図 3. ethinter のミクロな証拠

関数の間のデータと制御の関係: この例は、関数の間の三つのデータの関係のうち二つ、すなわちパラメータの受け渡しとグローバル変数を明らかにする。また、関数の間の三つの制御の関係すべてを示す。関数が名前で呼び出されること、関数が関数ポインタを用いて呼び出されること、そして二つの関数の間の非同期の制御である（制御はコンテキストスイッチによって ethwstrt から ethinter に渡される。ethinter は割り込み駆動の関数である）。

2.4 CE スキーマの適用可能性

CE スキーマは、安全性とセキュリティの性質の検証によく適している。多くの安全性とセキュリティの性質は、それらがもたらす解析と検証の課題の点で似ている。典型的な安全性の性質は次のように述べられる。すべての実行可能な実行パスで、イベント e1(O) の後にイベント e2(O) が続くことを検証する。ここで二つのイベントは同じオブジェクト O に対する操作である（例えば、lock の後には unlock が続かなければならない）。典型的なセキュリティの性質は次のように述べられる。すべての実行可能な実行パスで、イベント e1(O) の後にイベント e2(O) が続かないことを検証する。ここで二つのイベントは同じオブジェクト O に対する操作である。例えば、機密性の性質は、どの実行可能な実行パスでも、機密性の高いソースの後に悪意のあるシンクが続いてはならないというものである。このような安全性とセキュリティの性質を 2 イベントの対応付けと呼ぶ。第 4 節の事例研究には、ロックとアンロックの対応（LUP）とメモリリーク（ML）が含まれる。

一般的な応用として、CE スキーマは有限状態機械（FSM）で定義された性質、すなわちすべての実行可能な CF パスで、FSM が定義する受理の判定に従うイベントの出現を検証する性質の検証の証拠を示すのに役立つ。

2.5 CE スキーマの強み

CE スキーマは、認証機関が容易に理解できる証拠に焦点を当てることで、数学的解析の認証を実用的なものにする。証拠は、数学的解析がどのように動作するかではなく、何を達成したかに焦点を当てる。理解しやすい証拠を作るには、何をに焦点を当てることが重要である。例えば、素因数分解アルゴリズムが正しいことを認証するには、それが生成する素因数を証拠として与えればよい。素因数分解アルゴリズムの正しさを理解するには、数論の専門家である必要があるかもしれない。しかし、それらがどのように生成されたかを知らなくても、与えられた素因数が正しいことは容易に検査できる。

CE スキーマは、証拠の簡潔な視覚的表現を提供する。構造化されたグラフィカルな表現を用いて、証拠を視覚的な形で示す。よく構造化された安全性の論証はしばしば文章で与えられるが、文章が複雑な論証を表現する唯一の媒体である場合には問題が生じる [23]。安全性の論証にはグラフィカルな表記法が望ましい [23]。

CE スキーマは、数学的検証が正しいと納得させるうえで重要な役割を持つソフトウェアの側面を簡潔に反映する。数学的証明と実行時のソフトウェアの振る舞いとの対応を提供する。多数のソフトウェアの成果物と関係の中から、認証の目標に関連する振る舞いを制御する要素だけを抽出する。そうすることで、数学的解析のためのモデルと実際のソフトウェアとの間の隔たりを埋める。これは、実行時にソフトウェアを動かす必要なしに、数学的解析を準拠のために用いる場合に特に重要である。

CE スキーマは、テストを数学的検証で置き換えるための論証の構築によく適している。DO-178C [10] と UK Def Stan 00-56 [32] の両規格は、検証と妥当性確認の手法がなぜ、どのように認証の目標を達成するのかについて、根拠のある正当化を提出することを求める。実際には、根拠のある正当化を生み出すための支配的な手法はテストである。テストの品質は、要求カバレッジと構造カバレッジという二つのカバレッジの尺度で判断される。CE スキーマには、すべての CF パスのカバレッジとその実行可能性についての証拠が含まれる。

CE スキーマは、ディペンダビリティケースにセキュリティの考慮を含めるのによく適している。セキュリティの脆弱性は、ソフトウェアのディペンダビリティの性質について示された論拠を損ないうる。したがって、ディペンダビリティケースは、その他の側面を損ないうるセキュリティのリスクを明示的に考慮しなければならない。また、セキュリティの認証が攻撃への耐性について意味のある保証を与えることを確かにすることも重要である。一般に、テストはソフトウェアのセキュリティを保証するには十分でない。最大規模のテストスイートでさえ、ソフトウェアに脆弱性がないという証拠を与えるのに十分なパスを動かさないからである。CE スキーマは、CF パスがどのようにカバーされるかを示せる証拠に焦点を当てる。

CE スキーマには、他にもいくつかの望ましい特性がある。第 4 節の事例研究を通じて、これらの特性のいくつかを明らかにする。CE スキーマは、数学的解析を改善するための洞察を与えうる証拠を生成する。セキュリティや安全性の性質には、検証が必要な何千ものインスタンスがありうる。それほど多くのインスタンスを一つずつ調べるのは、認証機関にとって負担が大きすぎる。CE スキーマは、証拠の類似性に基づいてインスタンスを分類することを可能にする。何千ものインスタンスを少数の区分にまとめ、個々のインスタンスではなく区分に基づいて認証できれば、認証機関の作業ははるかに少なくなる。CE スキーマは網羅的な証拠を探すよう設計されているので、証拠が完全かどうかの判断に役立ち、したがって安全性の論証を行う際の落とし穴を避けるのに役立つ。

2.6 CE スキーマの限界

CE スキーマは現在、ハードウェアとソフトウェアの協調設計の欠陥から生じうる検証の問題を裏付ける証拠を含まない。例えば、CE スキーマには、リアルタイム組込みシステムの時間と空間の要求を裏付ける証拠は含まれない。これらは、航空電子機器、自動車、医療、その他のセーフティクリティカルなシステムにとって重要な要求である。European Space Agency は COMPASS プロジェクト（Correctness, Modeling, and Performance of Aerospace Systems）[5] を立ち上げた。その目標は、システムズエンジニアリングのレベルでシステムを開発するための、一貫した学際的な手法を開発することである。COMPASS プロジェクトは、Architecture and Analysis Design Language（AADL）とその Error Model Annex [2] を主要な形式手法として採用している。したがって、AADL のモデルに基づく証拠を組み込むよう CE スキーマを拡張することは、取り組む価値のある課題である。

3 関連研究

現代のシステムでソフトウェアがますます大きな役割を担うにつれて、「正しいコード」には開発者の主張以上のものが必要になっている [1]。企業は、ソフトウェアの障害による高額な現場サポート、製品のリコール、法的措置を避けたいと考えている。同時に、ソフトウェアの適格性確認と認証については多くの俗説がある [1]。

多くの論文 [11, 18–20, 22, 31] で論じられているように、ソフトウェアの認証には特別な考慮が必要である。それは、ソフトウェアの成果物が特定の性質に適合しているかどうかに関わる。適合の目的のため、Heck et al. [20] は次の性質の区分を述べている。(a) 一貫性: ソフトウェアの成果物（の各部分）は互いに適合しているか。(b) 機能: システムへの入力は期待される出力を生み出すか。(c) 振る舞い: システムはデッドロックがないことのような一般的な安全性の性質を満たすか。(d) 品質: 成果物は、性能、セキュリティ、使いやすさの分野で非機能要求を満たすか。(e) 準拠: 成果物は規格、ガイドライン、法令に適合しているか。この区分には改良が必要だが、よい出発点である。

Rushby は 1996 年の論文 [15] で次のように述べた。「長年の研究にもかかわらず、主流のソフトウェア設計に対する形式手法の全体的な影響は期待外れであった。対照的に、形式手法は商用のハードウェア設計では実際に浸透し始めている。」この状況は引き続き懸念されており、形式手法がなぜもっと広く使われないのかについて多くの記事が書かれている [15, 24, 25, 30]。

新しい規格 DO-178C [10] には、DO-333 として知られる形式手法の補足があり、次のように述べている。形式手法は、少数の目標に部分的に対処するためにごく選択的に使われることもあれば、開発と検証に関わる多くの目標を満たすための主要な証拠の源となることもある。全体として、ソフトウェアの認証に形式手法を用いることへの関心は高まっている [12, 17, 21, 28]。

Parnas は次のように述べている [29]。「ソフトウェア設計は工学である。技術者は仕事の多くで日常的に数学を使う。ソフトウェア設計者も同じようにすべきである。現場のソフトウェア技術者に提供される数学的手法はあまり実用的でなく、工学で使われる数学とはあまり似ていない。」プログラム検証と数学における証明についての画期的な論文 [13] で、De Millo、Lipton、Perlis（最初のチューリング賞受賞者）は、プログラム検証のためのツールは検証を裏付ける証拠を提供しなければならないと論じている。ミッションクリティカルなシステムのためのソフトウェア保証の必要性が高まるにつれ、証拠を伴う自動検証への関心が新たに高まっている [9]。

本論文で示すアイデアは、DARPA のサイバーセキュリティのプログラム APAC [3] と STAC [7] での我々の研究に由来する。複雑なソフトウェアセキュリティの問題について推論するためのグラフィカルな手法 [14] に関する我々の研究が、本論文で示す CE スキーマにつながった。

4 事例研究

CE の証拠の重要性をいくつかの異なる形で明らかにするため、Linux カーネルと Bftpd ソフトウェア [4] の事例研究を示す。

4.1 Linux カーネルの事例研究

検証実験は、(a) ロックとアンロックの対応（LUP）と (b) メモリリーク（ML）についてのものである。どちらの事例研究にも、合計 3,700 万行のコードからなる三つの Linux のバージョンの検証が含まれる。allmodconfig フラグによって、可能なすべての x86 のビルド構成を有効にした。検証実験は、LDV [6] と EV [27] のモデル検査器を用いて行った。

解析したインスタンスは、安全と検証済み、安全でないと検証済み、不完全な検証に分類される。LDV には追加の区分として潜在的なバグがある。LDV は安全でないインスタンスに対して反例を生成する。LDV は、安全なインスタンスの検証を裏付ける証拠を生成しない。不完全なインスタンスに対して LDV が生成するトレースは膨大で、理解するのが難しい。

この研究は、LDV と EV のモデル検査器の性能の違いを示す。LDV は確実なバグを一つも報告しない。興味深いことに、EV が見つけた Lock のバグの一つは、実際には LDV が誤って安全と検証したインスタンスである。このバグは論文 [26] で述べられている。EV は、安全なインスタンスを含むすべてのインスタンスについて証拠を生成する。安全なインスタンスの証拠は、認証にとって極めて重要である。

当初、我々は LUP と ML の問題は本質的に同じであると推測していた。どちらも、同じオブジェクトについて、実行可能な実行パスでイベント e1 の後にイベント e2 が続くことを求める。しかし、そうではない。LDV と EV はどちらも ML の問題では性能が低い。その違いは EV で特に顕著である。EV は LUP のインスタンスの 99.3% を検査できるが、ML のインスタンスは 37.5% しか検査できない。EV が生成する証拠は、失敗についての洞察を得てモデル検査器を改善するうえで非常に価値がある。失敗の分析と改善の目標は [33] で示している。

LUP の結果を表 1 に示す。最後の 2 行は、それぞれ三つのバージョンすべての合計と累積の割合を示す。EV が検証した Lock のインスタンスが 99.3% であることからわかるように、EV は LDV より大幅に優れた性能を示す。また、EV は LDV が見逃したバグを見つける。EV は、LDV が報告した多数の潜在的なバグが実際にはバグでないことを示す。

表 1. ロックとアンロックの対応に対する EV と LDV の検証結果
カーネルロックの
種類		ロックの
インスタンス		EVLDV
安全安全でない不完全な
検証		安全安全でない潜在的な
バグ		不完全な検証
クラッシュタイムアウト合計
3.17-rc1Mutex788778131735494091120011022302
Spin141801409718289620366218826644852
3.18-rc1Mutex7893780109254270982283852368
Spin14265141883749152038342364944730
3.19-rc1Mutex79917938152552701032272892361
Spin14393143142779204035843624694831
合計66609661518450437660139916541490321444
分布100.0%99.3%0.01%0.7%65.7%0.0%2.1%24.8%7.4%32.2%

メモリリークの問題の検証結果を表 2 に示す。バージョン（3.17-rc1）には 12.3 MLOC と 571, 012 個の関数がある。表 1 で報告した他の二つのバージョンは、メモリ割り当てのインスタンスの大部分について LDV と EV のツールに検証を完了させることに大きな困難があったため、検証しなかった。

表 2. メモリリークに対する EV と LDV の検証結果（Linux カーネル 3.17-rc1）
カーネルkmalloc の
インスタンス		EVLDV
安全安全でない不完全な
検証		安全安全でない潜在的な
バグ		不完全な検証
クラッシュタイムアウト合計
3.17-rc129631060501853357072055713291886
分布35.8%1.7%62.5%12.0%0.0%24.3%18.8%44.9%63.7%

認証を容易にするための証拠の利用: CE スキーマを用いて生成した証拠は、認証機関の労力を減らせる。簡潔な視覚的証拠は確実に労力を減らす。さらに、証拠が労力の削減に役立つ方法は他にもある。この事例研究では、労力を減らす一つの方法を示す。

Linux の事例研究からわかるように、安全性やセキュリティの性質には何千ものインスタンスがありうる。各インスタンスを検証しなければならない。インスタンスには、さまざまな種類と程度の難しさがありうる。認証のためには、似た難しさを持つインスタンスを分類することに意味がありうる。この分類は認証機関の労力を大幅に減らし、したがって数学的解析の利用を後押しできる。

第一の分類は、CF パスの実行可能性の検査が必要かどうかと、その検査の難しさである。これにより、実行可能性の検査が必要なインスタンスが切り分けられる。実行可能性の検査は、(i) 手続き内、すなわち関連する条件が一つの関数内にあるもの、または (ii) 手続き間、すなわち関連する条件が複数の関数にまたがるものである。手続き内の区分は、さらに容易と複雑に細分される。容易とは、SMT ソルバーを使わずに、いくつかの簡単な規則を用いるだけで実行可能性の検査が完了することを意味する。第二の分類は、検証が手続き内か手続き間かである。

表 3. 実行可能性の検査が必要な LUP のインスタンスの分布
カーネルロックの
種類		ロックの
インスタンス		手続き内手続き間パスの
実行可能性
が必要		手続き内の実行可能性の検査手続き間の
実行可能性
の検査
容易複雑合計
3.17-rc1Mutex78877,6891986676261063631
Spin1418013,3957851921621417616
3.18-rc1Mutex78937,6722216415931360635
Spin1426513,5077581961631317620
3.19-rc1Mutex79917,810181681653665922
Spin1439313,6337601911631217516
合計6660963,7062,9032,5682,360682,428140
分布100.0%95.6%4.4%3.8%3.5%0.1%3.6%0.2%

表 3 の結果は二つの分類を示す。調べた Linux のバージョンで手続き間の検証が必要な LUP のインスタンスは 4.4% にすぎないことに注意する。複雑な手続き内のパスの実行可能性の検査が必要な LUP のインスタンスは 0.1%、手続き間のパスの実行可能性の検査が必要な LUP のインスタンスは 0.2% にすぎない。

4.2 Bftpd の事例研究

Bftpd は、デスクトップ、サーバー、組込み機器、メディアセンターで広く使われている軽量な FTP サーバーである。2019 年の論文 [16]3 は、Bftpd [4] のバージョン 4.6 におけるメモリリークを報告した。論文 [16] は、これは攻撃者がサービス拒否攻撃を仕掛けるのに利用できる深刻度の高い脆弱性であると述べている。この脆弱性には CVE ID（CVE-2017-16892）が割り当てられ、Bftpd の開発者はパッチを公開した。

3 この論文は SAT ソルバーを用いたメモリリークの検出に関するものであり、2019 年 5 月の第 41st 回 International Conference on Software Engineering で Distinguished Paper Award を受賞した

この事例研究では、CE スキーマを用いることで、論文 [16] が見落とした決定的な証拠が得られることを示す。決定的な証拠は、論文における CVE についての論証が誤っており、検出されたメモリリークが偽陽性であることを示す。決定的な証拠と、それが論文 [16] の論証にどう反論するかを説明する。

論文 [16] は、次のメモリリークを論じている。関数 command_rnto は関数 bftpd_cwd_mappath を呼び出し、bftpd_cwd_mappath はメモリを割り当て、割り当てたメモリへのポインタを command_rnto に返す。図 4(b) の PCG に示すように、command_rnto は番号 3 のパスで割り当てられたメモリを解放しない。論文 [16] は、パス 3 は実行可能であり、したがってメモリリークであると主張している。

では、上の論証の問題を明らかにする決定的な証拠の最初の部分に移る。CE スキーマによれば、bftpd_cwd_mappath を呼び出すすべての関数 f は、割り当てられたメモリへのポインタを受け取るので関連する。図 5 に示すように、EV のモデル検査器はそのような関数を 14 個挙げる。これらの関数はそれぞれメモリリークを生じうるので、それぞれ検証しなければならない。論文 [16] は、そのような関数の一つ、すなわち command_rnto について論じている。bftpd_cwd_mappath を呼び出すもう一つの関数 command_rnfr を調べると、図 4(a) の PCG に示すように、番号 1 と 2 のパスでやはりメモリリークがある。この時点では、論文 [16] はこのもう一つのリークを見落としたように見える。しかし、次の証拠は論証に興味深いひねりを加える。

次の決定的な証拠は、メモリリークが偽陽性であることを示す。紙幅の制約のため、論証に興味深いひねりを加える次の決定的な証拠の一部だけを示す。bftpd_cwd_mappath を呼び出す 14 個の関数は、それ自体が関数 parsecmd（コマンドの解析）によって関数ポインタを用いて呼び出される。例えば、コマンド RNTO（rename to）を解析すると、parsecmd は command_rnto を呼び出す。この parsecmd 関数には、実行が許されるコマンドの列を規制する FSM が含まれる。FSM は次のプロトコルを保証する。FTP クライアントは、名前を変更する元のファイル名を指定する RNFR（rename from）コマンドを発行し、その後に新しいファイル名を指定する RNTO（rename to）コマンドを発行しなければならない。RNTO の前に RNFR がなければ、parsecmd は RNTO を実行する代わりにエラーメッセージを出す。この規制により、論文 [16] で報告されたメモリリークは防がれる。RNTO の前に RNFR が呼ばれるなら、図 4(b) の番号 3 のパスは実行可能でなく、したがって報告されたメモリリークは起こりえないからである。開発者が追加したパッチは、実際には望ましくない副作用を持つ。

並べて示した射影制御グラフ。左の command_rnfr は bftpd_cwd_mappath で割り当てを行いパス 1 から 4 に分かれ、右の command_rnto は同じように割り当てを行いパス 1 から 3 に分かれ、パス 3 は対応付けられたポインタの解放を飛ばす。
図 4. 関数の PCG: (a) command_rnfr、(b) command_rnto
command_rnfr、command_rnto、bftpd_cwd_chdir を含む 14 個のコマンド関数が bftpd_cwd_mappath につながり、bftpd_cwd_mappath は malloc につながり、その下に free が示されている。
図 5. 関数 bftpd_cwd_mappath におけるインスタンスのマクロモデルの証拠

まとめると、CE スキーマは網羅的な証拠を探すよう設計されているので、証拠が完全かどうかの判断に役立ち、したがって安全性の論証を行う際の落とし穴を避けられる。証拠の完全性は、明らかに認証にとって重要な考慮事項である。

.

5 結論

ソフトウェアモデル検査とは、プログラムの実行の性質を証明するためのプログラムのアルゴリズム的な解析である。本論文は、認証を目的として証拠を示すための認証証拠（CE）スキーマを導入する。簡潔な表現のため、このスキーマはミクロな証拠とマクロな証拠を統合する。ミクロな証拠は、検証のために関数内の制御フローパスがさまざまなグループに分けられることを示す。マクロな証拠は、検証のために関数の間の相互作用を示す。

本論文は、Linux カーネルの事例研究と、Bftpd ソフトウェアにおける深刻度の高いメモリリークの脆弱性（CVE-2017-16892）に関する事例研究を示す。これらの事例研究は、大規模な実世界のソフトウェアを検証するうえでの CE スキーマの適用可能性と重要性を示す。

参考文献

  1. 11 myths about software qualification and certification. https://www.electronicdesign.com/embedded/11-myths-about-software-qualification-and-certification
  2. Aadl error model annex. https://www.sae.org/standards/content/as5506/1a/
  3. Automated Program Analysis for Cybersecurity (APAC). https://www.fbo.gov/spg/ODA/DARPA/CMO/DARPA-BAA-11-63/listing.html
  4. Bftpd: Ftp server. http://bftpd.sourceforge.net/
  5. The compass project. http://www.compass-toolset.org/
  6. Linux driver verification (LDV) tool. http://linuxtesting.org/project/ldv
  7. Space/Time Analysis for Cybersecurity (STAC). https://www.fbo.gov/spg/ODA/DARPA/CMO/DARPA-BAA-14-60/listing.html
  8. XINU. http://en.wikipedia.org/wiki/XNU
  9. Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: exchanging verification results between verifiers. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 326–337. ACM (2016)
  10. Brosgol, B., Comar, C.: Do-178c: A new standard for software safety certification. Tech. rep., ADA CORE TECHNOLOGIES NEW YORK NY (2010)
  11. Brown, D., Delseny, H., Hayhurst, K., Wiels, V.: Guidance for using formal methods in a certification context (2010)
  12. Council, N.R., et al.: Software for dependable systems: Sufficient evidence? National Academies Press (2007)
  13. De Millo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Communications of the ACM 22(5), 271–280 (1979)
  14. Deering, T., Kothari, S., Sauceda, J., Mathews, J.: Atlas: a new way to explore software, build analysis tools. In: Companion Proceedings of the 36th International Conference on Software Engineering. pp. 588–591. ACM (2014)
  15. Dill, D.L., Rushby, J.: Acceptance of formal methods: Lessons from hardware design. IEEE Computer 29(4), 23–24 (1996)
  16. Fan, G., Wu, R., Shi, Q., Xiao, X., Zhou, J., Zhang, C.: Smoke: scalable path-sensitive memory leak detection for millions of lines of code. In: Proceedings of the 41st International Conference on Software Engineering. IEEE Press (2019)
  17. Galloway, A., Paige, R.F., Tudor, N., Weaver, R., Toyn, I., McDermid, J.: Proof vs testing in the context of safety standards. In: 24th Digital Avionics Systems Conference. vol. 2, pp. 14–pp. IEEE (2005)
  18. Garnacho, M., Périn, M.: Convincing proofs for program certification. Electronic Notes in Theoretical Computer Science 238(4), 41–56 (2009)
  19. Habli, I., Kelly, T.: A generic goal-based certification argument for the justification of formal analysis. Electronic Notes in Theoretical Computer Science 238(4), 27–39 (2009)
  20. Heck, P., Klabbers, M., van Eekelen, M.: A software product certification model. Software Quality Journal 18(1), 37 (2010)
  21. Heitmeyer, C.L.: On the role of formal methods in software certification: An experience report. Electronic Notes in Theoretical Computer Science 238(4) (2009)
  22. Kelly, T.: A systematic approach to safety case management. Tech. rep., SAE Technical Paper (2004)
  23. Kelly, T., Weaver, R.: The goal structuring notation–a safety argument notation. In: Proceedings of the dependable systems and networks 2004 workshop on assurance cases. p. 6. Citeseer (2004)
  24. Knight, J.C.: Challenges in the utilization of formal methods. In: International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. pp. 1–17. Springer (1998)
  25. Knight, J.C., DeJong, C.L., Gibble, M.S., Nakano, L.G.: Why are formal methods not used more widely? In: Fourth NASA formal methods workshop. Citeseer (1997)
  26. Kothari, S., Tamrawi, A., Mathews, J.: Human-Machine Resolution of Invisible Control Flow. In: Proceedings of the twenty-fourth IEEE International Conference on Program Comprehension (2016)
  27. Kothari, S., Awadhutkar, P., Tamrawi, A., Mathews, J.: Modeling lessons from verifying large software systems for safety and security. In: Proceedings of the 2017 Winter Simulation Conference. pp. 109:1–109:12. WSC ’17, IEEE Press, Piscataway, NJ, USA (2017), http://dl.acm.org/citation.cfm?id=3242181.3242297
  28. Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B.: Testing or formal verification: Do-178c alternatives and industrial experience. IEEE software 30(3) (2013)
  29. Parnas, D.L.: Mathematical methods: What we need and dont need. IEEE Computer 29(4), 28–29 (1996)
  30. Parnas, D.L.: Really rethinking. Computer (1), 28–34 (2010)
  31. Schiller, C.A.: The software certification process. http://www.ittoday.info/AIMS/DSM/82-01-17.pdf, accessed on: Jun 19, 2019
  32. Stan, D.: Stan 00-56. Safety Management Requirements for Defence Systems, UK Ministry of Defence, Defence Standard 00-56 (2) (1996)
  33. Tamrawi, A., Awadhutkar, P., Ram Santhanam, G., Mathews, J., Le, W., Kothari, S.: A study of linux verification: Where can automated program analysis help? In: submitted to the 34th IEEE/ACM international conference on Automated software engineering
  34. Tamrawi, A., Kothari, S.: Projected control graph for computing relevant program behaviors. Science of Computer Programming 163, 93–114 (2018)