Self-Verifying Execution (Position Paper)

Matt McCutchen, Daniel Song, Shuo Chen, Shaz Qadeer

Proceedings of the IEEE Cybersecurity Development Conference (SecDev) |

Published by IEEE - Institute of Electrical and Electronics Engineers

This paper proposes a notion called self-verifying execution (SVX). SVX substantially lowers several hurdles that real-world programmers face when adopting traditional program verification approaches. The current focus of SVX is to verify safety properties for programs that implement cloud-API integrations. We envision that, if adopted by real-world programmers, the SVX approach will enable a positive paradigm shift in the community toward more rigorous reasoning about security goals of cloud-API protocols.