A Symbolic Execution Framework for JavaScript

As AJAX applications gain popularity, client-side JavaScript code is becoming increasingly complex. However, few automated vulnerability analysis tools for JavaScript exist. In this paper, we describe the first system for exploring the execution space of JavaScript code using symbolic execution. To handle JavaScript code’s complex use of string operations, we design a new language of string constraints and implement a solver for it. We build an automatic end-to-end tool, Kudzu, and apply it to the problem of finding client-side code injection vulnerabilities. In experiments on 18 live web applications, Kudzu automatically discovers 2 previously unknown vulnerabilities and 9 more that were previously found only with a manually-constructed test suite.

• Publication year

  2010

• Venue

  IEEE Symposium on Security and Privacy

• Publication date

  2010-05-16

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1109/SP.2010.38
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Rex: Symbolic Regular Expression Explorer

  2010cited by this paper
• FLAX: Systematic Discovery of Client-side Validation Vulnerabilities in Rich Web Applications

  2010cited by this paper
• Automatic creation of SQL Injection and cross-site scripting attacks

  2009cited by this paper
• XCS: cross channel scripting and its impact on web applications

  2009cited by this paper
• A decision procedure for subset constraints over regular languages

  2009cited by this paper
• Secure Content Sniffing for Web Browsers, or How to Stop Papers from Reviewing Themselves

  2009cited by this paper
• Extracting Models of Security-Sensitive Operations using String-Enhanced White-Box Exploration on Binaries

  2009cited by this paper
• HAMPI: a solver for string constraints

  2009influential reference
• Path Feasibility Analysis for String-Manipulating Programs

  2009influential reference
• Staged information flow for javascript

  2009cited by this paper
• Symbolic String Verification: Combining String Analysis and Size Analysis

  2009cited by this paper
• GATEKEEPER: Mostly Static Enforcement of Security and Reliability Policies for JavaScript Code

  2009cited by this paper
• Saner: Composing Static and Dynamic Analysis to Validate Sanitization in Web Applications

  2008cited by this paper
• Automatic Generation of XSS and SQL Injection Attacks with Goal-Directed Model Checking

  2008cited by this paper
• Dynamic test input generation for web applications

  2008cited by this paper
• Automated Whitebox Fuzz Testing

  2008cited by this paper
• Finding bugs in dynamic web applications

  2008cited by this paper
• Crawling AJAX by Inferring User Interface State Changes

  2008cited by this paper
• XSS Cheat Sheet

  2007cited by this paper
• A Decision Procedure for Bit-Vectors and Arrays

  2007influential reference
• Satisfiability of word equations with constants is in PSPACE

  1999cited by this paper
• The expressibility of languages and relations by word equations

  1997cited by this paper
• Periodic Sets of Integers

  1994cited by this paper
• Definability in the Existential Theory of Concatenation and Undecidable Extensions of this Theory

  1988cited by this paper
• Equations between regular terms and an application to process logic

  1981cited by this paper
• The Equivalence Problem for Regular Expressions with Intersection is Not Polynomial in Tape

  1973cited by this paper

• The Power of Regular Constraint Propagation

  2025cites this paper
• Relia: Accelerating the Analysis of Cloud Access Control Policies

  2025cites this paper
• Static Inference of Regular Grammars for Ad Hoc Parsers

  2025cites this paper
• Word equations in synergy with regular constraints (extended version)

  2025cites this paper
• Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis

  2025influential citation
• Path-Minimal Objects in ArkTS Symbolic Execution: From Path Constraints to TypeScript Tests

  2025cites this paper
• An efficient string solver for string constraints with regex-counting and string-length

  2025cites this paper
• High-Throughput SAT Sampling

  2025cites this paper
• OSTRICH2: Solver for Complex String Constraints

  2025cites this paper
• Decision Procedure for A Theory of String Sequences

  2025cites this paper
• HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses(Technical Report)

  2025influential citation
• Do (Not) Follow the White Rabbit: Challenging the Myth of Harmless Open Redirection

  2025cites this paper
