Lundi 15 juin
9:30 Accueil
Session »Bases de données »
9:45 Mots de bienvenue
10:00 Diego Figueira : On reflexive-transitive navigation in the presence of data values [[abstract]
When working on data words or data trees, it is often important to be able to compare data values from positions far apart. In modal or navigational languages, such as LTL or XPath, this is done using transitive closure modalities (such as Future, or Descendant). As it turns out, this type of modalities very easily makes the satisfiability problem either undecidable or with non-primitive recursive complexity. However, in many of these cases, replacing modalities with their reflexive-transitive counterpart (as opposed to only transitive) entails a series of monotonicity properties useful to gain decidability, even elementarity. The purpose of this talk is to give an idea of why adding reflexivity improves things.
%% __11:00__ Pause café %%block __11:30__ »__Claudia Carapelle:__ Satisfiability of CTL* with local constraints » [[abstract]
In the last years there has been a lot of research on the question how temporal logics like LTL, CTL or CTL* can be extended in order to deal with quantitative properties. One way to approach this question is to add « local constraints » to such temporal logics, which allow to compare « concrete values » from some chosen domain D at different time points, confined to an arbitrary – but bounded! – number of steps in the future. We show that the satisfiability problem for CTL* with local constraints is decidable for an arbitrary domain D, provided that D satisfies certain properties. One instance of a suitable domain are the integers equipped with order and equality relations.
%% !Session doctorants __12:00__ »__Michael Blondin:__ Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-complete » __12:15__ »__Dimitri Racordon:__ Déterminer des propriétés quantitatives à l’aide de logiques temporelles » !Pause déjeuner __12:30__ (Bâtiment P, salle P2-131) [Map | https://www.google.com/maps/d/edit?mid=zp2PeCQcQAnU.k8VW3QkDP1AY&usp=sharing] !Session »Systèmes temporisés » %%block __14:00__ »__Nicolas Markey__: Weighted Timed Automata and Games » [[abstract]
Weighted (aka priced) timed automata have been introduced 15 years ago as an intermediary model between timed and rectangular hybrid automata. In weighted timed automata, extra quantities can be measured, but their values cannot be used in the guards or invariants to constrain the runs of the underlying timed automaton. As a result, various problems are decidable in these models, while reachability is already undecidable in rectangular automata. In this talk, I will survey some important results that have been obtained about weighted timed automata, and describe a few directions for future research.
%% %%block __15:00__ »__Aleksandra Jovanovic:__ Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions » [[abstract]
We propose a method to synthesise optimal values of timing parameters for probabilistic timed automata, in the sense that the probability of reaching some set of states is either maximised or minimised. Our first algorithm, based on forward exploration of the symbolic states, can only guarantee parameter values that correspond to upper (resp. lower) bounds on maximum (resp. minimum) reachability probability. To ensure precise reachability probabilities, we adapt the game-based abstraction refinement method. In the parametric setting, our method is able to determine all the possible maximum (or minimum) reachability probabilities that arise for different values of timing parameters, and yields optimal valuations represented as a set of symbolic constraints between parameters.
%% __15:30__ Pause café %%block __16:00__ »__Stefano Minopoli__: Reachability Analysis of Simulation Models with SpaceEx » [[abstract]
The SpaceEx tool platform provides an analysis core for reachability and safety verification where systems are modeled by verification models consisting of network of Hybrid Automata (HA). It provides several reachability algorithms based on different state-spaces representations (polyhedra, zonotopes), and tailored to different systems dynamics (piece-wise constant, affine, multi-affine, nonlinear). Since verification problems are generally undecidable for such systems, experimental results are vital for evaluating and developing new ideas. The SpaceEx environment is designed to facilitate the implementation of algorithms related to reachability and safety verification. One of the recent extension of the analysis core is the introduction of a novel and exact algorithm for performing reachability analysis on systems originally designed using simulation models (e.g. by tools like Simulink, Modelica or Ptolemy). To allow reachability analysis on such systems, simulation models need to be abstracted using verification models. The process of abstraction is not a trivial task, since discrete transitions in simulation mode are taken as-soon-as guards are satisfied (must semantics), and therefore can not be directly modeled using the (may semantics) of hybrid automata. The proposed algorithm is designed for the class of Linear HA extended by urgent conditions, which allows to naturally model the must semantics, hence opening the door to verification of systems originally designed using simulation models. To illustrate the approach, we show results of reachability analysis on a Simulink diagram abstracted by a SpaceEx model automatically generated by the experimental tool Simulink to SpaceEx (SL2SX). Finally, to allow reachability analysis on simulation models featuring more complex dynamics, an over-approximated algorithm for Affine Hybrid Automata is currently under investigation.
%% %%block __16:30__ »__Ocan Sankur:__ Symbolic Robustness Analysis of Timed Automata » [[abstract]
We study the robust safety problem for timed automata under guard imprecisions which consists in computing an imprecision parameter under which a safety specification holds. This problem allows one to obtain formal guarantees on the robustness, or the sensitivity of a real-time system. We give a symbolic semi-algorithm for the problem based on a parametric data structure, and evaluate its performance in comparison with a recently published one, and with a binary search on enlargement values.
%% !Open steering committee __17:15__ Discussion autour du GT Vérification !! Mardi 16 juin !Session »Vérification de code » %%block __9:00__ »__Julien Signoles:__ Runtime Assertion Checking within Frama-C and its Combinations with Static Analyses » [[abstract]
In this talk, we will first present the formal specification language E-ACSL. It is a behavioral first-order typed specification language which supports in particular function contracts, assertions, user-defined predicates and built-in predicates (like \valid(p) which indicates that the pointer p points to a memory location that the program can write and read). Then we will focus on the Frama-C plug-in E-ACSL which automatically converts a C program p_1 specified with E-ACSL annotations to another C program p_2 which monitors each annotation of p_1 at runtime in order to check its validity for the current execution. Finally, we will introduce how this plug-in can combine with static verification techniques (e.g. abstract interpretation and weakest precondition calculus) and emphasize the benefits and difficulties of these combinations. The talk will be illustrated on concrete examples of C programs within the Frama-C software analysis framework.
%% %%block __9:55__ »__Steven de Oliveira:__ Model-Checking de propriétés temporelles sur des programmes C » [[abstract]
Le (bon) séquencement des événements au fil du temps est un sujet important pour l’analyse de programmes, par exemple dans le cadre de protocoles d’échange d’information ou de systèmes embarqués. De nombreux travaux s’appuient sur la logique temporelle linéaire (LTL) pour décrire formellement le comportement attendu d’un programme, sous la forme d’une succession d’actions distinctes. Nous présentons CaFE, un outil de model-checking de programmes C, implanté dans la plate-forme d’analyse de programmes Frama-C. Plus précisément, CaFE vérifie automatiquement de manière approchée (mais correcte) qu’un programme C vérifie une formule logique CaRet donnée, où CaRet est une extension de LTL autorisant en particulier des raisonnements explicites sur la pile d’appel du programme.
%% %%block __10:20__ »__Robin David:__ Sound and Quasi-Complete Detection of Infeasible Test Requirements » [[abstract]
Software structural testing relies on coverage criteria to assess the quality of test cases: a code-based test adequacy criterion specifies the requirements to be covered by the test cases. However, the application of such criteria is limited in practice due to the well-known infeasibility problem, which concerns elements/requirements that cannot be covered by any test case. To deal with this issue we revisit and improve state-of-the-art static analysis techniques, such as Value Analysis and Weakest Precondition calculus. We propose a lightweight greybox scheme for combining these two techniques in a complementary way. In particular we focus on detecting infeasible test requirements in an automatic and sound way for condition coverage, multiple condition coverage and weak mutation testing criteria. Experimental results show that our method is capable of detecting almost all the infeasible test requirements, 95% on average, in a reasonable amount of time, i.e., less than 40 seconds, making it practical for the unit level.
%% __10:45__ Pause café %%block __11:15__ »__Anthony Fernandes Pirès:__ Verification of embedded software’s source code from its model » [[abstract]
To reduce the costs of verification and increase reliability, formal methods, such as static analysis, allow to automatically prove code properties. Unfortunately, these techniques are difficult to understand and to use by non-experts. In addition to the verification costs issue, today software and their development are subject to an increase in complexity. Model Driven Engineering (MDE) allows dealing with these difficulties by offering models, and tasks to capitalize on these models all along the development lifecycle. The aim of this work is to make the link between model based design and the code implementation of an embedded software in order to propose to non-expert users a formal and automatic software verification approach. We propose to automatically generate code annotations corresponding to the behavioral properties of a software. These properties are derived from the design model and they can be verified by static analysis tools. We present an approach based on a subset of UML state machine to model software and we give a formal semantics of this subset and the method for ACSL annotations generation. The code proof is then handled by Frama-C.
%% %%block __11:40__ »__Jacques-Charles Mbiada Njanda:__ Frama-C Compiler » [[abstract]
Frama-C est un outil d’analyse de code C. Il est toutefois toujours nécessaire de sortir du logiciel pour compiler le programme analysé. On perd ainsi les analyses effectuées par l’outil. LLVM est une infrastructure permettant de nombreuses optimisations et l’interprétation des programmes LLVM IR. Il est de plus possible d’indiquer des propriétés sur certaines instructions LLVM IR ; qui seront propagées jusqu’au processeur. L’article présente un greffon de compilation des programmes analysés par Frama-C vers LLVM. En prenant en compte différents résultats d’analyses pour permettre l’optimisation et l’instrumentation du programme binaire. Il est aussi présenté, comment sans connaissance de Frama-C ni de LLVM, le langage OCaml peut permettre la réalisation d’un tel plugin en un temps remarquable.
%% %%block __12:05__ »__Richard Genestier:__ Deductive verification of exhaustive generators with Frama-C and WP » [[abstract]
A structured array is an array satisfying given constraints, such as being sorted or having no duplicate values. Generation of all arrays with a given structure up to some given size has many applications, including bounded exhaustive testing. We use the C specification language ACSL to formally specify sequential generators of structured arrays by two C functions: the first one computes an initial array, and the second one steps from one array to the next one according to some total order on the set of arrays. We refine this specification into two programming and specification patterns. The first pattern formalizes the principle of generation in lexicographic order by suffix revision. The second pattern describes generation by filtering the output of an existing generator. We present a library of generators instantiating these patterns. We formalize and automatically prove two properties of these generators with the Frama-C platform. The soundness property states that both functions generate arrays satisfying the prescribed constraints. The progress property states that the second function generates arrays in increasing lexicographic order. It entails the termination of the generator. The general patterns and the verification of their properties facilitate the design and verification of the generation functions.
%% !Pause déjeuner __12:30__ (Bâtiment P, salle des thèses) [Map | https://www.google.com/maps/d/edit?mid=zp2PeCQcQAnU.k8VW3QkDP1AY&usp=sharing] !Session »Sécurité et protocoles cryptographiques » %%block __14:00__ »__Steve Kremer__: Verification of cryptographic protocols : from authentication to privacy » [[abstract]
Formal, symbolic techniques for modelling and automatically analyzing security protocols are extremely successful and were able to discover many security flaws. Initially, these techniques were mainly developed to analyze authentication and confidentiality properties. Both these properties are trace properties and efficient tools for their verification exist. In more recent years anonymity-like properties have received increasing interest. Many flavors of anonymity properties are naturally expressed in terms of indistinguishability and modeled as an observational equivalence in process calculi. However, only very few verification tools are currently able to automate the analysis of such indistinguishability properties. In this talk I will describe the techniques behind the aKiss protocol analyzer and illustrate its usefulness on examples from electronic voting.
%% %%block __15:00__ »__Antoine Delignat-Lavaud__: Closing the gap between verified cryptographic protocols and secure websites » [[abstract]
Formal security analysis of cryptographic protocols is a mature research topic backed up by powerful and efficient tools. Yet, it has a relatively poor track record of preventing major concrete attacks, which often abuse implementation problems and unmodeled features or attacker capabilities (however, it has been able to predict that some of these attacks would appear). In contrast, the type-based verification method of Fournet, Bhargavan et al., which relies on modeling protocols through dependent type annotations on a precise reference implementation, has enabled the discovery of several practical high-profile attacks against TLS, the most popular cryptographic protocol on the Web. In this talk, I will summarize the main results (both positive and negative) derived from this effort, as well as its impact on F*, the new state-of-the-art verification-oriented language with refinement types, effects, and SMT automation that miTLS is currently being ported to.
%% __15:30__ Pause café %%block __16:00__ »__Rémy Chrétien:__ Decidability of trace equivalence for protocols with nonces » [[abstract]
Privacy properties such as anonymity, unlinkability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.