plt formal methods resources Télécharger - plt formal methods resources Téléchargement du code source

plt formal methods resources

Autre code source

1.0.0

Télécharger

Théorie du langage de programmation et méthodes formelles - Ressources

Image Courtsey : Groupe Forsyte

Les méthodes formelles sont des techniques mathématiques utilisées pour la conception, la vérification et la spécification de problèmes logiciels et matériels. Il s’agit essentiellement d’un sous-ensemble de la recherche sur la théorie du langage de programmation qui est utilisé pour étudier des problèmes informatiques complexes.

L'analyse par méthodes formelles implique essentiellement ces étapes :

Formal Specification
Formal Proofs
Model Checking
Abstraction

Le développement formel de la preuve et la vérification du modèle sont principalement effectués à l'aide de prouveurs de théorèmes interactifs, souvent appelés assistants de preuve. L'abstraction crée des relations structurellement solides entre les parties des modèles.

Voici ma tentative de dresser une liste de matériels de lecture, de vidéos et d'outils utiles accompagnés de quelques défis à venir dans le domaine.

NOTE :

J'ai essayé de rendre le contenu plus axé sur la recherche actuelle et les applications industrielles. Les personnes recherchant une collection purement académique doivent se référer aux méthodes formelles en éducation - Jeremy Avigad.
Le lecteur doit avoir des connaissances de base en théorie des types . Un aperçu plus académique peut être trouvé ici learn-tt.

Contenu

Livres et conférences
Blogues
MOOC
Outils
Projets
Défis à venir
- Lié à la sécurité
  - Sécurité des logiciels
  - Confidentialité différentielle
  - Applications dans la sécurité de la chaîne de blocs
  - Les défis liés à la sécurisation de l’IA
  - Créer des systèmes cyberphysiques sécurisés
- Interprétation abstraite axée sur
- Recherche sur les langages de programmation
  - Programmation probabiliste
  - Développement d'un langage de programmation quantique
  - Raffinement du langage à l'aide de méthodes formelles
Industries et startups connexes

Livres et conférences

Fondements logiciels : je le conseille vivement comme matériau de départ pour approfondir ce domaine. Le livre est très utile pour construire des concepts de base et constitue une très bonne introduction au domaine. Des concepts magnifiquement illustrés avec des exemples de pratique sont fournis tout au long, ce qui rend l'apprentissage amusant et interactif.
FRAP - Adam Chlipala : Un livre qui vous aide à comprendre et à raisonner l'exactitude formelle des programmes. Des exemples de structures de données et d'algorithmes inspirés du langage impératif ( C ) aident énormément à commencer à réfléchir à leur vérification formelle.
Programmation certifiée avec types dépendants - Adam Chlipala : L'un des meilleurs theoretical books pour apprendre la preuve de théorèmes à l'aide de coq.
Vérification formelle - Jacques Fleuriot : Il s'agit d'un cours qui implique la démonstration de théorèmes à l'aide d'outils plus développés comme les solveurs SAT et SMT.
Interprétation abstraite - Patrick Cousot Le meilleur matériel disponible sur la théorie de l'interprétation abstraite. Il donne une analyse mathématique complète et pure des mutations du programme. Le comportement du programme en tant que relation en constante modification entre différentes structures mathématiques abstraites est expliqué et prouvé !!.
Logique et preuve - Introduction à la CMU et au Lean : Ce cours est conçu à la CMU et sert également de matériel d'introduction à la démonstration de théorèmes en Lean.

Si vous pensez avoir besoin d'informations plus théoriques, veuillez vous référer à la note ci-dessus.

Blogues

Premiers pas avec les méthodes formelles
K Framework et efforts de vérification formelle dans Blockchain
Pact Formal Verification for Blockchain smart contracts : Super court blog expliquant la méthodologie du Pact FV avec une petite introduction à la vérification formelle par les premiers principes.
Vers une IA robuste et vérifiée : tests de spécifications, formation robuste et vérification formelle - DeepMind
Le défi de la vérification et des tests du machine learning - Ian GoodFellow & Nicolas Papernot

MOOC

Vérification formelle du logiciel - edX
Vérification quantitative de modèles - Coursera
Cyber Physical Systems : Cours de l'UC Berkeley, axé sur l'utilisation de méthodes de vérification pour la modélisation des systèmes Cyper Physical (CPS).
Langages de programmation - Coursera

