証明を携帯するコード

本論文では、証明を携帯するコード（PCC）について説明します。これは、ホストシステムが信頼できないソースから提供されたプログラムを安全に実行できるかを確実に判断できるメカニズムです。これを可能にするために、信頼できないコードの作成者は、コードの安全ポリシーへの準拠を証明する安全性証明書を提供しなければなりません。ホストは、その後、暗号化を使用せず、外部エージェントに相談することなく、証明書を簡単かつ迅速に検証できます。PCCの予備的な経験を得るために、私たちはいくつかのケーススタディを実施しました。本論文では、証明を携帯するコードがいかにしてMLプログラムの安全なアセンブリ言語拡張を開発するために使用されるかを示します。このケーススタディの文脈において、私たちは安全ポリシー、安全性証明、および証明検証の具体的表現の適切性を示し、証明します。最後に、他の技術を使用して開発された類似のフィルタよりも高速で、特定のオペレーティングシステムの安全ポリシーに対して形式的に安全であることを保証されたネットワークパケットフィルタを開発するために、証明を携帯するコードをどのように使用するかについて簡単に論じます。