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 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 par ties 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), 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.
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.