Enabling real-world online-service developers to verify their protocol implementations
Shuo Chen
Abstract:
Logic flaws exist in real-world services that use security protocols such as OpenID, OAuth, and PayPal. Since 2011, we have been publishing a series of papers showing the prevalence of these flaws [1][2][3][4], which have serious real-life consequences, e.g., an attacker can purchase without making payment, or sign into a victim’s account without password. It is a superficial remark that “developers simply need to understand the protocols better”, because it understates the challenges in the root problem: (i) protocol specs use English as the primary language, whereas developers use programming languages; (ii) protocol designers think at an abstraction level, whereas developers build concrete systems; (iii) protocol designers think with a “centralized” view, whereas the reality is fairly “distributed” – security relies on whether developers of different parties effectively understand each other. I will show real cases to support these arguments, and convince you that there is good research to be done here.
Earlier this year, we published a technology called Certified Symbolic Transaction (CST) [5], and have made significant improvement since then. CST is a super light-weight technology for REAL-WORLD developers to build formally verified implementations. It represents a unique combination of several techniques, such as static verification, reflection ability in OO programming, inheritance/polymorphism, and something similar to hash-chaining. The talk will explain how they are put together in CST. I hope this work provokes some deep thoughts about protocol vs. implementation, dynamic vs. symbolic execution, and safety properties of abstract vs. concrete classes.
References:
[1] Rui Wang, Shuo Chen, XiaoFeng Wang, and Shaz Qadeer, How to Shop for Free Online – Security Analysis of Cashier-as-a-Service Based Web Stores, in Proceedings of the IEEE Symposium on Security and Privacy, May 2011.
[2] Rui Wang, Shuo Chen, and XiaoFeng Wang, Signing Me onto Your Accounts through Facebook and Google: a Traffic-Guided Security Study of Commercially Deployed Single-Sign-On Web Services, in Proceedings of the IEEE Symposium on Security and Privacy, May 2012.
[3] Rui Wang, Yuchen Zhou, Shuo Chen, Shaz Qadeer, David Evans, and Yuri Gurevich, Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization, in Proceedings of the USENIX Security Symposium, August 2013.
[4] Eric Chen, Yutong Pei, Shuo Chen, Yuan Tian, Robert Kotcher, and Patrick Tague, OAuth Demystified for Mobile Application Developers, in Proceedings of the ACM Conference on Computer and Communications Security, November 2014.
[5] Eric Chen, Shuo Chen, Shaz Qadeer, and Rui Wang, Securing Multiparty Online Services via Certification of Symbolic Transactions, in Proceedings of the IEEE Symposium on Security and Privacy, May 2015.
Bio:
Shuo Chen is a senior researcher at Microsoft Research Redmond. His interest is on studying real-world operational systems to understand their security challenges and flaws. Specifically, he spends significant time studying problems about software-as-a-service, browser, web privacy/security and memory-based issues. He served on the program committees for IEEE S&P, USENIX Security, ACM CCS, WWW, etc. Shuo obtained his Ph.D. degree in computer science under the guidance of Prof. Ravi Iyer from University of Illinois at Urbana-Champaign. He obtained his master's and bachelor's degree from Tsinghua University and Peking University, both in computer science.