Repairing DoS Vulnerability of Real-World Regexes

TL;DR

This paper introduces a novel program synthesis-based method to repair real-world regexes, ensuring they are invulnerable to ReDoS attacks by handling complex features like lookarounds and backreferences.

Contribution

It provides the first formal semantics and complexity analysis for real-world regexes, and develops a repair algorithm guaranteeing invulnerability based on a new unambiguity condition.

Findings

The method guarantees generation of invulnerable regexes.

It handles complex regex features like lookarounds and backreferences.

The approach extends previous PBE methods to real-world regexes.

Abstract

There has been much work on synthesizing and repairing regular expressions (regexes for short) from examples. These programming-by-example (PBE) methods help the users write regexes by letting them reflect their intention by examples. However, the existing methods may generate regexes whose matching may take super-linear time and are vulnerable to regex denial of service (ReDoS) attacks. This paper presents the first PBE repair method that is guaranteed to generate only invulnerable regexes. Importantly, our method can handle real-world regexes containing lookarounds and backreferences. Due to the extensions, the existing formal definitions of ReDoS vulnerabilities that only consider pure regexes are insufficient. Therefore, we first give a novel formal semantics and complexity of backtracking matching algorithms for real-world regexes, and with them, give the first formal definition of ReDoS vulnerability for real-world regexes. Next, we present a novel condition called real-world strong 1-unambiguity that is sufficient for guaranteeing the invulnerability of real-world regexes, and formalize the corresponding PBE repair problem. Finally, we present an algorithm that solves the repair problem. The algorithm builds on and extends the previous PBE methods to handle the real-world extensions and with constraints to enforce the real-world strong 1-unambiguity condition.