Space ROS (Robot Operating System)Advent Calendar 2024

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

Posted at 2024-12-17

はじめに

こんにちは。

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

今回は、NASAが作った C/C++ の静的解析ツール IKOS の解説記事、＜実践編＞です。
（基本編はコチラ）

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

この記事でわかること

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

インストール方法

コチラが IKOS のリポジトリです。

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

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

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

Homebrew
ソースからビルド

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

環境

Ubuntu 22.04 (WSL)

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

IKOS (厳密にいうとIKOS Analyzer²) は以下のライブラリを必要としています。
どうでもいいから手順を見せてくれ！という人はこの小節をスキップしてください。

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²
IKOS AR²
IKOS LLVM Frontend²

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

インストール手順

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

apt install

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

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

APRON のインストール

以下のリポジトリを好きなところにgit cloneします。

git clone git@github.com:antoinemine/apron.git

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

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

IKOS のクローン

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

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

IKOS Core のインストール

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

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

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のインストールに続いてインストールしていきましょう。

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 パッケージです。
続いてインストールしていきましょう。

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 パッケージです。
では、インストールしていきましょう。

これまでと違って、analyzerディレクトリに入りません！

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

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

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

IKOS を使ってみた

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

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

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

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

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;
}

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

ikos ikos-trial.c

すると、標準出力に以下が出力されます。

[*] 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でビルドする場合の例を示します。

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

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

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

ikos-scan make

すると、まず普段通りにビルドが開始されます。
ビルドが完了すると、次のように聞かれるので、y を入力します。

Analyze build/tools/elf2cfetbl/elf2cfetbl? [Y/n]

解析対象が複数ファイル存在すると、その分繰り返し y を入力する必要があります。ここはIKOSの要改善点ですね。

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

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

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

「総評：このプログラムは絶対に安全ではない」

おお。。。

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

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

以上です

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

基本編を読んでいない方はそちらも読み、IKOSがどのような静的解析ツールなのか理解を深めてみてください！

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

IKOS と Space ROS

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

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

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

もし本記事の方法でインストールに失敗したら、ぜひコメントで教えていただきたいです！
私も勉強になるので。。。 ↩
IKOSは４つのパッケージに分かれており、IKOS Analyzer をインストールすることで静的解析を利用することができます。
その前にIKOS Core、IKOS AR、IKOS LLVM Frontendをインストールする必要があります。なお、ARとは Abstract Representationのことです。 ↩ ↩² ↩³ ↩⁴
これは、手順を簡単にするためです。本記事のコードブロックをコピペするだけでインストールできるように、/usr/localに決め打ちで書いています。プレースホルダにすると、読者全員が書き換える必要がありますし、どこにインストールするか考える労力がかかります。しかし、決め打ちにすればそれ以外の場所にインストールしたい人だけが書き換えればよいです。 ↩
記事をストックしておけば、更新時に通知が届きます。 ↩

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up