Executable content presents special problems for users of secure systems. Not only must they worry about attackers from without scrutinizing the external interfaces to their systems for vulnerabilities, but also they have to worry about attackers subverting their systems from within.

Even as plain clever individuals -- as macro-viruses, can put a platform as the macro language in Microsoft Word to evil use clearly attests. In order to limit its potential for damage, executable content must be subject to scrutiny before being allowed to execute. There are several methods for verifying executable content and identifying erroneous or malicious code.

The Java byte-code verifier examines Java byte-code and verifies that it is safe to execute. The tests it performs ensure that a piece of code doesn't access a memory location as if it contained an integer at one point and later as if it contained a reference to a class, and that object fields and methods are always accessed via the correct class type.

The Java byte-code verifier is complicated -- early implementations suffered from bugs that lessened the security offered by the Java environment. Java byte-code verification also places most of the burden for detecting incorrect code on the shoulders of the recipient.

Proof-carrying code shifts the burden of proving that a piece of unknown code is safe to execute from the recipient to the creator. The code creator generates a formal proof that the proposed code meets the safety requirements specified by the recipient. The recipient then uses a much simpler proof-checker to check the proof against the accompanying code.