Messages étiquettés Méthode formelle

Soutenance de thèse

Génération de tests de vulnérabilité appliquée à la vérification de code intermédiaire Java Card

 

Bonjour, j’ai le plaisir de vous informer que ma soutenance de thèse aura lieu le jeudi 30 juin. La présentation est publique. En France, elle auras lieux à la Faculté des sciences et techniques de l’Université de Limoges et débutera à 14h30 dans la salle de conférence de XLIM. Au Canada, elle auras lieux à l’Université de Sherbrooke et débuteras à 8h30 dans la salle de vidéoconférence de la Faculté des sciences, au D3-1058. La présentation est désormais disponible ici Présentation thèse.

 

Résumé:

«La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n’étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG («Vulnerability Test Generation», génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d’intrusions est généré. Cette méthode s’inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d’application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L’extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d’une instruction. Cette méthode nous a permis de tester différents mécanismes d’implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d’étude, la méthode proposée est générique et a été appliquée à d’autres cas d’études.»

Tags: , , , , , , , , , , , , , , , , , , , ,

Développer pour Rodin 3.0 (3/3): Utilisation simple de l’API Rodin

Dans la partie précédente, nous avons vue comment utiliser Rodin comme plateforme d’exécution. Dans cette article, nous allons voire un exemple d’utilisation simple de l’API de Rodin. Avec la version 3.0 de Rodin, cette étape as été grandement simplifiée. [toc]

Dépendances

Le fichier MANIFEST.MF permet de configurer différentes informations relatives à notre plug-in. Pour utiliser les API de Rodin, rendez-vous dans l’onglet dependences en bas à gauche puis, dans la section Required plug-ins cliquez sur le bouton Lire le reste de cet article »

Tags: , , , , , ,

The API JavaDoc of Rodin 3.0.0

Rodin 3.0.0. is out 😉

I generate the JavaDoc of this new version: http://tmp.aymericksavary.fr/Rodin-3.0.0-JavaDoc/

Generate it by yourself:

First I clone the Robin repository available here: http://sourceforge.net/p/rodin-b-sharp/rodincore/ci/master/tree/

In a fresh Eclipse workspace I import the Rodin maven projet. Don’t care about dependences problems, just continue and ignore errors. When it’s finish Eclipse will restart. Refresh all your projects and go in Preferences -> Plug-in Development. Set option Missing API baseline to Warning. Apply and refresh your projects.

Finally, select all your projects and go to Project -> Generate Javadoc… and clic on Finish. The window Update Javadoc Location appear. Just select No To All.

Tags: , , , , , ,

Mise en place de ma plateforme de développement pour Rodin 2.4 (partie 3/3)

Dans cette dernière partie, nous allons voire comment utiliser l’API Rodin.

Maintenant que nous savons comment lancer un plug-in dans Rodin il est intéressant de pouvoir manipuler les différentes API mises à notre disposition. Pour commencer, nous allons voir à travers un petit exemple comment, lire une machine, afficher la liste de ses invariants, la liste de ses théorèmes ainsi que la liste des événements et de leurs gardes respectifs.

Pour commencer, nous allons devoir récupérer l’API sous forme d’un ensemble des .jar. Rendez-vous sur wiki.event-b.org cliquez sur Download now puis sélectionnez la version contenant la chaine -dev.

Lire le reste de cet article »

Tags: , , , , , ,

Mise en place de ma plateforme de développement pour Rodin 2.4 (partie 1/3)

Dans cet article je vais vous expliquer comment j’ai mis en place tout mon environnement de développement afin de construire rapidement un premier plug-in pour la plateforme Rodin tout en utilisant les API de Rodin et de Event-B (cf wiki.event-b.org).

Tout d’abord, Rodin est un Eclipse modifié. La procédure pour développer un plug-in Rodin est donc très similaire à celle pour développer un plug-in pour Eclipse. Commençons par installer Eclipse RCP qui est disponible ici.

Lire le reste de cet article »

Tags: , , , , , ,

Installer Rodin 2.1 + ProB 1.3.3

Installation de Rodin

Obtention de Rodin

[toc]Pour commencer, vous allez devoir télécharger la version 2.1 de Rodin correspondant à votre système d’exploitation. Pour ce faire, rendez-vous sur la page de téléchargement de la version 2.1 : http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.1/ (ou alors http://www.event-b.org/install.html).
Une fois l’archive téléchargée, vous devez l’extraire. Vous obtenez un répertoire contenant tous les fichiers nécessaires au fonctionnement du logiciel.

Installation des modules complémentaires

Il nous faut maintenant installer différents modules nous permettant de profiter pleinement de cet outil. Nous allons donc voir comment installer 3 d’entre eux : Atelier B Provers, Camille Text Editor et ProB.
Commencez par exécuter le fichier «rodin» ou «rodin.exe» qui se trouve dans le répertoire extrait. Choisissez un « workspace », qui sera votre répertoire de travail et dans lequel se trouvent tous vos projets. Ensuite dans le menu cliquez sur : Help -> Install New Software…
J’ai choisi de vous expliquer comment les installer un à un mais vous pouvez aussi les installer tous d’un seul coup. Lire le reste de cet article »

Tags: , , , , ,