Automated Repair of OpenID Connect Programs (Extended Version)

TL;DR

This work tackles the problem of repairing OpenID Connect implementations, where protocol complexity and strict specification adherence make automatic fixes challenging. The authors introduce AuthFix, a counterexample-guided repair engine that combines LLM-assisted fault localization and patch synthesis with a Petri-net–based verifier that enforces specification conformance. The approach demonstrates substantial practical impact, repairing 17 of 23 real-world OpenID bugs (74%) and achieving semantic equivalence to human patches in a large portion of cases. By integrating formal verification into the repair loop and leveraging domain-specific DSLs and schemas, AuthFix advances robust, specification-driven automated repair for security-critical protocol software.

Abstract

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.

Figures (9)

• Figure 1: Interactions between the Relying Party (RP) and OpenID Provider (OP) during the authentication process of Authorization Code Flow in OIDC.
• Figure 2: Workflow of AuthFix on a concrete example. Here, AuthFix first takes a buggy OpenID program and its corresponding English specification as inputs and then generates repair sketches based on the fault localization by an LLM agent. The tool then performs patch enumeration while transforming the repair candidates into their corresponding Petri-net models, which are verified against the Petri-net specification constructed (manually) from the English specification.
• Figure 3: An overview of AuthFix.
• Figure 4: An example of an LLM query for fault localization in a partial OpenID Connect program. This query has four text components Q = [$q_1$, $q_2$, $q_3$, $q_4$], where $q1$ and $q_4$ are static components that provide instructions to the LLM agent and $q_2$ and $q_3$ are dynamic components that provide the specification and buggy program, respectively.
• Figure 5: An LLM response for the query described in \ref{['fig:llm-query']}.

Theorems & Definitions (2)

• Example 1
• Example 2