Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Student works
  4. Formal Verification of Memoized Backtracking for JavaScript Regexes
 
master thesis

Formal Verification of Memoized Backtracking for JavaScript Regexes

Ammann, Sophie
July 5, 2024

In the context of regular expressions, many techniques have been developed to accelerate the matching process. Backtracking engines are widespread today as they support all extended regex features and exhibit better performance in most use cases. However, they are subject to ReDoS attacks due to their exponential worst-case complexity. To mitigate this risk, memoization is one solution. It involves recording the results of a recursive function to avoid redundant computations. Most JavaScript’s engines are based on a backtracking algorithm, which could thus benefit from memoization. Currently, no existing optimizations in this direction are present in the various implementations of JS engines. This study formalizes a memoized backtracking algorithm for a subset of JS regexes. The initial implementation covers a simple backtracking algorithm. Then, a memoized version is presented with a subsequent proof of equivalence between the first algorithm and the memoized version. During the process, core properties are presented concerning the memoization table. Future directions include verifying equivalence with ECMAScript semantics, proving termination, and extending capabilities to encompass more JS regex features. This research aims to enhance understanding and practical application of regex optimization techniques in JS environments.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

Formal Verification of Memoized Backtracking for JavaScript Regexes.pdf

Type

Main Document

Version

Submitted version (Preprint)

Access type

openaccess

License Condition

N/A

Size

1.66 MB

Format

Adobe PDF

Checksum (MD5)

966d5431a7f5deccfb8064d346fbcc2d

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés