Automata-based symbolic string analysis for vulnerability detection

DOI10.1007/s10703-013-0189-1zbMath1291.68272OpenAlexW1982132104MaRDI QIDQ2248096

Muath Alkhalaf, Tevfik Bultan, Fang Yu, Oscar H. Ibarra

Publication date: 30 June 2014

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-013-0189-1

zbMATH Keywords

automated verificationvulnerability analysisstring analysisweb application security

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Internet topics (68M11)

Related Items

Relaxed Parsing of Regular Approximations of String-Embedded Languages ⋮ Relational string abstract domains ⋮ Word equations in synergy with regular constraints ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Unnamed Item ⋮ Twinning automata and regular expressions for string static analysis ⋮ Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions ⋮ Trading Plaintext-Awareness for Simulatability to Achieve Chosen Ciphertext Security ⋮ Completeness of string analysis for dynamic languages

Uses Software

• CUTE
• MONA
• Stranger
• HAMPI
• Symbolic automata
• StrSolve
• PHP
• Saner

Cites Work

• Unnamed Item
• Unnamed Item
• Translating regular expression matching into transducers
• Symbolic Automata: The Toolkit
• Symbolic finite state transducers
• MONA IMPLEMENTATION SECRETS
• RELATIONAL STRING VERIFICATION USING MULTI-TRACK AUTOMATA
• Path Feasibility Analysis for String-Manipulating Programs
• Computer Aided Verification
• Computer Aided Verification
• A Practical String Analyzer by the Widening Approach
• Ambiguity in Graphs and Expressions
• Efficient Symbolic Representations for Arithmetic Constraints in Verification