Certification of Symbolic Transaction

Established: May 6, 2015

Logic flaws are prevalent in multiparty cloud services, which cause serious consequences, e.g., an attacker can make purchases without paying, or gets into other people’s accounts without password. For decades, researchers have been advocating formal verification as a solution, but in the real world developers face many major hurdles to do it. We introduce a technology that significantly lowers these hurdles, and show its effectiveness in real-world deployments.

Online services enhanced by CST

(Note: SymT-caching is an important mechanism in CST. For the demo purpose only, you can check and change the setting for caching. (opens in new tab) Disabling it forces the system to go through the entire verification procedure for every transaction.)

Source Code
Click here for source code of these implemented systems and some vPrograms of successful transactions (opens in new tab).
(Note: CST was named DSV previously. All the source files still refer to it as DSV.)

Online shopping — Amazon Simple Pay and PayPal Standard
* Video demo 1 (using PayPal) (opens in new tab)            Video demo 2 (using Amazon) (opens in new tab)
* Click here to try or test it (opens in new tab). If you don’t want to create your own accounts, we have existing ones.
+ username/password for the shopping site: [email protected]/QWer7890
+ username/password for Amazon Payments: [email protected]/QWer7890
+ username/password for PayPal: [email protected]/QWer7890

Third-party authentication — OpenID 2.0
* Video demo
(opens in new tab)
* Click here to try or test it (opens in new tab).
+ In the OpenID box, enter our IdP’s URL “http://protoagnostic.cloudapp.net:8100/” and click Login. (After idling for hours, the IdP might need to be woken up, so this step might need to be done twice.)
+ If you haven’t logged into the OpenID Provider, you will be asked for username and password. Try username “bob” and password “test”.

Live Connect SDK for authentication
* Click here to try or test it (opens in new tab).
+ Any Microsoft Live account works. You can try [email protected] with password QWer7890.

Third-party authentication — Facebook OAuth
* Video demo (opens in new tab)
* Click here to try or test it (opens in new tab).
+ Any Facebook account works. You can sign in Facebook as [email protected] with password QWer7890.

A gambling system with four independent services
* Video demo (opens in new tab)
* Click here to try or test it (opens in new tab).
+ username/password for Amazon Payments: [email protected]/QWer7890

You can inspect the web traffic to better understand CST. A nice proxy to use is Fiddler2 (opens in new tab). (Note: The SymT field was previously called “symval” and “path_digest”, as a result of our terminology change over time.)

vPrograms for some approved transactions
+ An approved purchase transaction using Amazon Simple Pay on NopCommerce: the vProgram (opens in new tab)
+ An approved purchase transaction using PayPal Standard on NopCommerce: the vProgram (opens in new tab)
+ An approved sign-on transaction using OpenID of DotNetOpenAuth: the vProgram (opens in new tab)
+ An approved sign-on transaction using Facebook’s OAuth: the vProgram (opens in new tab)
+ An approved gambling transaction: the vProgram (opens in new tab)

(Note that CST was previously named DSV. Some projects still use the term DSV.)
+ Source code of all projects (opens in new tab)
+ Source code of LiveID OAuth Sign-on SDK (opens in new tab)

People

Portrait of Shuo Chen

Shuo Chen

Senior Principal Researcher