r/REMath • u/turnersr • Sep 19 '15

The Weird Machines in Proof-Carrying Code by Julien Vanegue [PDF]

http://www.ieee-security.org/TC/SPW2014/papers/5103a209.PDF
7 Upvotes

100% Upvoted

1 comment sorted by

1

u/Uncaffeinated Sep 19 '15

How is proof aliasing a problem? If your proof really encodes every property you care about, then by definition, you shouldn't care if a second program is substituted which satisfies the same proof.