It is a well-known fact that it is usually easier to check a proof than to generate one. This idea is used in a mechanism called proof-carrying code. Using PCC, the designer of a host system defines a safety policy and makes it public. Then, using this policy, any application writer can provide binaries in a special form that contains, in addition to the native code, a formal proof of that the code adheres to the safety policy. The host system can then quickly and easily validate the proof without using cryptography and without consulting any external trusted entities. If the validation succeeds, the code is guaranteed to respect the safety policy without relying on run-time checks. This guarantee holds even if the certificate or native code are tampered with.
One of the major tools for creating PCC binaries is the certifying compiler. A certifying compiler starts with a high-level source language---in this case, Java---and compiles it into optimized native code with an attached proof of safety. This talk will describe a certifying compiler for Java, including an overview of its internal structure and a short demonstration of how it works. This will be followed by a brief discussion of the benefits that PCC provides in compiler construction, and directions for future work.