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 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.
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.