Summary: In an environment where more and more code cannot be trusted to behave safety it is becoming necessary to employ mechanisms for detecting and preventing unsafe program behavior. This paper first reviews various such mechanisms and then focuses on static mechanisms with an emphasis on Proof-Carrying Code and its expressiveness. Proof-Carrying Code is a technique that allows a code receiver to verify statically that the code has certain required properties, which are stated in the form of a safety policy. To make this possible the code is accompanied by a representation of an easily checkable formal proof of compliance with the safety policy. This paper discusses first the general properties of the Proof-Carrying Code technique and then explores a particular implementation of the idea using verification condition generators. As a surprising result we prove that by adopting such an implementation choice we limit ourselves to safety properties, which constitute but a subset (albeit a very important one) of all the interesting program properties. We further speculate on what it takes to extend Proof-Carrying Code to handle more that safety properties.
For the entire collection see [Zbl 0921.00026].