PCCやTALって何？

PCC (Proof Carrying Code) やTAL (Typed Assembly Language)というのは一言で言うと、アセンブリ言語（又は機械語）に付加情報をつけてプログラムの正しさを検証できるようにしたものです。従来は、プログラムの正しさの検証は、ML での型検査に代表されるように、高級言語のソースプログラムレベルで行なわれるのが普通でした（し、今でもそれは行なわれています）。ところが、最近になって、バイトコード(Javaなど）や機械語など低レベル言語での検証も重要視されてきています。それには次のような理由が挙げられます。

インターネットの普及に伴い、今まで以上に容易に他人の書いたプログラムを取ってきて、即座に実行することが可能になった。その際、取ってくるプログラムは必ずしもソースプログラムではなく、バイトコードや機械語であることが多い（仮にソースコードも提供されていても、それをコンパイルしてから実行するのには時間がかかるし、かといってバイトコードや機械語が付随していたソースコードに対応しているとはかぎらない）。
システムが巨大になり、一つのシステムを単一のプログラミング言語で記述するのではなく、複数のプログラミング言語で記述することが多くなった。その際、言語間のインタフェースの整合性(calling conventionがあっているかどうかなど）をチェックするには低レベル言語で行なわなければならない。
コンパイラが本当に正しいコードを出力するという保証がない（コンパイラにバグがあるかもしれない）ので、出力されたコードの検査をしてから実行したい。

そこで、登場したのが、PCCやTAL, Java のbytecode verifier というわけです。 PCC ではHoare 論理に似た体系を利用して、プログラムの提供者は、機械語にそのプログラムがどのような性質を満たすかとその証明を付加し、使用する側はその証明が正しいことを検査してからプログラムを実行します。そうすると、例えば「レジスタr0 に格納されたアドレスにはアクセスしない」というような性質を保証することができます。 TAL は、普通のアセンブリ言語に型情報を加えたもので、「レジスタr1 には整数が入っている」とか「レジスタr2にはレジスタr1に整数を格納してjumpすべきアドレスが入っている」というような性質を保証することができ、型つきなので、当然型検査が通ったアセンブリプログラムを実行したらcore dump することはありません。興味のある人は課題６を選んでみて下さい。

課題のリスト

koba@is.s.u-tokyo.ac.jp