2014/05/27 by Asiri Rathnayake, Rathnayake, Asiri, Hayo Thielecke +1 · 1 citation
Computer Science · #Advanced Malware Detection Techniques #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1405.7058
openalex publication_date 2014/05/27 · openalex created_date 2022/08/29 · openalex updated_date 2026/07/28
Regular expression matching using backtracking can have exponential runtime, leading to an algorithmic complexity attack known as REDoS in the systems security literature. In this paper, we build on a recently published static analysis that detects whether a given regular expression can have exponential runtime for some inputs. We systematically construct a more accurate analysis by forming powers and products of transition relations and thereby reducing the REDoS problem to reachability. The correctness of the analysis is proved using a substructural calculus of search trees, where the branching of the tree causing exponential blowup is characterized as a form of non-linearity.