Loading article…
証明付きコード（PCC）は、ホストシステムがアプリケーションの実行可能コードに付随する形式証明を通じて、アプリケーションの特性を検証できるようにするソフトウェアメカニズムです。ホストシステムは証明の妥当性を迅速に検証し、証明の結論を自身のセキュリティポリシーと比較することで、アプリケーションが安全に実行できるかどうかを判断できます。これは、メモリの安全性を確保する（バッファオーバーフローなどの問題を防止する）際に特に役立ちます。
1996年に発表された証明コードに関する最初の論文[ 1 ]では、パケットフィルタを例として使用しました。ユーザーモードのアプリケーションは、マシンコードで記述された関数をカーネルに渡し、その関数がアプリケーションが特定のネットワークパケットの処理に関心があるかどうかを判断します。パケットフィルタはカーネルモードで実行されるため、カーネルデータ構造に書き込む悪意のあるコードが含まれている場合、システムの整合性が損なわれる可能性があります。この問題に対する従来のアプローチには、パケットフィルタリング用のドメイン固有言語の解釈、各メモリアクセスに対するチェックの挿入（ソフトウェア障害分離）、および実行前にカーネルによってコンパイルされる高水準言語でのフィルタの記述などがあります。これらのアプローチは、パケットフィルタのように頻繁に実行されるコードに対してパフォーマンス上の欠点がありますが、カーネル内コンパイルのアプローチは例外で、コードは実行されるたびにではなく、ロードされたときにのみコンパイルされます。
証明付きコードでは、カーネルがセキュリティポリシーを公開し、パケットフィルタが従わなければならない特性を指定します。たとえば、パケットフィルタはパケットとそのスクラッチメモリ領域以外のメモリにはアクセスしません。定理証明器を使用して、マシンコードがこのポリシーを満たしていることを示します。この証明の手順は記録され、カーネルプログラムローダーに渡されるマシンコードに添付されます。プログラムローダーは証明を迅速に検証できるため、その後は追加のチェックなしでマシンコードを実行できます。悪意のある第三者がマシンコードまたは証明のいずれかを変更した場合、結果として得られる証明付きコードは無効になるか、または無害になります（セキュリティポリシーは依然として満たします）。