Proof Carrying Code

Q&A

  • What is the threat model in PCC?
    • What if the proof and binary are changed at the same time by malicious compiler?

PCC @ POPL’97 1, Necula Thesis’98 2.

  1. Proof-Carrying Code. George C. Necula. POPL, 1997. ↩
  2. Compiling with Proofs. PhD thesis by George Ciprian Necula. 1998. ↩
Created Aug 13, 2019 // Last Updated Nov 27, 2019

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?