コンピュータサイエンスにおいて、静的プログラム解析（静的解析または静的シミュレーションとも呼ばれる）は、統合環境でプログラムの実行中に実行される動的プログラム解析とは対照的に、コンピュータプログラムを実行せずに実行される解析である。[1] [2]

この用語は通常、自動化ツールによって実行される分析に適用されます。人間による分析は、一般的に「プログラム理解」、「プログラム理解」 、または「コードレビュー」と呼ばれます。コードレビューでは、ソフトウェア検査やソフトウェアウォークスルーも使用されます。ほとんどの場合、分析はプログラムのソースコードのバージョンに対して実行されますが、場合によってはオブジェクトコードの一部に対して実行されることもあります。

リソース認証における2つの主要なアプローチは、静的解析（SA）と暗黙的計算複雑性（ICC）です。SA​​は本質的にアルゴリズム的です。つまり、選択された広範なプログラミング言語に焦点を当て、その言語で与えられたプログラムが実行可能かどうかを構文的な手段によって判断しようとします。対照的に、ICCは、複雑性クラスを定義する専用のプログラミング言語またはメソッドを最初から作成しようとします。したがって、SAはコンパイル時間に焦点を当てており、プログラマーに負担をかけません。一方、ICCは言語設計の分野です。

— D.レイヴァント（2020）[3]

根拠

ツールによって実行される解析の洗練度は、個々の文や宣言の振る舞いのみを考慮するもの[4]から、プログラムのソースコード全体を解析に含めるものまで様々です。解析から得られる情報の用途は、潜在的なコーディングエラーの指摘（例：lintツール）から、特定のプログラムの特性（例：その振る舞いが仕様と一致すること）を数学的に証明する 形式手法まで多岐にわたります。

ソフトウェアメトリクスとリバースエンジニアリングは、静的解析の一形態と言える。特に組み込みシステムの開発においては、いわゆるソフトウェア品質目標を定義することで、ソフトウェアメトリクスの導出と静的解析が併用されることが増えている。[5]

静的解析の商業的利用は、安全性が重要なコンピュータシステムで使用されるソフトウェアの特性検証​​や、潜在的に脆弱なコードの特定において増加しています。[6]例えば、以下の業界では、ますます高度化・複雑化するソフトウェアの品質を向上させる手段として、静的コード解析の利用が認識されています。

  1. 医療ソフトウェア：米国食品医薬品局（FDA）は医療機器における静的解析の使用を認めている。[7]
  2. 原子力ソフトウェア：英国では、原子力規制庁（ONR）が原子炉保護システムにおける静的解析の使用を推奨している。[8]
  3. 航空ソフトウェア（動的解析との組み合わせ）[9]
  4. 自動車と機械（機能安全機能は、各自動車製品開発段階の不可欠な部分を形成します。ISO 26262、セクション 8）。

VDCリサーチによる2012年の調査では、調査対象となった組み込みソフトウェアエンジニアの28.7%が静的解析ツールを利用しており、39.7%が2年以内に利用する予定であると報告されています。[10] 2010年の調査では、欧州の研究プロジェクトでインタビューを受けた開発者の60%が、少なくとも基本的なIDE組み込みの静的解析ツールを利用していることがわかりました。しかし、その他の（おそらくより高度な）解析ツールを追加で利用していたのはわずか10%程度でした。[11]

アプリケーションセキュリティ業界では、静的アプリケーションセキュリティテスト（SAST）という名称も用いられています。SASTは、Microsoft [12]が定義したセキュリティ開発ライフサイクル（SDL）の重要な部分であり、ソフトウェア企業では一般的な手法となっています。[13]

ツールの種類

OMG（オブジェクト管理グループ）は、ソフトウェア品質の測定と評価に必要なソフトウェア分析の種類に関する調査を発表しました。「CISQ勧告に準拠した、回復力があり、安全で、効率的で、変更が容易なITシステムを実現する方法」に関するこの文書では、ソフトウェア分析の3つのレベルについて説明しています。[14]

ユニットレベル
特定のプログラムまたはサブルーチン内で、そのプログラムのコンテキストに接続せずに実行される分析。
技術レベル
ユニット プログラム間の相互作用を考慮した分析により、プログラム全体をより総合的かつセマンティックに把握し、問題を発見して明らかな誤検知を回避します。
システムレベル
特定のテクノロジーやプログラミング言語に限定されず、ユニット プログラム間の相互作用を考慮した分析。

ソフトウェア分析のさらなるレベルを定義できます。

