DOCSEARCHbyAlgolia
Submit Docs

recheck

website·Indexed 30 days ago

https://makenowjust-labs.github.io/recheck/

A tool for detecting and analyzing Regular Expression Denial of Service (ReDoS) vulnerabilities. It supports practical regular expression features, including backreferences, and can be used as a Scala library, a JavaScript/TypeScript library, or an ESLint plugin. The tool utilizes static analysis, fuzzing, and automata theory to identify unsafe regular expressions.

Tokens
6.5K
Snippets
20
Records
45
Agent score
75%

What's inside recheck

  1. Overview of the recheck fuzzing algorithm for ReDoS detection

    The recheck tool uses a dynamic analysis fuzzing algorithm based on evolutionary computation (genetic algorithms) to detect ReDoS vulnerabilities. The process follows three primary stages:

    1. Seeding: Statically analyzes the regular expression to create an initial generation of test strings.
    2. Incubation: Uses a genetic algorithm to evolve these strings into inputs that increase matching time.
    3. Attack: Verifies if the generated strings cause exponential or polynomial matching time increases to confirm a vulnerability.

  2. Overview of recheck ReDoS detection capabilities

    recheck is a library designed to detect Regular Expression Denial of Service (ReDoS) vulnerabilities. It employs a state-of-the-art algorithm that combines static analysis with fuzzing. The library supports practical regular expression features, including backreferences and look-around operations, and can be embedded directly into applications as a library.

  3. Detect ReDoS vulnerabilities using the recheck library

    recheck is a library available in JavaScript and Scala used to statically analyze regular expressions for ReDoS vulnerabilities. It can identify vulnerabilities and generate a corresponding attack string to prove the flaw.

    Key capabilities include:

    • Hybrid detection: Uses a combination of automata theory and fuzzing with static analysis.
    • Broad support: Supports ECMA-262 (JavaScript) specifications, including complex operations like backreferences and look-around.
    • Recall validation: Validates suspected vulnerabilities using a real interpreter.
    • Integration: Available as a library for embedding in applications or as an ESLint plugin for immediate code analysis.

  4. Understand Regular Expression Denial of Service (ReDoS) vulnerabilities

    ReDoS (Regular expression Denial of Service) is a computational complexity attack that occurs when a regular expression engine using a backtracking approach takes exponential or superlinear time to process a specific input string. This can lead to application outages, as seen in historical cases with StackOverflow and Cloudflare. While some languages (like Go and Rust) use Deterministic Finite Automaton (DFA) approaches to avoid this, many other programming languages use backtracking, making them susceptible to ReDoS.

  5. Accelerate regular expression matching in recheck using selective memoization

    recheck uses selective memoization (based on the work by Davis et al.) to accelerate regular expression matching. This approach ensures that the time taken for matching is linear to the length of the input string in most cases by ensuring that a certain state at a certain position in the input string is reached at most once.

    Unlike DFA-based acceleration, this method preserves the behavior of backtracking, allowing recheck to accurately determine how long matching takes and mimic existing matching implementations. Because recheck's matching is VM-based, memoization is applied to the confluence of branch instructions rather than the confluence of branches in a transition diagram.

  6. Understand the relationship between Regular Expression ambiguity and ReDoS

    A regular expression is considered ambiguous if there are multiple matching processes for a single string. While finite ambiguity does not necessarily lead to ReDoS, the combination of ambiguity and repetition quantifiers can create 'partially infinite ambiguity,' which leads to exponential matching time complexity and ReDoS vulnerabilities.
    // Ambiguous but not ReDoS vulnerable (finite ambiguity)
/^(a|ab)(bc|c)$/

// ReDoS vulnerable (ambiguity + repetition = exponential complexity)
/^((a|ab)(bc|c))*$/

  7. Evolve ReDoS test strings using Incubation

    The Incubation phase uses a genetic algorithm to transform seeds into strings that maximize matching time. Instead of normal strings, recheck uses 'strings with repetition structures' as genes—represented as a sequence of a normal string $w$ and a repeated string $(w)^n$. This allows the number of repetitions to be adjusted as a variable, making mutation and crossover more efficient.

    To accelerate the process, recheck determines if matching takes significant time by counting the number of times a character is read during matching, rather than measuring actual wall-clock time.

  8. Cancel a recheck operation using AbortSignal

    The check method accepts an optional signal (of type AbortSignal) within the params argument to abort the operation.

    Caveats:

    • The signal parameter only works when using the external CLI command backends (native or java) or the worker backend. It is ignored by the pure backend and the synchronous checkSync API.
    • For simple timeouts, it is recommended to use the timeout parameter in params instead of a manual AbortController.
    import { check } from "recheck";

const controller = new AbortController();
const signal = controller.signal;

// Aborts check after 100ms
await Promise.all([
  check("^a+a+$", "", { signal }),
  new Promise((resolve) => setTimeout(() => {
    controller.abort();
    resolve(null);
  }, 100)),
]);

  9. Use attack strings and hotspots to fix ReDoS vulnerabilities

    When a diagnostic status is vulnerable, two fields are provided to help identify and fix the issue:

    1. attack: Contains a theoretical attack string designed to trigger a matching time explosion (ReDoS). The string is structured with pumps, a suffix, and a base repetition count. Each pump contains a prefix, repeating substrings, and an individual repetition count n. The final string is constructed as: prefix + repeating.repeat(base + n) + ... + suffix.

      • Note: Because of engine optimizations, theoretical attack strings may not always trigger an explosion; recall validation is recommended.

    2. hotspot: Identifies the specific substring within the regular expression that is executed most frequently against the attack string, pinpointing where the fix should be applied.

  11. Generate initial fuzz seeds via static analysis

    Seeding creates the initial generation for the genetic algorithm by statically analyzing the regular expression for specific state pairs $(q_1, q_2)$ in the EDA (Exponential Depth Automata) or IDA (Inconsistent Depth Automata) structures. A seed is identified when:

    • There are two different transitions from $q_1$ with the same letter $a$.
    • $q_1$ and $q_2$ can both transition with the same letter $b$.
    • $q_2$ can transition with the letter $a$.

    recheck adds repeated strings between these states to the initial generation to efficiently increase matching time. Note: Regular expression extensions that cannot be converted to NFA (like backreferences) are handled by replacing them with the regular expression of the referent.

  12. Determine the appropriate ReDoS detection algorithm

    The system prioritizes the automata-theory based algorithm for efficiency and theoretical accuracy. If the automata-theory approach cannot correctly detect the vulnerability or is impossible to use, the system falls back to the fuzzing algorithm.

    In practice, the system attempts NFA (Nondeterministic Finite Automaton) conversion first. If the size of the resulting NFA exceeds a predefined threshold, the system automatically switches to the fuzzing algorithm.