1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@yuotsuka

システムプログラミング向けプログラム検証ツールまとめ

1
Last updated at Posted at 2025-12-01

本記事は(nishishinjuku-ctf Advent Calender)の1日目の記事です。

nishishinjuku-ctf 勉強会の発端となった42tokyoで、様々な学習上の制約の下、Cコードと共にシステムプログラミングについて思いを馳せる機会がありました。その過程で補助となるツールとして gdb / valgrind / libasan などに触れ、「プログラム検証」という、素朴にコードを書いているとそのうち必ずぶつかる苦行を、どうやって乗り越えるかをそこそこ真剣に考えるようになりました。
本記事は、その延長として「次に触ってみたい検証ツール」を整理しておくための下調べメモです。
2026年に具体的な抱負が見つけられなかったらここにまとめたツールで遊ぼうかなと思います。

導入

C でシステム寄りのコードを書いていると、

  • gdb でステップ実行したり
  • valgrind でメモリリークを調べたり
  • -fsanitize=address（libasan）でメモリアクセス違反の詳細を見たり

などと手を替え品を替え、このようなプログラム検証のための仕組みがとても頼りになります。

まだ自分は このあたりのツールを「きちんと使いこなせるように試行錯誤手を動かして慣れる段階」なのですが、
先の話として

  • もっと仕様寄りのレベルでバグを探すツール
  • C プログラム全体をモデルとして解析／検査してくれるツール
  • テストケースを自動生成してくれるツール

などがあるらしいので、個人的な学習ロードマップの参考として一度きちんと整理しておこうと思いました。

そこでこの記事では、

「gdb / valgrind / libasan を使いつつ、
その先の“もう少し本格的なプログラム検証ツール”を下調べしておくメモ」

という位置づけで、SLEBoKのProVerB を眺めながら、
今後自分が試してみたいツールをいくつかピックアップして整理してみます。

1. ツールを整理するための枠組み： ProVerB

まず前提としてツールの紹介の分類法として参考に使用するものが、ProVerB (Program Verification Book) というプロジェクトです。(ProVerB)

  • SLEBoK（Software Language Engineering Body of Knowledge）の一部

  • 数ある検証ツールを「どんなレベルの形式性・自動化を持つか」で分類したデータセット

  • 各ツールに対して

    • 何を入力にするか
    • 何を出してくれるか
    • どの PV レベル (PV0〜PV6) に属するか
      をまとめてくれています

ProVerB では、ツールをざっくり0~6の7段階(0-indexed)に分類しています：

  • PV0

    • ユーザが自分で仕様を書くわけではないが、コードやモデルをそれなりに厳密な内部表現へ変換して扱うツール群

  • PV1

    • 「扱うものに対する形式的な期待（制約）」を内部に持ち、
      それに違反しているところを教えてくれるツール
    • 例：型チェッカ、静的解析ツール、Lint 系など

  • PV2

    • 形式モデルや仕様から「実行可能な何か」を生成するツール
    • 例：モデルからテスト入力を大量に生成するテスト生成器など

  • PV3

    • ユーザが 「何をチェックしたいか」 をある程度制御できるツール

    • 例：assert やプロパティを与えると、それが常に成り立つか検査するモデルチェッカ（CPAchecker など）* PV4

    • ツール側にあらかじめ形式仕様が組み込まれていて、
      その形式的意味論の中で自動的にたくさんの性質をチェックしてくれる

    • 例：SMT ソルバ、特定のメモリモデルや並行モデルに基づいて安全性を検査するツールなど

  • PV5

    • ユーザが自分で仕様を書き、それをプログラムや別の仕様の形式表現と組み合わせて
      「プログラムで検証する」 ことができるツール
    • 使いこなせれば「新しいプログラムの機能正当性を証明」みたいな話まで狙えるクラス

  • PV6

    • Coq / Isabelle / Lean のような 定理証明支援系
    • かなり自由なロジックを扱え、証明オブジェクトまで生成できるツール群

ここで大事な注意として、ProVerB 内に記載されている事項として：

The PV-hierarchy does not represent how “worthy” or “important” a tool is, merely how much it expects and demands of its end user, and what it can offer back.

