Twinning automata and regular expressions for string static analysis

DOI10.1007/978-3-030-67067-2_13MaRDI QIDQ2234078zbMATH OpenOpenAlexFDO

Authors Luca Negrini, Vincenzo Arceri, Pietro Ferrara, Agostino Cortesi

Publication date 18 October 2021

Full work available at URL https://arxiv.org/abs/2006.02715

zbMATH Keywords

abstract interpretationstatic analysisstring analysis

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: In this paper we formalize and prove the soundness of Tarsis, a new abstract domain based on the abstract interpretation theory that approximates string values through finite state automata. The main novelty of Tarsis is that it works over an alphabet of strings instead of single characters. On the one hand, such approach requires a more complex and refined definition of the widening operator, and the abstract semantics of string operators. On the other hand, it is in position to obtain strictly more precise results than than state-of-the-art approaches. We implemented a prototype of Tarsis, and we applied it on some case studies taken from some of the most popular Java libraries manipulating string values. The experimental results confirm that Tarsis is in position to obtain strictly more precise results than existing analyses.

Recommendations

• String analysis as an abstract interpretation
• A Practical String Analyzer by the Widening Approach
• String abstract domains and their combination
• scientific article; zbMATH DE number 2090837
• An Evaluation of Automata Algorithms for String Analysis

Cites work

• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• A Practical String Analyzer by the Widening Approach
• A parametric abstract domain for lattice-valued regular expressions
• Abstract Interpretation Frameworks
• Abstract domains for type juggling
• Abstract program slicing: an abstract interpretation-based approach to program slicing
• Abstract symbolic automata: mixed syntactic/semantic similarity analysis of executables
• Applications of symbolic finite automata
• Automata-based symbolic string analysis for vulnerability detection
• Chain-free string constraints
• Completeness of abstract domains for string analysis of JavaScript programs
• Computer Aided Verification
• Computer aided verification. 26th international conference, CAV 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 18--22, 2014. Proceedings
• Dashed strings for string constraint solving
• Making abstract interpretations complete
• Minimization of symbolic automata
• Programming Languages and Systems
• Widening and narrowing operators for abstract interpretation

Cited in

(9)

• An Evaluation of Automata Algorithms for String Analysis
• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• String analysis as an abstract interpretation
• A Practical String Analyzer by the Widening Approach
• Improving dynamic code analysis by code abstraction
• Relational string abstract domains
• String abstract domains and their combination
• Inferring grammatical summaries of string values
• Reference abstract domains and applications to string analysis

This page was built for publication: Twinning automata and regular expressions for string static analysis

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