Outils

Assistants de preuve

coq : Le prouveur de théorème le plus populaire et le plus utilisé. Il prend en charge de nombreuses fonctionnalités, notamment l'extraction ML, l'empaquetage de projets (création de projets et de Makefile). Il existe de nombreux documents how-to disponibles qui utilisent coq pour la formalisation. Tout le monde pourrait trouver ces 100 théorèmes en Coq très intéressants.
lean : un prouveur de théorèmes assez nouveau par Microsoft Research . A un joli didacticiel interactif, il est facile de démarrer.
Vérificateur de modèle PRISM : Il s'agit d'un vérificateur de modèle développé par l'Université d'Oxford.
Nuprl : Prouveur de théorèmes par Cornell dans le cadre du projet Proof Refinement Logic.
Agda : un assistant de preuve assez mature. Possède des fonctionnalités similaires à Coq. facile à apprendre après une certaine expérience en coq.
Isabelle : C'est un vieux théorème démontrant. A une bonne implémentation de la logique de base mais manque d'autres fonctionnalités liées à l'UX.
VCC : Un vérificateur mécanique pour les programmes C simultanés de Microsoft.
TLA+ : Langage de haut niveau pour la modélisation de langages et de systèmes (notamment concurrents et distribués).

Solveurs SAT/SMT/SMC

Solveurs SAT :

MiniSat.

Solveurs SMT :

Z3
CVC4
MathSAT5
SMTInterpol
Princesse

Solveurs SMC :

Publication

Solveurs hybrides

Les assistants de preuve ont des implémentations très solides de la logique du programme. Parfois, il peut ne pas être tactiquement possible de réaliser des preuves complexes uniquement en les utilisant. Par conséquent, les recherches actuelles combinent ce principe de raisonnement logique fort avec de puissants solveurs SMT et SMC pour faciliter le développement de la preuve. Quelques exemples sont ci-dessous :

Fstar(F*)
- Il est possible d'extraire du code F* vers C en utilisant KreMLin.
SMTCoq

Projets

La plupart des projets concernent plus ou moins le développement des prouveurs de théorèmes ou des solveurs SAT/SMT/SMC/ et peuvent donc être consultés ici. Ce sont quelques-uns des autres projets activement développés.

DeepSpec est un projet parapluie qui se concentre sur la création de systèmes logiciels vérifiés. Les principaux sous-projets suivants sont activement travaillés :
- Compcert
- LLVM vérifié (VeLLVM)
- Chaîne d'outils logiciels vérifiés (VST)
ikos est un compilateur C fiable et sans bug basé sur la théorie de l'interprétation abstraite.
Projet Everest : Il s'agit d'un projet de recherche qui vise à créer un écosystème HTTPS sécurisé et vérifié.
CertiCrypt : Il s'agit d'un projet axé sur la modélisation de la cryptographie à clé publique à l'aide de l'assistant de preuve coq.
Iris : Iris est un cadre logique de séparation simultanée d'ordre supérieur implémenté et vérifié dans l'assistant de preuve Coq.
VeriDeep - Vérification de la sécurité des réseaux de neurones profonds
VeHICal : Projet axé sur le développement des bases d'une co-conception vérifiée d'interfaces et de contrôle pour les systèmes cyber-physiques humains.
FastSMT - Outil pour augmenter votre solveur SMT en apprenant à optimiser ses performances pour votre ensemble de données de formules. Il est développé par le laboratoire SRI de l'ETH Zurich et construit sur le solveur Z3 SMT.
fm4cps - Méthodes formelles pour les systèmes cyber-physiques, efforts conjoints de l'INRIA et de l'ECNU Shanghai.

Défis à venir

Lié à la sécurité

Sécurité des logiciels
- Lectures
  - Méthodes formelles de sécurité, atelier NSF
  - Relation symbolique entre les méthodes formelles et la sécurité
  - Documents de recherche du Projet Everest
  - Méthodes formelles en sécurité logicielle
  - Méthodes formelles pour des systèmes informatiques sûrs et sécurisés
  - La solidité informatique du chiffrement formel
  - Structures de sécurité utilisant des méthodes formelles
  - Vérification de la primitive cryptographique
  - Certification formelle des preuves cryptographiques basées sur le jeu
  - Certification formelle des preuves cryptographiques basées sur du code