PV レベルは「価値」や「重要性」ではなく「ツールがユーザに何を要求し、何を返してくれるかの違い」

である、という点です。

またPVのヒエラルキーの分類上の特性についての言及として:

lower-PV-level tool is more preferable because it is easier in use and is less ambitious about the effort investment. Often tools of a lower PV-level are built “on top” of tools of higher level which they run as a backend.

とありますが、これは単にPV が大きいから検証ツールとして強力・小さいから貧弱、という話ではなく、
「どのくらい自分で仕様を書き、その見返りにどの程度の強い保証を得たいか」 で選ぶ感じです。
ソフトウェア検証においても、トレードオフはつきものです。

この記事では、この枠組みを参考にしながら、

いま個人的に身近にある gdb / valgrind / asan から次点で個人的に関心のあるツールをProver Bのリストからピックアップしてざっと眺めてみます。

2. いま使っている・使い倒していきたい基本ツールの位置づけ

まずは手元で触りやすいツールから。

2.1 gdb

Prover B: PV 現状未登録

  • C / C++ の代表的なデバッガ

  • 実行を一時停止して

    • 現在の行
    • ローカル変数の値
    • コールスタック
      などを見ることができる

  • ブレークポイントやウォッチポイントを使って、
    「この条件になったら止まってほしい」といった指定もできる

役割としては、プログラムをstep by stepで動的に観察する「プログラマの頭の補助」 です。
習熟度は

  • ロジックがおかしい
  • 条件分岐が期待と違う
  • ある関数の呼び出し順序が想定と違う

こういった「実装の意図」と「実際の挙動」のギャップを、人間が目で追うための道具。

ProVerB 的には、gdb 自体は登録されておらず、
「形式仕様を直接扱うツール」ではありません。
ただし、PV5/PV6 の世界の証明を信頼するためにも、
デバッガでの感覚を持っていることが大事、という位置づけかなと思っています。

2.2 valgrind（memcheck, helgrind など） ― 実行時のメモリを監視する

Prover B: PV5

  • 実行中のプログラムをエミュレータ上で走らせて、メモリの使い方を監視する

  • 代表的なサブツール：

    • memcheck

      • 解放済みメモリへのアクセス
      • 未初期化メモリの利用
      • メモリリーク

    • helgrind

      • スレッド・ロックの使い方（データ競合など）

イメージとしては、

「C プログラムに、強めのメモリチェック付きのランタイムを載せて走らせる」

という感じです。

valgrind, helgrindの引数にコンパイル済みCプログラムを渡すだけで使用できるのでかなり気軽に使用できて、お世話になっている人が多いのではないでしょうか。

ProVerB では、Valgrind は “PV5 レベルのフレームワーク” として登録されています。(slebok.github.io)

  • Frameworks カテゴリに入りつつ
  • PV5 側では「動的解析ツールを構成するための枠組み」として扱われている

この記事の文脈では、深入りはしないのでツールの印象として

「実行時にメモリまわりをかなり真面目に見てくれるツール」

という雰囲気で止めておきます。

2.3 libasan（AddressSanitizer 他） ― コンパイラ内蔵の軽量な動的検査

Prover B: PV 未登録

-fsanitize=address などで有名な サニタイザ系 も、
「実行しながらエラーを検出する」という意味では valgrind と同じグループに入ります。(ただし、Prover Bでは現状未分類)

  • AddressSanitizer (ASan)

    • バッファオーバーフロー
    • use-after-free
    • ダブルフリー …など

  • UndefinedBehaviorSanitizer (UBSan)

    • 整数オーバーフロー
    • 未定義シフト
    • 無効なキャスト …など

  • ThreadSanitizer (TSan)

    • データ競合

など、コンパイル時オプションで有効化できるのが強みです。

  • valgrind より軽い
  • CI で常時有効にしやすい
  • 「Debug ビルドは必ず ASan/UBSan ON」という運用もしやすい

ProVerB には libasan のエントリはありませんが、やっていることはかなり Valgrind に近いので、
「実行しながら不正な振る舞いを強くチェックしてくれる層」としてまとめて意識しておくと良さそうです。

