{"id":171460,"date":"2015-05-06T15:39:12","date_gmt":"2015-05-06T15:39:12","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/certification-of-symbolic-transaction\/"},"modified":"2019-08-19T10:32:13","modified_gmt":"2019-08-19T17:32:13","slug":"certification-of-symbolic-transaction","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/certification-of-symbolic-transaction\/","title":{"rendered":"Certification of Symbolic Transaction"},"content":{"rendered":"
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\u2019s 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.<\/div>\n

<\/p>\n

\n

Online services enhanced by CST<\/h1>\n

(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)<\/span><\/a> Disabling it forces the system to go through the entire verification procedure for every transaction.)<\/p>\n

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

Online shopping — Amazon Simple Pay and PayPal Standard<\/b>
\n* Video demo 1 (using PayPal) (opens in new tab)<\/span><\/a>\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0\u00a0 Video demo 2 (using Amazon) (opens in new tab)<\/span><\/a>
\n* Click here to try or test it (opens in new tab)<\/span><\/a>. If you don’t want to create your own accounts, we have existing ones.
\n+ username\/password for the shopping site: johndoe.test.789@gmail.com\/QWer7890
\n+ username\/password for Amazon Payments: johndoe.test.789@gmail.com\/QWer7890
\n+ username\/password for PayPal: johndoe.test.789@gmail.com\/QWer7890<\/p>\n

Third-party authentication — <\/b>OpenID 2.0<\/b>
\n* Video demo
\n (opens in new tab)<\/span><\/a>* Click here to try or test it (opens in new tab)<\/span><\/a>.
\n+ 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.)
\n+ If you haven’t logged into the OpenID Provider, you will be asked for username and password. Try username “bob” and password “test”.<\/p>\n

Live Connect SDK for authentication
\n<\/b>* Click here to try or test it (opens in new tab)<\/span><\/a>.
\n+ Any Microsoft Live account works. You can try johndoe.test.789@hotmail.com with password QWer7890.<\/p>\n

Third-party authentication — <\/b>Facebook OAuth<\/b>
\n* Video demo (opens in new tab)<\/span><\/a>
\n* Click here to try or test it (opens in new tab)<\/span><\/a>.
\n+ Any Facebook account works.\u00a0You can\u00a0sign in Facebook as johndoe.test.789@gmail.com with password QWer7890.<\/p>\n

A gambling system with four independent services
\n<\/b>* Video demo (opens in new tab)<\/span><\/a>
\n* Click here to try or test it (opens in new tab)<\/span><\/a>.
\n+ username\/password for Amazon Payments: johndoe.test.789@gmail.com\/QWer7890<\/p>\n

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

\n

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

(Note that CST was previously named DSV. Some projects still use the term DSV.)
\n+ Source code of all projects (opens in new tab)<\/span><\/a>
\n+ Source code of LiveID OAuth Sign-on SDK (opens in new tab)<\/span><\/a><\/p>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

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\u2019s 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 […]<\/p>\n","protected":false},"featured_media":0,"template":"","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"footnotes":""},"research-area":[13560,13558],"msr-locale":[268875],"msr-impact-theme":[],"msr-pillar":[],"class_list":["post-171460","msr-project","type-msr-project","status-publish","hentry","msr-research-area-programming-languages-software-engineering","msr-research-area-security-privacy-cryptography","msr-locale-en_us","msr-archive-status-active"],"msr_project_start":"5\/6\/2015","related-publications":[168033],"related-downloads":[],"related-videos":[],"related-groups":[],"related-events":[],"related-opportunities":[],"related-posts":[],"related-articles":[],"tab-content":[],"slides":[],"related-researchers":[{"type":"user_nicename","display_name":"Shuo Chen","user_id":33637,"people_section":"Group 1","alias":"shuochen"}],"msr_research_lab":[],"msr_impact_theme":[],"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171460"}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/msr-project"}],"version-history":[{"count":1,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171460\/revisions"}],"predecessor-version":[{"id":604230,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-project\/171460\/revisions\/604230"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=171460"}],"wp:term":[{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=171460"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=171460"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=171460"},{"taxonomy":"msr-pillar","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-pillar?post=171460"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}