Certification of Symbolic Transaction

Established: May 6, 2015

Publications

Overview

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. 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.
(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)            Video demo 2 (using Amazon)
* Click here to try or test it. If you don’t want to create your own accounts, we have existing ones.
+ username/password for the shopping site: johndoe.test.789@gmail.com/QWer7890
+ username/password for Amazon Payments: johndoe.test.789@gmail.com/QWer7890
+ username/password for PayPal: johndoe.test.789@gmail.com/QWer7890

Third-party authentication — OpenID 2.0
* Video demo
* Click here to try or test it.
+ 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.
+ Any Microsoft Live account works. You can try johndoe.test.789@hotmail.com with password QWer7890.

Third-party authentication — Facebook OAuth
* Video demo
* Click here to try or test it.
+ Any Facebook account works. You can sign in Facebook as johndoe.test.789@gmail.com with password QWer7890.

A gambling system with four independent services
* Video demo
* Click here to try or test it.
+ username/password for Amazon Payments: johndoe.test.789@gmail.com/QWer7890

You can inspect the web traffic to better understand CST. A nice proxy to use is Fiddler2. (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
+ An approved purchase transaction using PayPal Standard on NopCommerce: the vProgram
+ An approved sign-on transaction using OpenID of DotNetOpenAuth: the vProgram
+ An approved sign-on transaction using Facebook’s OAuth: the vProgram
+ An approved gambling transaction: the vProgram

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

People