今日，ネットワークを介したプログラムの配信・ダウンロード・実行は日常的に行われており，悪性プログラムから計算機を守る技術の重要性はますます高まってきています．
現在，公開鍵暗号を応用した電子署名つきプログラム配信方式が広く実用化されています．この方式では，開発者が電子的な「印鑑」をプログラムに捺印し，それを受け取った利用者がその「印鑑」を検証することで，プログラムが信頼できる開発者から送られてきたことを確認できるようになっています．ところが，開発者が信頼できたからと言ってプログラムも信頼できるとは限りません．信頼できる開発者が慎重に作ったとしてもプログラムにはバグが混入しやすいからです．プログラムそのものの安全性を利用者が直接検証することはできないのでしょうか？
それを可能にする技術として，安全性証明つきプログラム配信方式（Proof-Carrying Code, PCC）が提案されています．この方式では，プログラムが安全に動作すること（例えば，与えられた入力条件のもとでプログラムを実行した場合，結果が出力条件を満たし，実行時には禁止されたメモリ領域へのアクセスが全くないこと）の数学的証明をプログラムに添付し，プログラムと証明を同時に流通させます．利用者は受け取った証明を証明チェッカと呼ばれるソフトウェアを用いて機械的に検査することで，プログラムの安全性を自動的に検証することができます．中規模サイズのプログラムの比較的簡単な安全性に対しては，この方式の有効性が実験によって示されています．
しかし，安全性証明はプログラム本体の指数オーダのサイズになりうることが知られています．つまり，プログラムと証明をそのままペアにして流通させる上記方式を大規模なプログラムに素朴に適用した場合，巨大な証明のチェックを利用者に強いることになってしまい，とても現実的とは言えません．
巨大な証明を一気にチェックするのは困難ですが，証明の部分的なチェックを繰返すだけならば容易です．このアイデアに基づき，私たちは，上記方式を対話的に拡張した対話型安全性証明つきプログラム配信方式（Interactive Proof-Carrying Code, iPCC）を提案しています [1, 2, 3, 4, 5]．まだ理論段階ではありますが，この方式により，指数オーダの巨大な安全性証明を効率的に検証できる可能性があります．
ネットワークのブロードバンド化により，流通するコンテンツはますます巨大・複雑になることが予想されます．私たちは，大規模なプログラムの複雑な安全性を効率的に検証する技術の探究を通じて，安全なプログラム流通のための基盤を創出していきたいと思っています．