ソフトウエアのバグがないことを証明してくれるツールをMonoidicsが拡販へ

英国ロンドンを拠点として日米にもオフィスを置く、モノイディクス（Monoidics）社は、2年前にロンドン大学のピーター・オーハン教授と米カーネギーメロン大学のジョン･C･レイノルズ教授が打ち立てたプログラムの正しさを証明する理論を利用して、それを製品化し商品名「Infer」と名付けた。二人の教授は今でもモノイディクス社の顧問でもある。

同社日本支社ディレクタであるRichard Rettig氏によると、このツール「Infer」は世の中にあるC/C++で書いたプログラムならどれでも適用できるが、同社の狙う市場は組み込みソフトの分野だという。組み込み系の大規模なSoCやFPGAのプログラム開発ではC言語を使う例が増えているからだ。

「Infer」のメリットは、コストを抑えたままバグのないソフトウエアプログラムを証明できる点である。これまでバグを除去する場合は、ソフトウエア全体のプログラムをつぶさに調べると時間(コスト)がかかってしまうが、調査対象のプログラム部分を減らすと時間は短くなるが、カバレージ（網羅性）が下がってしまいプログラムの品質が落ちてしまう。できるだけ短時間でバグのないことが証明できればありがたい。「Infer」は短時間でバグを調べバグがなくなったことを証明するソフトウエアである。ただし、プロシージャ（プログラムの中で、繰り返し登場する処理を行うために一連の命令を一つの手順(procedure）としてまとめたもの）レベルでのコードが安全であることを証明する訳であり、プロシージャレベルではないコードに関しては必ずしも安全という訳ではない。

「Infer」は3つのソフトウエア部品からなる。発見しにくいバグを捉えるBug Catchingと、欠陥のないことを証明するFormal Verification、ソフトウエアの品質をビジュアルに表示するInferクオリティチャート、である。Bug Catchはソースコードの画面上にエラーがあるとそれをハイライトで表示し、Formal Verificationはプロシージャごとに証明ダイアグラムを発行する。Inferクオリティチャートでは、修正の優先順位と、カバー率を表示しプログラムの品質をビジュアル化する。

この中で、Formal Verificationツールと呼ばれるものは従来もあった。しかし、これまでのツールではプログラムコードをチェックし、バグのある所に優先度を付けそれぞれ直していくという作業が中心だったという。「Infer」のFormal Verificationツールは、バグがないことを数学的に証明するものであり、プログラムの品質をチェックする時間を短縮、すなわち検査コストを下げることができる。

図1　プログラムの品質を図で表示　出典：Monoidics

Inferクオリティチャートは、ソフトウエアの品質をCall Rankという指標と、証明の(プルーフ)カバレージという指標を使って表すもの(図1)。横軸のプルーフカバレージは0%から100%まであるが、縦軸のCall Rankはプロシージャが呼ばれる割合で、高い方ほどよく呼ばれていることを示す。欠陥のある部分を赤、橙、黄でそれぞれ多い、中くらい、少ない、を表している。欠陥がないコードは緑で表す。図1の右側ほど安全であり、左側に欠陥を含む可能性が多いことを表している。

「Infer」はコードとメモリとの関係をきっちり保証することが実現のカギだという。見つけにくいバグの中でもメモリリークと呼ばれる、メモリ領域が徐々に減ってしまう現象に強い。メモリリークはOSのメモリ管理方法に問題があったり、アプリケーションにバグが残っていたりすると起きやすい、と言われている。

「Infer」の有利な点は、サードパーティのコードに対しても品質をチェックできることだ(図2)。経済産業省の組込みソフトウエア産業実態調査報告書2010によると、世の中にある全てのソフトウエアの平均的なプログラム行数は99.8万行であり、そのうち全くゼロから開発するコードは45.4万行である。残りの54.4万行はソフトの再利用ということになる。となるとサードパーティのソフトを流用することがごく一般的になってきていることになる。ただし、「サードパーティのコードには品質基準がない。その品質基準は他のコードとの互換性もない」とRichard Rettig氏は言う。また、サードパーティのコードがたとえ正しくても、組み合わせると欠陥となるケースもあるという。

図2　サードパーティのソフトのチェックにも有効　出典：Monoidics

そこで、サードパーティも含めたソフトウエアの品質をチェックするために、ドライバからライブラリ、ミドルウエア、アプリケーションの全てに渡ってチェックすることが必要になってくる。それもできるだけ開発の上流工程で行い、バグを製品近い工程まで持っていかないことが重要になる。特に、Androidデバイスに使われるソフトウエアはサードパーティだらけなので再利用のチェックは不可欠である。

このソフトの入手方法として、PCやサーバーにインストールするパッケージソフトの他に、クラウドを利用する方法も揃えている。「Infer」はC/C++をサポートしているが、2012年にはJavaプログラムにも対応する予定だ。