Vetting Single Sign-On SDK Implementations via Symbolic Reasoning
summary
Builds an automated tester called S3KVetter that symbolically analyzes compiled SSO SDKs, simulates multi‑party flows by scheduling request orders and synthesizing IDP nonces, and checks concrete security clauses. Applied to ten popular SDKs it reports seven classes of logic flaws (four previously unknown), including access token injection and state misuse that enable account hijack or activity sniffing. Compared to baseline concolic runs it raises statement coverage ~17% and branch coverage ~19% and finds eight additional vulnerabilities.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:39Single SignOn
- 4:26SDKs
- 5:36Literature
- 6:52Research
- 8:09S3Kveta
- 8:43HighLevel Idea
- 9:14Technical Challenges
- 10:09Existing Approaches
- 11:13Design
- 11:59Scheduling
- 12:40Coordinate Multiple Parties
- 14:16Practical Tree
- 14:32Security Properties
- 17:19New Abilities
- 18:25Code Snippet
- 20:08Conclusion
related talks
57mSelf-Verifying Authentication – A Framework For Safer Integrations of Single-Sign-On Services
16mIs your SSO on point, or is it more like Single Sign-Oh-no?
46mSecure SSO Authentication: Strategies to Eliminate Vulnerabilities
42mConfirming Safety of IAM Specifications and their OSS Implementations: Keycloak as a Case Study
41mOSBT: OpenID Connect Scenario-Based Tester
31mIdentity Theft: Attacks on SSO Systems
37mThe Seven Deadly Sins of Web Apps, or a Bit About SSO Bugs
40mModern Single Sign-On: On the Security of Single Sign-On ...