OpenID Connect has revolutionized online authentication based on single sign-on (SSO) by providing a secure and convenient method for accessing multiple services with a single set of credentials. Despite its widespread adoption, critical security bugs in OpenID Connect have resulted in significant financial losses and security breaches, highlighting the need for robust mitigation strategies. Automated program repair presents a promising solution for generating candidate patches for OpenID implementations. However, challenges such as domain-specific complexities and the necessity for precise fault localization and patch verification must be addressed. We propose AuthFix, a counterexample-guided repair engine leveraging LLMs for automated OpenID bug fixing. AuthFix integrates three key components: fault localization, patch synthesis, and patch verification. By employing a novel Petri-net-based model checker, AuthFix ensures the correctness of patches by effectively modeling interactions. Our evaluation on a dataset of OpenID bugs demonstrates that AuthFix successfully generated correct patches for 17 out of 23 bugs (74%), with a high proportion of patches semantically equivalent to developer-written fixes.

Single Sign-On (SSO)-based authentication protocols, like OpenID Connect (OIDC), play a crucial role in enhancing security and privacy in today's interconnected digital world, gaining widespread adoption among the majority of prominent authentication service providers. These protocols establish a structured framework for verifying and authenticating the identities of individuals, organizations, and devices, while avoiding the necessity of sharing sensitive credentials (e.g., passwords) with external entities. However, the security guarantees of these protocols rely on their proper implementation, and real-world implementations can, and indeed often do, contain logical programming errors leading to severe attacks, including authentication bypass and user account takeover. In response to this challenge, we present AuthSaber, an automated verifier designed to assess the real-world OIDC protocol implementations against their standard safety specifications in a scalable manner. AuthSaber addresses the challenges of expressiveness for OIDC properties, modeling multi-party interactions, and automation by first designing a novel specification language based on linear temporal logic, leveraging an automaton-based approach to constrain the space of possible interactions between OIDC entities, and incorporating several domain-specific transformations to obtain programs and properties that can be directly reasoned about by software model checkers. We evaluate AuthSaber on the 15 most popular and widely used OIDC libraries and discover 16 previously unknown vulnerabilities, all of which are responsively disclosed to the developers. Five categories of these vulnerabilities also led to new CVEs.

OAuth protocols have been widely adopted to simplify user authentication and service authorization for third-party applications. However, little effort has been devoted to automatically checking the security of the libraries that service providers widely use. In this paper, we formalize the OAuth specifications and security best practices, and design Cerberus, an automated static analyzer, to find logical flaws and identify vulnerabilities in the implementation of OAuth service provider libraries. To efficiently detect security violations in a large codebase of service provider implementation, Cerberus employs a query-driven algorithm for answering queries about OAuth specifications. We demonstrate the effectiveness of Cerberus by evaluating it on datasets of popular OAuth libraries with millions of downloads. Among these high-profile libraries, Cerberus has identified 47 vulnerabilities from ten classes of logical flaws, 24 of which were previously unknown. We got acknowledged by the developers of eight libraries and had three accepted CVEs.

Mobile developers use OAuth APIs to implement Single-Sign-On services. However, the OAuth protocol was originally designed for the authorization for third-party websites not to authenticate users in third-party mobile apps. As a result, it is challenging for developers to correctly implement mobile OAuth securely. These vulnerabilities due to the misunderstanding of OAuth and inexperience of developers could lead to data leakage and account breach. In this paper, we perform an empirical study on the usage of OAuth APIs in Android applications and their security implications. In particular, we develop OAUTHLINT, that incorporates a query-driven static analysis to automatically check programs on the Google Play marketplace. OAUTHLINT takes as input an anti-protocol that encodes a vulnerable pattern extracted from the OAuth specifications and a program P. Our tool then generates a counter-example if the anti-protocol can match a trace of Ps possible executions. To evaluate the effectiveness of our approach, we perform a systematic study on 600+ popular apps which have more than 10 millions of downloads. The evaluation shows that 101 (32%) out of 316 applications that use OAuth APIs make at least one security mistake.