pith. sign in

arxiv: 2606.19654 · v1 · pith:WWXTH3YQnew · submitted 2026-06-17 · 💻 cs.CR · cs.SE

PUFFERDOS: Efficient and Effective Attack String Generation for Regular Expression Denial of Service Vulnerabilities

Pith reviewed 2026-06-26 20:04 UTC · model grok-4.3

classification 💻 cs.CR cs.SE
keywords ReDoSregular expressionattack string generationdenial of servicevulnerability detectionconcolic executionprogram analysissecurity testing
0
0 comments X

The pith

PUFFERDOS generates attack strings for regex denial-of-service that stay short enough and work when run on real programs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to show that prior methods for finding ReDoS problems produce strings that are either too long to be realistic or fail to trigger the vulnerability once placed inside an actual program. It does this by first identifying three specific vulnerable patterns through observation and formal checks. From those patterns the method builds candidate strings, then uses a targeted form of compositional concolic execution to shorten and test them directly against the program. The result is a set of strings that fit normal input-size limits yet still force the regex engine into its worst-case behavior. A sympathetic reader would care because such strings let developers locate and remove these availability threats during ordinary testing rather than after an attack succeeds.

Core claim

PUFFERDOS first defines three vulnerable patterns based on observation and formal verification. According to the patterns it conducts a synthesis technique to generate attack strings, then refines and validates the strings with ReDoS-specific compositional concolic execution to guarantee real-world exploitability within realistic length budgets.

What carries the argument

Three vulnerable patterns plus synthesis followed by ReDoS-specific compositional concolic execution for refinement and program-level validation.

If this is right

  • Attack strings become short enough to be sent over normal network channels yet still trigger the vulnerability.
  • Strings that previously failed to exploit real programs are replaced by ones that have been validated at the program level.
  • Detection can occur earlier in development because the strings are both feasible and effective.
  • Remediation effort focuses on regexes that actually produce measurable resource exhaustion when attacked.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same pattern-plus-validation approach could be tried on other resource-exhaustion problems that depend on input structure.
  • If the three patterns turn out to miss some real-world cases, adding a fourth pattern would be the direct next step.
  • The validation step could be run automatically on any regex found inside application source during routine builds.

Load-bearing premise

The three vulnerable patterns identified from observation and formal verification cover the ReDoS cases that matter in practice.

What would settle it

Run the generated strings on programs that contain the three patterns and measure whether CPU time or execution steps rise sharply within short input lengths while the same strings produce no such rise on equivalent non-vulnerable regexes.

Figures

Figures reproduced from arXiv: 2606.19654 by Benjamin Turnbull, Nan Sun, Shangzhi Xu, Shuangxiang Kan, Siqi Ma, Xiao Cheng, Yuekang Li, Ziqi Ding.

