Loading article…
 | |
| 開発者 | Commissariat à l'Énergie Atomic ( CEA-List ) およびInria |
|---|---|
| リポジトリ |
|
| 書かれた | オカムル |
| オペレーティング·システム | Microsoft Windows、FreeBSD、OpenBSD、Linux、Mac OS X |
| 利用可能 | 英語 |
| タイプ | 形式検証、静的コード解析 |
| ライセンス | 大部分はLGPL、一部はBSDライセンス |
| Webサイト | frama-c.com |
Frama-C [1] は、Framework for Modular Analysis of C programsの略です。Frama-Cは、 Cプログラム用の相互運用可能なプログラムアナライザーのセットです。Frama-Cは、フランスの原子力・代替エネルギー委員会（CEA-List）[2]とInriaによって開発されました。また、 Core Infrastructure Initiativeからも資金提供を受けています。Frama-Cは静的アナライザーとして、プログラムを実行せずに検査します。その名前にもかかわらず、このソフトウェアはフランスのプロジェクトFramasoftとは関係ありません。
建築
Frama-CはEclipse（ソフトウェア）やGIMPに匹敵するモジュラープラグインアーキテクチャ[3]を備えています。
Frama-C は CIL ( C 中間言語)を利用して抽象構文ツリーを生成します。抽象構文ツリーはANSI/ISO C 仕様言語(ACSL) で記述された注釈をサポートします。
いくつかのモジュールは抽象構文ツリーを操作してANSI/ISO C 仕様言語(ACSL) 注釈を追加できます。よく使用される[あいまい]プラグインには次のものがあります。
- 値分析 – プログラム内の各変数の値または可能な値のセットを計算します。このプラグインは抽象解釈技術を使用し、他の多くのプラグインがその結果を利用します。
- Jessie – 演繹的にプロパティを検証します。JessieはWhy [4]またはWhy3バックエンドに依存して、証明義務をZ3、Simplify、Alt-Ergoなどの自動定理証明器やCoqやWhyなどの対話型定理証明器に送信できるようにします。Jessieを使用すると、バブルソートの実装やおもちゃの電子投票システムがそれぞれの仕様を満たしていることを証明できます。Jessieは分離ロジックに触発された分離メモリモデルを使用します。
- WP (Weakest Precondition) – Jessieに似ており、プロパティを演繹的に検証します。Jessie とは異なり、メモリ モデルに関するパラメータ化に重点を置いています。WP は、C プログラムを直接 Why 言語にコンパイルする Jessie とは異なり、値分析プラグインなどの他の Frama-C プラグインと連携するように設計されています。WP は、オプションで Why3 プラットフォームを使用して、他の多くの自動化されたインタラクティブな証明器を呼び出すことができます。
- E-ACSL – ( Executable ACSLの略) プログラムをインストルメント化して、プロパティの実行時検証を実行します。値分析や WP などの他のプラグインを補完することもできます (たとえば、他のプラグインでは静的に検証できなかったプロパティの実行時のアサーションをチェックするなど)。
- 影響分析 - C ソース コードの変更による影響を強調表示します。
- スライシング –プログラムのスライスを可能にします。これにより、いくつかの特定のプロパティを保持したまま、より小さな新しいCプログラムを生成することができます。[5]
- スペアコード - C プログラムから不要なコードを削除します。
その他のプラグインは次のとおりです:
特徴
Frama-C は次の目的で使用できます。
- 自分で書いていない C コードを理解する。特に、Frama-C を使用すると、値のセットを観察し、プログラムを短いプログラムに分割し、プログラム内を移動することができます。
- コードの形式的な特性を証明する。ANSI /ISO C仕様言語で記述された仕様を使用することで、あらゆる動作に対するコードの特性を保証することができる。Frama-Cは浮動小数点数を処理します。[6]
- カスタムプラグインを使用してCソースコードにコーディング標準またはコード規約を強制する[7]
- Cコードをセキュリティ上の欠陥から保護するため[8]
参照
- SPARK（プログラミング言語）
- フラマトム— フラマCと長期にわたるパートナーシップを結んでいる[9] [10]
参考文献
- ^ 「Frama-C」. frama-c.com . 2016年11月5日閲覧。
- ^ CEA LIST. 「CEA LIST、スマートデジタルシステム」。2016年11月5日閲覧。
- ^ Pascal Cuoq; et al. (2009 年 8 月). 「経験レポート: 産業用レベルの静的解析フレームワークとしての OCaml」. ACM SIGPLAN Notices . 44 (9): 281–286. doi :10.1145/1631687.1596591.
- ^ 「なぜホームページなのか」。
- ^ Benjamin Monate、Julien Signoles (2008)。「コードのセキュリティのためのスライシング」。信頼できるコンピューティング-課題とアプリケーション。コンピュータサイエンスの講義ノート。Vol. 4968/2008。pp. 133–142。doi :10.1007/978-3-540-68979-9_10。ISBN 978-3-540-68978-2。
- ^ Sylvie Boldo ; Thi Minh Tuyen Nguyen (2010). 「ハードウェアに依存しない数値プログラムの証明」(PDF) . NFM 2010 の議事録。
- ^ David Delmas、Stéphane Duprat、Victoria Moya Lamiel、Julien Signoles。「Taster、コーディング標準を強制する Frama-C プラグイン」(PDF)。Embedded Real Time Software and Systems 2010、トゥールーズ、フランス。
- ^ Jonathan-Christofer Demay、Éric Totel、Frédéric Tronel (2009)。「非制御データ攻撃の検出のための自動ソフトウェアインストルメンテーション」。侵入検知の最近の進歩。コンピュータサイエンスの講義ノート。Vol. 5758/2009。pp. 348–349。doi : 10.1007/ 978-3-642-04342-0_19。ISBN 978-3-642-04341-3。
- ^ 「Frama- Cで実際の C コードを検証して学んだ教訓」。YouTube。2021年 7 月 11 日。
- ^ https://cea.hal.science/cea-04477151/file/2021_cacm.pdf
外部リンク
- 公式サイト
- Frama-C ディスカッション リスト 2008-12-30 にWayback Machineでアーカイブされました
- Frama-C バグ追跡システム