- Vidéos
  - Spécification approfondie pour Dropbox
  - DSL pour les calculs multipartites sécurisés vérifiés en F*
  - Utiliser des méthodes formelles pour le développement de systèmes hautement sécurisés
  - Sécurité grâce à des méthodes formelles et une architecture sécurisée (CERIAS - Purdue University)
  - Techniques basées sur le langage pour la cryptographie et la confidentialité
Confidentialité différentielle
- Lectures
  - Vérification formelle de la confidentialité différentielle pour les systèmes interactifs
  - Méthodes formelles de confidentialité
  - LightDP - Vers l'automatisation des preuves de confidentialité différentielles
  - EasyCrypt - Confidentialité différentielle informatique vérifiée avec applications pour compteur intelligent
  - Prouver la confidentialité différentielle dans Hoare Logic
  - Programmation bayésienne différentiellement privée
  - Couplage probabiliste avancé pour une confidentialité différentielle
- Vidéos
  - Méthodes formelles et preuves des propriétés de confidentialité - 1
  - Méthodes formelles et preuves des propriétés de confidentialité - 2
  - Méthodes formelles et preuves des propriétés de confidentialité - 3
  - Prouver la confidentialité différentielle à l'aide de types relationnels
Applications dans la sécurité de la chaîne de blocs
Méthodes formelles pour les chaînes de blocs : Il s'agit du tout premier atelier axé sur l'utilisation de méthodes formelles dans la technologie Block Chain. Ce sera le 11 octobre 2019 .
CertiK : Il s'agit d'une startup axée sur l'utilisation de méthodes formelles pour rendre les blockchains sécurisées de manière vérifiable.
- Lectures
  - Comment l'analyse et la vérification formelles ajoutent de la sécurité aux systèmes basés sur la blockchain - Tutoriel @ MIT
  - Contrats intelligents et opportunités pour les méthodes formelles
  - K Framework et efforts de vérification formelle dans Blockchain, une collection impressionnante de documents explicatifs sur le framework K et son application dans la vérification des systèmes Blockchain.
  - Pact Formal Verification for Blockchain smart contracts : Super court blog expliquant la méthodologie du Pact FV avec une petite introduction à la vérification formelle par les premiers principes.
  - Blockchains temporels - une analyse formelle
  - Validation des contrats intelligents décentralisés grâce à la théorie des jeux et aux méthodes formelles
- Vidéos
  - Conception formelle, mise en œuvre et vérification des langages BlockChain
  - CertiK - Plateforme de vérification formelle des contrats intelligents (revue)
  - Simplicité - Un nouveau langage pour les blockchains
Les défis liés à la sécurisation de l’IA
FLoC 2018 - Le sommet de l'apprentissage automatique rencontre les méthodes formelles
Verified Machine Learning - Radboud University Nijmegen : Cours universitaire sur l'utilisation des méthodes de vérification en Machine Learning.
Les méthodes formelles rencontrent l'apprentissage automatique - RWTH Aachen University : séminaire 2018 sur les progrès de l'apprentissage automatique vérifiablement sécurisé à l'aide de méthodes formelles.
- Lectures
  - Vers une intelligence artificielle vérifiée - S. Seshia
  - Vers une IA robuste et vérifiée : tests de spécifications, formation robuste et vérification formelle - DeepMind
  - Développer des systèmes d'apprentissage automatique sans bogues avec des mathématiques formelles
  - Mélange de méthodes formelles, d'apprentissage automatique et d'interaction homme-machine
  - Apprentissage automatique dans les méthodes formelles
  - Apprentissage automatique et méthodes formelles
  - Algorithmes de vérification des réseaux de neurones profonds
  - Vérification de la sécurité des réseaux de neurones profonds
  - Le défi de la vérification et des tests du machine learning - Ian GoodFellow & Nicolas Papernot
  - Vérification des propriétés des réseaux de neurones profonds binarisés
  - Reluplex : un solveur SMT efficace pour vérifier les réseaux de neurones profonds
  - Vérification des réseaux à action directe linéaire par morceaux
  - Défis liés à la vérification des algorithmes d'apprentissage par renforcement
  - Application de méthodes formelles à l'apprentissage par renforcement - Galois Inc.
  - Vers prouver la robustesse contradictoire des réseaux de neurones profonds
