Avec le soutien
du 
et de
l'
.
Avec le soutien
du et de
l'.
Cette page sera mise à jour régulièrement, n'hésitez pas à y revenir.
Inscription avant le 19 novembre 2018
Cette journée est co-localisée avec la journée MTV2 (Méthodes de test pour la validation et la vérification), qui aura lieu le 7 décembre au même endroit.
Deux exposés invités seront présentés (résumés ci-dessous) :
Les thèmes du groupe de travail LTP (Langages, Types et Preuves) du GdR GPL du CNRS sont :
L'inscription à la journée est gratuite mais nécessaire pour assurer le bon déroulement de l'événement.
La journée, y compris le repas du midi, est financée par le GdR GPL du CNRS. Une subvention est également fournie par l'ENSIIE.
L'ENSIIE est facilement accessible depuis Paris Gare de Lyon ou Châtelet-Les halles via le RER D (gare d'Évry-Courcouronnes). Attention ne pas prendre les trains s'arrêtant à Évry Val de Seine, bien prendre ceux qui s'arrêtent à Évry-Courcouronnes.
La journée aura lieu dans une salle du C-19, le cluster Jeux vidéos de l'ENSIIE. L'accès se fera par le 19 cours Blaise Pascal (sortie RER Cours Blaise Pascal). (Un accès par l'entrée principale de l'ENSIIE sera toutefois également possible.)
Plus d'informations sur le site de l'ENSIIE.
Hôtels à proximité de l'ENSIIE (non testés, cette liste ne doit pas être considérée comme un soutien) :
Embedding Impure ML Oracles into Coq Verified Code, Illustrated on SatAns-Cert, a Coq-Verified (Boolean) SAT-Solver.
Oracles are a key ingredient in the success of CompCert (an industrial C-Compiler which is formally verified in Coq). Such an oracle is an untrusted foreign code (written in OCaml) producing outputs that are checked by Coq-verified code. However, in CompCert, oracles are currently invoked through an unsafe FFI (Foreign Function Interface) of Coq. I will detail some pitfalls of this FFI and propose how to overcome them. Moreover, I conjecture that by using an adequate FFI, we can derive "theorems for free" a la Wadler in Coq from the ML type of imperative polymorphic oracles. This discharges a part of the proof effort on the OCaml typechecker. I will illustrate this idea on a few examples, including "SatAnsCert", a verified checker of boolean SAT-solvers.
Calcul et langages de programmation quantique
Dans cet exposé, je présenterai le calcul quantique, ses promesses, et l'état de l'art sur le front des langages de programmation quantique.
Le programme suivant est préliminaire, il est encore susceptible d'être modifié.
| 9h15-10h | Accueil, café |
| 10h00-11h15 | Session 1 (3x25min, 20 min exposé + 5 min questions) |
| Gabriel RADANNE, University of Freiburg. Kindly Bent to Free Us: Linear types for ML | |
| Virgile ROBLES, CEA List, Laboratoire Sûreté et Sécurité des Logiciels. MetAcsl: Specification and Verification of High-Level Properties | |
| Amélie LEDEIN, ENSIIE/Samovar. FaCiLe en Coq | |
| 11h15-11h40 | Pause café |
| 11h40-12h40 | Session 2 (conférencier invité) |
| Sylvain BOULMÉ (Laboratoire Verimag, Grenoble-INP) : Embedding Impure ML Oracles into Coq Verified Code | |
| 12h40-14h00 | Déjeuner |
| 14h00-14h50 | Session 3 (2x25min, 20 min exposé + 5 min questions) |
| Florian FAISSOLE, LRI / VALS, A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers | |
| Nicolas MAGAUD, ICUBE/IGG. Preuves sur des modèles finis de la géométrie projective | |
| 14h50-15h50 | Session 4 (conférencier invité) |
| Benoît VALIRON (LRI/Modhel, Paris Saclay) : Calcul et langages de programmation quantique | |
| 15h50-16h10 | Pause café |
| 16h10-17h00 | Session 5 (2x25min, 20 min exposé + 5 min questions) |
| Olivier LEVILLAIN, Télécom SudParis. Parsifal: une solution pour écrire rapidement des parsers binaires robustes et efficaces | |
| Dara LY, CEA List, Laboratoire Sûreté et Sécurité des Logiciels. Soundness of a Dataflow Analysis for Memory Monitoring | |
| 17h00-17h10 | Annonces, fin de journée |
Les inscriptions pour proposer un exposé sont closes, mais il reste encore des places pour assister aux exposés.
Envoyez votre inscription par e-mail à renaud.rioboo@ensiie.fr et guillaume.burel@ensiie.fr (cliquez ici, ou recopiez le bulletin ci-dessous).
===================================
Nom :
Prénom :
Laboratoire/équipe :
[N] je souhaite présenter des travaux.
Titre et format de la présentation :
Résumé (optionnel, à transmettre avant le 5/12) :
[] j'accepte que mes nom, prénom, équipe et éventuel titre de présentation
apparaissent sur la page web de la journée, dès mon inscription.
[] je participerai au repas du midi.
Pour le déjeuner, mes contraintes sont (végétarien, sans sel, ...) :
[] je participerai également à la journée MTV2 le lendemain.
(pour information uniquement, l'inscription devra se faire des deux
côtés.)
====================================
Oracles are a key ingredient in the success of CompCert (an industrial C-Compiler which is formally verified in Coq). Such an oracle is an untrusted foreign code (written in OCaml) producing outputs that are checked by Coq-verified code. However, in CompCert, oracles are currently invoked through an unsafe FFI (Foreign Function Interface) of Coq. I will detail some pitfalls of this FFI and propose how to overcome them. Moreover, I conjecture that by using an adequate FFI, we can derive "theorems for free" a la Wadler in Coq from the ML type of imperative polymorphic oracles. This discharges a part of the proof effort on the OCaml typechecker. I will illustrate this idea on a few examples, including "SatAnsCert", a verified checker of boolean SAT-solvers.
A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers
Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when computations are done in radix 10. This is in particular the case for the computation of the average of two floating-point numbers. Several radix-2 algorithms are available, including one that provides the correct rounding, but none hold in radix 10. This paper presents a new radix-10 algorithm that computes the correctly-rounded average. To guarantee a higher level of confidence, we also provide a Coq formal proof of our theorems, that takes gradual underflow into account. Note that our formal proof was generalized to ensure this algorithm is correct when computations are done with any even radix.
La programmation par contraintes a pour objectif de résoudre des problèmes hautement combinatoires qui peuvent se modéliser sous la forme de la donnée d'un ensemble de variables ou d'inconnues munies chacune d'un domaine (c'est-à-dire l'ensemble des valeurs possibles) et d'un ensemble de contraintes sur ces variables. Différentes techniques de résolution de ces problèmes de satisfaction de contraintes ont été proposées et implantées dans des solveurs, Choco par exemple ou des bibliothèques spécialisées, la bibliothèque OCaml FaCiLe (Barnier, Brisset, 1997) par exemple. L'idée principale sous-jacente aux algorithmes de résolution est d'éliminer des domaines des variables, les valeurs qui ne peuvent figurer dans une solution du problème. La représentation d'un domaine peut différer d'un solveur à l'autre : listes d'intervalles, listes de "trous", ensembles, "bitvectors", etc. La bibliothèque FaCiLe, ainsi que de nombreux autres solveurs, implantent un domaine comme une liste d'intervalles. Nous avons traduit et vérifié formellement en Coq une grande partie du module de FaCiLe qui implante le type des domaines. Dans ce travail, l'effort s'est porté non seulement sur la preuve mais surtout sur la spécification des fonctions de ce module.
Notre objectif à plus long terme est d'utiliser le module Coq correspondant dans le solveur de contraintes développé en Coq par Carlier et al, afin d'obtenir de meilleures performances. Ce travail participe à l'effort de vérifier en Coq les bibliothèques OCaml existantes
Parsifal: une solution pour écrire rapidement des parsers binaires robustes et efficaces
L'implémentation de protocoles réseau passe par une étape souvent négligée : le parsing (ou dissection) des messages. Cette étape, qui consiste à interpréter une structure plus ou moins complexe à partir d'une chaîne d'octets, est également essentielle dans le traitement de fichiers. De nombreuses failles sont régulièrement mises au jour dans le code responsable de cette étape.
Pour répondre à ce problème de manière efficace et robuste, j'avais écrit il y a quelques années Parsifal, un langage dédié à la description des formats binaires, permettant la génération du plus gros du code lié aux parsers. Parsifal s'est montré efficace pour traiter des protocoles réseau (TLS, DNS, BGP, etc.) mais aussi des formats de fichiers (X.509, UEFI, OpenPGP, etc.).
Malgré ses bons et loyaux services, Parsifal mériterait une mise à jour. Tout d'abord, les outils utilisés pour la génération de code (le préprocesseur camlp4) ne sont peut-être plus les plus adaptés. Ensuite, le langage lui-même gagnerait à être nettoyé et rendu plus expressif. Enfin, il serait intéressant, au-delà des messages échangés, de décrire, au moins partiellement, les automates des protocoles réseau d'une manière similaire.
Ma présentation traitera donc du parsing, de la solution apportée par Parsifal, et des objectifs à court et moyen termes autour de l'outil.
Soundness of a Dataflow Analysis for Memory Monitoring
An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g. their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.
Preuves sur des modèles finis de la géométrie projective
We formalize two ‘small' finite projective spaces pg(3,2) and pg(3,3) using the Coq proof assistant. We reuse a formal description of pg(3,3) provided by Alan Prince in the late nineties. We found that the formal description of the projective spaces pg(3,3) is incorrect and fixed it in order to be able to complete the proofs. These proofs are huge (they feature several millions of cases). We exploit some symmetry arguments as well as some smart proof techniques to make proof search and verification faster and thus tracktable using the Coq proof assistant.
Kindly Bent to Free Us: Linear types for ML
Several integrations of linear types into functional programming languages have been proposed with very different approaches, ranging from direct adaptation of linear logic to ownership-based approaches. Unfortunately, such proposals often do not mesh well with features from the ML family of programming languages such as strictness, complete type inference and module-based type abstraction.
We present a work-in-progress extension of ML with affine types. This extension aims to be a simple conservative extension of ML that can be retro-fitted on top of an existing language. It supports principal type inference, ML-style type abstraction, and does not require any linearity annotations inside terms. This extension makes use of a novel combination of qualified types and subkinding to track the linearity of variables in types.
MetAcsl: Specification and Verification of High-Level Properties
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its specified contract. However, not all high-level (e.g. security-related) properties of a software module can be easily expressed through function contracts. To address this issue, this tool demo paper proposes a new specification mechanism, called meta-properties, able to express a rich set of high-level properties. A meta-property can be seen as an enhanced global invariant specified for all or a subset of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can then be proved by deductive verification tools in a usual way. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove several safety- and security-related meta-properties in two illustrative case studies.
Calcul et langages de programmation quantique
Dans cet exposé, je présenterai le calcul quantique, ses promesses, et l'état de l'art sur le front des langages de programmation quantique.