Logiciels
Les logiciels suivants sont publiés par le LSV.
- Csur
- Csur est un projet d'analyse automatique de programmes C implantant des protocoles cryptographiques,
fondé sur une nouvelle technique hybride pour l'analyse de code C, où les programmes représentent des rôles d'agents de
protocoles. Des propriétés de confidentialité peuvent être analysés
par Csur dans le modèle de Dolev-Yao; des erreurs d'implantation
peuvent aussi être détectées avec nos techniques.
- Cosmos
- Cosmos est un model checker statistique.
Il a pour formalisme d'entrée les réseaux de Petri stochastiques
et évalue des formules de la logique quantitative HASL.
Cette logique, basée sur les automates hybrides linéaires,
permet de décrire des indices de
performance complexes relatifs aux chemins d'exécution acceptés
par l'automate. HASL fournit ainsi un moyen d'unifier l'évaluation
de performance et la vérification dans un cadre très général.
- evatrans v.2
- evatrans est la seconde version d'un environnement
développé dans le cadre du projet RNTL EVA
pour l'analyse syntaxique, la vérification de types et la compilation
de protocoles de sécurité spécifiés dans un langage abstrait ad-hoc vers
des formats pouvant être pris en compte par différents outils vérification.
- FAST
- FAST est un model-checker pour systèmes infinis modelisés
par des automates à compteurs. Grâce à des méthodes symboliques et des
techniques d'accélération, FAST vérifie automatiquement
des propriétés de sûreté en calculant l'ensemble des états accessibles.
- H1
- Une bibliothèque d'automates d'arbres finis, de contraintes ensemblistes, de démonstration automatique pour la classe
décidable H1. Ecrit principalement en
HimML.
- ISpi
- Outil de vérification de protocoles cryptographiques (version préliminaire),
développé dans le cadre du projet RNTL Prouvé.
Documentation provisoire.
- Net-Entropy
- Un vérificateur d'entropie de connections réseaux chiffrés. Cet outil
permet de détecter les attaques pouvant être effectués sur les
programmes implémentant les couches de sécurité(SSH, SSL, VPN, ...).
- ORCHIDS
- ORCHIDS est un logiciel de détection d'intrusions temps
réel, multi-événements, multi-sources,
fondé sur une approche efficace de model-checking de logique temporelle
(en cours de développement).
- Securify
-
Securify est un outil de vérification automatique pour les protocoles
cryptographiques. Il est dédié à la preuve de propriété de secret pour un
nombre non borné de sessions et de participants.
- IMITATOR
- IMITATOR est une implémentation de l'algorithme de méthode inverse appliquée aux automates temporisés.
Il généralise le comportement des automates temporisés parametré en synthétisant une contrainte sur les paramètres.
- Heap-Hop
-
Heap-Hop est un outil de vérification automatique pour les programmes
concurrents manipulant la mémoire, et qui utilisent des moniteurs de
Hoare et des échanges de messages pour se synchroniser. Plus
précisément, les programmes sont annotés à l'aide de pré et
post-conditions, et d'invariants de boucles, écrits dans un fragment
de la logique de séparation ; les communications sont régies par des
contrats, une forme de session types. Heap-Hop prouve alors
l'absence de fautes mémoires, de races et, grâce aux contrats,
l'absence de fuites mémoire ainsi que certaines conditions de progrès.
- Cunf
-
L'outil Cunf est capable de construire le dépliage d'un réseau de Petri
contextuel.
- PRALINE
-
PRALINE est un outil pour le calcul des Equilibres de Nash dans les jeux
concurrents.
- Shrinktech
-
Shrinktech est un outil de vérification de robustesse pour les automates
temporisés.
- QuantiS
-
QuantiS est un outil pour évaluer des spécifications quantitatives.