FR 3006784 A1 20141212 FR 1355374 A 20130611 Procédé et dispositif d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique La présente invention concerne un procédé d'élaboration automatique, à l'aide d'un dispositif programmable, d'un modèle de comportement d'un appareil fournissant une interface cryptographique. L'invention concerne également un dispositif programmable d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique associé et un programme d'ordinateur associé. L'invention se situe dans le domaine des appareils fournissant des interfaces cryptographiques, et trouve une application particulière dans le domaine de la validation de fiabilité et de robustesse à d'éventuelles attaques des appareils fournissant une interface cryptographique. En effet, les appareils fournissant une interface cryptographique sont utilisés de manière courante dans de nombreux domaines, comme par exemple le domaine bancaire, et plus généralement dans toute application nécessitant une garantie de confidentialité des données auxquelles l'appareil permet l'accès. De tels appareils à interface cryptographique proposent en général au moins une des fonctionnalités suivantes : génération de clé cryptographique, chiffrement et déchiffrement, partage de clé de façon sûre entre plusieurs appareils. Ces fonctionnalités sont fournies par une interface publique, suivant un standard d'interface cryptographique, comme par exemple un des standards PKCS (« public key cryptography standards »). Les fournisseurs de tels appareils cherchent à assurer une sécurité maximale, afin d'éviter tout type de piratage de l'appareil permettant d'exploiter d'éventuelles failles de fonctionnement pour accéder sans autorisation à des données à accès restreint. Les pirates ne disposent pas de la spécification précise qui sous-tend le fonctionnement d'un tel appareil, mais seulement de l'interface publique fournie. Il est donc utile d'être en mesure de valider la fiabilité d'un appareil fournissant une interface cryptographique uniquement à partir de l'interface publique fournie. De manière connue, un audit de sécurité peut être effectué par des experts, qui mettent en place des tests de sécurité ad-hoc. Un tel audit de sécurité est coûteux et son efficacité est largement dépendante de l'expert qui le met en place. Il est préférable d'avoir des outils automatiques aptes à réaliser un audit de sécurité. Pour ce faire, une solution possible consiste à chercher à modéliser le comportement de l'appareil à partir de l'interface cryptographique publique disponible, et à utiliser la modélisation obtenue pour en déduire des failles cryptographiques. A cet effet, l'invention propose, selon un premier aspect, un procédé d'élaboration automatique, à l'aide d'un dispositif programmable, d'un modèle de comportement d'un appareil fournissant une interface cryptographique. Le procédé de l'invention comporte les étapes suivantes, mises en oeuvre par un processeur du dispositif programmable : -obtention d'un ensemble de tests à exécuter par l'appareil fournissant une interface cryptographique, -pour chaque test de l'ensemble de tests, requête d'exécution dudit test par l'appareil fournissant une interface cryptographique et mémorisation du résultat dudit test, -obtention d'une table de vérité représentative d'une formule logique d'une fonction booléenne à partir des résultats mémorisés, -calcul et mémorisation des impliquants premiers à partir de la table de vérité, et -construction et mémorisation d'un modèle de comportement de l'appareil fournissant une interface cryptographique à partir des impliquants premiers mémorisés. Avantageusement, le procédé de l'invention permet d'élaborer automatiquement un modèle de comportement d'un appareil fournissant une interface cryptographique, ce modèle étant particulièrement fiable grâce à l'utilisation d'un calcul des impliquants premiers. Le procédé selon l'invention peut présenter une ou plusieurs des caractéristiques ci-dessous. Il comporte, en outre, une étape de suppression d'impliquants premiers non pertinents avant la construction d'un modèle de comportement de l'appareil fournissant une interface cryptographique. L'étape de suppression comporte les sous-étapes de : -construction d'une formule logique de description de l'ensemble de tests, -pour chaque impliquant premier mémorisé, construction d'une formule logique d'implication à partir de la formule logique de description et des autres impliquants premiers calculés, et - validation de la formule logique d'implication. Pour un impliquant premier traité, en cas de validation positive de la formule logique d'implication dudit impliquant premier traité, ledit impliquant premier traité est labélisé comme non pertinent. En outre, un impliquant premier labélisé comme non pertinent est supprimé de l'ensemble d'impliquants premiers mémorisés. Pour un impliquant premier traité, en cas de validation négative de la formule logique d'implication dudit impliquant premier traité, ledit impliquant premier traité est labélisé comme pertinent. En outre, un impliquant premier labélisé comme pertinent est maintenu dans l'ensemble d'impliquants premiers mémorisés. A l'étape de construction du modèle de comportement de l'appareil fournissant une interface cryptographique à partir des impliquants premiers mémorisés, ledit modèle est construit comme conjonction de l'ensemble d'impliquants premiers mémorisés. Par ailleurs, l'obtention d'un ensemble de tests à exécuter par l'appareil fournissant une interface cryptographique, comporte un paramétrage d'un niveau de fiabilité. Selon un deuxième aspect, l'invention propose un dispositif programmable d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique. Ce dispositif comporte : - des moyens d'obtention d'un ensemble de tests à exécuter par l'appareil fournissant une interface cryptographique, -pour chaque test de l'ensemble de tests, des moyens d'envoi d'une requête d'exécution dudit test par l'appareil fournissant une interface cryptographique et des moyens de mémorisation du résultat dudit test, - des moyens d'obtention d'une table de vérité représentative d'une formule logique d'une fonction booléenne à partir des résultats mémorisés, -des moyens de calcul et de mémorisation des impliquants premiers de la formule logique obtenue, et -des moyens de construction d'un modèle de comportement de l'appareil fournissant une interface cryptographique à partir des impliquants premiers mémorisés. Le dispositif selon l'invention comporte des moyens de mise en oeuvre de toutes les caractéristiques du procédé d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique selon l'invention brièvement rappelées ci-dessus. Selon un troisième aspect, l'invention concerne un programme d'ordinateur comportant des instructions pour mettre en oeuvre les étapes d'un procédé d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique tel que brièvement décrit ci-dessus, lors de l'exécution du programme par un processeur d'un dispositif programmable. D'autres caractéristiques et avantages de l'invention ressortiront de la description qui en est donnée ci-dessous, à titre indicatif et nullement limitatif, en référence aux figures annexées, parmi lesquelles : -la figure 1 est un schéma représentant les blocs fonctionnels d'un dispositif programmable apte à mettre en oeuvre l'invention ; -la figure 2 est un schéma bloc d'un système de test d'un appareil fournissant une interface cryptographique ; -la figure 3 est un organigramme d'un procédé d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique ; - les figures 4 à 6 illustrent un exemple de tests mis en oeuvre et de résultat obtenu ; - la figure 7 illustre les étapes mises en oeuvre pour la suppression d'impliquants premiers non pertinents. La figure 1 illustre les principaux blocs d'un dispositif apte à mettre en oeuvre le procédé d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique selon l'invention. Un dispositif programmable 10 apte à mettre en oeuvre l'invention, typiquement un ordinateur, comprend un écran 12, un moyen 14 de saisie des commandes d'un opérateur, par exemple un clavier, optionnellement un moyen supplémentaire de pointage 16, tel une souris, permettant de sélectionner des éléments graphiques affichés sur l'écran 12, une unité centrale de traitement 18, ou CPU, apte à exécuter des instructions de programme informatique lorsque le dispositif 10 est mis sous tension. Le dispositif 10 comporte également des moyens de stockage d'informations 20, par exemple des registres, aptes à stocker des instructions de code exécutable permettant la mise en oeuvre de programmes comportant des instructions de code aptes à mettre en oeuvre le procédé selon l'invention. Les divers blocs fonctionnels du dispositif 10 décrits ci-dessus sont connectés via un bus de communication 22. Comme illustré à la figure 2, un système de test d'un appareil fournissant une interface cryptographique comporte un dispositif programmable 10, auquel est branché un appareil fournissant une interface cryptographique 30. Le branchement est effectué directement via une liaison filaire ou à distance, par l'intermédiaire d'un réseau de communication. D'un point de vue fonctionnel, le dispositif 10 est apte à envoyer des requêtes 32 selon un format défini par une interface de programmation API 34 de l'appareil fournissant une interface cryptographique 30, et à recevoir des réponses 36. Cet échange de requêtes et réponses permet, comme expliqué plus en détail ci- après, de faire exécuter un ensemble de tests à l'appareil fournissant une interface cryptographique 30 et à recueillir un ensemble de résultats de test. Ces résultats sont traités par le dispositif programmable 10 pour obtenir une formule logique d'une fonction booléenne représentative du comportement de l'appareil à interface cryptographique. La figure 3 représente les principales étapes mises en oeuvre dans un procédé d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique, mises en oeuvre par un processeur 18 d'un dispositif programmable 10. Le procédé est appliqué pour l'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique 30 donné. Dans une première étape 40 du procédé, un ensemble de tests de l'appareil 30 est obtenu. Cet ensemble de tests peut être obtenu automatiquement en fonction du standard implémenté par l'interface API de l'appareil fournissant une interface cryptographique à tester, et peut être paramétré par un opérateur. En effet, selon le paramétrage, l'ensemble de tests à effectuer est plus ou moins complet. Plus un ensemble de tests est complet, plus le niveau de fiabilité du modèle de comportement obtenu est élevé, au prix d'un temps calculatoire plus élevé. Ainsi, un compromis entre temps calculatoire et niveau de fiabilité est sélectionnable par un opérateur. Par exemple, il est possible de tester les commandes dans le cas où la valeur en entrée possède exactement 0, 1 ou 2 attributs. On peut aussi choisir quels attributs seront testés en fixant la valeur des autres attributs, afin de limiter le nombre total de calculs à effectuer et par conséquent, de réduire le temps de calcul. Un opérateur peut alors paramétrer le niveau de test selon le nombre d'attributs testés, correspondant à un niveau de fiabilité donné. Si l'appareil à interface cryptographique 30 fournit une interface suivant le standard PKCS#11, un ensemble de commandes normalisées est à tester. Chaque commande est paramétrée par un ensemble d'attributs binaires en entrée, et le résultat de chaque commande, après exécution par l'appareil 30, est également binaire. Par exemple, un ensemble de quatre tests Test1 à Test4, tel qu'illustré au tableau 41 de la figure 4, est obtenu pour tester la commande C Wrap selon le standard PKCS#11, qui sert à enchiffrer une clé cryptographique K1 (« cipher key ») à l'aide d'une clé cryptographique K2 (« wrapped key »). Dans cet exemple, l'attribut pour la clé cryptographique K1 est CKA WRAP, et les attributs pour la clé cryptographique K2 sont CKA WRAP, CKA UNWRAP, CKA SENSITIVE et CKA EXTRACTABLE. Pour chaque attribut, on fait varier la valeur T pour « true » et F pour « false » de l'attribut. Pour chaque test Test1 à Test4, les valeurs des attributs sont montrées dans les colonnes du tableau 41. Ensuite, à l'étape 42, le dispositif 10 envoie des commandes d'exécution des tests à l'appareil fournissant une interface cryptographique 30, et reçoit une réponse comprenant le résultat de chaque test exécuté par cet appareil. Chaque résultat est mémorisé dans une zone mémoire 20 du dispositif programmable 10, par exemple sous la forme d'un tableau contenant le résultat booléen de chaque test exécuté. Il est à noter que l'exécution des tests et l'obtention des résultats peut être effectuée soit de manière séquentielle, soit de manière groupée. Par exemple, pour l'ensemble des tests Test1 à Test4 pour tester la commande C Wrap, le tableau 43 de résultats de la figure 5 est obtenu. Les résultats booléens sont respectivement la réussite du test, c'est-à-dire son résultat positif (CKR OK) ou son échec, c'est-à-dire son résultat négatif (CKR NOT WRAPPABLE). A l'étape suivante d'obtention 44, une table de vérité décrivant les résultats mémorisés est obtenue. La figure 6 illustre la table de vérité 45 obtenue. Cette table de vérité 45 est une extension du tableau 41 de la figure 4, auquel on rajoute une colonne « résultat ». Dans cette nouvelle colonne, la valeur T pour « true » et F pour « false » indique le résultat, respectivement positif ou négatif, de chaque test. A l'étape suivante de calcul 46, les impliquants premiers de la table de vérité obtenue à l'étape précédente sont calculés, afin d'obtenir les éléments permettant de calculer la formule logique la plus simple représentative du comportement de l'appareil fournissant une interface cryptographique. La méthode connue de Quine-Mc Cluskey est par exemple utilisée. De préférence, l'implémentation de la méthode de calcul des impliquants premiers est celle décrite dans le brevet EP0568424 B1, inclus ici par référence, utilisant une représentation arborescente d'un diagramme de décision binaire associé à une table de vérité, et des éléments intermédiaires normalisés, permettant ainsi de réduire la consommation en espace mémoire lors du calcul des impliquants premiers. Toute autre méthode d'implémentation d'un calcul d'impliquants premiers permettant de maintenir la consommation en espace mémoire compatible avec l'espace mémoire disponible dans le dispositif mettant en oeuvre l'invention est utilisable. Un atome logique est associé à chaque attribut, par exemple W1 est associé à CKA_WRAP pour K1 (clé qui enchiffre), W2 à CKA WRAP pour K2 (clé qui est enchiffrée), U à CKA UNWRAP, S pour CKA SENSITIVE et E pour 30 CKA_EXTRACTABLE. Pour le cas de l'exemple illustré aux figures 4 à 6, on obtient à l'issue de l'étape 46 les impliquants premiers suivants, où -1 représente le « NON » logique : E. Ces impliquants premiers expriment le fait que l'attribut CKA WRAP pour la clé qui enchiffre et l'attribut CKA_EXTRACTABLE sont obligatoirement T, car aucun des tests 35 parmi les tests Test1 à Test4 n'a réussi sans ces attributs, et que les attributs CKA_WRAP et CKA_UNWRAP pour la clé enchiffrée doivent être mis à F. L'étape 46 de calcul des impliquants premiers est suivie d'une étape 48 de suppression des impliquants premiers non pertinents. Cette étape de suppression a pour objectif de filtrer les impliquants premiers obtenus précédemment qui ne sont pas pertinents vis-à-vis du comportement de l'appareil à interface cryptographique mais qui découlent de l'ensemble des tests sélectionné à l'étape 40. Le détail de mise en oeuvre de l'étape 48 selon un mode de réalisation de l'invention est décrit en référence à la figure 7. Lors d'une première étape 60, une formule logique de description de l'ensemble de tests exécutés est construite, indépendamment du résultat de chacun des tests. Ainsi, pour l'exemple décrit ci-dessus en référence à la table décrivant les tests Test-I à Test4, la formule logique de description est la suivante où A représente le « ET » loqiue et y représente le « OU » logique : FE) = (Wi A-1W2 A-1UA SA E)v( VY A-1Un-ISA v(-1Win-11/1/2 A-VA SA E)V(Wi A-1W2 A-VA SA-1E) Ensuite, pour chaque impliquant premier lk sélectionné lors d'une étape 62, parmi les impliquants premiers calculés à l'étape 46, une formule logique d'implication, notée F(Ik), est construite à l'étape 64. La formule logique d'implication est construite de la manière suivante. A gauche de cette formule se trouve la conjonction de FD et de tous les impliquants premiers sauf lk dont on cherche à estimer la pertinence. A droite de la formule logique d'implication se trouve l'impliquant premier lk dont on cherche à estimer la pertinence. De manière générale : F(Ik) : FD A VI, j # k Ainsi, en reprenant l'exemple développé ci-dessus, les formules d'implication suivantes sont construites successivement sont : F(w) : FD A-1w2 A-ILJ E Vy pour l'impliquant premier W1 F(-11/1/2) : FD AW1 A -iU n E -'W2 pour l'impliquant premier -,W2 F(-iU) : FD A W1 A -114/2 n E pour l'impliquant premier -'U F(E) : FD AW, n -'W2 n -iU E pour l'impliquant premier E. Pour chaque formule logique d'implication, la validité de la formule est testée lors d'une étape de test de validité 66. Si la formule F(Ik) est invalide, c'est-à-dire si l'implication exprimée n'est pas vérifiée, l'impliquant premier lk est labélisé comme étant pertinent et doit donc rester dans l'ensemble d'impliquants premiers à utiliser pour la construction d'un modèle de l'appareil fournissant une interface cryptographique. L'étape de test de validité 66 est alors suivie de l'étape 68 de mémorisation de l'impliquant premier lk. Selon un mode de réalisation, les impliquants premiers calculés lors de l'étape précédente de calcul des impliquants premiers 46 sont déjà mémorisés, par exemple dans un tableau, et l'étape 68 ne nécessite aucune action supplémentaire. Si la formule F(Ik) est valide, c'est-à-dire si l'implication exprimée est vérifiée, il en est déduit que l'impliquant premier lk est une conséquence du choix des tests effectués et des autres impliquants premiers, donc il est labélisé comme non pertinent pour ce qui est de la modélisation du comportement de l'appareil à interface cryptographique. Dans ce cas, l'étape 66 est suivie d'une étape 70 de suppression de l'impliquant premier lk des impliquants premiers mémorisés à l'issue de l'étape de calcul d'impliquants premiers 46. Par exemple, si les impliquants premiers calculés lors de l'étape précédente de calcul des impliquants premiers 46 sont déjà mémorisés dans un tableau, l'étape 70 consiste à effacer l'élément lk de ce tableau. Dans l'exemple considéré avec les tests Test-I à Test4, la formule F(Wl) est invalide, ainsi que la formule F(E). Il en est déduit que les impliquants premiers W1 et E sont pertinents. Par contre, les formules F(-114/2) et F( ) sont valides, donc les impliquants premiers-114/2 et -U ne sont pas pertinents. En effet, par exemple en considérant -114/2, il apparaît clairement que cet attribut n'a jamais été testé avec une valeur T (pour « true »), donc l'impliquant -114/2 est une conséquence du choix des tests. De retour à la figure 3, après l'étape 48 de suppression d'impliquants premiers non pertinents, un ensemble réduit d'impliquants premiers pertinents est conservé. Avantageusement, cet ensemble restreint permet d'accélerer les calculs par la suite et de rendre le résultat plus fiable, en évitant l'utilisation d'impliquants premiers non pertinents qui sont uniquement une conséquence de l'ensemble de tests sélectionnés. Finalement, l'ensemble d'impliquants premiers restants est utilisé lors de l'étape suivante de construction 50 pour la construction d'un modèle de l'appareil fournissant une interface cryptographique traité. Dans un mode de réalisation, le modèle est exprimé comme conjonction des impliquants premiers pertinents mémorisés. Dans l'exemple traité, le modèle est donné par Wi n E . Lors de l'étape 50 de construction de modèle de l'appareil fournissant une interface cryptographique, le modèle est mémorisé dans un format approprié, par exemple enregistré dans un fichier texte. De préférence, l'enregistrement utilise le standard d'interface cryptographique, de manière à être facilement ré-utilisable. Dans le cas de l'exemple traité, le modèle est par exemple enregistré sous la forme : CKA WRAP(cipher key) && CKA EXTRACTABLE (wrapped key). Le modèle ainsi enregistré est ensuite utilisable lors d'une étape ultérieure 52 d'utilisation pour validation de l'appareil fournissant une interface crytographique 30. Par exemple, en utilisant en outil d'exploration de modèle (model-checker) on peut examiner tous les enchaînements possibles des commandes pour découvrir si une séquence existe qui compromet la politique de sécurité. Chaque séquence obtenue correspond à un état du modèle de comportement de l'appareil obtenu par le procédé décrit ci-dessus, et la politique de sécurité définit les états acceptables ou autorisés et les états non autorisés Il est entendu que l'exemple décrit ci-dessus, en référence aux figures 4 à 6, est un exemple simplifié à but explicatif. En pratique, un très large ensemble de tests est utilisé pour l'élaboration d'un modèle de comportement d'un appareil fournissant une interface cryptographique. REVENDICATIONS1.- Procédé d'élaboration automatique, à l'aide d'un dispositif programmable (10), d'un modèle de comportement d'un appareil (30) fournissant une interface cryptographique, caractérisé en ce qu'il comporte les étapes suivantes, mises en oeuvre par un processeur (18) du dispositif programmable : -obtention (40) d'un ensemble de tests à exécuter par l'appareil (30) fournissant une interface cryptographique, -pour chaque test de l'ensemble de tests, requête (42) d'exécution dudit test par l'appareil (30) fournissant une interface cryptographique et mémorisation du résultat dudit test, -obtention (44) d'une table de vérité représentative d'une formule logique d'une fonction booléenne à partir des résultats mémorisés, -calcul et mémorisation (46) des impliquants premiers à partir de la table de vérité, et -construction et mémorisation (48) d'un modèle de comportement de l'appareil (30) fournissant une interface cryptographique à partir des impliquants premiers mémorisés. 2.- Procédé selon la revendication 1, caractérisé en ce qu'il comporte, en outre, une étape de suppression (48) d'impliquants premiers non pertinents avant la construction (50) d'un modèle de comportement de l'appareil (30) fournissant une interface cryptographique. 3.- Procédé selon la revendication 2, caractérisé en ce que l'étape de suppression comporte les sous-étapes de : -construction (60) d'une formule logique de description de l'ensemble de tests, -pour chaque impliquant premier mémorisé, construction (64) d'une formule logique d'implication à partir de la formule logique de description et des autres impliquants premiers calculés, et - validation (66) de la formule logique d'implication. 4.- Procédé selon la revendication 3, caractérisé en ce que, pour un impliquant premier traité, en cas de validation positive de la formule logique d'implication dudit impliquant premier traité, ledit impliquant premier traité est labélisé (70) comme non pertinent. 5.- Procédé selon la revendication 4, caractérisé en ce qu'un impliquant premier labélisé comme non pertinent est supprimé de l'ensemble d'impliquants premiers mémorisés. 6.- Procédé selon la revendication 3, caractérisé en ce que, pour un impliquant premier traité, en cas de validation négative de la formule logique d'implication dudit impliquant premier traité, ledit impliquant premier traité est labélisé (68) comme pertinent. 7.- Procédé selon la revendication 6, caractérisé en ce qu'un impliquant premier labélisé comme pertinent est maintenu dans l'ensemble d'impliquants premiers mémorisés. 8.- Procédé selon l'une quelconque des revendications précédentes, caractérisé en ce qu'à l'étape de construction (50) du modèle de comportement de l'appareil (30) fournissant une interface cryptographique à partir des impliquants premiers mémorisés, ledit modèle est construit comme conjonction de l'ensemble d'impliquants premiers mémorisés. 9.- Procédé selon l'une quelconque des revendications précédentes, caractérisé en ce que l'obtention (40) d'un ensemble de tests à exécuter par l'appareil (30) fournissant une interface cryptographique, comporte un paramétrage d'un niveau de fiabilité. 10. Dispositif programmable d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique, caractérisé en ce qu'il comporte : - des moyens d'obtention d'un ensemble de tests à exécuter par l'appareil fournissant une interface cryptographique, -pour chaque test de l'ensemble de tests, des moyens d'envoi d'une requête d'exécution dudit test par l'appareil fournissant une interface cryptographique et des moyens de mémorisation du résultat dudit test, - des moyens d'obtention d'une table de vérité représentative d'une formule logique d'une fonction booléenne à partir des résultats mémorisés, -des moyens de calcul et de mémorisation des impliquants premiers de la formule logique obtenue, et-des moyens de construction d'un modèle de comportement de l'appareil fournissant une interface cryptographique à partir des impliquants premiers mémorisés. 11. Programme d'ordinateur comportant des instructions pour mettre en oeuvre les étapes d'un procédé d'élaboration automatique d'un modèle de comportement d'un appareil fournissant une interface cryptographique selon l'une des revendications 1 à 9 lors de l'exécution du programme par un processeur d'un dispositif programmable. 15