CodePeer

Ada言語向け静的解析ツール

CodePeerは、コードの理解を深め、信頼性が高くセキュアなソフトウェアシステムを構築することができます。

CodePeerは、ランタイムエラーとロジックエラーを検出できるAdaソースコード解析ツールで、プログラムを未実行で潜在的なバグを確認できる自動レビューツールであり、開発ライフサイクルのどの段階でもエラーを発見できます。

CodePeerは、WindowsおよびLinuxプラットフォーム上で動作するAda言語向けスタンドアロンツールで、GNAT Pro開発環境に統合でき、Common Weakness Enumerationの「ソフトウェアエラー上位25」を検出できます。 さらにAdaのすべてのバージョン（83、95、2005、2012）に対応しています。

CodePeerは、DO-178BおよびEN 50128ソフトウェア安全規格の下で検証ツールとして認定されています。

 

開発ライフサイクルの早い段階で問題点を認識できることは、プロジェクトをスケジュールどおりに進め、予算内に収めることができます。

不具合修正コスト

 

CodePeerの静的解析機能は、プログラム未実行でバグを検出可能

開発ライフサイクルの早い段階でCodePeerを使用することで、コードのすべてを数学的に解析し、かつ、プログラムの入力とのパスを検証するので、不具合の早期発見につながり不具合修正コストを削減します。 このツールは、既存のコードに遡及的に使用して、潜在的な脆弱性を検出することも可能です。

CodePeerは独自の「ボトムアップ」アプローチを使用しており、各サブプログラムは個別に解析され、その結果は呼び出し元解析のために要約/伝達されます。 これにより、CodePeerは大規模なアプリケーションも解析可能で、ドライバやスタブを必要とせずに部分的な解析（たとえば、ライブラリや、コンテキストを含まない特定のユニット）も可能です。 さらに、マルチコアアーキテクチャを利用して、実行時間を高速化する際にも有効です。

 

CodePeerの機能とツールセット

CodePeerは以下のエラーを検出可能

🔸バッファオーバーフロー、数値オーバーフロー、ヌルポインター逆参照、ゼロ除算など、定義されたランタイムの不正

🔸非初期化変数の使用

🔸到達不能、冗長、または無用のコード

🔸並列実行不良（データ競合状態）

🔸事前/事後条件、アサーション、タイプ・インバリアント（type invariants）、サブタイププリディケイト（subtype predicates）を含むユーザー定義チェックの不正

CodePeerには、以下の検査ツールも付属

🔹コーディング標準チェッカ（GNATcheck）

🔹ソフトウェア安全規格の認定を受けているツール

🔹メトリクス計算/レポート作成（GNATmetric）

CodePeerは、GNAT StudioやGNATbench 開発環境と統合され、HTML出力を表示するためのWebサーバとも統合されています。 また、JenkinsとGNATdashboardのプラグインも付属しています。

チームで活用できる多目的ツール

開発エンジニア向け：統合化作業前、コードを記述時に、問題点を検出します。

レビュー担当者向け： CWE関連の潜在的な問題点を検出してコードに注釈を付けます。

プロジェクトマネージャーと品質管理者向け：脆弱性を解析し、問題点を特定します。

ソフトウエア監査担当者向け：脆弱性、問題箇所の特定、ならびに品質基準の遵守を評価する解析を行います。Certification Engineers, to reduce the effort needed for safety or security certification認証担当エンジニア向け：安全、セキュリティ認証に必要な労力を削減できます。

CWE互換ツール

CodePeerは、MITRE社のCommon Weakness Enumeration（CWE）互換性および有効性プログラムによりCWE互換（CWE-Compatible）として指定されており、CWEの上位25ソフトウェアエラーまたは同じクラスに含まれる、コードの弱点を検出できます。

CWE-120 (バッファオーバーフロー)

「入力バッファのサイズが出力バッファのサイズより小さいことを確認せずに入力バッファを出力バッファにコピーするプログラムは、バッファオーバーフローを引き起こします。」

CWE-131 (バッファサイズ誤計算)

「ソフトウェアは、バッファを割り当てるときに使用するサイズを正しく計算しないため、バッファオーバーフローが発生する可能性があります。」

CWE-190 (整数オーバーフローまたはラップアラウンド)

「結果の値が常に元の値よりも大きいと想定される場合、ソフトウェアは整数のオーバーフローまたはラップアラウンドが発生する可能性のある計算を実行します。 この計算がリソース管理または実行制御に使用されると、他の脆弱性が発生する可能性があります。」

CodePeerは、次のCWE weaknessを検出可能。

CWE weakness	Description
CWE 120, 124, 125, 126, 127, 129, 130, 131	Buffer overflow/underflow
CWE 136, 137	Variant record field violation, Use of incorrect type in inheritance hierarchy
CWE 190, 191	Numeric overflow/underflow
CWE 362, 366	Race condition
CWE 369	Division by zero
CWE 457	Use of uninitialized variable
CWE 476	Null pointer dereference
CWE 561	Dead (unreachable) code
CWE 563	Unused or redundant assignement
CWE 570	Expression is always false
CWE 571	Expression is always true
CWE 628	Incorrect arguments in call
CWE 667	Improper locking
CWE 682	Incorrect calculation
CWE 820	Missing synchronization
CWE 821	Incorrect synchronization
CWE 835	Infinite loop

DO-178BおよびEN 50128安全規格認定

CodePeerは、民間航空機システム向けのDO-178Bソフトウェア規格の検証ツールとして認定されており、ソフトウェアの正確性と一貫性に関するそのobjectivesに関連するアクティビティが自動化されます。EN 50128の認定も受けており、鉄道の制御および保護システムのソフトウェアに関する国際安全規格です。 EN 50128認定資料は、境界値解析（バッファオーバーフローなどの検出）、制御フロー解析（到達不能コードなどの検出）、ならびに、データフロー解析（非初期化変数の参照などのエラー検出）に対応しています。