はじめに
こんにちは。
本記事は、2024年12月のアドベントカレンダー「Space ROS」に投稿された一連の記事の１つです。
今回は、NASAが作った C/C++ の静的解析ツール IKOS の解説記事、＜基本編＞です！
（実践編はコチラ）
この記事でわかること
- IKOS とは何か
- Abstract Interpretation（抽象解釈）とは何か
目次
- IKOS とは
- IKOS と Space ROS
- IKOS の機能
- Abstract Interpretation とは
- 参考リンク集
IKOS とは
IKOS は、実行時のエラーを無くすことを目的とする、オープンソースのC/C++の静的解析ツールです（ｶｯｺｲｲ）。
IKOS は、Inference Kernel for Open Static Analyzers の略称です（ｲｶｼﾃﾙ）。
IKOS は、Abstract Interpretation（抽象解釈） をベースとした理論に基づいています（ﾅﾝｼﾞｬｿﾘｬ）。
また、IKOS は sound です（ﾄﾞﾕｲﾐ?）。
何を言っているかわかりませんね。この記事を読めば、それがわかります。
概要を理解するだけなら、難しくありません。
IKOS と Space ROS
解説の前に、Space ROSとの関係をお話しします。
IKOS は、Space ROSに標準装備される予定です1。
予定と言っているのは、まだ正常に使えるよう組み込まれていないためです。
一応、Space ROSには既にIKOSが組み込まれていますが、使おうとしてもエラーが発生します。2
IKOSは、amentベースのビルドおよびテストシステムに統合された状態でSpace ROSに組み込まれており3、Space ROSで作成されたアプリケーションのビルドまたはテスト時にIKOSによる静的解析を実行できるようになっています。
Space ROS は IKOS の力を使うことで、宇宙製品に求められる高水準4を満たすことができるようになります！
それがオープンソースで、NASAの人たちによって作られています。素晴らしい。。
みなさんも、IKOSに興味がわいてきたのではないでしょうか。そして、Space ROSでロボット（さらに言えば宇宙ロボット）を動かしたくなってきたのではないでしょうか。
IKOS の機能
解析対象
IKOSは以下の形式のファイルを解析することができます。
.c.cpp.bc
.bcとは、LLVMのbitcodeファイルのことです5。C/C++のソースファイルから生成された.bcファイルを解析することもできるというわけです。
解析項目
解析項目を以下に列挙します。
| 解析項目 | 説明 |
|---|---|
| バッファオーバーフロー解析 | バッファオーバーフローや配列外アクセスの検出 |
| ゼロ除算解析 | ゼロによる整数除算の検出 |
| ヌルポインタ解析 | ヌルポインタの逆参照の検出 |
| 未アラインポインタ解析 | 未アラインのポインタ逆参照の検出 |
| 未初期化変数解析 | 未初期化変数の読み取りの検出 |
| 符号付き整数オーバーフロー解析 | 符号付き整数のオーバーフローの検出 |
| 符号なし整数オーバーフロー解析 | 符号なし整数のオーバーフローの検出 |
| シフトカウント解析 | 不正なシフト操作の検出（シフト量がオペランドのビット幅以上またはゼロ未満の場合） |
| ポインタオーバーフロー解析 | ポインタの算術オーバーフローの検出 |
| ポインタ比較解析 | 異なるオブジェクトを参照するポインタ間の比較の検出 |
| 健全性解析 | 解析の健全性（バグの見落とし）を損なう可能性のある命令の検出 |
| 関数呼び出し解析 | 不正な型を持つ関数ポインタ経由の関数呼び出しの検出 |
| deadコード解析 | 到達不能なコードの検出 |
double free 解析 |
二重free、不正なfree、解放後のfree、リターン後のfreeの検出 |
| デバッガ | プログラム実行中の変数の値や不変条件（invariant）を出力してデバッグを支援 |
| メモリ監視 | 指定されたメモリアドレスに対して行われる書き込み操作を監視し、その詳細を出力 |
| soundness 解析 | 解析結果が不完全になり得るコードパスや命令を検出（IKOS がバグを見逃すリスクを特定） |
最後の soundness が気になると思いますが、後半の Abstract Interpretation の章で説明します。
解析結果の分類
IKOSはコードのそれぞれの文に対して解析を実施し、それぞれに対して以下のいずれかの判定を下します。
| 分類 | 意味 |
|---|---|
| safe | 安全 |
| error | その文で必ずエラーになる、または実行されない。 |
| unreachable | その文は実行されない |
| warning | その文でエラーになる場合がある。 または結論を出すための情報が不足している。 またはエラーが起こらないことを証明できない。 |
IKOS のコマンド
IKOSはコマンドで実行される。
単一ファイルを解析する場合
ikos <filename>
でよい。
複数のファイルから成るパッケージ全体を解析する場合
この場合、ビルドコマンドの前に ikos-scan を付けるだけです。
例えば以下のように。
ikos-scan make
ikos-scan colcon build
仕組みとして、ikos-scan コマンドは、環境変数CCとCXXを上書きしてコンパイラコマンドをインターセプトすることで動作します。
このプロセスでビルドをしながら.bcファイルが生成され、ビルド後にさまざまな解析を実行します。
解析時の生成物
ikosまたはikos-scanコマンドを実行すると、output.dbファイルが生成されます。
これは、ikos-reportコマンドを使えばターミナル上で指摘事項を確認することができ、あるいは ikos-viewコマンドを使えばブラウザ上で指摘事項を確認することができます。
ikos-report output.db
ikos-view output.db
Abstract Interpretation とは
IKOS は Abstract Interpretation（抽象解釈）という理論に基づいています。
以下では、読者のあなたに、Abstract Interpretation のなんとなくのイメージを手に入れていただくことを目標として、初歩の初歩を説明していきます。
【ストレスなく理解するためのヒント】
初めから完全に理解しようとせず、もやもやしたイメージを抱いている程度の状態でも、一度最後まで読んでみてください。
静的解析ツールが目指すこと
あるプログラムについて、そのプログラムが実行されている任意の時刻 $t$ において
\boldsymbol{x}(t) \equiv (\ \text{入力変数}(t),\ \text{状態}(t),\ \text{出力変数}(t)\ )
を定義すると、この $\boldsymbol{x}(t)$ は時刻$t$におけるプログラムの「状態」を表します。
以下のC言語で書かれたプログラム example.c を例に挙げてみましょう。
#include <stdio.h>
int main(){
int a = 1;
int b = 2;
int c = a + b;
printf("a + b = %d\n", c);
return 0;
}
このプログラムにおける$\boldsymbol{x}(t)$とは、例えば
\boldsymbol{x}(t) = (\text{aの値}(t),\ \text{aのメモリアドレス}(t),\ \text{aのサイズ}(t),\ \text{標準出力バッファの内容}(t),\ ...)
と、プログラムの動作に関わるパラメタのことです。
状態変化 $\boldsymbol{x}(t)$のイメージを図１に示します。１つの線が１つのプログラムの１回の実行を表しています。
図１：さまざまなプログラム実行時の状態変化 $\boldsymbol{x}(t)$（→経路と呼ぶことにする）
図を見たときの直観に一致するよう、本記事では図上の線、つまり状態変化 $\boldsymbol{x}(t)$のことを「経路」と呼ぶことにしましょう。
静的解析ツールが目指す理想の目標とは、『その静的解析ツールが対象とするあらゆるプログラムの全ての状態変化 $\boldsymbol{x}(t)$（あらゆる経路上）で起こりうる危険6を検出すること』です。7
※ 以降、「危険」のことを「エラー」と呼びます（わかりやすさのため）。
解析の理想と現実
しかし、$\boldsymbol{x}(t)$の場合の数は、数学的に無限ではないものの、計算不可能という意味で無限です。全ての状態変化 $\boldsymbol{x}(t)$を調べることはできません。
だからといって、解析対象のプログラムを実行して調べることは本末転倒です。
そこで、プログラムを実行せずにできるだけ正確にエラーを検出する手法を考案したいわけです。
そのための理論の１つが、Abstract Interpretation です。
Abstract Interpretation の第一歩
無限の経路があって、一つ一つを調べていくことができないのに、いったいどうやってエラーの有無をチェックすればよいのでしょうか。
ここで、先ほどの図１がイメージを手助けしてくれます。
図１において、エラーが発生している状態$\boldsymbol{x}(t)$の領域を塗りつぶしてみましょう。
ただし、今回は全ての線が１つの特定プログラムが辿る経路とします。
図２：エラーが発生する領域を黄色く塗りつぶした。橙色の経路はエラー発生領域に侵入しているため、この経路が実行された場合はエラーが発生する。
こうやって塗りつぶしたことで、静的解析ツールの目標は次のように言い換えることができます：
『エラー発生領域に侵入する経路があれば、それを検出する。または、どの経路もエラー発生領域に侵入しないかどうかを判定する。』
では、エラー発生領域に各経路が侵入していないかどうかを調べるために、図３のようなことを考えてみましょう。
図３：Abstract Semantics をピンク色で図示したもの。
ピンク色は、このプログラムの全ての経路を含む領域です。
この領域のことを Abstract Semantics といいます8。
１本１本の線がどのような経路をたどるかわからなくても、ピンク色の Abstract Semanticsがエラー発生領域と重複するかどうかさえ調べれば、少なくともそのプログラムがエラーを発生させるかどうかはわかります。
Abstract Interpretation は、図３のピンク色の Abstract Semantics について考えます。
Abstract Semantics のイメージを持つことが、Abstract Interpretation を理解するための第一歩です。
どうやって Abstract Semantics を得るか
Abstract Semantics を調べることでコード解析ができることがわかりました。
ならば、次の興味は、「どうやって Abstract Semantics を得るか？」でしょう。
しかし、それについて語ろうとすると、この記事に書くにはヘビーになってしまうため、ここでは触れません。
より詳しく知りたい方は、コチラのサイトがおすすめです。末尾の参考リンク集でも言及していますが、Abstract Interpretationの創始者さんによる説明を読むことができます。
最後に、Abstract Semanticsに要求される性質の説明をして、Abstract Interpretationの説明を締めくくります。
Abstract Semantics が満たすべき性質
Abstract Semantics は、"適切に" 作らなければなりません。
"適切な" Abstract Semanticsとは、次の２つの性質を満たしているものを言います9。
① 全ての経路を含んでいる（漏れがない）
② エラーを誤検出しない1011
ちなみに、①の性質を満たしているものを "sound" という形容詞で表します。
IKOS は sound です！
以下の折りたたみ内で、①と②を図示しておきます。補助資料としてご覧ください。
不適切なAbstract Semanticsのイメージ
下図に、①の意味で不適切な（＝soundでない）Abstract Semantics を示します（図３と同じです）。
図：ピンク色のAbstract Semanticsは、全ての経路を含んでいる。これがsoundということです。
下図に、②の意味で不適切なAbstract Semantics を示します。
図：正しくはエラー発生しないところで Abstract Semanticsがエラー発生している12ため、この Abstract Semantics は適切でない。
しかし、残念ながら、「解析の理想と現実」の節で触れたように、①と②の性質を満たす "適切な" Abstract Semantics は、計算することができません13。できちゃったら、とんでもないことですよね。
Abstract Interpretation 初歩の初歩 まとめ
Abstract Interpretation は、
- プログラムの「状態$\boldsymbol{x}(t)$」という概念を導入し、その時間変化を考える。
- 全ての状態変化（＝$\boldsymbol{x}(t)$の経路）を含む Abstract Semantics を作り出し、それに基づいて解析する。
というものです。
Abstract Interpretation の理論がもっと知りたい！現論文を読みたい！と思った方は、Abstract Interpretationの創始者 Patrickさんの解説サイトから飛んでみてください。ただし、最終更新が10年以上前なので、最新論文はGoogle Scholarなどから探してください。
長々と書いてきましたが、ようやく終わりです。
IKOSや、それを使おうとしているSpace ROSに興味がわきましたら、ぜひ下記参考リンク集を漁ってみてください。
最後まで読んでいただき、ありがとうございました！
参考リンク集
実践編へのリンクはコチラ
-
Space ROS 公式Webサイト
まずはFAQから読むことをおすすめします。気になることは大体回答されています。 -
Abstract Interpretation in a Nutshell
本記事のAbstract Interpretationの解説パートのベースとなったものです。
ちなみに著者のPatrick Cousotさん（フランス人なので、おそらくパトリック・クソーと読みます）はAbstract Interpretationの理論を創始した、非常に著名な計算機科学者です。現在はニューヨーク大学の教授のようです。
本記事内で言及されている ASTREE という静的解析ツールは、Patrickさんが作成したものです。 -
Abstract Interpretation
同じくPatrickさんの記事で、また別の内容が書かれています。
-
Space ROSの公式ドキュメントに記されているように、IKOSだけでなくCobraも搭載される予定です。CobraもNASA (JPL) で開発された静的解析ツールです。 ↩
-
Space ROSに組み込まれたIKOSの実行に成功したら、是非コメントでご教授願います！ ↩
-
現在、Space ROSはROS2ベースで作られています。 ↩
-
例えば、NASAのNPR-7150.2やRTCAのDO-178Cといった標準です。 ↩
-
LLVM (Low Level Virtual Machine) は、プログラムのコンパイルや最適化を行うためのオープンソースのフレームワークです。コンパイラ、デバッガ、コード解析ツールなどの基盤となる技術として広く使われているものです。
そしてbitcodeとは、LLVMによって生成された中間表現（テキスト形式）をバイナリに変換するためのフォーマットです。 ↩ -
ここで言う「危険」とは、エラーのことだと思っていただいても問題ありません。こういった表現は、厳密さとわかりやすさのシーソーゲームですね。 ↩
-
ちなみに、あらゆる経路の各時点において各変数（つまり$\boldsymbol{x}(t)$の要素）が取りうる全ての具体的な値の集合のことを、Concrete Semanticsと呼びます。もし、図１に描かれた５本の経路があらゆるプログラムの全ての経路を網羅しているならば、Concrete Semanticsとはそれらの経路上の任意の点における各変数の具体的な値の集合であり、Concrete Semanticsにおいて起こりうる危険の全てを検出することが静的解析ツールの目標と言えます。 ↩
-
Concrete Semanticsは全ての経路の集合です。それを包含するように抽象化された領域がAbstract Semanticsというわけです。「象」「キノコ」「人間」を抽象化した「生物」という言葉が「象」「キノコ」「人間」を含むのと同じです。そういう意味で、Abstract な Semantics なのですね。 ↩
-
"適切な" という言葉は私が勝手に作ったものです。 ↩
-
誤検出による通知を false alarm または false positive と呼びます。 ↩
-
エラー誤検出の逆に、エラー見逃しがないか、という観点も必要じゃないかと思われたかもしれません。しかし、それについては、①のsoundnessが満たされていれば十分です。 ↩
-
これまで注釈をきちんと読んできた読者のために。つまり、Concrete Semanticsでエラーが発生しないところで Abstract Semanticsがエラーを出しているということです。逆も不適切です。 ↩
-
数学的には求めることができるようです。 ↩