Journée “vérification formelle de systèmes distribués”

20th November 2019

Journée du GT AFSEC du GDR GPL

Vérification formelle de systèmes distribués

Quand: Le 11 décembre 2019
Lieu: ENSEEIHT, Toulouse (salle F-501)
2 rue Charles Camichel, Toulouse
Métro ligne B station François Verdier ou ligne A station Jean Jaurès
L’inscription (gratuite) est nécessaire pour la bonne organisation de l’événement (envoi d’un email à ; objet : “Inscription AFSEC 11 décembre”) (cliquer sur le lien) – préciser : Nom et Affiliation.

Programme :

  • 10h – 10h30 accueil, café
  • 10h30 – 11h15 Stephan Merz, LORIA
    Formal Techniques for the Verification and Synthesis of Security Chains
    • We describe work on the formal verification (using SMT solving and symbolic model checking) and on the synthesis of chains of networking functions intended to limit the ability of mobile applications to carry out attacks on servers and networking infrastructure. In order to generate a security chain dedicated to a particular application, represent its networking activity as a Markov chain, based on network flows captured on-device. Rules expressed as Horn clauses that take into account the structure of the Markov chain and thresholds provided by network operators classify the network activity according to different types of attacks and infer predicates representing network rules. Chains for individual applications are merged and then optimized for deployment in a given infrastructure. The security chains are expressed in Pyretic, a domain-specific language for programming software-defined networks and can be deployed in a cloud infrastructure. Preliminary experiments in a network simulator indicate that the proposed approach for synthesizing and deploying security chains appears feasible, although the precision of detecting attacks remains to be improved for some types of applications.
  • 11h15 – 12h Philippe Queinnec, IRIT
    Tasks in Modular Proofs of Concurrent Algorithms
    • Proving correctness of distributed or concurrent algorithms is a mind-challenging and complex process. Slight errors in the reasoning are difficult to find, calling for computer-checked proof systems. In order to build computer-checked proofs with usual tools, such as Coq or TLA+, having sequential specifications of all base objects that are used as building blocks in a given algorithm is a requisite to provide a modular proof built by composition. Alas, many concurrent objects do not have a sequential specification. This article describes a systematic method to transform any task, a specification method that captures concurrent one-shot distributed problems, into a sequential specification involving two calls, Set and Get. This transformation allows system designers to compose proofs, thus providing a framework for modular computer-checked proofs of algorithms designed using tasks and sequential objects as building blocks. The Moir & Anderson implementation of renaming using splitters is an iconic example of such algorithms designed by composition.
  • 12h – 14h déjeuner – buffet
  • 14h – 14h45 Robin Pelle, LRI
    Mouvement Asynchrone, Continus vs. Discrets: une approche certifié pour les robots mobiles
    • Oblivious Mobile Robots have been studied both in continuous Euclidean spaces, and discrete spaces (that is, graphs). However the obtained literature forms distinct sets of results for the two settings. In this paper, we explore the possibility of transforming results obtained in one model into results for the other one. Our approach focuses on certified results using the COQ proof assistant.
  • 14h45 – 15h30 Julien Brunel, ONERA
    Vérification formelle du protocole distribué Chord
    • Chord is a protocol that provides a scalable distributed hash table over an underlying peer-to-peer network. Since it combines data structures, asynchronous communications, concurrency, and fault tolerance, it features rich structural and temporal properties that make it an interesting target for formal specification and verification. Previous work has mainly focused on (semi-)automatic proofs of safety properties, instead of studying the full correctness of the protocol (a liveness property). We report here on an automated verification of the correctness property using our model checker Electrum, and on the first mechanized (and partly manual) proof of the same property.
  • 15h30 – 16h15 Quentin Peyras, ONERA
    Un fragment expressif et décidable de la logique temporelle du premier-ordre FO-LTL
    • First-Order Linear Temporal Logic (FOLTL) is well-suited to specify infinite-state systems, and distributed systems in particular. However, FOLTL satisfiability is not even semi-decidable, thus preventing automated verification. To address this, a possible track is to constrain specifications to a decidable fragment of FOLTL, but known fragments are too restricted to be usable in practice. In this paper, we exhibit various fragments of increasing scope that provide a pertinent basis for abstract specification of infinite-state systems. We show that these fragments enjoy the Bounded Domain Property (any satisfiable FOLTL formula has a model with a finite, bounded FO domain), which provides a basis for complete, automated verification by reduction to LTL satisfiability. Finally, we present a toy distributed system illustrating the applicability and limitations of our results.

Leave a Reply

You must be logged in to post a comment.