3. PV1〜PV2：C 向けの静的解析・形式仕様付き解析 ― Frama-C

次は、「コンパイル前にもっと賢くチェックしたい」方向です。

3.1 Frama-C

Frama-C は、C 用の静的解析フレームワークです。(haslab.github.io)

  • ISO C99 を対象とした解析プラットフォーム

  • プラグインを組み合わせて

    • 抽象解釈
    • 仕様に基づく証明
    • テスト生成
      などを行える

  • ProVerB では “Frameworks” カテゴリ に入っており、
    C プログラムを形式的な artefact として扱うための土台、という位置づけになっています。(slebok.github.io)

Frama-C の特徴は、ACSL（ANSI/ISO C Specification Language） という仕様記述言語を使えることです。(frama-c.com)
ACSLはC99 semanticsを検証対象のモデル(仕様)にしているそうですが、C11 semanticsに基づいたCerberusというプロジェクトもあるようです。(cerberus)

ACSL で仕様を書く

たとえば、次のような関数を考えます：

/*@ requires 0 <= n < INT_MAX;
    ensures \result >= n;
 */
int incr(int n) {
    return n + 1;
}

ここで

  • requires は プログラムの前提条件（precondition）
  • ensures は プログラムの事後条件（postcondition）

に対応しています。(この辺の形式的な意味の土台となる論理式的な記法についてはホーア論理・分離論理等で調べると色々でてきます。)

例として先に出てきたコメントブロックに埋め込まれたACSL:

/*@ requires 0 <= n < INT_MAX;
    ensures \result >= n;
 */

を自然言語に翻訳すると

この関数は、呼び出されるとき (ANSI/ISO C99が大前提で)
引数 n が 0 以上 INT_MAX 未満 であることを前提条件として仮定する。
その前提のもとで、関数の戻り値（result）は n 以上であることを要求する。

といった具合になります。

Frama-C + 各種プラグインを使うと、この仕様から：

  • 抽象解釈で値の範囲を追いかけて、配列境界・ヌルポインタなどを静的チェック
  • Hoare 論理ベースの WP プラグインで、「ensures が常に成り立つか？」を証明
  • 必要に応じて Coq などの定理証明器をバックエンドにして、証明を補う
  • 逆に、仕様を実行時アサートとして挿入し、実行時チェックもできる

といったことができます。(frama-c.com)

「C のコードにコメントとして仕様を書き、それを使って解析する」 というスタイルなので、

  • 既存コードに少しずつ仕様を生やしていく
  • 安全性が重要な関数だけ仕様を厚くする

といった段階的な使い方もしやすそうです。

3.2 ProVerB 的な立ち位置

Frama-C 自体は フレームワーク として登録されていて、
その上で動く各プラグインが PV1〜PV5 のレンジをカバーしています。(slebok.github.io)

  • 単純な静的チェックなら PV1〜PV3 相当
  • WP プラグインで ACSL 仕様をがっつり証明するなら PV5 寄り
  • バックエンドに Coq/Why3 を使えば、PV6 の世界ともつながる

という感じで、「C 向けのミニ検証エコシステム」 になっているイメージです。

4. PV3：C プログラム全体をモデルとして検査するツール

次は、C プログラムを 「論理式や遷移系のモデル」 に落として検査するツール群です。

gdb / valgrind / ASan が

実行しながら「たまたま踏んだ経路」でバグを見つける

のに対し、ここで紹介するツールはおおよそ

「ある範囲の経路を 網羅的/半網羅的 に探索し、条件を満たさない経路がないか探す」

というアプローチを取ります。

ここで言う「網羅的/半網羅的」は、検証が停止することなどを仮定した理想化したニュアンスで使っていて、PV3に含まれるような、例としてSAT/SMT ベースのツールは状態空間爆発と計算量の制約から、有界モデル検査やアブストラクションを行うため、「全経路を完全に調べる」というより「制約の範囲でできるだけ広くカバーする」程度を指します。制約等の問題設定はツールのユーザが制御します。

4.1 CPAchecker

