Security Protocols

Security protocols are ubiquitous and play an important role in our life. Thus, formal methods for verifying them are of great practical importance. Moreover, they also raise many interesting theoretical questions. Security protocols generate inherently infinite-state systems for which even simple properties are undecidable. Over the years, people have extensively studied decidability questions for various restricted versions of the basic problem: is there an execution scenario of the protocol that allows an active bad guy (who controls the insecure network) to learn a designated secret that is communicated between two honest principals? A more basic problem (which has also been extensively studied) is to decide whether a passive bad guy (who only observes messages passing through the network) learns some designated secrets. This is just a version of the derivability question for certain proof system. This question becomes more
interesting as we try to capture more cryptographic operators in our proof rules.

For solving such decision problems, automata-theoretic techniques proved to be successful. For instance, a recent DEXPTIME-completeness result for one such proof system uses an application of the saturation construction for alternating automata to prove the upper bound while establishing the lower-bound via reduction to alternating pushdown systems. We propose to explore such automata-based techniques for studying various versions of the secrecy problem (for passive intruders).

Static Analysis of Concurrent Programs

The class of data-race-free concurrent programs emerged as an important class of programs due to the standardisation of the “SC-for-DRF” semantics for popular concurrent programming languages like Java and C++. Under this standartisation, data-race-free programs are guaranteed to be executed with the standard “Sequentially Consistent” or interleaving semantics, while data-racy programs will be run with little or no guarantees. It has thus become important to classify a concurrent program as being data-race-free or not. What we would like to focus on, however, is the following question: Given that a program is known to be data-race-free, can we analyze it more efficiently? Recent work has shown that it is indeed possible to lift some standard data-flow analyses of sequential programs to concurrent (data-race-free) ones. We would like to investigate the potential of doing this for other kinds of analysis (as in the work of Gotsman
et. al. on shape analysis) and verification techniques (e.g., for assume-guarantee-based reasoning).

Analysis of Concurrent Recursive Programs

A typical recursive sequential program has an infinite state space. This arises for two different reasons: firstly the variables might take values from an unbounded domain, and secondly the size of the program stack may increase unboundedly. One useful abstraction restricts the variables to a finite domain (e.g., boolean values) and leaves the stack as it is. The program is thus modeled as a classical finite state machine with a pushdown storage (pushdown system) and hence has an infinite state space. Over the last decade it has been shown that pushdown systems are amenable to the verification of a variety of properties: control state reachability, computing the forward and backward reachable sets, verifying properties expressible in temporal logics such as LTL.

However, the pushdown system model fails to capture behaviors of multi-threaded programs, as each thread evolves with its own stack. To model such programs we need systems with multiple pushdown stores. Unfortunately, finite state machines with unrestricted access to two pushdown stores are Turing powerful and hence impossible to verify. This leads us to the question: Which reasonable restrictions can one place on pushdown access so that the resulting model is analyzable? Several restrictions have been considered in the literature. Nevertheless, a more general problem is still open: Is there a uniform technique that underlies all the different algorithms proposed to analyze these different models? Most of the existing results on multiple pushdown systems restrict themselves to linear-time model checking; it would also be interesting to study the tractability of branching time properties of such systems.

Analysis of Timed Systems

Timed systems, as well as message passing systems, have been studied extensively over the last two decades. However in many real-life applications, as exemplified in the UML language, it is necessary to deal with systems that incorporate both message-passing concurrency and real time behaviors. The study of such systems started only recently and most of the obtained results are negative — showing the undecidability of fairly elementary properties. There have been a few positive results, especially when one restricts the message-passing communication to be bounded and further imposes restrictions on the permitted timing constraints. We believe that these positive results are only the beginning and suggest models that can be analyzed by combining techniques from the two domains in a nontrivial manner.

Dynamic Distributed Systems Nowadays, computer systems are marked by the interaction of numerous processes, whose number and communication topology are in general not fixed and evolve dynamically durint the execution. Examples include protocols for mobile computing and ad-hoc networks, which are designed for an open world, where the participating actors are not all known in advance. Unfortunately, the most well-studied notions in the context of distributed systems such as communicating finite-state machines, message sequence charts, or multi-pushdown systems, restrict to fixed architectures with a predetermined set of processes. While notions for fixed architectures come with a mature theory and robust models, a similar framework for the dynamic setting is missing. We therefore aim at developing models and notions that extend the state of the art and serve as a framework for analysis and synthesis of dynamic distributed systems.

A first automata model —tailored to the message sequence charts mentioned in the previous paragraph— was defined by Bollig and Hélouet. However, language theoretical properties and connections with logic are still unknown. In particular, a basic notion of regularity, as it was established for message sequence charts by Mukund et al., would be a starting point to obtain robust automata models and logics. Interestingly, there seem to be connections with data words/trees (over infinite alphabets), which recently attracted a lot of interest from the database community. It would be worthwhile to transfer these results to our, more specialized setting, where the infinite alphabet will be used to model process identifiers.

Quantitative Query Languages for XML Documents Formal methods for specifying and verifying qualitative as well as probabilistic properties of critical systems are already well-developed. But other quantitative properties of systems are of interest, e.g., energy consumption, waiting time, various kinds of costs or rewards, their probabilistic versions such as expected rewards, etc. Weighted automata provide a very general framework for the modeling of quantitative systems but a strong theory for specifying and verifying quantitative properties still needs to be developed. In 2005, Droste and Gastin introduced a quantitative (weighted) extension of MSO logic and established its relationship with weighted automata. This result has been generalized to numerous settings such as trees, pictures, concurrent systems, but weighted extensions of temporal logics (linear time or branching time) are lacking. A corresponding study would also add value to issues in database theory: Query languages such as XPath are used to perform queries in XML trees, in order to select nodes having certain desired property, and to extract the relevant information. In this framework, queries are Boolean: a node is selected or not by a query.

Our aim is to extend Boolean queries to quantitative ones, to express for instance the cost required to answer a query at a given node, or the probability that a node is selected by a query. In the same way in which MSO properties on words are captured by finite automata, appropriate types of tree-walking automata can capture boolean properties expressed by query languages. We want to extend classical tree-walking automata with weights to capture the expressive power of weighted queries and obtain decidability results. For the word case, some positive results have recently been obtained. In the context of databases and XML, however, they have to be extended to trees, which will require substantially more work and different techniques.