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.
Email me: yuchen at virginia dot edu. Feel free to ask any questions you may have.