- Vidéos
  - Vérification de la sécurité des réseaux de neurones profonds -ICST 2018
  - Vérification de la sécurité des réseaux de neurones profonds - Marta Kwiatkowska - CAV 2017
  - Vérification de sécurité des réseaux de neurones profonds -INRIA
  - Règles de vérification du Machine Learning, des bugs basés sur les données à l'IA explicable
  - Vérification des programmes d'apprentissage automatique
  - Reluplex : un solveur SMT efficace pour vérifier les réseaux de neurones profonds - Vidéo de conférence
  - Développer des modèles d'apprentissage automatique sans bug à l'aide de Certigrad - Daniel Selsam
Créez des systèmes cyberphysiques sécurisés
VeHICal : Projet axé sur le développement des bases d'une co-conception vérifiée d'interfaces et de contrôle pour les systèmes cyber-physiques humains.
fm4cps - Méthodes formelles pour les systèmes cyber-physiques, efforts conjoints de l'INRIA et de l'ECNU Shanghai.
- Lectures
  - Conception de systèmes cyber-physiques : fondements formels, méthodes et chaînes d'outils intégrées
  - Nouvelles frontières dans les méthodes formelles : apprentissage, systèmes cyber-physiques, éducation et au-delà
  - Vérification de modèles statistiques pour les systèmes cyber-physiques
  - Vérification formelle des systèmes cyberphysiques de transport
  - Vérification des systèmes cyber-physiques
  - Vérification et validation dans les systèmes cyberphysiques : défis de recherche et voie à suivre
  - Détection d'anomalies dans les systèmes cyber-physiques : une approche de méthodes formelles
  - Vérification de la composition des systèmes cyber-physiques auto-adaptatifs
- Vidéos
  - Une charte de méthodes formelles pour les systèmes cyber-physiques et l'Internet industriel des objets
  - Vérification formelle des systèmes cyberphysiques
  - Surveillance des systèmes cyberphysiques

Interprétation abstraite axée sur

Certification de robustesse rapide et efficace : projet DeepZ - pour certifier la robustesse des réseaux neuronaux basée sur une interprétation abstraite.
AI2 : Certification de sécurité et de robustesse des réseaux de neurones avec interprétation abstraite
Renforcer la certification de robustesse des réseaux de neurones : utilise l'interprétation abstraite dans sa méthodologie.

Recherche sur les langages de programmation

Programmation probabiliste
- Lectures
  - Une introduction à la programmation probabiliste
  - Vérification formelle des programmes probabilistes d'ordre supérieur
  - Programmation logique probabiliste et réseaux bayésiens
  - Fonctions probabilistes et oracles cryptographiques dans la logique d'ordre supérieur - Andreas Lochbihler
  - Vérification relationnelle probabiliste des implémentations cryptographiques
  - Les preuves de couplage sont des programmes de produits probabilistes
  - Couplage probabiliste avancé pour une confidentialité différentielle
  - Méthodes formelles pour la programmation probabiliste
  - Méthodes formelles pour les programmes probabilistes : diapositives du cours
  - Programmation probabiliste - Véritable défi de vérification
  - FairSquare : Vérification probabiliste de l'équité du programme
  - VPHL : une logique de correction partielle vérifiée pour les programmes probabilistes
  - Unifier la logique et la probabilité
- Vidéos
  - Vérification formelle des programmes probabilistes d'ordre supérieur - Vidéo de la conférence POPL 2019
  - Programmation logique probabiliste et ses applications - Luc De Raedt, Louvain
Développement d'un langage de programmation quantique
- Lectures
  - Qwire : Vérification formelle des programmes quantiques en Coq
  - Une logique pour la vérification formelle des programmes quantiques
  - Techniques de couplage pour raisonner sur les programmes quantiques
  - Vérification formelle vs incertitude quantique
  - Vérification de modèles de protocoles quantiques récursifs
- Vidéos
  - Informatique quantique adaptée aux missions pour la vérification et la validation de logiciels (VV) - CMU
  - Dominique Unruh : Vérification formelle de la cryptographie quantique
Raffinement des langages à l’aide de méthodes formelles

Il s'agit notamment de l'amélioration de certaines propriétés (comme le parallélisme et la concurrence) des langages de programmation existants. Beaucoup de choses peuvent être facilement recherchées à ce sujet, car après tout, c'est la seule raison la plus importante d'étudier la théorie PL. Toutes les conférences répertoriées ici ACM SIGPLAN contiennent la majorité des articles de recherche sur le développement de langages de programmation, consultez-les.