Automata-based symbolic string analysis for vulnerability detection

DOI10.1007/S10703-013-0189-1MaRDI QIDQ2248096zbMATH OpenOpenAlexFDO

Authors Fang Yu, Muath Alkhalaf, Tevfik Bultan, 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 verificationstring analysisvulnerability analysisweb application security

Mathematics Subject Classification ID

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

Recommendations

• String Analysis via Automata Manipulation with Logic Circuit Representation
• Automata-based model counting for string constraints
• Relational string verification using multi-track automata
• Relational string verification using multi-track automata
• Simple linear string constraints

Cites work

• A Practical String Analyzer by the Widening Approach
• Ambiguity in Graphs and Expressions
• Computer Aided Verification
• Computer Aided Verification
• Efficient Symbolic Representations for Arithmetic Constraints in Verification
• scientific article; zbMATH DE number 1670791 (Why is no real title available?)
• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• MONA IMPLEMENTATION SECRETS
• Path Feasibility Analysis for String-Manipulating Programs
• Relational string verification using multi-track automata
• Symbolic automata: the toolkit
• Symbolic finite state transducers: algorithms and applications
• Translating regular expression matching into transducers

Cited in

(23)

• Automata-based model counting for string constraints
• Completeness of string analysis for dynamic languages
• Relational string abstract domains
• Twinning automata and regular expressions for string static analysis
• Trading plaintext-awareness for simulatability to achieve chosen ciphertext security
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• Pattern-based vulnerability discovery
• Static analysis of string encoders and decoders
• Relational string verification using multi-track automata
• An Evaluation of Automata Algorithms for String Analysis
• Relaxed parsing of regular approximations of string-embedded languages
• Relational string verification using multi-track automata
• Static detection of DoS vulnerabilities in programs that use regular expressions
• Symbolic String Verification: Combining String Analysis and Size Analysis
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• Detection techniques of format-string vulnerabilities in binary files
• Word equations in synergy with regular constraints
• Verified verifying: SMT-LIB for strings in Isabelle
• Solving string constraints using SAT
• Certainty in formalising SMT-LIB for strings in Isabelle
• A theory of injection-based vulnerabilities in formal grammars
• Word equations in synergy with regular constraints (extended version)
• Harnessing static analysis to help learn pseudo-inverses of string manipulating procedures for automatic test generation

Describes a project that uses

Uses Software

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

This page was built for publication: Automata-based symbolic string analysis for vulnerability detection

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2248096)