CPAchecker は、C プログラムを抽象モデルに変換して検査するフレームワークです。(CPAchecker)

  • 入力：

    • C プログラム
    • その中の assert と、ERROR というラベル
    • どのような解析をするかを決める設定ファイル

  • 出力：

    • エラーがないかどうか
    • あれば、どの経路で発生するかを示す反例

特徴として：

  • フレームワークとして解析の「精度」や「手法」を設定で切り替えられる
  • HTML レポートで抽象状態や反例パスを可視化できる

などがあり、

「自作 C プログラムのこの地点に到達可能か？」
「この assert(0) は本当に“不到達コード”か？」

を機械的に確かめる用途にも向いています。

4.2 SeaHorn

SeaHorn は、C プログラムを Horn 節 と呼ばれる論理形式に変換して検査するツールです。(arXiv)

  • CHC（Constrained Horn Clause）としてプログラムの振る舞いを表現
  • 背景の SMT ソルバを使って安全性を検査
  • プロパティ検査だけでなく、情報フローやセキュリティ系の研究にも使われている

ProVerB では、SeaHorn 自体は別ツール（IFC-BMC のバックエンドなど）の土台としても使われていて、
「C → 論理（Horn 節）」の橋渡しの役目です。(slebok.github.io)

4.3 KLEE（シンボリック実行）

KLEE は、LLVM ビットコードを対象とした シンボリック実行エンジン です。(GitHub)

  • C/C++ などで書いたプログラムを clang -emit-llvm して .bc を作る

  • 入力を「シンボリック変数」とみなし、
    分岐を可能な限りすべて辿る

  • その過程で

    • 多くのパスをカバーするテストケースを自動生成
    • assert などにぶつかると、その入力を返す

KLEE は

  • 「高カバレッジなテスト生成器」
  • かつ 「テスト駆動のバグ探索エンジン」

として見ると理解しやすいです。

  • 手書きテストではどうしても漏れがちな条件分岐
  • fuzzing ではなかなか拾えない細かいパス

を埋めていく道具として、テスト自動生成の文脈でもかなり使われています。(klee-se.org)

5. PV4〜PV5：より自動寄りの安全性検査ツール

PV3 が「ユーザが書いた assert や簡単な仕様を検査する層」だとすると、
PV4〜PV5 は ツール側がかなり頑張ってくれる層 です。

ここでは、C プログラムの安全性検証ツールをいくつか。

5.1 Symbiotic ― スライシング＋シンボリック実行

Symbiotic は、C プログラム向けのバグ検出・検証フレームワークです。(staticafi.github.io)

特徴：

  • C / LLVM プログラムを プログラムスライシング で簡約
  • 必要な部分に計測用コード（instrumentation）を挿入
  • エンジンとして KLEE などのシンボリック実行を利用
  • 目標（アサーション違反か、特定のラベル到達か）に応じて手法を組み合わせる

目的としては、

「通常の実行ではなかなか出ないクラッシュや、メモリの不正利用を自動で見つけたい」

という場合の選択肢になりそうです。

5.2 ESBMC ― SMT ベースのコンテキスト有界モデルチェッカ

ESBMC (Efficient SMT-based Context-Bounded Model Checker) は、
C / C++ 向けの SMT ベースモデルチェッカです。(GitHub)

  • 単一・マルチスレッドの C/C++ プログラムを対象

  • SMT ソルバをバックエンドに用いて、安全性を検査

    • 配列境界・ポインタ安全性
    • オーバーフロー
    • データ競合
    • ユーザ定義の assert など

  • ループ回数・スレッドコンテキストを有界にして検査（bounded）

ProVerB では PV4 に分類されていて、
「C プログラムの安全性プロパティをチェックし、必要に応じて不変条件（インバリアント）も自動生成するツール」と説明されています。(slebok.github.io)

CBMC に比べると、

  • SMT ソルバを前提にしている
  • ループ不変条件の自動推論など、より“賢い”部分がある

というあたりが特徴として挙げられます。

5.3 Verifast / Viper ― separation logic (分離論理) によるメモリ安全性検証