Figure 1
Figure 1. Figure 1: A motivating example [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Illustrative example of attack string generation. [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: PUFFERDOS workflow. For each extracted regex, PUFFERDOS applies ReDoS detectors to identify vulnerable cases and retains only those confirmed as vulnerable for subsequent analysis. 4.2. Structure-Driven Attack String Generation Given the vulnerable regexes identified in Section 4.1, this section describes how PUFFERDOS generates a high￾cost attack string for each regex. To systematically approach attack ge… view at source ↗
Figure 4
Figure 4. Figure 4: An illustrative example of rAST and rPath. [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Distribution of R¯ T on baseline. The extreme values reach 105 , 106 , and 107 at T = 0.1, 1, and 10, respectively. complex user interactions and the construction of highly specific input structures. As the concolic executor does not fully model these interactions, the exploitation failed. Among the six cases where RENGAR failed but PUFFER￾DOS succeeded, four were caused by complex path condi￾tions involvi… view at source ↗
read the original abstract

ReDoS attacks constitute a critical class of resource-exhaustion vulnerabilities. In such attacks, adversaries exploit the pathological worst-case execution behavior of regular expression (regex) engines to induce highly asymmetric computational workloads, ultimately exhausting system resources and degrading service availability. To protect systems against ReDoS attacks, numerous detection techniques have been proposed that simulate the attack process by generating attack strings to proactively exploit ReDoS vulnerabilities at the early development stage and facilitate remediation. Existing techniques broadly fall into two classes: static analyses that search for pathological regex structures, and dynamic exploration methods that synthesize candidate attack strings. However, the generated attack strings are often impractical for real-world exploitation because they usually assume unrealistic input-length budgets and do not validate the effectiveness and efficiency of the attack at the program level. Therefore, many generated strings fail to trigger vulnerable regexes when applied to real-world programs, further limiting the practical utility. To address these shortcomings, we introduce an effective and efficient attack string generator, PUFFERDOS, designed to synthesize attack inputs that are both feasible within realistic length budgets and validated at the program level, enabling effective exploitation of ReDoS vulnerabilities in real-world programs. Specifically, we first define three vulnerable patterns based on our observation and formal verification. According to the patterns, PUFFERDOS conducts a synthesis technique to generate attack strings, and then refines and validates the strings with ReDoS-specific compositional concolic execution to guarantee real-world exploitability.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper introduces PUFFERDOS, an attack string generator for ReDoS vulnerabilities. It defines three vulnerable patterns based on observation and formal verification, synthesizes attack strings according to these patterns, and refines/validates them via ReDoS-specific compositional concolic execution to produce strings that are feasible within realistic length budgets and exploitable in real-world programs.

Significance. If the central claims hold with supporting evidence, the work would address a practical gap in ReDoS detection by producing attack strings that existing static and dynamic methods often fail to make usable in real programs, potentially improving early-stage vulnerability remediation.

major comments (2)
  1. [Abstract] Abstract: the manuscript asserts that the generated strings are 'validated at the program level' and 'guarantee real-world exploitability' via compositional concolic execution, yet the abstract (and the provided text) contains no evaluation data, success rates, comparison baselines, or quantitative results on how many strings were validated or their performance on real programs, leaving the headline claim unsupported.
  2. [Abstract] Abstract (paragraph describing the synthesis technique): the approach is defined exclusively over the three vulnerable patterns identified from observation and formal verification. No evidence is supplied that these patterns were tested for exhaustiveness against a corpus of known ReDoS-vulnerable regexes or that they capture the structures producing exploitable worst-case behavior under realistic length budgets, which is required for the claim that the method enables effective exploitation in practice.
minor comments (1)
  1. The three patterns would benefit from explicit formal definitions, examples, and a dedicated section or figure rather than being described only at high level in the abstract.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on the abstract. We will revise the manuscript to better support the central claims with quantitative evidence and additional discussion on the patterns. Below we respond point by point.

read point-by-point responses
  1. Referee: [Abstract] Abstract: the manuscript asserts that the generated strings are 'validated at the program level' and 'guarantee real-world exploitability' via compositional concolic execution, yet the abstract (and the provided text) contains no evaluation data, success rates, comparison baselines, or quantitative results on how many strings were validated or their performance on real programs, leaving the headline claim unsupported.

    Authors: We agree that the abstract, as a concise summary, does not present specific quantitative results. The full manuscript includes a dedicated evaluation section reporting success rates for program-level validation, comparisons against baselines, and performance on real-world programs. To address the concern, we will revise the abstract to incorporate key quantitative highlights from the evaluation (e.g., validation success rate and exploitability metrics under realistic length budgets). revision: yes

  2. Referee: [Abstract] Abstract (paragraph describing the synthesis technique): the approach is defined exclusively over the three vulnerable patterns identified from observation and formal verification. No evidence is supplied that these patterns were tested for exhaustiveness against a corpus of known ReDoS-vulnerable regexes or that they capture the structures producing exploitable worst-case behavior under realistic length budgets, which is required for the claim that the method enables effective exploitation in practice.

    Authors: The three patterns were derived from systematic observation of ReDoS vulnerabilities reported in the literature and were formally verified to produce the pathological worst-case behavior. The formal verification establishes that they capture the relevant structures for exploitable behavior under realistic budgets. The current manuscript does not include an exhaustive corpus study; we will add a clarifying discussion of the observation-plus-verification methodology and, space permitting, results from applying the patterns to a corpus of known vulnerable regexes. revision: partial

Circularity Check

0 steps flagged

No circularity; derivation is self-contained

full rationale

The abstract describes defining three vulnerable patterns from observation and formal verification, then synthesizing strings according to those patterns and refining them via compositional concolic execution. No equations, fitted parameters, or self-referential reductions appear. The synthesis technique and validation step are presented as independent contributions rather than quantities forced by prior definitions or self-citations within the paper. The workflow does not equate any claimed result to its inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on the domain assumption that three observed patterns suffice and that concolic execution can reliably confirm exploitability; no free parameters or invented entities are mentioned.

axioms (1)
  • domain assumption Three vulnerable patterns identified by observation and formal verification cover the relevant ReDoS cases
    Stated in the abstract as the basis for synthesis

pith-pipeline@v0.9.1-grok · 5815 in / 1137 out tokens · 24121 ms · 2026-06-26T20:04:18.575241+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

88 extracted references · 2 linked inside Pith

  1. [1]

    Rengar: Regular expression denial-of-service analyzer,

    “Rengar: Regular expression denial-of-service analyzer,” https://sites. google.com/view/rengar/resources?authuser=0

  2. [2]

    PUFFERDOS: Anonymous artifact repository,

    “PUFFERDOS: Anonymous artifact repository,” https://anonymous. 4open.science/r/PufferDoS-7E0D/

  3. [3]

    CVE-2017-16098: Apache Charset Regular Expression Denial of Service (ReDoS),

    “CVE-2017-16098: Apache Charset Regular Expression Denial of Service (ReDoS),” https://cvefeed.io/vuln/detail/CVE-2017-16098, 2017, affected package:charset¡= 1.0.0. Regular expression DoS via crafted input. CWE-400: Uncontrolled Resource Consumption. CVSS v3.0 Score: 7.5 (High). Published: 2018-06-07, Last Modified: 2024-11-21

  4. [4]

    CVE-2017-16137: Regular Expression Denial of Service in debug module ( ¨o¨formatter),

    “CVE-2017-16137: Regular Expression Denial of Service in debug module ( ¨o¨formatter),” https://nvd.nist.gov/vuln/detail/ CVE-2017-16137, 2017, affected product:debug(Node.js). Vulnerable versions: ¿=2.0.0 ¡2.6.9; ¿=3.0.0 ¡3.1.0; ¿=3.2.0 ¡3.2.7; ¿=4.0.0 ¡4.3.1. ReDoS issue via untrusted input intooformatter. Requires 50k characters to block for about 2 se...

  5. [5]

    CVE-2023-39663: MathJax Regular Expression Denial of Ser- vice (ReDoS),

    “CVE-2023-39663: MathJax Regular Expression Denial of Ser- vice (ReDoS),” https://www.suse.com/security/cve/CVE-2023-39663. html, 2023, affects MathJax up to v2.7.9: two ReDoS vulner- abilities viapatternandmarkdownPattern. SUSE states “Does not affect SUSE products.” CVSS v3.1 Base Score: 7.5 (A V:N/AC:L/PR:N/UI:N/S:U/C:N/I:N/A:H). Overall severity: Impo...

  6. [6]

    Hifrog: Smt-based function summarization for software verification,

    L. Alt, S. Asadi, H. Chockler, K. Even Mendoza, G. Fedyukovich, A. E. Hyv ¨arinen, and N. Sharygina, “Hifrog: Smt-based function summarization for software verification,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2017, pp. 207–213

  7. [7]

    Demand-driven composi- tional symbolic execution,

    S. Anand, P. Godefroid, and N. Tillmann, “Demand-driven composi- tional symbolic execution,” inInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2008, pp. 367–381

  8. [8]

    Counterexample- guided abstraction refinement for linear programs with arrays,

    A. Armando, M. Benerecetti, and J. Mantovani, “Counterexample- guided abstraction refinement for linear programs with arrays,”Au- tomated Software Engineering, vol. 21, no. 2, pp. 225–285, 2014

  9. [9]

    cvc5: A versatile and industrial-strength smt solver,

    H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. N ¨otzliet al., “cvc5: A versatile and industrial-strength smt solver,” inInternational Confer- ence on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2022, pp. 415–442

  10. [10]

    Exploiting input sanitization for regex denial of service,

    E. Barlas, X. Du, and J. C. Davis, “Exploiting input sanitization for regex denial of service,” inProceedings of the 44th International Conference on Software Engineering, 2022, pp. 883–895

  11. [11]

    Inference of regular expressions for text extraction from examples,

    A. Bartoli, A. De Lorenzo, E. Medvet, and F. Tarlao, “Inference of regular expressions for text extraction from examples,”IEEE Transactions on Knowledge and Data Engineering, vol. 28, no. 5, pp. 1217–1230, 2016

  12. [12]

    Sok: A literature and engineering review of regular expression denial of service (redos),

    M. H. M. Bhuiyan, B. C ¸ akar, E. H. Burmane, J. C. Davis, and C.-A. Staicu, “Sok: A literature and engineering review of regular expression denial of service (redos),” inProceedings of the 20th ACM Asia Conference on Computer and Communications Security, 2025, pp. 1659–1675

  13. [13]

    An additional non-backtracking regexp engine · v8,

    M. Bidlingmaier, “An additional non-backtracking regexp engine · v8,” https://v8.dev/blog/non-backtracking-regexp, 2021

  14. [14]

    Klee: unassisted and automatic generation of high-coverage tests for complex systems programs

    C. Cadar, D. Dunbar, D. R. Engleret al., “Klee: unassisted and automatic generation of high-coverage tests for complex systems programs.” inOSDI, vol. 8, 2008, pp. 209–224. 14

  15. [15]

    regexploit: Find regu- lar expressions which are vulnerable to redos,

    B. Caller, L. Carettoni, and Doyensec, “regexploit: Find regu- lar expressions which are vulnerable to redos,” https://github.com/ doyensec/regexploit, 2021, release v1.0.0 (Mar 11, 2021). License: Apache-2.0

  16. [16]

    Exploring regular expression usage and context in python,

    C. Chapman and K. T. Stolee, “Exploring regular expression usage and context in python,” inProceedings of the 25th International Symposium on Software Testing and Analysis, 2016, pp. 282–293

  17. [17]

    Rethinking regex engines to address redos,

    J. C. Davis, “Rethinking regex engines to address redos,” inPro- ceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Soft- ware Engineering, 2019, pp. 1256–1258

  18. [18]

    The impact of regular expression denial of service (redos) in practice: an empirical study at the ecosystem scale,

    J. C. Davis, C. A. Coghlan, F. Servant, and D. Lee, “The impact of regular expression denial of service (redos) in practice: an empirical study at the ecosystem scale,” inProceedings of the 2018 26th ACM joint meeting on european software engineering conference and symposium on the foundations of software engineering, 2018, pp. 246–256

  19. [19]

    Z3: an efficient smt solver,

    L. De Moura and N. Bjørner, “Z3: an efficient smt solver,” in Proceedings of the Theory and Practice of Software, 14th Interna- tional Conference on Tools and Algorithms for the Construction and Analysis of Systems, ser. TACAS’08/ETAPS’08. Berlin, Heidelberg: Springer-Verlag, 2008, p. 337–340

  20. [20]

    Detecting asymmetric application-layer{Denial-of- Service}attacks{In-Flight}with{FineLame},

    H. M. Demoulin, I. Pedisich, N. Vasilakis, V . Liu, B. T. Loo, and L. T. X. Phan, “Detecting asymmetric application-layer{Denial-of- Service}attacks{In-Flight}with{FineLame},” in2019 USENIX Annual Technical Conference (USENIX ATC 19), 2019, pp. 693–708

  21. [21]

    regexploit: Regular expression security tooling,

    doyensec, “regexploit: Regular expression security tooling,” https:// github.com/doyensec/regexploit, 2025, gitHub repository

  22. [22]

    Friedl,Mastering regular expressions

    J. Friedl,Mastering regular expressions. ” O’Reilly Media, Inc.”, 2006

  23. [23]

    Compositional dynamic test generation,

    P. Godefroid, “Compositional dynamic test generation,” inProceed- ings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2007, pp. 47–54

  24. [24]

    Dart: directed automated random testing,

    P. Godefroid, N. Klarlund, and K. Sen, “Dart: directed automated random testing,” inProceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, ser. PLDI ’05. New York, NY , USA: Association for Computing Machinery, 2005, p. 213–223. [Online]. Available: https://doi.org/10. 1145/1065010.1065036

  25. [25]

    pytype: A static type analyzer for python,

    Google, “pytype: A static type analyzer for python,” https://github. com/google/pytype, 2025

  26. [26]

    RE2: Linear-time regular expression engine,

    Google, “RE2: Linear-time regular expression engine,” https://github. com/google/re2, 2025

  27. [27]

    Details of the cloudflare out- age on july 2, 2019,

    J. Graham-Cumming, “Details of the cloudflare out- age on july 2, 2019,” https://blog.cloudflare.com/ details-of-the-cloudflare-outage-on-july-2-2019/

  28. [28]

    Model context protocol (mcp) at first glance: Studying the security and maintainability of mcp servers,

    M. M. Hasan, H. Li, E. Fallahzadeh, G. K. Rajbahadur, B. Adams, and A. E. Hassan, “Model context protocol (mcp) at first glance: Studying the security and maintainability of mcp servers,”arXiv preprint arXiv:2506.13538, 2025

  29. [29]

    Introduction to automata theory, languages, and computation,

    J. E. Hopcroft, R. Motwani, and J. D. Ullman, “Introduction to automata theory, languages, and computation,” Boston, MA, 2006, iSBN 978-0321455369

  30. [30]

    Towards automatic detection and exploitation of java web application vulnerabilities via concolic execution guided by cross- thread object manipulation,

    X. Huang, L. Zhang, Y . Liu, P. Deng, Y . Cao, Y . Zhang, and M. Yang, “Towards automatic detection and exploitation of java web application vulnerabilities via concolic execution guided by cross- thread object manipulation,” in34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 8367–8384

  31. [31]

    Outage postmortem — july 20, 2016,

    S. E. Inc., “Outage postmortem — july 20, 2016,” https://stackstatus. tumblr.com/post/147710624694/outage-postmortem-july-20-2016

  32. [32]

    Model checking embedded control software using os-in-the-loop cegar,

    D. Kim and Y . Choi, “Model checking embedded control software using os-in-the-loop cegar,” in2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2019, pp. 565–576

  33. [33]

    Pbe-based selective abstraction and refinement for efficient property falsification of embedded software,

    Y . Kim and Y . Choi, “Pbe-based selective abstraction and refinement for efficient property falsification of embedded software,”Proceedings of the ACM on Software Engineering, vol. 1, no. FSE, pp. 293–315, 2024

  34. [34]

    Target-driven compositional concolic testing with function summary refinement for effective bug detection,

    Y . Kim, S. Hong, and M. Kim, “Target-driven compositional concolic testing with function summary refinement for effective bug detection,” inProceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019, pp. 16–26

  35. [35]

    Static analysis for reg- ular expression denial-of-service attacks,

    J. Kirrage, A. Rathnayake, and H. Thielecke, “Static analysis for reg- ular expression denial-of-service attacks,” inInternational conference on network and system security. Springer, 2013, pp. 135–148

  36. [36]

    Oniguruma: Regular expression library,

    kkos, “Oniguruma: Regular expression library,” https://github.com/ kkos/oniguruma, 2025, gitHub repository

  37. [37]

    S. C. Kleene,Representation of events in nerve nets and finite automata. Princeton University Press Princeton, 1956, vol. 34

  38. [38]

    {ReDoSHunter}: A combined static and dynamic approach for regular expression{DoS}detection,

    Y . Li, Z. Chen, J. Cao, Z. Xu, Q. Peng, H. Chen, L. Chen, and S.-C. Cheung, “{ReDoSHunter}: A combined static and dynamic approach for regular expression{DoS}detection,” in30th USENIX Security Symposium (USENIX Security 21), 2021, pp. 3847–3864

  39. [39]

    {RegexScalpel}: Regular expression denial of service ({{{{{ReDoS}}}}}) defense by{Localize-and-Fix},

    Y . Li, Y . Sun, Z. Xu, J. Cao, Y . Li, R. Li, H. Chen, S.-C. Cheung, Y . Liu, and Y . Xiao, “{RegexScalpel}: Regular expression denial of service ({{{{{ReDoS}}}}}) defense by{Localize-and-Fix},” in 31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 4183–4200

  40. [40]

    {CO3}: Concolic co-execution for firmware,

    C. Liu, A. Mera, E. Kirda, M. Xu, and L. Lu, “{CO3}: Concolic co-execution for firmware,” in33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 5591–5608

  41. [41]

    A unified framework for compressed and encrypted text direct processing,

    Y . Liu, F. Zhang, Y . Zhang, S. Ma, E. Bertino, and X. Du, “A unified framework for compressed and encrypted text direct processing,” in ICDE, 2026

  42. [42]

    Revealer: Detecting and exploiting regular expression denial-of-service vulnerabilities,

    Y . Liu, M. Zhang, and W. Meng, “Revealer: Detecting and exploiting regular expression denial-of-service vulnerabilities,” in2021 IEEE Symposium on Security and Privacy (SP). IEEE, 2021, pp. 1468– 1484

  43. [43]

    Goshawk: Hunting memory corruptions via structure- aware and object-centric memory operation synopsis,

    Y . Lyu, Y . Fang, Y . Zhang, Q. Sun, S. Ma, E. Bertino, K. Lu, and J. Li, “Goshawk: Hunting memory corruptions via structure- aware and object-centric memory operation synopsis,” in2022 IEEE Symposium on Security and Privacy (SP). IEEE, 2022, pp. 2096– 2113

  44. [44]

    Pythonregexmodule on pypi,

    Matthew Barnett, “Pythonregexmodule on pypi,” https://pypi.org/ project/regex/

  45. [45]

    Redos vulnerability reports: Relevant or noisy nuisance,

    D. McInerney, W. Woodruff, and A. Nygate, “Redos vulnerability reports: Relevant or noisy nuisance,” https://mlsecops.com/podcast/ redos-vulnerability-reports-security-relevance-vs.-noisy-nuisance? utm source=chatgpt.com

  46. [46]

    Regulator: Dynamic analysis to detect{ReDoS},

    R. McLaughlin, F. Pagani, N. Spahn, C. Kruegel, and G. Vigna, “Regulator: Dynamic analysis to detect{ReDoS},” in31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 4219–4235

  47. [47]

    Common vulnerabilities and exposures (cve),

    MITRE, “Common vulnerabilities and exposures (cve),” https://www. cve.org/, 2025

  48. [48]

    Nielsen,Usability Engineering

    J. Nielsen,Usability Engineering. San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 1994

  49. [49]

    Node.js official website,

    Node.js Foundation, “Node.js official website,” https://nodejs.org/en/ about

  50. [50]

    Badger: complexity analysis with fuzzing and symbolic execution,

    Y . Noller, R. Kersten, and C. S. P ˘as˘areanu, “Badger: complexity analysis with fuzzing and symbolic execution,” inProceedings of the 27th ACM SIGSOFT international symposium on software testing and analysis, 2018, pp. 322–332

  51. [51]

    Openjdk regular expression engine commit,

    OpenJDK Project, “Openjdk regular expression engine commit,” https://github.com/openjdk/jdk/commit/b45ea89

  52. [52]

    java.util.regexpackage documen- tation,

    Oracle Corporation, “java.util.regexpackage documen- tation,” https://docs.oracle.com/javase/8/docs/api/java/util/regex/ package-summary.html. 15

  53. [53]

    Sound static analysis of regular expressions for vulnerabilities to denial of service attacks,

    F. Parolini and A. Min ´e, “Sound static analysis of regular expressions for vulnerabilities to denial of service attacks,”Science of Computer Programming, vol. 229, p. 102960, 2023

  54. [54]

    Slowfuzz: Automated domain-independent detection of algorithmic complexity vulnerabilities,

    T. Petsios, J. Zhao, A. D. Keromytis, and S. Jana, “Slowfuzz: Automated domain-independent detection of algorithmic complexity vulnerabilities,” inProceedings of the 2017 ACM SIGSAC conference on computer and communications security, 2017, pp. 2155–2168

  55. [55]

    “re—regular expression operations — python 3 library reference

    Python Software Foundation, ““re—regular expression operations — python 3 library reference”,” https://docs.python.org/3/library/re.html

  56. [56]

    Static analysis for regular expression exponential runtime via substructural logics,

    A. Rathnayake and H. Thielecke, “Static analysis for regular expression exponential runtime via substructural logics,”CoRR abs/1405.7058, 2014

  57. [57]

    Pycg: Practical call graph generation in python. in 2021 ieee/acm 43rd international conference on software engineering (icse),

    V . Salis, T. Sotiropoulos, P. Louridas, D. Spinellis, and D. Mitropou- los, “Pycg: Practical call graph generation in python. in 2021 ieee/acm 43rd international conference on software engineering (icse),”IEEE, IEEE, Madrid, Spain, pp. 1646–1657, 2021

  58. [58]

    Towards a scalable software model checker for higher-order programs,

    R. Sato, H. Unno, and N. Kobayashi, “Towards a scalable software model checker for higher-order programs,” inProceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation, 2013, pp. 53–62

  59. [59]

    Crosshair: A symbolic execution framework for python,

    P. Schanely, “Crosshair: A symbolic execution framework for python,” https://github.com/pschanely/CrossHair, 2025

  60. [60]

    Interpolation-based function summaries in bounded model checking,

    O. Sery, G. Fedyukovich, and N. Sharygina, “Interpolation-based function summaries in bounded model checking,” inHaifa verification conference. Springer, 2011, pp. 160–175

  61. [61]

    Rescue: crafting regular expression dos attacks,

    Y . Shen, Y . Jiang, C. Xu, P. Yu, X. Ma, and J. Lu, “Rescue: crafting regular expression dos attacks,” inProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 225–235

  62. [62]

    Understanding regular expression denial of service (redos): Insights from llm- generated regexes and developer forums,

    M. L. Siddiq, J. Zhang, and J. C. D. S. Santos, “Understanding regular expression denial of service (redos): Insights from llm- generated regexes and developer forums,” inProceedings of the 32nd IEEE/ACM International Conference on Program Comprehension, 2024, pp. 190–201

  63. [63]

    The state of open-source security,

    Snyk, “The state of open-source security,” https://snyk.io/, 2020

  64. [64]

    A regular-expression matcher,

    H. Spencer, “A regular-expression matcher,” inSoftware solutions in C, 1994, pp. 35–71

  65. [65]

    Symbolic boolean deriva- tives for efficiently solving extended regular expression constraints,

    C. Stanford, M. Veanes, and N. Bjørner, “Symbolic boolean deriva- tives for efficiently solving extended regular expression constraints,” inProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 620–635

  66. [66]

    Towards an effective method of{ReDoS}detection for non-backtracking engines,

    W. Su, H. Huang, R. Li, H. Chen, and T. Ge, “Towards an effective method of{ReDoS}detection for non-backtracking engines,” in33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 271– 288

  67. [67]

    Programming techniques: Regular expression search algorithm,

    K. Thompson, “Programming techniques: Regular expression search algorithm,”Communications of the ACM, vol. 11, no. 6, pp. 419–422, 1968

  68. [68]

    Counting in regexes considered harmful: Exposing{ReDoS} vulnerability of nonbacktracking matchers,

    L. Turo ˇnov´a, L. Hol´ık, I. Homoliak, O. Leng´al, M. Veanes, and T. V o- jnar, “Counting in regexes considered harmful: Exposing{ReDoS} vulnerability of nonbacktracking matchers,” in31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 4165–4182

  69. [69]

    Abstracting concolic execution for soft contract verification,

    B. Vandenbogaerde, Q. Sti ´evenart, and C. De Roover, “Abstracting concolic execution for soft contract verification,” in32nd Static Analysis Symposium, 2025

  70. [70]

    oo7: Low-overhead defense against spectre attacks via program analysis,

    G. Wang, S. Chattopadhyay, I. Gotovchits, T. Mitra, and A. Roy- choudhury, “oo7: Low-overhead defense against spectre attacks via program analysis,”IEEE Transactions on Software Engineering, vol. 47, no. 11, pp. 2504–2519, 2019

  71. [71]

    A modular nfa architecture for regular expression matching,

    H. Wang, S. Pu, G. Knezek, and J.-C. Liu, “A modular nfa architecture for regular expression matching,” inProceedings of the 18th annual ACM/SIGDA international symposium on Field programmable gate arrays, 2010, pp. 209–218

  72. [72]

    {NLP-EYE}: Detecting memory corruptions via{Semantic-Aware} memory operation function identification,

    J. Wang, S. Ma, Y . Zhang, J. Li, Z. Ma, L. Mai, T. Chen, and D. Gu, “{NLP-EYE}: Detecting memory corruptions via{Semantic-Aware} memory operation function identification,” in22nd International Sym- posium on Research in Attacks, Intrusions and Defenses (RAID 2019), 2019, pp. 309–321

  73. [73]

    Wacana: A concolic analyzer for detecting on-chain data vulnerabilities in wasm smart contracts,

    W. Wang, C. Tu, Z. Meng, W. Huang, and Y . Xiong, “Wacana: A concolic analyzer for detecting on-chain data vulnerabilities in wasm smart contracts,”ACM Transactions on Software Engineering and Methodology, 2024

  74. [74]

    Effective redos detection by principled vulner- ability modeling and exploit generation,

    X. Wang, C. Zhang, Y . Li, Z. Xu, S. Huang, Y . Liu, Y . Yao, Y . Xiao, Y . Zou, Y . Liuet al., “Effective redos detection by principled vulner- ability modeling and exploit generation,” in2023 IEEE Symposium on Security and Privacy (SP). IEEE, 2023, pp. 2427–2443

  75. [75]

    Compiling parallel symbolic execution with continuations,

    G. Wei, S. Jia, R. Gao, H. Deng, S. Tan, O. Bra ˇcevac, and T. Rompf, “Compiling parallel symbolic execution with continuations,” in2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE). IEEE, 2023, pp. 1316–1328

  76. [76]

    An- alyzing matching time behavior of backtracking regular expression matchers by using ambiguity of nfa,

    N. Weideman, B. Van Der Merwe, M. Berglund, and B. Watson, “An- alyzing matching time behavior of backtracking regular expression matchers by using ambiguity of nfa,” inInternational Conference on Implementation and Application of Automata. Springer, 2016, pp. 322–334

  77. [77]

    Static detection of dos vulnerabilities in programs that use regular expressions,

    V . W¨ustholz, O. Olivo, M. J. Heule, and I. Dillig, “Static detection of dos vulnerabilities in programs that use regular expressions,” inIn- ternational Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2017, pp. 3–20

  78. [78]

    Scheduling constraint based abstraction refinement for weak memory models,

    L. Yin, W. Dong, W. Liu, and J. Wang, “Scheduling constraint based abstraction refinement for weak memory models,” inProceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018, pp. 645–655

  79. [79]

    {QSYM}: A practi- cal concolic execution engine tailored for hybrid fuzzing,

    I. Yun, S. Lee, M. Xu, Y . Jang, and T. Kim, “{QSYM}: A practi- cal concolic execution engine tailored for hybrid fuzzing,” in27th USENIX Security Symposium (USENIX Security 18), 2018, pp. 745– 761

  80. [80]

    Z3: The theorem prover,

    Z3Prover, “Z3: The theorem prover,” https://github.com/Z3Prover/z3, 2025

Showing first 80 references.