Explicating SDKs: Uncovering Assumptions Underlying Secure Authentication and Authorization
Rui Wang1*, Yuchen Zhou2*,
Shuo Chen1, Shaz Qadeer1, David Evans2 and Yuri Gurevich1
(*Co-first authors)
1Microsoft Research and 2University of Virginia
Last updated: Aug 10th, 2013
General approach to study system behavior to uncover implicit assumptions.
• Introduction
Security vulnerabilities often emerges because some implicit assumptions are missed by the application developers. The main goal of this project is to secure web/mobile applications integrating third-party services, in particular, Single-Sign On(SSO) services by uncovering implicit security-critical assumptions required by the service provider.
The idea is to use symbolic execution engine as a verifier to assist researchers study system behavior and gain insights. As the above flowgraph describes, we approach this problem using an iterative approach - starting with an initial model of the system with an initial set of assumptions and assertions, the verifier tries to reason about the model and outputs counterexamples for the assertions. We manually inspect the counterexamples and try to find real-world vulnerabilities which map to them.
Two lead authors spent a total of 6 months to explicate three SDKs and uncovered dozens of implicit assumptions. We reported our findings to related parties and got acknowledgements and bug bounties from them. We also checked popular applications against these vulnerabilities and found that the majority of the applications missed at least one of the assumptions.
The idea is to use symbolic execution engine as a verifier to assist researchers study system behavior and gain insights. As the above flowgraph describes, we approach this problem using an iterative approach - starting with an initial model of the system with an initial set of assumptions and assertions, the verifier tries to reason about the model and outputs counterexamples for the assertions. We manually inspect the counterexamples and try to find real-world vulnerabilities which map to them.
Two lead authors spent a total of 6 months to explicate three SDKs and uncovered dozens of implicit assumptions. We reported our findings to related parties and got acknowledgements and bug bounties from them. We also checked popular applications against these vulnerabilities and found that the majority of the applications missed at least one of the assumptions.
Single-Sign On system architecture and threat model.
• Publication
Our USENIX Sec 13' paper can be found at here.
• Real-World Impact
Facebook awarded us with three bug bounties, each of which ($1500) is three times the basic bounty amount ($500). We donated all money to charity, and Facebook matched our donations 1-to-1, making the total donation amount $9000.
Microsoft Live Connect team also updated their developer's guide to reflect our findings. OAuth working group added a paragraph in the security consideration sections according to our suggestion.
Various application developers thanked us for informing them of their application's vulnerabilities.
Microsoft Live Connect team also updated their developer's guide to reflect our findings. OAuth working group added a paragraph in the security consideration sections according to our suggestion.
Various application developers thanked us for informing them of their application's vulnerabilities.
• Model
The models of explicated SDKs can be found at our Github repository. You can find instructions on how to run the model inside the repository README.
• Questions?
Email me: yuchen at virginia dot edu. Feel free to ask any questions you may have.
• People
- - Yuchen Zhou, Fourth-Fifth year PhD student in computer science/engineering at University of Virginia.
- - David Evans, associate professor in computer science department at Univeristy of Virginia.