データフロー分析とはコールフローグラフ（CFG）を使ってプログラムを分析する手法です。ソフトウェアのセキュリティ対策にもデータフロー分析は広く利用されています。例えば、静的ソースコード検査ツールは静的（＝プログラムを動作させず）にプログラム実行時のデータフローを分析し、問題を発見する手法です。 コールフローグラフ データフロー分析の基礎知識はハーバード大学コ…

脆弱性を呼ばれた側の責任にする、は常に通用する考え方ではありません。 ライブラリに脆弱性があるなら、ライブラリの脆弱性を直す（呼ばれた側の責任にする） 外部アプリケーションに脆弱性があるなら、外部アプリケーションの脆弱性を直す（呼ばれた側の責任する） は一見正しく見えます。しかし、通用しません。 理由は簡単で、セキュリティ上困った動作をするライブラリやプログ…

形式的検証とは 形式的検証（けいしきてきけんしょう）とは、ハードウェアおよびソフトウェアのシステムにおいて形式手法や数学を利用し、何らかの形式仕様記述やプロパティに照らしてシステムが正しいことを証明したり、逆に正しくないことを証明することである 英語ではFormal Verificationとされ formal verification is the act…

少し設計よりの話を書くとそれに関連する話を書きたくなったので出力の話は後日書きます。 契約による設計（契約プログラミング）（Design by Contract - DbC）は優れた設計・プログラミング手法です。契約による設計と信頼境界線について解説します。