MALPAS ソフトウェア静的解析ツールセット

MALPAS は、厳密な形式の静的プログラム分析を適用してソフトウェアの正しさを調査および証明する手段を提供するソフトウェア ツールセットです。このツールは、有向グラフと正規代数を使用して分析対象のプログラムを表します。MALPAS の自動化ツールを使用すると、アナリストはプログラムの構造を記述し、データの使用を分類し、入力データと出力データ間の情報関係を提供できます。また、コードが仕様を満たしていることの 正式な証明もサポートします。

MALPASは、原子力、^[1]、航空宇宙^[2]、防衛^{[3]産業における}安全性が重要なアプリケーションの正確性を確認するために使用されてきました。また、原子力産業においてSizewell B ^[4]のコンパイラの正確性を提供するためにも使用されてきました。分析された言語には、Ada、C、PLM、Intel Assemblerなどがあります。

MALPASは、多くのプログラミング言語を扱える厳密さと柔軟性により、英国の健康安全局の原子炉用コンピュータベース保護システムに関するガイドラインで要求される独立した静的解析に適しています。 ^[5]

MALPAS ツールセットは、プログラムのさまざまな特性に対応する 5 つの特定の分析ツールで構成されています。アナライザーへの入力は、MALPAS 中間言語 (IL) で記述する必要があります。これは、手書きすることも、元のソース コードから自動翻訳ツールで生成することもできます。自動翻訳ツールは、Ada、C、Pascalなどの一般的な高水準プログラミング言語や、 Intel 80*86、PowerPC、68000などのアセンブラ言語用に用意されています。IL テキストは、「IL リーダー」を介して MALPAS に入力され、分析対象のプログラムの有向グラフと関連するセマンティクスが構築されます。グラフは、一連のグラフ削減手法を使用して削減されます。

MALPASツールセットは5つのアナライザーで構成されています: ^[6]

1. 制御フロー アナライザー。プログラム構造を検査し、エントリ/終了ポイント、ループ、分岐、到達不能コードなどの主要な特徴を特定します。望ましくない構造に注意を喚起し、プログラム構造の複雑さを示す概要レポートを提供します。
2. データ使用アナライザー。プログラムで使用される変数とパラメータを、その使用方法に応じて異なるクラスに分類します。(つまり、書き込まれる前に読み取られるデータ、読み取られずに書き込まれるデータ、または読み取りを介さずに 2 回書き込まれるデータ)。レポートでは、初期化されていないデータや、すべてのパスに書き込まれていない関数出力などのエラーを識別できます。
3. 情報フロー アナライザー。各出力変数またはパラメータのデータと分岐の依存関係を識別します。コード全体のすべてのパスで、不要な依存関係や予期しない依存関係を明らかにすることができます。未使用の変数や冗長なステートメントに関する情報も提供されます。
4. セマンティック アナライザー (シンボリック実行とも呼ばれます)。コード内の意味的に実行可能なすべてのパスにわたって、すべての入力と出力間の正確な機能関係を明らかにします。
5. コンプライアンス アナライザー。コードの数学的動作を正式な IL 仕様と比較し、どこが他と異なるかを詳細に示します。IL 仕様は、前提条件と事後条件、およびオプションのコード アサーションとして記述されます。コンプライアンス分析を使用すると、仕様に対するコードの機能的正確性について非常に高いレベルの信頼性を得ることができます。

このツールセットのオリジナル研究と初期世代は、イギリスのマルバーンにある英国王立信号・レーダー研究所(RSRE) によって作成されました (これが MALvern Programming Analysis Suite という名前に由来しています)。このツールセットは、1980 年代に民間の原子力および兵器分野で広く使用され、当時は Rex、Thompson and Partners によってサポートされていました。このグループによって MALPAS ユーザー グループが設立され、初代議長は David H Smith (現在は Frazer-Nash 所属) で、その後 Advantage Technical Consulting ( 2008 年にAtkinsに買収) が務めました。

最初の大規模な静的解析作業は、サイズウェル B発電所の一次原子炉保護システムに関するものでした。これは、壊滅的な故障に対する第一防衛線としてコンピューターベースの保護システムを採用した英国初の原子力発電所でした。さらに、チェコ共和国のCEZ は、テメリン原子力発電所の原子炉保護システムの信頼性を高めるために MALPAS を採用しました。1995 年、英国空軍は、安全性が極めて重要であると評価されたロッキード マーティン C130Jの航空電子機器ソフトウェアの独立した解析を委託しました。MALPAS は、Spark Ada で記述され、Spark ツールセットで検証されたミッション コンピューター ソフトウェアとは別に、このソフトウェアの解析に使用されました。^[7] MALPAS は現在、ヒンクリー ポイント C の 2 つの原子炉を監視する原子炉保護システムのソフトウェアを独立して評価するために使用されています。^[8]