少し理論寄りですが、所有権やメモリ安全性をがっつりやりたいときに顔を出すのがこのあたりです。(slebok.github.io)

  • Verifast

    • C / Java を対象
    • separation logic に基づき、ポインタ・ヒープの所有権を明示的に扱う
    • データ競合や二重解放などを、論理レベルで防ぐ

  • Viper

    • 独自言語でプログラムと仕様を記述
    • 所有権・パーミッションの概念を用いて、メモリ安全性を検証する

どちらも、

「仕様を書くのがちょっと大変だけれど、その代わりかなり強い保証が得られる」

という方向のツールで、並行データ構造や複雑なメモリ管理を真面目にやるなら、
いつかは触ることになりそうな世界です。

6. テスト生成という観点から見たツール

形式検証というと「証明」のイメージが強いですが、
実務寄りの文脈では 「強力なテスト生成ツール」 として使われているケースも多いです。

ここではテスト生成よりの話を少し。

6.1 Frama-C PathCrawler / LTest など

Frama-C には、テスト生成系のプラグインも存在します。

  • PathCrawler(frama-c.com)

    • C のソースコードをアップロードすると、

      • プログラムの経路を解析
      • 制御フローの各パスをカバーするテストケースを自動生成

    • Web サービス版（PathCrawler-online）も提供されており、教育用途にもよく使われている

  • Frama-C/LTest

    • テストカバレッジの計測
    • 自動テスト生成
    • 「意味のないテスト目標」の検出 …など
    • 静的解析＋動的解析を組み合わせた、ホワイトボックステスト支援ツール

「この if 文の両側を必ず通るテストが欲しい」 といったときに、
手で条件を解いてテストを書く代わりに、ツールに生成させるイメージです。

6.2 KLEE ― 高カバレッジテスト生成器として

KLEE は前節では「シンボリック実行エンジン」として紹介しましたが、
テスト生成という観点からも強力です。

  • LLVM ビットコードを入力に
  • 可能な限り多くの分岐をカバーするよう、テスト入力を自動生成
  • 生成されたテストを、そのままユニットテストや回帰テストに組み込める

従来の手書きテストでは難しい、

  • 「エラーハンドリングの深いパス」
  • 「型はあっていても単純な型ではチェックしきれない境界条件の組み合わせ」

を埋めていくのに役立ちます。

7. まとめ

ここまで見てきたのは、あくまで

「gdb / valgrind / libasan を活用しつつ、
その先にどんなツールがあるのかを整理した下調べメモ」

に過ぎません。

ProVerB の PV レベルの視点を取り入れて整理するしてみると、

  • PV0〜PV1 相当

    • 比較的単純な静的解析ツール など

  • PV2〜PV3 相当

    • テスト生成器（PathCrawler, KLEE）
    • モデルチェッカ（CBMC, CPAchecker, SeaHorn など）

  • PV4〜PV5 相当

    • ESBMC, Symbiotic, Frama-C + WP/ACSL
    • separation logic ベースの Verifast / Viper

  • PV6

    • Coq / Isabelle / Lean / HOL などの定理証明支援系

という感じで、「どこまで仕様を書き、どこまで自動的に頑張ってもらうか」 の選択肢が大体ですが、一望できるような気がします。

自分自身の当面の目標としては、

  • 改めてgdb等や基本的なデバッガ等の習熟に加えて並行して、

    • ACSL で簡単な関数に仕様を書いてみる
    • CBMC / CPAchecker で、非同期処理等の C プログラムに assert を入れて勘所を磨く
    • KLEE / Symbiotic 等のツールでテスト生成＆バグ探索を試してみる

といったところから、少しずつ 検証ツールの勘 を磨いてプログラムを見る目を養いつつ、ソフトウェアプログラムの品質向上みたいな話に接続できればと思います。

以上、「gdb / valgrind / libasan の先に、どんなツールが並んでいるか」を一度棚に並べ直してみたメモでした。

もしこの記事が、次に身につけてみたいソフトウェアまわりの技能を考えるうえでの一助になれば幸いです。
また、このあたりの話はまだ手探りで情報を集めている段階でもあるので、技術的・内容的なご指摘や、他にも面白そうなツールの情報などを共有いただけると励みになります。

1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?