ミッション/ビジネスレベル
エンタープライズまたはプログラム/ミッション層の活動の一環としてソフトウェアシステムを運用するために実装されているビジネス/ミッション層の用語、ルール、およびプロセスを考慮した分析。これらの要素は特定の技術やプログラミング言語に限定されず、多くの場合複数の言語に分散して実装されていますが、ミッションアシュアランスのためのシステム理解を目的として静的に抽出・分析されます。

形式手法

形式手法とは、ソフトウェア（およびコンピュータハードウェア）の解析において、厳密な数学的手法のみを用いて結果を得る手法を指す。用いられる数学的手法には、表示的意味論、公理的意味論、操作的意味論、抽象的解釈などがある。

停止問題に直接還元することで、（チューリング完全言語であれば）任意のプログラムにおける実行時エラー（より一般的には、プログラムの最終結果における仕様違反のすべて）を見つけることが決定不可能であることを証明できます。つまり、任意のプログラムが実行時エラーを起こすかどうかを常に正確に答えられる機械的な方法は存在しません。この結果は、1930年代のチャーチ、ゲーデル、チューリングの研究に由来します（停止問題とライスの定理を参照）。多くの決定不可能な問題と同様に、有用な近似解を与えることを試みることは可能です。

形式的静的解析の実装技術には次のようなものがある: [15]

データ駆動型静的解析

データ駆動型静的解析は、広範なコードベースを活用してコーディングルールを推論し、解析精度を向上させます。[17] [18]例えば、GitHubで利用可能なすべてのJavaオープンソースパッケージを利用して、優れた解析戦略を学習することができます。ルール推論には機械学習技術を活用できます。[19]また、過去の大量の修正や警告から学習することも可能です。[17]

修復

静的解析ツールは警告を生成します。特定の種類の警告については、自動修復技術を設計・実装することが可能です。例えば、LogozzoとBallはC# cccheckの自動修復技術を提案しています。[20]

参照

