証明コード

証明付きコード( PCC ) は、アプリケーションの実行可能コードに付随する正式な証明を介して、ホスト システムがアプリケーションのプロパティを検証できるようにするソフトウェア メカニズムです。ホスト システムは、証明の有効性を迅速に検証し、証明の結論を独自のセキュリティ ポリシーと比較して、アプリケーションの実行が安全かどうかを判断できます。これは、メモリの安全性を確保する(つまり、バッファ オーバーフローなどの問題を防ぐ)場合に特に役立ちます。

証明付きコードは、1996 年にGeorge NeculaとPeter Leeによって最初に説明されました。

1996 年の証明付きコードに関する最初の出版物^[1]では、パケット フィルタを例として使用していました。ユーザー モード アプリケーションは、マシン コードで記述された関数をカーネルに渡します。この関数は、アプリケーションが特定のネットワーク パケットの処理に関心があるかどうかを判断します。パケット フィルタはカーネル モードで実行されるため、カーネル データ構造に書き込む悪意のあるコードが含まれていると、システムの整合性が損なわれる可能性があります。この問題に対する従来のアプローチには、パケット フィルタリング用のドメイン固有言語の解釈、各メモリ アクセスに対するチェックの挿入 (ソフトウェア障害分離)、実行前にカーネルによってコンパイルされる高級言語でのフィルタの記述などがあります。これらのアプローチは、パケット フィルタのように頻繁に実行されるコードではパフォーマンス上の不利な点があります。ただし、カーネル内コンパイル アプローチは例外で、このアプローチでは、実行されるたびにではなく、ロードされたときにのみコードをコンパイルします。

証明付きコードでは、カーネルは、パケット フィルタが従う必要があるプロパティを指定するセキュリティ ポリシーを公開します。たとえば、パケット フィルタは、パケットとそのスクラッチ メモリ領域の外部のメモリにアクセスしません。定理証明器は、マシン コードがこのポリシーを満たしていることを示すために使用されます。この証明の手順は記録され、カーネル プログラム ローダーに渡されるマシン コードに添付されます。プログラム ローダーは、証明を迅速に検証し、その後は追加のチェックなしでマシン コードを実行できます。悪意のある人物がマシン コードまたは証明のいずれかを変更した場合、結果として得られる証明付きコードは無効または無害になります (セキュリティ ポリシーを満たしたまま)。

• 型付きアセンブリ言語
• プログラムの導出
• 形式検証
• バークレーパケットフィルタ

• George C. Necula および Peter Lee。証明コード。技術レポート CMU-CS-96-165、1996 年 11 月。(62 ページ)
• George C. Necula および Peter Lee。証明付きコードを使用した安全で信頼できないエージェント。モバイル エージェントとセキュリティ、Giovanni Vigna (編)、Lecture Notes in Computer Science、Vol. 1419、Springer-Verlag、ベルリン、ISBN  3-540-64792-9、1998年。
• George C. Necula.証明付きコンパイル。博士論文、カーネギーメロン大学コンピュータサイエンス学部、1998 年 9 月。