Proof-carrying code とは

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