Serious logic vulnerabilities exist in real-world services that use security protocols such as OpenID, OAuth, and PayPal Standard. We introduce Certified Symbolic Transaction (CST), an approach for building provably secure multiparty online services. The kind of provable security that we focus on is actually an extreme form, which we call protocol-agnostic security – it holds a system implementation to an end-to-end global security predicate completely independent of the adopted protocol, and thus fundamentally guards the implementation against logic flaws in the protocol and developers’ misunderstandings of the protocol.
We show that it is entirely practical for developers to apply CST on real-world systems. Unlike traditional verification approaches, CST invokes static verifications at runtime: it treats every multiparty transaction as a runtime process for creating a proof obligation for a general-purpose (thus protocol-agnostic) static program verifier. We have applied CST on five commercially deployed systems, and show that, with only tens (or 100+) of lines of code changes per party, the enhanced implementations achieve protocol-agnostic security. We also stress-tested CST by building a gambling system integrating four different services, for which there is no existing protocol to follow. Our security analysis shows that 12 out of 14 logic vulnerabilities reported in the literature will be prevented by CST. Because transactions are symbolic and cacheable, CST has near-zero amortized runtime overhead. We make the source code of these systems public, which can be immediately deployed for real-world uses.