C/C++の静的解析ツール・事例まとめ

C/C++の静的解析は、どう考えても大変なんだけどどう考えても需要が高いので、やはり色々なソフトウェアや事例があるようだ。まとまった情報が欲しいけど見つからなかったので自分の調べた範囲でまとめることにした。

他にも耳寄りな情報があったら教えてほしい。

静的解析を行うことができるソフトウェア

調べてみると結構たくさんある。それぞれの特徴とかあまりよくわからない。

(個人的には、とりわけ網羅的な形式的検証ができるツールの性能に興味があるので、それを中心に集めていたが、やはり網羅的とは限らないで探すともっとたくさん見つかるようだ。もちろん網羅性にはトレードオフがある)

  • Frama-C …… C言語に形式手法を適用するための汎用のフレームワークで、静的検証のためのプラグインも多数(WPとかValueとか)存在する。網羅的な検証から発見的な手法、動的な手法まで様々ある。研究で使うのに便利そう
  • Astrée Runtime Error Analyzer …… 飛行機などミッションクリティカル環境を主に想定した網羅的な静的分析器のようだ。昔のページ→The Astrée Static Analyzerを見ると、再帰と動的メモリ確保のないプログラムを対象としていたようだが、現在は再帰のないプログラムなら動的メモリ確保があっても検査できるようだ。フランスのINRIAとかその辺が関わっていそうな雰囲気がある
  • VCC …… 名前に "concurrent" が含まれていたり、並行性が何かとプッシュされているように見える。codeplexに置いてあるしMSRかな
  • SLAyer …… 最近MSが出したらしい。これも分離論理でメモリ安全性を調べるパターン(なので網羅性あるのかな)。
  • VeriFast …… これもCのプログラムが検証できるらしい。
  • Escher C/C++ Verifier …… 説明を見る限り、網羅的な検査をすると言っているように読める。C++も検証できると主張しているので強そう。会社概要を見る限り、これが主力商品のようだ
  • Infer …… Facebookが買収したことで有名。分離論理使うくらいだから何らかの意味で網羅的なんだろうか。一般的なC/C++プログラムを検証できそうな雰囲気
  • CBMC …… 有界モデル検査をするツールのようだ
  • CodeSonar …… Z3使うらしい(ということはwhite-box testingとかかな)。網羅的とは書いていないように見えるので発見的な手法かな
  • Coverity …… これも静的解析ツールとしては強いらしい。網羅性はパッと見では確認できなかった ← grafiさんが紹介してくれた記事にunsoundと書いてあった
  • QAC …… これも網羅性は確認できなかった

余裕があれば上記のソフトウェアを以下のような観点から整理したい。

  • 標準準拠 …… 言語仕様である ISO C, ISO C++. POSIXの仕様であるSUSやThe Open Group Specification. コーディング標準であるCWE, CERT C, MISRA-C. 安全性の規格であるDO-178B level A, ISO 26262, IEC 61508. ……などがあるらしいので、それぞれへの対応度を調べる。
  • 網羅性 …… 一部の静的解析ツールは、ある種の問題(例えば実行時エラー)がないことを保証できる場合がある。例えばAstréeのページにはsound(健全)という言葉があるが、これはこの網羅性をあらわしている。
  • 精度と再現率 …… 実際の問題に適用したときには、見つけられなかったバグの数や誤検出された問題の数が重要になると考えられる。
  • 適用可能なプログラムの範囲 …… Astréeは再帰のないプログラムに限定して検証すると書かれている。このように、適用対象を絞ることで高性能な静的解析を提供している場合があるようだ。
  • 適用可能なアサーションの表現力 …… プログラムにコメントでアサーションを入れるタイプの静的解析ツールでは、そのアサーションの表現力に違いがあるかもしれないので、その辺りを調べる。また、そうでない静的解析ツールでは、発見できるバグの種類がこれに相当すると考えられる。

検証済みコンパイラ

コンパイラ自体が(主に最適化まわりで)バグってることはたまにあるので、ミッションクリティカルな用途ではコンパイラ自体の正しさも気になるという事情があるようだ。

  • CompCert …… Astréeと同じあたりが作ってるやつ。

プログラミング言語の形式仕様

C言語のプログラムやコンパイラに関して正確に論証したいとなるとそもそも仕様が必要になるが、ここで紹介しているのがまさにそれだ。

  • Verifiable C …… Coqで書かれたC言語の仕様。便利そう。CompCertの正しさはこの仕様と照らしあわせて検証されている。

動的検査するやつ

静的解析ではないような気がするけど。

事例

更新履歴