Keynote Speaker: Ahmed Bouajjani (Université Paris Diderot-Paris 7, France)
Title: Verification of Concurrent Programs: Decidability, Complexity, Reductions
Abstract: Concurrency is present at different levels, from applications using high level synchronization mechanisms and abstract data structures under atomicity and isolation assumptions, to low level code implementing concurrent/distributed data structures and system services over multi-core architectures/large scale networks.
We will address the problem of verifying automatically concurrent programs, from the point of view of decidability and complexity, we will show the difficulties that raise in addressing this problem at of the levels mentioned above (huge amount of computations, complex control due to recursion and dynamic task creation, weak memory models, etc.), and we will overview existing approaches for tackling these issues. We will show in particular how the verification problems that must be considered in this context can be reduced to "simpler" problems (stated as reachability queries either on sequential programs, or on concurrent but sequentially consistent programs) for which there are already know verification algorithms and tools.
Speaker: Gilles Dowek (INRIA, France)
Title: Proofs and Model Checking
Abstract: In model checking, the truth of a formula is usually defined as the validity in a given model. I will discuss in this talk the advantages there might be to define it also as provability in a proof-system.
Speaker: Lijun Zhang (ISCAS, China)
Title: LTL Satisfiability Checking Revisited
Abstract: We propose a novel algorithm for the satisfiability problem for Linear Temporal Logic (LTL). Existing approaches first transform the LTL formula into a B\"uchi automaton and then perform an emptiness checking of the resulting automaton. Instead, our approach works on-the-fly by inspecting the formula directly, thus enabling finding a satisfying model quickly without constructing the full automaton. This makes our algorithm particularly fast for satisfiable formulas. We report on a prototype implementation, showing that our approach significantly outperforms state-of-the-art tools.
Speaker: Peng Wu (ISCAS, China)
Title: Assume-guarantee reasoning with local specifications
Abstract: We investigate assume-guarantee reasoning for global specifications consisting of conjunctions of local specifications. We present a sound and complete assume-guarantee methodology that enables us to establish properties of a composite system by checking local specifications of its individual modules. We illustrate our approach with an example from the field of network congestion control, where different agents are responsible for controlling packet flow across a shared infrastructure. In this context we derive an assume-guarantee system
for network stability and show its efficiency to reason about any number of agents, any initial flow configuration, and any topology of bounded degree.
Speaker: Hugo Daniel Macedo (INRIA, France)
Title: Mining malware specifications through static reachability analysis
Abstract: The number of malicious software (malware) is growing out of control. Syntactic signature based detection cannot cope with such growth and manual construction of malware signature databases needs to be replaced by computer learning based approaches. Currently, a single modern signature capturing the semantics of a malicious behavior can be used to replace an arbitrarily large number of old-fashioned syntactical signatures. However, teaching computers to learn malware behaviors is a challenge. Existing work relies on dynamic analysis to extract malicious behaviors, but such technique does not guarantee the coverage of all behaviors. To sidestep this limitation, we show how to learn malware signatures using static reachability analysis. The idea is to model binary programs using pushdown systems (that can be used to model the stack operations occurring during the binary code execution), use reachability analysis to extract behaviors in the form of trees, and use subtrees that are common among the trees extracted from a training set of malware files as signatures. To detect malware, we propose to use a tree automaton to compactly store malicious behavior trees and check if any of the trees extracted from the file under analysis contains a subtree corresponding to a malicious behavior. Experimental data shows that our approach can be used to learn signatures from a set of malware files and use them to detect a much larger set of malware obtaining promising results.
Joint work with Tayssir Touili.
Speaker: Kailiang Ji (Université Paris Diderot-Paris 7, France)
Title: Automated method in proving inductive and coinductive properties on graphs
Abstract: Given a proposition, if it is provable in predicate logic, it is true independently of all the consistency models. However, in proving graph problems, the graph is given, what we need to do is to check whether some properties are true in this graph. What we are doing is to define a theory in predicate logic such that the propositions provable in this theory are those that are true in a given graph. To efficiently proving the first order description of graph properties, we added some special simplification rules to the resolution system, without losing its completeness.
Keynote Speaker: Glynn Winskel (University of Cambridge, UK)
Title: A language for distributed strategies
Abstract: The concept of strategy is potentially as fundamental as that of relation. Distributed/concurrent strategies arise from basing the behaviour of games and strategies on event structures, the concurrent analogue of trees, in which histories take the form of partial orders of events. I'll motivate a definition of distributed strategy and present some recent (unfinished) work on a language and operational semantics for distributed strategies.
Speaker: Thomas Ehrhard (Université Paris Diderot-Paris 7, France)
Title: A tree oriented extension of CCS
Abstract: CCS can be considered as a most natural extension of finite state automata in which interaction is made possible thanks to parallel composition. We propose here a similar extension for top-down tree automata. We introduce a parallel composition which is parameterized by a graph at the vertices of which subprocesses are located. Communication is allowed only between subprocesses related by an edge in this graph. We define an observational equivalence based on barbs as well as weak bisimilarity equivalence and prove an adequacy theorem relating these two notions.
Joint work with Jiang Ying.
Speaker: Yongjian Li (ISCAS, China)
Title: Enhanced symbolic simulation of a round-robin arbiter
Abstract: A round-robin arbitration is a key component in network-based systems. This paper presents an automated formal verification method for hardware design of round-robin arbiter. The approach is based on symbolic trajectory evaluation (STE) which performs symbolic simulation for liveness checking of round-robin arbitration. The experiments demonstrate that the enhanced STE specification for realistic hardware design can be completed in a reasonable time. The work gives the first attempt to verify liveness properties for round-robin arbiters by STE.
Speaker: Pierre Louis Curien (Université Paris Diderot, France)
Title: Towards direct models of classical Logic
Abstract: We elaborate on Guillaume Munch's notion of duploid to suggest how to get models of classical logic that are direct in the sensé that no implicit translation is made prior to interpretation.
Speaker: Yu Zhang (ISCAS, China)
Title: Program Equivalence in Linear Contexts
Abstract: Program equivalence in linear contexts, where programs are used or executed exactly once, is an important issue in programming languages. However, existing techniques like those based on bisimulations and logical relations only target at contextual equivalence in the usual (non-linear) functional languages, and fail in capturing non-trivial equivalent programs in linear contexts, particularly when non-determinism is present. We propose the notion of linear contextual equivalence to formally characterize such program equivalence, as well as a novel and general approach to studying it in higher-order languages, based on labeled transition systems specifically designed for functional languages. We show that linear contextual equivalence indeed coincides with trace equivalence. We illustrate our technique in both deterministic (a linear version of PCF) and non-deterministic (linear PCF in Moggi's framework) functional languages.
Joint work with Yuxin Deng.
Speaker: Alejandro Díaz-Caro (INRIA, France)
Title: Identifying isomorphic propositions
Abstract: In typed lambda-calculus, in programming languages, and in proof theory, two types A and B are said to be isomorphic, if there exists two functions phi from A to B and psi from B to A such that psi composed with phi is the identity in A, and phi composed with psi the identity in B. In some cases, isomorphic types are identified. For instance, in Martin-Löf's type theory, in the Calculus of Constructions, and in Deduction modulo, definitionally equivalent types are identified. However, definitional equality is weaker than isomorphism and, for example, the isomorphic types A AND B and B AND A are not usually identified: a term of type A AND B does not have type B AND A. Not identifying such types has many drawbacks, for example if a library contains a proof of B AND A, a request on a proof of A AND B fails to find it, if r and s are proofs of (A AND B)=>C and (B AND A) respectively, it is not possible to apply r to s to get a proof of C, but we need to explicitly apply a function of type (B AND A)=>(A AND B) to s before we can apply r to this term. This has lead to several projects aiming to identify in a way or another isomorphic types in type theory, for example with the univalence axiom.
We introduce an extension of simply typed lambda calculus with pairs where isomorphic types are identified. In this calculus we have focused on three isomorphisms: associativity and commutativity of conjunction, and the distributivity of implication over conjunction. Identifying some types requires to also identify some terms via an equivalence relation on terms, leading to an interesting calculus, which is related to several known algebraic and non-deterministic calculi. In this talk I will present the system and a proof of normalisation based on a non-trivial adaptation of the reducibility candidates technique. Also I will show some ongoing ideas to introduce the curryfication: (A AND B) => C ~ A => B => C.
Keynote Speaker: Luc Maranget (INRIA, France)
Title: Testing (and Defining) Weak Memeory Models
Abstract: Shared memory multicore and multiprocessor machines do not follow the simple execution model of Sequential Consistency (SC). In this model, parallel execution results from the interleaving of thread executions and stores to memory take effect immediately. Actual systems allow more behaviours that the SC model, and hence follow "relaxed" memory models.
In this talk we shall first run tests on an actual machine to demonstrate that the machine does not follow the SC model. We shall then describe how to generate relevant tests and review some weak memory models. We shall focus on a recent, axiomatic, model for the very relaxed
IBM Power and ARM machines.
Speaker: Catuscia Palamidessi (INRIA and Ecole Polytechnique, France)
Title: Quantitative Approaches to Information Protection
Abstract: Secure information flow is the problem of ensuring that the information made publicly available by a computational system does not leak information that should be kept secret. Since it is practically impossible to avoid leakage entirely, in recent years there has been a growing interest in considering the quantitative aspects of information flow, in order to measure and compare the amount of leakage. In this talk, we revise the main recent approaches which have been proposed to quantify and reason about leakage, the information-theoretic approaches based on Shannon entropy and on Rényi min-entropy, and a novel one based on decision theory. Furthermore, we study the relation with differential privacy, a notion which has been proposed to cope with the problem of statistical disclosure control in the area of databases. Finally, we consider a generalization of differential privacy, which can be naturally applied to protect sensitive information also in domains other than databases. The talk is based on the papers below.
References:
1. Alvim, M.S., Andrés, M.E., Chatzikokolakis, K., Palamidessi, C.: On the relation between Differential Privacy and Quantitative Information Flow. In Luca Aceto, Monika Henzinger, J.S., ed.: 38th International Colloquium on Automata, Languages and Programming (ICALP). Volume 6756 of Lecture Notes in Computer Science., Zurich, Springer (2011) 60–76
2. Alvim, M.S., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF). (2012) 265–279
3. Chatzikokolakis, K., Andrés, M.E., Bordenabe, N.E., Palamidessi, C.: Broadening the scope of Differential Privacy using metrics. In E. De Cristofaro and M. Wright, editors, Proceedings of the 13th International Symposium on Privacy Enhancing Technologies (PETS), volume 7981 of Lecture Notes in Computer Science, pages 82–102. Springer, 2013
Speaker: Angsheng Li (ISCAS, China)
Title: Provable security of networks
Abstract: I will introduce a recent work by my team on network security, including mathematical definition of network security, and the principles for provable security of networks. The main results of my talk include a fundamental principle of networks, a community structure principle, a degree priority principle, an inclusion and infection principle, and an infection priority tree principle. These principles ensure that there exists an algorithm by natural mechanisms of homophyly, randomness and preferential attachment which constructs dynamically provably secure networks.
Speaker: Lili Xu (ISCAS, China)
Title: Metrics for Differential Privacy in Concurrent Systems
Abstract: Originally proposed for privacy protection in the context of statistical databases, differential privacy is now widely adopted in various models of computation. In this paper we investigate techniques for proving differential privacy in the context of concurrent systems. Our motivation stems from the work of Tschantz et al., who proposed a verification method based on proving the existence of a stratified family of bijections between states, that can track the privacy leakage, ensuring that it does not exceed a given leakage budget. We improve this technique by investigating state properties which are more permissive and still imply differential privacy. We consider three pseudometrics on probabilistic automata: The first one is essentially a reformulation of the notion proposed by Tschantz et al. The second one is a more liberal variant, still based on the existence of a family of bijections, but relaxing the relation between them by integrating the notion of amortization, which results into a more parsimonious use of the privacy budget. The third one aims at relaxing the bijection requirement, and is inspired by the Kantorovich-based bisimulation metric proposed by Desharnais et al. We cannot adopt the latter notion directly because it does not imply differential privacy. Thus we propose a multiplicative variant of it, and prove that it is still an extension of weak bisimulation. We show that for all the pseudometrics the level of differential privacy is continuous on the distance between the starting states, which makes them suitable for verification. Moreover we formally compare these three pseudometrics, proving that the latter two metrics are indeed more permissive than the first one, but incomparable with each other, thus constituting two alternative techniques for the verification of differential privacy.
Keywords: differential privacy, probabilistic automata, bisimulation metrics, verification.
Speaker: Jean Jaques Lévy (ISCAS - INRIA)
Title: Experiments with Why3
Abstract: We present several proofs of correctness for several sorting algorithms in Why3 + Coq + Ssreflect. We show how small variations of programs greatly modify the proof of correctness. Why3 is a fantastic system developped at LRI and INRIA (see http://why3.lri.fr) It combines calls to automatic provers and interactive proof checkers.
Speaker: Zhilin Wu (ISCAS, China)
Title: Extensions and restrictions of data automata
Abstract: Formalisms over infinite alphabets have recently received much focus in the community of theoretical computer science, with momentum from database theory and formal verification. Data automaton is a formal model for words over an infinite alphabet, that is, the product of a finite set of labels and an infinite set of data values, proposed by Bojanczyk, Muscholl, Schwentick et. al. in 2006.
A data automaton consists of two parts, a nondeterministic letter-to-letter transducer, and a class condition given by a regular language (e.g. specified by a finite automaton), which acts as a condition on each subword of the outputs of the transducer corresponding to a maximal set of positions with the same data value. We propose two variants of data automata by extending and restricting respectively the class conditions. For the extension of data automata, we prove the decidability of the nonemptiness problem by establishing their correspondence with priority multicounter automata, whose decidability was shown by Reinhardt in 2005. For the restriction, we propose commutative data automata, that is, data automata with class conditions restricted to commutative regular languages. While it is open whether the nonemptiness of data automata can be solved in elementary time, we show that the nonemptiness problem of commutative data automata can be solved in 3NEXPTIME.