Proof Carrying Code

Mobile code is code that traverses a network during its lifetime and executes at the destination machine. In its most powerful guise, the same piece of mobile code is able to run on multiple platforms (both Unix boxes and Win32 machines, for example). This code need not be compiled to tens of platforms and distributed only after determining the target platform. Instead, mobile code is written once and then runs wherever it ends up. There are many well-known systems for creating and using mobile code, including Java, JavaScript, VBScript.
The risks of downloading and running a random person's code on your machine are clear. If the code has a virus attached, it can infect your machine. This has to address threats due to rogue code being loaded and run. Proof carrying code is a technique by which a code consumer (e.g. host can verify that code provided by an untrusted code producer (e.g. untrusted Internet agent) adhenes to predefined set of safety. A code receiver establishes a set of safety rules that guarantee safe behavior of programs, and the code producer creates a formal safety proof that proves, for the untrusted code, adherence to the safety rules. Then, the receiver is able to use a simple and fast proof validator to check, with certainty that the proof is valid and hence the untrusted code is safe to execute.


FULL PAPER LINK