• Negated String Containment is Decidable (Technical Report)

  2025cites this paper
• JSimpo: Structural Deobfuscation of JavaScript Programs

  2025cites this paper
• Novel Datasets and Traffic Generation Tools for Intrusion Detection in IoT Communications

  2025cites this paper
• Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly

  2024cites this paper
• A Constraint Solving Approach to Parikh Images of Regular Languages

  2024cites this paper
• Rogueone: Detecting Rogue Updates via Differential Data-Flow Analysis Using Trust Domains

  2024cites this paper
• Concolic Testing of JavaScript using Sparkplug

  2024cites this paper
• Undefined-oriented Programming: Detecting and Chaining Prototype Pollution Gadgets in Node.js Template Engines for Malicious Consequences

  2024cites this paper
• On the Verification of Control Flow Attestation Evidence

  2024cites this paper
• The Great Request Robbery: An Empirical Study of Client-side Request Hijacking Vulnerabilities on the Web

  2024cites this paper
• Solving String Constraints with Concatenation Using SAT

  2024cites this paper
• Detecting Malicious Websites From the Perspective of System Provenance Analysis

  2024cites this paper
• Solving String Constraints Using SAT

  2023cites this paper
• In-Situ Concolic Testing of JavaScript

  2023cites this paper
• Chain-Free String Constraints (Technical Report)

  2023cites this paper
• JS Capsules: A Framework for Capturing Fine-grained JavaScript Memory Measurements for the Mobile Web

  2023cites this paper
• Intelligent Form Generator Using Expert Systems

  2023cites this paper
• DAppHunter: Identifying Inconsistent Behaviors of Blockchain-based Decentralized Applications

  2023cites this paper
• Scaling JavaScript Abstract Interpretation to Detect and Exploit Node.js Taint-style Vulnerability

  2023cites this paper
• It’s (DOM) Clobbering Time: Attack Techniques, Prevalence, and Defenses

  2023cites this paper
• Black Ostrich: Web Application Scanning with String Solvers

  2023cites this paper
• Parikh’s Theorem Made Symbolic

  2023cites this paper
• FProbe: The Flow-Centric Detection and a Large-Scale Measurement of Browser Fingerprinting

  2023cites this paper
• Solving String Constraints with Lengths by Stabilization

  2023influential citation
• A decision procedure for string constraints with string/integer conversion and flat regular constraints

  2023cites this paper
• An Empirical Evaluation of Using Large Language Models for Automated Unit Test Generation

  2023cites this paper
• A Regular Matching Constraint for String Variables

  2023cites this paper
• On Detecting and Measuring Exploitable JavaScript Functions in Real-world Applications

  2023cites this paper
• Toward the flow-centric detection of browser fingerprinting

  2023cites this paper
• Even Faster Conflicts and Lazier Reductions for String Solvers

  2022cites this paper
• Dazzle-attack: Anti-Forensic Server-side Attack via Fail-Free Dynamic State Machine

  2022cites this paper
• TensileFuzz: facilitating seed input generation in fuzzing via string constraint solving

  2022cites this paper
• Subsequences With Gap Constraints: Complexity Bounds for Matching and Analysis Problems

  2022cites this paper
• Word Equations in Synergy with Regular Constraints (Technical Report)

  2022cites this paper
• Concolic Execution for WebAssembly

  2022cites this paper
• Enhancing Cybersecurity and Privacy with Artificial Intelligence

  2022cites this paper
• On the Feasibility of Automated Built-in Function Modeling for PHP Symbolic Execution

  2021cites this paper
• ObliCheck: Efficient Verification of Oblivious Algorithms with Unobservable State

  2021cites this paper
• On Solving String Constraints

  2021influential citation
• DiverJS: path exploration heuristic for difference analysis of event-driven code

  2021influential citation
• Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables (Technical Report)

  2021influential citation
• BIROn - Birkbeck Institutional Research Online is decidable about string constraints with the ReplaceAll function.

  2021cites this paper
