Published: 11th November 2011|
|Preface Fang Yu and Chao Wang|
|Keynote: String Analysis Tevfik Bultan||1|
|Invited Paper: Practical Distributed Control Synthesis Doron Peled and Sven Schewe||2|
|Invited Presentation: Shape Analysis Based on Forest Automata Lukas Holik||18|
|Invited Presentation: Informed Swarm Verification of Infinite-State Systems Anton Wijs||19|
|Trees over Infinite Structures and Path Logics with Synchronization Alex Spelten, Wolfgang Thomas and Sarah Winter||20|
|Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems Laurent Fribourg, Bertrand Revol and Romain Soulat||35|
|A coinductive semantics of the Unlimited Register Machine Alberto Ciaffaglione||49|
|Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements Christian Krause and Holger Giese||64|
|A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking Takashi Tomita, Shigeki Hagihara and Naoki Yonezaki||79|
This volume contains the proceedings of the 13th International Workshop on Verification of Infinite-State Systems (INFINITY 2011). The workshop was held in Taipei, Taiwan on October 10, 2011, as a satellite event to the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA). The INFINITY workshop aims at providing a forum for researchers who are interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.
The program committee of INFINITY 2011 consisted of
Each workshop paper submission was reviewed by 3-4 committee members or external reviewers. We thank the external referees Torben Amtoft, Lukas Holik, Chih-Duo Hong, Ondrej Lengal, and Arnaud Sangnier for their help.
We thank Lukas Holik and Anton Wijs for their presentations. We also want to thank the ATVA 2011 Organizing Committee for taking care of the local organization and accommodating our special requests.
The keynote speakers at the workshop were
Tevfik Bultan (University of California, Santa Barbara, USA)
Doron A. Peled (Bar Ilan University, Israel)
The final proceedings will appear in the Electronic Proceedings in Theoretical Computer Science (EPTCS) series. We thank Rob Van Glabbeek and Rajeev Alur for their support.
October 2011, Fang Yu and Chao Wang
Most important Web application vulnerabilities, such as SQL Injection, Cross Site Scripting and Malicious File Execution, are due to inadequate manipulation of string variables. String analysis is a static analysis technique that determines the values that a string expression can take during program execution at a given program point. This information can be used to detect security vulnerabilities and program errors, and to verify that program inputs are sanitized properly. In this talk I will discuss my research group's work on automata-based symbolic string analysis techniques for automatic verification of string manipulating programs. Our approach consists of three phases: Given an attack pattern, we first conduct a vulnerability analysis to identify if strings that match the attack pattern can reach security-sensitive functions. Next, we compute the vulnerability signature which characterizes all input strings that can exploit the discovered vulnerability. Given the vulnerability signature, we then construct sanitization statements that 1) check if a given input matches the vulnerability signature and 2) modify the input in a minimal way so that the modified input does not match the vulnerability signature. We have developed a tool called Stranger that implements our automata-based symbolic string analysis approach. Stranger can be used to find and eliminate string-related security vulnerabilities in PHP applications.
We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We come with a novel representation of sets of shape graphs based on tree automata which combines advantages of automata-based approaches (higher generality and flexibility of abstraction) with some advantages of separation-logic-based approaches (efficient local reasoning). In our approach, a heap is split into several separated parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we come with a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can be easily encoded as operations on our representation. This makes it possible to use a method based on a symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking, and verify efficiently properties like null-pointer dereferences, absence of garbage, shape properties, etc.
Swarm verification and parallel randomised depth-first search are very effective parallel techniques to hunt bugs in large explicit state spaces. In case bugs are absent, however, scalability of the parallelisation is completely lost. Informed swarm verification is an extension, in which workers periodically communicate with a manager to perform bounded searches. The workers do not synchronise with each other, though. This scheme helps each worker to perform a finite search, even if the state space is infinitely large, while still benefitting from randomisation to find bugs quickly. Because the workers operate independently, this technique is very suitable for large-scale parallel explicit state space exploration on a computer cluster. A prototype of this technique has been implemented in the LTSmin toolset, developed at the University of Twente.