RELATIONAL STRING VERIFICATION USING MULTI-TRACK AUTOMATA

Citations Over TimeTop 10% of 2011 papers

Abstract

Verification of string manipulation operations is a crucial problem in computer security. In this paper, we present a new relational string verification technique based on multi-track automata. Our approach is capable of verifying properties that depend on relations among string variables. This enables us to prove that vulnerabilities that result from improper string manipulation do not exist in a given program. Our main contributions in this paper can be summarized as follows: (1) We formally characterize the string verification problem as the reachability analysis of string systems and show decidability/undecidability results for several string analysis problems. (2) We develop a sound symbolic analysis technique for string verification that over-approximates the reachable states of a given string system using multi-track automata and summarization. (3) We evaluate the presented techniques with respect to several string analysis benchmarks extracted from real web applications.

Related Papers

• → Decidability of reachability in vector addition systems (Preliminary Version)(1982)319 cited
• → Continuous Reachability for Unordered Data Petri Nets is in PTime(2019)9 cited
• → Some decidable results on reachability of solvable systems(2013)5 cited
• → Reachability problems for cyclic protocols(2002)5 cited
• → Continuous Reachability for Unordered Data Petri nets is in PTime(2019)