Sites Inria

English version

Prix scientifique

Marie Collin (*) - 28/09/2010

L'équipe PLANETE obtient le premier prix de la compétition SAT Race 2010

Illustration Codage

CryptoMiniSat , logiciel de vérification de logiciels ou d'architectures matérielles complexes, remporte le premier prix de la compétition internationale SAT Race 2010 .

Vérifier la fiabilité ou le bon fonctionnement d'un logiciel, d'un process ou d'un composant matériel est primordial dans de nombreuses applications industrielles.

Ces vérifications sont parfois complexes lorsque le système comporte des millions de paramètres ou états possibles pour l'ensemble des différents éléments qui le composent. Une technique de vérification de ces systèmes complexes consiste à décrire le système sous forme de contraintes et propriétés de fonctionnement  (description CNF) puis à vérifier la cohérence ou "satisfaisabilité" de toutes ces contraintes. Il s'agit de la résolution de problèmes SAT (Satisfaibility problem) .

Pour contribuer aux recherches sur ce sujet, l'équipe Planète de Grenoble, a développé le logiciel de vérification : CryptoMiniSat .
Ce logiciel (de type SAT solver ) a été spécialement développé pour les vérifications en cryptographie mais il est applicable à tout problème SAT .
En juillet 2010, CryptoMiniSat  a remporté le "SAT Race 2010" , challenge international organisé à l'occasion de la conférence internationale annuelle consacrée aux problèmes SAT .

Parmi les 20 logiciels, industriels ou académiques, participant au challenge, CryptoMiniSAT a obtenu les meilleures performances de résolution et de vitesse d'exécution sur un corpus de 100 applications-tests, issues des domaines de la cryptographie et de la vérification matérielle et logicielle.

Avec ses 10 000 lignes de code spécifiques, en complément du coeur logciel de base des logiciels SAT , CryptoMiniSat prend en compte 15 critères de vérification mathématique supplémentaires dont :

  • des clauses XOR pour traiter plus rapidement les problèmes de vérifications logicielles et de cryptographie ;
  • des algorithmes plus élaborés pour forcer des variables à des valeurs fixes ;
  • un arbre de recherche plus aléatoire pour trouver des solutions"satisfiables" plus rapidement ;
  • une estimation hybride de valeur des clauses pour une approximation plus fine des solutions.

Mots-clés : Logiciel Mate Soos Claude Castelluccia Equipe PLANETE Inria Grenoble Rhône-Alpes Prix

Haut de page

Suivez Inria