参考文献

  1. ^ Wichmann, BA; Canning, AA; Clutterbuck, DL; Winsbarrow, LA; Ward, NJ; Marsh, DWR (1995年3月). 「産業的視点から見た静的解析」(PDF) . Software Engineering Journal . 10 (2): 69– 75. doi :10.1049/sej.1995.0010. 2011年9月27日時点のオリジナル(PDF)からのアーカイブ。
  2. ^ Egele, Manuel; Scholte, Theodoor; Kirda, Engin; Kruegel, Christopher (2008-03-05). 「自動化された動的マルウェア分析技術とツールに関する調査」 . ACM Computing Surveys . 44 (2): 6:1–6:42. doi :10.1145/2089125.2089126. ISSN  0360-0300. S2CID  1863333.
  3. ^ Leivant, Daniel (2020). 「多項式時間のための汎用命令型言語」. arXiv : 1911.04026 [cs.CC].
  4. ^ Khatiwada, Saket; Tushev, Miroslav; Mahmoud, Anas (2018-01-01). 「十分なセマンティクス：IRベースのソフトウェアバグ特定のための情報理論的アプローチ」 .情報・ソフトウェア技術. 93 : 45– 57. doi :10.1016/j.infsof.2017.08.012.
  5. ^ 「ソースコードのソフトウェア品質目標」Wayback Machineに2015年6月4日アーカイブ（PDF）。議事録：Embedded Real Time Software and Systems 2010 Conference、ERTS2010.org、トゥールーズ（フランス）：Patrick Briand、Martin Brochet、Thierry Cambois、Emmanuel Coutenceau、Olivier Guetta、Daniel Mainberte、Frederic Mondot、Patrick Munier、Loic Noury、Philippe Spozio、Frederic Retailleau。
  6. ^ 精密な静的および実行時解析によるソフトウェアセキュリティの向上 Archived 2011-06-05 at the Wayback Machine (PDF)、Benjamin Livshits、セクション7.3「セキュリティのための静的手法」。スタンフォード大学博士論文、2006年。
  7. ^ FDA (2010-09-08). 「FDAにおける輸液ポンプソフトウェアの安全性研究」. 食品医薬品局. 2010年9月1日時点のオリジナルよりアーカイブ。 2010年9月9日閲覧。
  8. ^ コンピュータベースの安全システム - デジタルコンピュータベースの保護システムのソフトウェア面の評価に関する技術ガイダンス、「コンピュータベースの安全システム」(PDF) 。 2013年1月4日時点のオリジナル(PDF)からアーカイブ。 2013年5月15日閲覧。
  9. ^ ポジションペーパー CAST-9. ソフトウェア保証における安全工学アプローチの評価に関する考慮事項 Archived 2013-10-06 at the Wayback Machine // FAA、認証機関ソフトウェアチーム（CAST）、2002年1月：「検証。申請者/開発者は、静的解析と動的解析の両方の組み合わせを指定し、ソフトウェアに適用する必要があります。」
  10. ^ VDC Research (2012-02-01). 「組み込みソフトウェア品質のための自動欠陥予防」VDC Research. 2012年4月11日時点のオリジナルよりアーカイブ。 2012年4月10日閲覧。
  11. ^ Prause, Christian R., René Reiners, Silviya Dencheva. 「高度に分散化された研究プロジェクトにおけるツールサポートの実証的研究」 Global Software Engineering (ICGSE), 2010 第5回IEEE国際会議 IEEE, 2010 https://ieeexplore.ieee.org/Xplore/login.jsp?url=%2Fielx5%2F5581168%2F5581493%2F05581551.pdf&authDecision=-203
  12. ^ M. Howard、S. Lipner著『セキュリティ開発ライフサイクル：SDL：より安全なソフトウェアを開発するためのプロセス』Microsoft Press、2006年。ISBN 978-0735622142
  13. ^ Achim D. BruckerとUwe Sodan. 大規模アプリケーションにおける静的セキュリティテストの導入（2014年10月21日アーカイブ、Wayback Machine） . GI Sicherheit 2014. Lecture Notes in Informatics, 228, 91-101ページ、GI, 2014.
  14. ^ 「OMGホワイトペーパー | CISQ - 情報とソフトウェア品質のためのコンソーシアム」(PDF) 。 2013年12月28日時点のオリジナルよりアーカイブ(PDF) 。 2013年10月18日閲覧。
  15. ^ Vijay D'Silva他 (2008). 「形式的ソフトウェア検証のための自動化技術の概説」(PDF) . Transactions On CAD. 2016年3月4日時点のオリジナルよりアーカイブ(PDF) . 2015年5月11日閲覧.
  16. ^ Jones, Paul (2010-02-09). 「医療機器ソフトウェア解析への形式手法に基づく検証アプローチ」. Embedded Systems Design. 2011年7月10日時点のオリジナルよりアーカイブ。2010年9月9日閲覧。
  17. ^ ab 「他者の失敗から学ぶ：データ駆動型コード分析」www.slideshare.net . 2015年4月13日。
  18. ^ Söderberg, Emma; Church, Luke; Höst, Martin (2021-06-21). 「オープンデータ駆動型静的コード解析のユーザビリティ向上とその課題」.ソフトウェアエンジニアリングにおける評価と評価. EASE '21. ニューヨーク州ニューヨーク: Association for Computing Machinery. pp.  272– 277. doi :10.1145/3463274.3463808. ISBN 978-1-4503-9053-8。
  19. ^ Oh, Hakjoo; Yang, Hongseok; Yi, Kwangkeun (2015). 「ベイズ最適化によるプログラム分析適応戦略の学習」. 2015 ACM SIGPLAN 国際オブジェクト指向プログラミング、システム、言語、アプリケーション会議 - OOPSLA 2015 論文集. pp.  572– 588. doi :10.1145/2814270.2814309. ISBN 9781450336895. S2CID  13940725。
  20. ^ Logozzo, Francesco; Ball, Thomas (2012-11-15). 「モジュール式で検証済みの自動プログラム修復」 . ACM SIGPLAN Notices . 47 (10): 133– 146. doi :10.1145/2398857.2384626. ISSN  0362-1340.

さらに読む

  • Ayewah, Nathaniel; Hovemeyer, David; Morgenthaler, J. David; Penix, John; Pugh, William (2008). 「静的解析を用いたバグの発見」. IEEE Software . 25 (5): 22– 29. CiteSeerX  10.1.1.187.8985 . doi :10.1109/MS.2008.130. S2CID  20646690.
  • ブライアン・チェス、ジェイコブ・ウェスト（Fortify Software）（2007年）『静的解析によるセキュアプログラミング』Addison-Wesley社、ISBN 978-0-321-42477-8。
  • フレミング・ニールソン、ハンネ・R・ニールソン、クリス・ハンキン（2004年12月10日）『プログラム分析の原則』（1999年（2004年訂正）版）シュプリンガー社、ISBN 978-3-540-65410-0。
  • 「抽象解釈と静的解析」、国際意味論・応用冬季講座2003、David A. Schmidt著