Title:  Foundational proof-carrying code for proving memory safety of machine language programs

Abstract:

This presentation focuses on proof-carrying code (PCC), a mechanism for ensuring the safety of a host system when running programs obtained from some code producer. In particular, we consider foundational proof-carrying code (FPCC) that provides increased security and greater flexibility in the construction of proofs of safety. An example of the machine instruction program that manipulates an integer list and its semantic encoding will be given, as well as the typing rules for the memory safety policy. The safety proof of this example program is formalized in the Coq proof assistant. And a project will be introduced which (written in OCaml) implements a verification condition generator (VCG) to help automate proofs in Coq of memory safety.