• Solving string constraints with Regex-dependent functions through transducers with priorities and variables

  2021cites this paper
• Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost

  2021cites this paper
• Defeating Program Analysis Techniques via Ambiguous Translation

  2021cites this paper
• Mathematical Programming Modulo Strings

  2021cites this paper
• Wenqing Xu-Research Paper

  2021cites this paper
• CertiStr: a certified string solver

  2021influential citation
• Concolic Execution of NMap Scripts for Honeyfarm Generation

  2021cites this paper
• Concolic-Fuzzing of JavaScript Programs using GraalVM and Truffle

  2021cites this paper
• Completeness of string analysis for dynamic languages

  2021cites this paper
• ZaligVinder: A generic test framework for string solvers

  2021cites this paper
• If It’s Not Secure, It Should Not Compile: Preventing DOM-Based XSS in Large-Scale Web Development with API Hardening

  2021cites this paper
• Systematic Generation of Conformance Tests for JavaScript

  2021cites this paper
• Reusing Solutions Modulo Theories

  2021cites this paper
• Program Specialization as a Tool for Solving Word Equations

  2021cites this paper
• Diversifying Focused Testing for Unit Testing

  2021cites this paper
• String Theories involving Regular Membership Predicates: From Practice to Theory and Back

  2021cites this paper
• UFuzzer: Lightweight Detection of PHP-Based Unrestricted File Upload Vulnerabilities Via Static-Fuzzing Co-Analysis

  2021cites this paper
• JAW: Studying Client-side CSRF with Hybrid Property Graphs and Declarative Traversals

  2021influential citation
• The Client Insourcing Refactoring and Its Applications to Optimizing and Enhancing Distributed Execution

  2020cites this paper
• Reductions for Strings and Regular Expressions Revisited

  2020cites this paper
• String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report)

  2020influential citation
• Dashed strings for string constraint solving

  2020cites this paper
• PMForce: Systematically Analyzing postMessage Handlers at Scale

  2020influential citation
• Finding Client-side Business Flow Tampering Vulnerabilities

  2020cites this paper
• Prioritising Server Bugs via Inter-process Concolic Testing

  2020cites this paper
• An SMT Solver for Regular Expressions and Linear Arithmetic over String Length

  2020cites this paper
• A Length-aware Regular Expression SMT Solver

  2020cites this paper
• Inter-theory dependency analysis for SMT string solvers

  2020influential citation
• Dashed Strings and the Replace(-all) Constraint

  2020cites this paper
• Rule-based Word Equation Solving

  2020cites this paper
• On Solving Word Equations via Program Transformation

  2020cites this paper
• Efficient machine learning for attack detection

  2020cites this paper
• A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

  2020cites this paper
• String Constraint Solving: Past, Present and Future

  2020cites this paper
• Automatic Model Completion for Web Applications

  2020cites this paper
• Efficient handling of string-number conversion

  2020cites this paper
• Augmenting Network Flows with User Interface Context to Inform Augmenting Network Flows with User Interface Context to Inform Access Control Decisions Access Control Decisions

  2020cites this paper
• On the Separability Problem of String Constraints

  2020cites this paper
• Web Engineering: 20th International Conference, ICWE 2020, Helsinki, Finland, June 9–12, 2020, Proceedings

  2020cites this paper
• Gillian, part i: a multi-language platform for symbolic execution

  2020cites this paper
• Gelato: Feedback-driven and Guided Security Analysis of Client-side Web Applications

  2020cites this paper
• Monadic Decomposition in Integer Linear Arithmetic

  2020cites this paper
• Enhancing Web App Execution with Automated Reengineering

  2020cites this paper
• Client Insourcing: Bringing Ops In-House for Seamless Re-engineering of Full-Stack JavaScript Applications

  2020cites this paper
• A Survey on String Constraint Solving

  2020cites this paper
• A Decision Procedure for String to Code Point Conversion

  2020cites this paper