【コア #5】NASAが作った静的解析ツール「IKOS」実践編

# はじめに
こんにちは、先輩クン後輩さんです。

本記事は、2024年12月のアドベントカレンダー「Space ROS」に投稿された一連の記事の１つです。

今回は、NASAが作った C/C++ の静的解析ツール **IKOS** の解説記事、＜実践編＞です。
（基本編は[コチラ](https://qiita.com/LuckyCat/items/b8188ffd5efa5aa4bbbf)）

実践編では、IKOSを実際に使っていきます。

# この記事でわかること

- IKOS のインストール方法
- IKOS を実際に使ったときの画面

# 目次

- インストール方法
- IKOS を使ってみた
- IKOS と Space ROS

# インストール方法

[コチラ](https://github.com/NASA-SW-VnV/ikos)が IKOS のリポジトリです。

https://github.com/NASA-SW-VnV/ikos

**重要なことですが、（少なくとも私のWSL環境では）<font color="red">公式のインストール手順にしたがってもインストールできません</font>。**
おそらく、IKOSのインストール手順はあまり整備されていない状態なのだと思われます。

私はかなりの試行錯誤を経て、以下の方法でインストールできそう、という結論に至りました。
WSL内の環境がぐちゃぐちゃになってしまい、まともな検証はできていませんが、きっとできるはずです......！[^1]

[^1]: もし本記事の方法でインストールに失敗したら、ぜひコメントで教えていただきたいです！
私も勉強になるので。。。

インストール手順は以下の２通り存在します。

- Homebrew
- ソースからビルド

Homebrewでインストールすると一撃なので楽ですが、私の環境（WSL）ではエラーが発生し、断念しました。
本記事ではソースからビルドするインストール手順を示します。

### 環境

-  Ubuntu 22.04 (WSL)

### これからインストールするライブラリ

IKOS <font color="darkgrey">(厳密にいうとIKOS Analyzer[^2])</font> は以下のライブラリを必要としています。
どうでもいいから手順を見せてくれ！という人はこの小節をスキップしてください。

- A C++ compiler that supports C++14 (gcc >= 4.9.2 or clang >= 3.4)
- CMake >= 3.4.3
- GMP >= 4.3.1
- Boost >= 1.55
- Python >= 3.3
- SQLite >= 3.6.20
- TBB >= 2
- LLVM and Clang 14.0.x
- APRON >= 0.9.10
- IKOS Core[^2]
- IKOS AR[^2]
- IKOS LLVM Frontend[^2]

[^2]: IKOSは４つのパッケージに分かれており、`IKOS Analyzer` をインストールすることで静的解析を利用することができます。
その前に`IKOS Core`、`IKOS AR`、`IKOS LLVM Frontend`をインストールする必要があります。なお、ARとは Abstract Representationのことです。

**APRON**は公式ドキュメントには Optional と書かれていますが、必須です。

## インストール手順

:::note warn
C++コンパイラ、Python、SQLiteのインストールは以下に含みません。
事前に各自でインストールしてください。
:::

### apt install

ここでは、以降で必要になるライブラリのうち、`apt`でインストールできるものをまとめてインストールしています。

```shell
sudo apt install libtbb-dev libgmp-dev libmpfr-dev libglpk-dev libflint-dev libppl-dev libboost-all-dev cmake llvm
```

### APRON のインストール

以下のリポジトリを好きなところにgit cloneします。
```shell
git clone git@github.com:antoinemine/apron.git
```

https://github.com/antoinemine/apron

続いてビルドします。
今回はjava対応とOCaml対応を外して必要最低限のセットアップにしましょう。

```shell
cd apron
./configure –no-java –no-ocaml
make
make install
```

#### IKOS のクローン

IKOS を好きなところにgit cloneします。
この中に、`IKOS Core`、`IKOS AR`、`IKOS LLVM Frontend`、`IKOS Analayzer` が含まれています。

```shell
git clone git@github.com:NASA-SW-VnV/ikos.git
```

https://github.com/NASA-SW-VnV/ikos

### IKOS Core のインストール

クローンしたIKOSのディレクトリに移動してください。
その中の `core` ディレクトリが IKOS Core パッケージです。
では、インストールしていきましょう。

:::note warn
本記事では、IKOS の各ライブラリのインストール先を `/usr/local` に決め打ちしています (`-DCMAKE_INSTALL_PREFIX=/usr/local` がそれに対応しています)。[^3]
:::

[^3]: これは、手順を簡単にするためです。本記事のコードブロックをコピペするだけでインストールできるように、`/usr/local`に決め打ちで書いています。プレースホルダにすると、読者全員が書き換える必要がありますし、どこにインストールするか考える労力がかかります。しかし、決め打ちにすればそれ以外の場所にインストールしたい人だけが書き換えればよいです。

```shell
cd core
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=/usr/local -DGMP_ROOT=/usr/local/lib ..
sudo make install
```

インストールできたかどうか確認しておきたい方は、`make check`することができます。
ただし、これはかなり時間がかかりました。
さっさと進めたい方は、`make check`せずに次に進むことをおすすめします。

### IKOS AR のインストール

IKOS の`core`と同じディレクトリにある`ar`ディレクトリが、IKOS AR パッケージです。
IKOS Coreのインストールに続いてインストールしていきましょう。

```shell
cd ../../ar
mkdir build && cd build
cmake -DCMAKE_INSTALL_PREFIX=/usr/local -DCORE_ROOT=/usr/local ..
make 
sudo make install
```

### IKOS LLVM Frontend のインストール

IKOS の`frontend/llvm`ディレクトリが、IKOS LLVM Frontend パッケージです。
続いてインストールしていきましょう。

```shell
cd ../../frontend/llvm
mkdir build && cd build
sudo -E cmake -DCMAKE_INSTALL_PREFIX=/usr/local -DLLVM_CONFIG_EXECUTABLE=/usr/lib/llvm-14/bin/llvm-config -DCORE_ROOT=/usr/local -DAR_ROOT=/usr/local ..
sudo make
sudo make install
```

### IKOS Analyzer のインストール

IKOS の`analyzer`ディレクトリが、IKOS Analyzer パッケージです。
では、インストールしていきましょう。

<font color="red">**これまでと違って、analyzerディレクトリに入りません！**</font>

**まず、IKOS のルートディレクトリに `build` ディレクトリを作ってください。**
**今、`frontend/llvm`ディレクトリにいるなら、`cd ../..`です。**

```shell
cd <ikos root directory> # frontend/llvm/buildディレクトリからなら cd ../../..

mkdir build && cd build
cmake –DCMAKE_PREFIX_PATH=/usr/local -DCMAKE_INSTALL_PREFIX=/usr/local -DLLVM_CONFIG_EXECUTABLE=/usr/lib/llvm-14/bin/llvm-config -DAR_ROOT=/usr/local ..
make
sudo make install
```

:::note info
以下のような画面が出てきたら、インストール成功です！
:::

![IKOS Analyzerインストール成功時のスクショ](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2603341/4fa26673-51c7-9f38-f28b-7afb4e59b281.png)

# IKOS を使ってみた

ここでは、ソースコードに IKOS による静的解析をかけたときの結果を紹介します。

### 単一ファイルを解析する場合

まずは、簡単な単一ファイルにかけてみます。

対象のソースコードは以下です。

```c: ikos-trial.c
#include <stdio.h>

int main(){
    int a = 1;
    int b = 2;

    int c = a + b;

    printf("c = a + b = %d + %d = %d\n", a, b, c);

    return 0;
}
```

これに対し、以下のコマンドで解析します。

```shell
ikos ikos-trial.c
```
すると、標準出力に以下が出力されます。
```io
[*] Compiling ikos-trial.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.664 sec
ikos-analyzer: 0.081 sec
ikos-pp      : 0.118 sec

# Summary:
Total number of checks                : 4
Total number of unreachable checks    : 0
Total number of safe checks           : 4
Total number of definite unsafe checks: 0
Total number of warnings              : 0

The program is SAFE

# Results
No entries.
```

同時に、`output.db`が生成されます。
これは、あとで解析結果を見るためのものです。
`ikos-report output.db` で、コマンドラインで警告などの内容を再確認できます。
あるいは、`ikos-view output.db` で、ブラウザで確認することもできます。
※ブラウザによる確認は、私はうまく動きませんでした。

### プロジェクト全体を解析する場合

続いて、複数のファイルから成るプロジェクト全体を解析してみます。

`make`でビルドする場合の例を示します。

ソースコードは現状明示しませんが、その正体はアドベントカレンダーの後半の記事が公開されたときに、この記事を更新する形で明かす予定です。[^4]

[^4]: 記事をストックしておけば、更新時に通知が届きます。

プロジェクト全体に適用する方法は簡単で、単にビルドコマンドの前に `ikos-scan` を付けるだけです。

次のコマンドを実行します。

```shell
ikos-scan make
```

すると、まず普段通りにビルドが開始されます。
ビルドが完了すると、次のように聞かれるので、`y` を入力します。
```plaintext
Analyze build/tools/elf2cfetbl/elf2cfetbl? [Y/n]
```
解析対象が複数ファイル存在すると、その分繰り返し `y` を入力する必要があります。<font color="darkgrey">ここはIKOSの要改善点ですね。</font>

最も見ごたえのあるファイルの結果を以下に示します。

![ikos-scan makeの結果](https://qiita-image-store.s3.ap-northeast-1.amazonaws.com/0/2603341/870d3888-5c46-ad0a-f37b-8b57c9c9ec96.png)

表示形式は単一ファイル解析時と同じです。
4145項目のチェック対象が存在したようですね。
結果を日本語に翻訳すると次のようになります。

|項目|該当数|
|----|------|
|実行されない項目|71|
|安全と判断された項目|3428|
|絶対に安全ではない項目|11|
|警告が出された項目|635|

「<font color="red">総評：このプログラムは絶対に安全ではない</font>」

おお。。。

指摘内容は、「項目数が多すぎるので出力ファイルを見てくれ」とのことです。
`ikos-report `コマンドで確認することができます。

`ikos-report`の出力結果は、どんなソースコードを用いたのかを明らかにする際、見せます。
『絶対に安全ではない』と指摘されているのは、全てポインタの初期化がされていないというものでした。

### 以上です

これ、試してみると結構面白いです。特に、IKOS がどのような理論に基づいていて、どのような機能を持っているかを知っていると、より面白さを感じることができます！

:::note info
[基本編](https://qiita.com/TheJuniorTheSenior/items/807d7ec5d14ebe85116a)を読んでいない方はそちらも読み、IKOSがどのような静的解析ツールなのか理解を深めてみてください！
:::

:::note info
ぜひ、あなたのソースコードにも IKOS を試してみてください！
:::

# IKOS と Space ROS

IKOSはSpace ROSに組み込まれています（本記事を執筆した時点では、うまく動作しませんが）。

ビルドするたびに必ずIKOSが実行されることで、開発者は安全な宇宙品質のコードを書くことができるようになるのです！

宇宙品質のロボットを作る Space ROS に興味がある方は、一度 Space ROS を覗いてみてください！

https://space.ros.org/

https://github.com/space-ros/space-ros