Two different approaches to Proof-Carrying Code (PCC)
Abstract:
Proof carrying
code is a new technology and it is promising; it has been used for safely
executing untrusted code. It is a technique which
allows a code producer to associate a program with a proof for its safety; the
proof should be machine-checkable. Generally for a typical PCC case, there is a
code receiver, a code producer. The code receiver builds a set of safety rules
to guarantee the code will be executed safely. The code producer sets up a
formal proof which to prove the safety rules generated by the code receiver.
The verifier is used by the code consumer to get a set of verification
condition (VC) to validate the safety of the code. The verifier consists of an
instruction decoder and a verification condition generator (VCG). The
instruction decode is responsible for interpreting individual
instructions’ semantics; while the verification condition generator is
responsible for handling code’s control flow. Verification condition is
generated by the verification condition generator, and it should be proved by
the safety rules established by the code consumer. Then the code receiver will
validate the proof by using a proof validator to
check the proof is valid for some level and the untrusted
code is safe to execute.