Self-Verifying Execution (Position Paper) - McCutchen, Matt; Song, Daniel; Chen, Shuo; Qadeer, Shaz (Proceedings of the IEEE Cybersecurity Development Conference (SecDev), 2016)
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.