Brevet FR2798490A1 — publié le 20010316

Procédé et dispositif de résolution de modèles et utilisation pour la détection des attaques contre les systèmes informatiques La présente invention concerne un procédé et dispositif de résolution de modèles et son utilisation pour la détection des attaques contre les systèmes informatiques. Les systèmes informatiques sécurisés peuvent être soumis à des attaques ou tentatives d'introduction frauduleuse. En général, on essaie de parer à ces attaques en établissant des fichiers compte-rendu, par exemple, des fichiers compte-rendu système (log system) ou des fichiers compterendu réseau (log réseau) et en effectuant des filtrages sur ces fichiers pour détecter un incident ou une intrusion. Les systèmes qui font de l'audit de fichiers de compte-rendu reposent généralement sur une méthode compliquée qui pose des problèmes à l'écriture et, de plus, l'audit résultant est difficile à lire. Par ailleurs, lorsque l'intrusion se fait en plusieurs étapes successives non concomitantes, le système peut très bien ne pas la détecter. Par ailleurs, l'écriture des conditions d'audit est peu souple, peu modifiable et pose des problèmes de modularité. Ainsi, dans la plupart des systèmes fonctionnant à l'aide de règles il est nécessaire de décrire les conditions d'audit sous forme de programmes décrivant les déclenchements de règles conditionnés par des événements ; par exemple, pour décrire une condition d'audit spécifiant une étape A, suivie quelque temps plus tard de B, suivie quelque temps plus tard de C, il faudra décrire des règles d'attente de l'étape A, qui en cas de succès devront déclencher des règles d'attente de l'étape B, qui en cas de succès devront déclencher des règles d'attente de l'étape C. Cette façon de décrire la suite A, B, C est lourde, est cause d'erreurs difficiles à détecter par une simple lecture. Enfin, certains systèmes connus nécessitent de balayer plusieurs fois les fichiers compte-rendu. Un but de l'invention est donc de proposer un procédé performant de résolution de spécifications. Ce but est atteint par le fait que le procédé performant de résolution de spécifications comporte : a) une étape de formulation des conditions d'audit que l'on veut détecter à l'aide de formules de spécification, exprimant des schémas d'attaque ou d'introduction frauduleuse, ou encore d'anomalies, ceci n'étant pas limitatif, à vérifier par l'examen des enregistrements du fichier compterendu du système ; b) une étape d'expansion des formules en sous-formules; c) une étape consistant à engendrer pour chaque formule expansée à chaque enregistrement des clauses de Horn à résoudre pour détecter si la formule est valide ou non à cet enregistrement, les clauses de Hom exprimant les implications résolvantes des sous-formules pour chaque enregistrement balayé, en clauses positives, c'est-à-dire ne comptant qu'un littéral positif, et en clauses non positives, c'est-à-dire comptant au moins un littéral négatif, lesquels littéraux négatifs forment la partie négative de la clause. d) une étape de mémorisation des clauses de Horn positives dans une pile de sous-formules #uvrées et une étape de mémorisation dans un tableau comportant une représentation de la ou des sous-formules impliquantes constituant la partie négative de la clause et du lien avec la ou les sous-formules impliquées constituant la partie positive de la clause et mémorisation dans un compteur du nombre de formules ou sous-formules présentes dans la partie négative de la clause pour chaque sous-formule impliquée ; e) une étape de résolution du tableau à partir de chaque clause positive rencontrée ; f) une étape d'itération des étapes b) à e) jusqu'au parcours complet de tous les enregistrements du fichier compte-rendu. Un autre but est de permettre une grande flexibilité. Ce but est atteint par le fait que le procédé utilise pour la formulation de la spécification une logique temporelle. Selon une autre particularité, le tableau est matriciel et indexé en colonnes par les indices des formules apparaissant dans la partie négative des clauses de Horn et les lignes sont exactement les clauses de Horn. Selon une autre particularité le tableau est représenté sous forme de matrice creuse, les colonnes étant représentées au moyen de listes chaînées et les lignes demeurant implicites, est préférée. Selon une autre particularité, une optimisation de l'expansion des formules est obtenue par une table de hachage dans le but d'assurer qu'une même formule n'est pas expansée plus d'une fois à chaque enregistrement. Selon une autre particularité, le fichier compte-rendu n'est parcouru qu'une seule fois du début jusqu'à la fin. Un autre but est de proposer un dispositif permettant la mise en #uvre du procédé. Ce but est atteint par le fait que le dispositif performant de résolution d'une spécification comporte : - un logiciel adaptateur permettant de traduire les informations du fichier compte-rendu, formulées dans le langage spécifique de la machine en un langage compréhensible de l'interpréteur ; -un interpréteur recevant les informations de l'adaptateur et recevant la formulation de la spécification dans la logique temporelle en une formule de spécification pour expanser cette formule et remplir le tableau et la pile de sous-formules #uvrées décrits plus haut résultant du balayage du fichier compte-rendu de la machine ; - un algorithme de traitement de clauses permettant de résoudre les clauses de Horn utilisant les informations du tableau et de la pile de sousformules #uvrées, cet algorithme de traitement de clauses générant un fichier de sortie ou générant une action. D'autres particularités et avantages de la présente invention apparaîtront plus clairement à la lecture de la description ci-après faite en référence aux dessins annexés dans lesquels : - la figure 1 représente une vue schématique des éléments matériels et logiciels permettant la mise en #uvre du procédé. - la figure 2 représente le contenu de la table, des compteurs de formules ou sous-formules présentes dans les parties négatives des clauses, et de la pile, et leur évolution au cours de la mise en #uvre du procédé. La figure 1 représente les éléments nécessaires à la mise en #uvre du procédé selon l'invention. Le fichier compte-rendu (1) est généralement présent sur toutes les machines et peut être le fichier compte-rendu réseau lorsque la machine est connectée à un réseau, ou un fichier compte-rendu système ou tout autre fichier sur lequel on veut vérifier une spécification. Ce fichier communique avec un adaptateur (2) qui est un logiciel permettant de traduire les informations contenues dans le fichier compte-rendu et exprimées dans le langage spécifique à la machine en un langage évolué compréhensible par un interpréteur (3). L'interpréteur (3) reçoit également d'un module (4) la formule de la spécification à vérifier exprimée dans une logique temporelle. Cet interpréteur (3) réalise l'expansion de la formule en sous-formules et le balayage de chaque enregistrement Ei (Annexe 2) du fichier compte-rendu (1) pour générer, à l'aide de cette expansion et de ce balayage, un tableau et une pile résultants exprimant des clauses de Horn mémorisées dans une mémoire (5). La notion de clause de Hom est bien connue de l'homme du métier, et est décrite par exemple dans (GoubaultLarrecq, Jean et Mackie, lan, Proof Theory and Automated Deduction, édité par Kluwer, 1996). Ce tableau et cette pile sont exploités par un algorithme (6) de traitement de clauses qui reçoit un ordre de lancement de l'interpréteur (3) une fois que ce dernier a rempli le tableau (5) contenant une table de compteurs (7), ainsi qu'une pile (18), après avoir parcouru tous les enregistrements Ei du fichier. Cet algorithme va chercher la résolution de la spécification par rapport à l'ensemble des enregistrements. Lors de la détection du balayage complet du fichier d'enregistrement (1), l'algorithme de traitement de clauses génère, soit un fichier de sortie, soit une action du système ou de la machine. Selon une optimisation du procédé selon l'invention, la phase de remplissage du tableau (6) et de la pile (18) et la phase de traitement de clauses sont effectuées de façon concomitantes, de sorte que l'algorithme de traitement de clauses puisse générer le fichier de sortie ou l'action du système ou de la machine au plus tôt, et en général avant la détection du balayage complet du fichier d'enregistrement (1 ). Pour mieux comprendre le procédé mis en #uvre, celui-ci va être explicité à l'aide d'un exemple dont les formules figureront en annexe à la fin de la description. Tout d'abord, un fichier de compte-rendu (log) est une suite d'enregistrements E = (E1, ..., EN ) telle que représentée à l'annexe 2. Chaque enregistrement Ei comporte un certain nombre d'informations telles que la date, l'opération concernée, la machine, un résultat, un sujet, cette liste n'étant pas limitative. Ainsi E1 signale que l'utilisateur machin a tenté de se connecter mais a échoué. Pour formuler une spécification, telle que celle représentée à l'annexe 1, que l'on veut détecter ou résoudre, on utilise une formule de spécification dans une logique temporelle. Cette formule est décrite selon la production formule suivante de la grammaire en format BNF bien connu de l'homme du métier (Aho, Alfred V. et Sethi, Ravi et Ullman, Jeffrey D., Compilers : Principles, Techniques and Tools, Addison-Wesley, 1986) : formule : : = atome formule A formule formule V formule formule U formule ) formule W formule atome : : = record (formule) #~ atome 10 atome, la ligne suivante existe et à la ligne suivante, l'atome est vrai ## atome, si la ligne suivante existe alors à la ligne suivante, l'atome est vrai ## atome, il existe une ligne, soit la ligne courante, soit une ligne ultérieure, l'atome est vrai # atome, pour toutes les lignes à partir de la ligne courante, l'atome est vrai Les opérateurs entre formules sont l'opérateur A pour exprimer un ET logique, V pour exprimer un OU logique, U pour exprimer la formulation jusqu'à (until), W pour exprimer la formulation (Waiting-for) en attente de, O pour exprimer la formulation à la ligne suivante, qui existe, 0 pour exprimer la formulation à la ligne suivante, si elle existe, 0 pour exprimer la formulation à la ligne courante ou à une ligne ultérieure , pour exprimer la formulation à la ligne courante et à toute ligne ultérieure. Cette notation est bien connue de l'homme du métier, voir par exemple (Manna, Zohar et Pnueli, Amir, The Temporal Logic of Reactive and Concurrent Systems Specification, Springer, 1992). Ainsi, la formulation temporelle F = F1 W F2 permet une formulation aisée d'une spécification à vérifier. Supposons que l'opérateur ait introduit, grâce à une interface (4) homme-machine permettant la génération de formule temporelle, une formule temporelle telle que celle figurant en annexe 1. L'interface (4) va traduire cette formule de l'annexe 1 en une formule temporelle où F et H sont des formules atomiques dans lesquelles F représente {op = connection , resuit = failed , ...}et H représente {op = connection , result = success , ...}. Par ailleurs, nous supposons que le fichier de compte-rendu (1) contient les enregistrements E1 à E3 représentés en annexe 2. Dans un premier temps, l'interpréteur (3) procède à l'expansion de la formule pour chaque enregistrement E1, E2, E3, comme représenté à l'annexe 6, en générant des sous-formules pour chaque enregistrement afin d'en déduire des clauses de Horn qui rendent compte des implications logiques qui existent entre une formule et ses sous-formules et de la possibilité de satisfaire les formules atomiques, comme représenté à l'annexe 6. Ainsi pour l'enregistrement E1, la formule est expansée en la sous-formule F à laquelle correspond la clause (f2), en la sous-formule OH à laquelle correspond la clause (f2) A (f3)->(fl), etc. L'interpréteur (3) comporte une procédure d'optimisation qui permet de supprimer les redondances et les étapes inutiles du tableau de l'annexe 6 et après optimisation, l'interpréteur retiendra uniquement les clauses engendrées correspondant au tableau de l'annexe 7. Pour faciliter la compréhension du tableau de l'annexe 7 ou du tableau de l'annexe 6, la notation OH signifie : il existe une ligne, soit la ligne courante de l'enregistrement, soit une ligne ultérieure où la formule H est vérifiée ; pour vérifier si F A OH est vraie à l'enregistrement E1, on numérote les couples (formule, enregistrement) appelés configurations, dans l'exemple le couple (F A OH, E1) est numéroté (1). L'interpréteur (3) expanse la formule F A OH à l'enregistrement E1 en les formules F et OH. Le couple (F, E1) est numéroté /2, le couple (OH, E1) est numéroté f3, et l'interpréteur génère la clause (f2) A (f3)-(f,), qui exprime que si la configuration f2 et la configuration f3 sont vérifiées alors la configuration f1 est vérifiée, c'est-à-dire que F est vérifiée à l'enregistrement E1. O(OH) signifie : la ligne d'enregistrement suivante existe et à la ligne suivante OH est vraie , ceci correspond à la configuration f6 pour le premier enregistrement. La formule HVO (OH) H est vrai ou la ligne d'enregistrement suivante existe et à la ligne suivante, il existe une ligne, soit la ligne courante, soit une ligne ultérieure où H est vrai , ceci correspond aux configurations (f4) pour l'enregistrement E1, (f9) et (f14) pour l'enregistrement E2 et (f19), (/23) et (f28) pour l'enregistrement E3. L'ensemble des clauses de Horn figurant dans la partie droite du tableau de l'annexe 7 est stocké dans la table (5), dans le compteur (7) et dans la pile (18) représentés figure 2 de la façon suivante. Les colonnes de la table (5) sont indexées par les indices ( 2), ( f 3), (f 4), (f 5), (f s), (f 8), (f 11), (f 12) des formules apparaissant dans la partie négative de la clause. Seuls les indices impliquant une conclusion sont conservés. Les lignes de la table (5) sont indexées par les indices (f 1), (f3), (f7) des formules apparaissant dans la partie positive de la clause. La partie négative de la clause est la partie située à gauche de la flèche d'implication que l'on appellera par la suite la ou les sous-formules impliquantes. La partie positive est à droite de la flèche et sera appelée la formule impliquée. Cette représentation n'est pas limitative et la représentation sous forme de matrice creuse, les colonnes étant représentées au moyen de listes chaînées et les lignes demeurant implicites, est préférée Toutefois pour bien comprendre l'invention celle-ci va être expliquée à l'aide des notations de la figure 2. Pour bien comprendre la notation du tableau 7, la clause (f2) A (/3) (f1) signifie que si la configuration f2 est vérifiée et la configuration f3 est vérifiée alors la configuration fi est vérifiée. La clause f7 - /3 signifie que si la configuration f7 est vérifiée alors la configuration f3 aussi. Par ailleurs, au cours de l'expansion des formules par l'interpréteur (3), celui-ci a stocké dans une pile (18) les clauses positives correspondant aux formules qui peuvent être satisfaites. Ainsi à la fin de l'expansion, les formules f2 et f8 sont dans la pile (18i), comme représenté à la figure 2, et la table des compteurs de littéraux négatifs des clauses du tableau est constituée des informations représentées par la référence (71) sur cette figure. Dans la phase de résolution, l'algorithme de traitement de clauses (6), lorsqu'il est lancé par l'interpréteur une fois que celui-ci a rempli les tables (5, 7 et 18) après avoir examiné les lignes d'enregistrements du fichier compte-rendu, va commencer par examiner le dessus de la pile (18) et en extraire l'information que la configuration f8, en l'occurrence, est satisfaite. L'algorithme examine ensuite dans la table (5) les clauses qui ont cette configuration en partie négative, en l'occurrence la configuration f7, et en déduit le compteur qu'il doit décrémenter. Le compteur (72) représente l'évolution dans le compteur (71) du compteur qui est associé à la formule représentée dans la partie positive. L'algorithme décrémente le compteur correspondant, en l'occurrence celui de la configuration f7, et met dans le haut de la pile la valeur 7 de la configuration qui est vraie, comme représenté dans la case (182) qui représente l'évolution de la pile (18) alors que la colonne (72) représente l'évolution du compteur. Puis l'algorithme de résolution des clauses va procéder par itération en recherchant les clauses qui ont la configuration f7 en partie négative pour en déduire que la configuration f3 est vraie et décrémenter le compteur correspondant à cette ligne de configurations, comme représenté dans la colonne (73). L'algorithme (6) continue ainsi jusqu'à ce que la pile (18) soit vide ou contienne des configurations déjà traitées et l'on obtient dans la pile (185) la seule configuration f1 qui vérifie la spécification. L'algorithme d'expansion évite de répliquer inutilement des configurations identiques, représentées par leur pointeur en mettant en place une table de hachage. La structure de données de table de hachage et les algorithmes associés sont bien connus de l'homme du métier, voir par exemple (Knuth, Donald Erwin, The Art of Computer Programming, vol. 3, Sorting and Searching, Addison-Wesley, seconde édition, 1998). Par ailleurs, on peut également effectuer des optimisations liées à l'expansion des formules, de façon à éviter plusieurs étapes. Ainsi au lieu d'expanser la formule OF en FVO (OF) en F et O(OF) et ensuite en OF à l'état suivant, on l'expanse directement en F et en OF à l'état suivant. De même, lorsqu'on a une formule du type F A G où soit F, soit G peut être évalué à l'état courant en faux, on arrête l'expansion de la formule. La méthode développée par l'invention, présente un avantage par rapport à la méthode connue de l'art antérieur où l'on établit dans un premier temps, une table de vérité de chaque formule atomique telle que celle représentée en annexe 4 puis dans un deuxième temps, on établit les tables de vérité (annexe 5) des sous-formules non atomiques à l'aide de la table de vérité de l'annexe 4. La vérification de modèles se fait ensuite en deux temps. Tout d'abord on vérifie que les formules atomiques sont vraies ou fausses, ce qui oblige pour chaque formule un parcours des états puis, dans un second temps, pour établir les vérités des sous-formules on est contraint de regarder pour chaque formule atomique comment elle se comporte dans chaque état, ce qui revient à faire plusieurs parcours des enregistrements. Cela reviendrait à faire des retours en arrière dans le fichier de compte-rendu avec toutes les opérations de lecture et de positionnement qui s'en suivent, ce qui, étant donné la grande taille d'un fichier de compte-rendu, peut être très coûteux en temps. La méthode développée par l'invention est beaucoup plus performante et économe même en taille et mémoire pour mémoriser les états interméd iaires. Pour permettre une meilleure compréhension de l'algorithme, nous allons le décrire brièvement, puis nous le présenterons de manière formelle. On considère Fs, le fichier de spécification, comme une suite finie de formules Fs dont la syntaxe et la sémantique sont définies plus haut. Notons F l'ensemble de toutes les formules dont la syntaxe et la sémantique sont définies plus haut. (Ri,..., RI NI) (avec N égal au nombre d'enregistrements dans le fichier) le fichier de 109SA Les fichiers de logs sont des fichiers de compte-rendu de tout ce qui se passe dans un système (par exemple, un fichier retraçant les connexions et les déconnexions des utilisateurs sur les machines). Un enregistrement (record) est une fonction R de domaine et codomaine finis de #* vers #*, où l'ensemble des chaînes de caractères R : #* # #*. Notons respectivement dom (R) codom (R) pourle domaine de R et le codomaine de R. Exemple 1 (record) Considérons l'enregistrement R d'un fichier de logs : Date = 27 : 02 : 2000, opération = connection, machine = papillon, resultat = succès, sujet = Machin on aura alors : dom(R) = {date, opération, machine, resultat, sujet]} où dom(R) est le domaine et codom le codomaine codom(R) = {27 : 02 : 2000, connection, papillon, succes, Machin} et R: #*# #* date-)- 27:02:2000 opérations connection machines papillon résultats succes sujets Machin. Un fichier de logs est donc une suite (finie) d'enregistrements R1, ..., R#N#. Soit Current et Next , des ensembles de représentations de formules (dans la suite de la description, on dira "formule" pour "représentation de formule") ; Current est l'ensemble des formules à examiner à l'état courant, et Next est l'ensemble des formules qu'il faudra examiner à l'état suivant. A chaque état, l'ensemble Current est l'union de l'ensemble Next et des formules Fs associées à l'état courant. C'est ce que dit l'étape 2 de l'algorithme. L'état courant est représenté par l'entier i, 1 # i # 1 NI . On parcourt en une fois le fichier de compte-rendu logs , et pendant ce parcours, à chaque état, c'est-à-dire à chaque enregistrement (record) du fichier, on regarde quelles sont les formules de l'ensemble Current qui sont vérifiées, et pour celles qui contiennent des opérateurs du futur, on les ajoute à l'ensemble Next pour pouvoir les examiner à l'état suivant. C'est ce que fait la procédure Expand à l'étape 3) de l'algorithme. Cette procédure extrait les sous-formules de chaque formule récursivement, stocke leurs implications logiques les concernant sous forme de clauses de Horn dans une matrice M (par exemple, pour une formule F = F1 V F2, on aura les clauses Fi # F et F2 # F, et pour celles qui sont atomiques, si elles sont vérifiées à l'état courant (c'est ce que cherche la procédure match qui apparaît dans Expand , elle les stocke dans une pile (Stack) qui est une pile de représentation de formules. Une fois que toutes les formules ont été expansées à l'état courant, on résoud ce qui peut l'être à l'aide de la matrice et de la pile (c'est ce que fait la procédure resolve matrice à l'étape 4) de l'algorithme. Ainsi, grâce aux formules atomiques qui l'étaient et aux clauses, on trouvera mémorisé dans le fichier ResForm (qui est un ensemble de représentations de formules) toutes les formules qui sont vérifiées. Ces étapes sont itérées jusqu'à la fin du fichier de logs (on le voit à l'étape 4) de l'algorithme). Enfin, quand tout le fichier de logs est parcouru, la procédure Satis de l'étape 5) compare les formules du fichier ResForm, qui sont toutes des formules vérifiées à un certain état mais qui sont des sous-formules de formules du fichier de spécification, et les formules du fichier de spécification, pour pouvoir dire lesquelles sont vérifiées et à quel(s) état (s). Voici maintenant l'algorithme proprement dit : 1) i = 0 ; Current := 0 ; Next := 0 ; ResForm := 0 ; Stack := pile~vide M = () ; 2) Current := {Repr(F, i) /F # Fs} U Next ; où Repr(F, i) est une représentation mémorisée de F à l'état i Next 0 ; 3) tant que Current # 0 faire : soit f E Current ; Current := Current\ {f} ; Expand( f ) ; 4) resolve matrice ; si i Nous allons maintenant définir les différentes procédures utilisées dans l'algorithme : Procédure Expand(f) , où f est une représentation de formules. Pour plus de clarté, nous allons présenter cette procédure à l'aide d'un tableau dont nous allons expliquer la signification : - la colonne "Formule" est exactement : form (/), c'est-à-dire la formule représentée par f, - la colonne "Currenf' (resp. "Next") désigne toutes les représentations de formules qui sont ajoutées à l'ensemble "Current" (resp. "Next', - la colonne "Clause" désigne les clauses qui sont stockées dans la matrice avec la procédure insérer clause décrite plus loin, - les représentations de formules ajoutées à l'ensemble "Currenf' se font à leur tour expanser récursivement, - les formules atomiques et les formules de la forme F, où F, est une formule atomique, sont traitées séparément : si la formule atomique correspond à l'enregistrement courant (match Irecord) (la procédure match sera définie plus loin), alors cette formule est vérifiée à l'état i ; si la formule atomique F1 ne matche pas le record courant, alors ~F1 est vérifiée à l'état i. Plus formellement : - Si form(f) est une formule atomique, si match(f) = TRUE alors Stack = Empiler(Stack, f); - Si form(f) est de la forme ~F1, F1 formule atomique, soit f = Repr(F1, i) ; si match(f 1) FALSE alors Stack = Empiler (Stack, f) ; Formule Current Next Clause F, A F2 f = Repr(F,, i) /, 1\ /2 -+ / f2 = Repr(F2, i) F, V F2 /1 - Repr(F,, i) /1 -+ / f = Repr(F2, i) f2 f OF, f, = Repr(Fh i + 1) f, f OF, f, = Repr(F,, i + 1) f 1 f sii "* 1 NI (*) OF, f, = Repr(Fi, i) f2 = Repr(OF,, i + /1 -+ / 1) f2 f OF, /1 - Repr(F,, i) f2 = Repr(OF,, i + f, A fi / 1) F, U F2 /1 = ReprfF, A O(F, U /1 -+ / F2), i) f2#f f2 = Repr(F2, i) F, WF2 f, = Repr(F,, i) /1 -+ tf2 = Repr(F, U Fz" i) f2 ---> f -,(F21\ Fs) f, = Repr(-,F2 v -,F3. i) /1 -+ / -, (F2 VF3) fi = Repr(-,Fz 1\ -,F3, i) /1 -+ / -, (-,F2J /1 = Repr(F2, i) /1 -+ / -, (OF2J fi = Repr(O(-,F2. i) /1 -+ / -, (OF2J /1 = Repr(O(-,F2. i) /1 -+ / -, (OF2J f, = Repr(D (-,F2. i) f, -i f (D Fz) f 1 Repr(O (-,F2, i) /1 -+ / (F2UF3) f = Repr(D (F3, i) /1 -+ / f2 = Repr(F3 U (Fz, f2 f 1\,0 F3), i) -,(F2 W F3) F, Repr -iF3) U (-,F2, /1 -+ / 1\ ,-' F3). i) (*) : sinon, c'est-à-dire si i = 1 NI , fui = Repr(F1, i) Stack = Empiler(Sfack, f 1) ; Procédure match(/) , où f est une représentation de formules Cas form ( f ) : - si c'est de la forme {id, = tri idn = tn,...}, alors : - si Vj, 1 zij - si c'est de la forme {id1= t1,..., idn= tn}, alors : - si n= |dom(Ri) 1 et j, 1 - sinon FALSE - si t est une variable x : Notation : p (x) est une fonction partielle de l'ensemble des variables V vers l'ensemble des chaînes de caractères #* - si p (x) défini - si p(x) = w - alors TRUE - sinon FALSE - si p (x) pas défini, alors Notation : E est l'environnement constitué des couples dont la première composante est prise dans l'ensemble des variables et la deuxième composante dans l'ensemble des chaînes de caractères -E: = E U {(x,w)} ; -TRUE; Procédure Insérer-clause (H), où H est une clause de Horn ayant une ou deux représentations de formules en partie négative : Notation : Si M est une matrice m x n, m, n E: N, notons m@,f l'élément de la ième ligné indéxé par f, et de manière semblable mf,l et mf1,f2 Cas H : - si H est de la forme f1 # f, alors - s'il existe déjà une colonne de M indiquée par f1 - alors, ajouter une ligne indicée par f avec mf,f1 = 1 ; - sinon, ajouter une colonne indicée par f et une ligne indicée par f1 avec mf,f1= 1 ; - si H est de la forme f1 ^f2, alors : - si ni f1, ni f2ne sont indice d'aucune colonne de M - alors, ajouter 2 colonnes indicées par f1 et f2 et une ligne indicée par/ avec mf,f1= mf,f2=2 - si seulement l'un des f@, i = 1,2 n'est pas indice d'une colonne de m alors : - ajouter une colonne indicée par f@ et une ligne indicée par f avec mf, f, = rnf,fj = 2, où j E: {1,2} \ {i} - si f1et f2 sont indices de colonnes de M, alors : - ajouter une ligne indicée par f avec mf,f1= mf,f2= 2 Procédure resolve-matrice - si Stack = pile-vide, alors rien ; - sinon soit f : = dépiter (Stack) ; V, tel que m@.f est l'élément existe faire : - m,f = m,f - 1 - Vjtel que nrig existe faire : mi := nriy -1 - si m@,@ = 0, alors ; - soit f1l'indice de la ligne m@,f - si f1 # Res-Form, alors : - Stack : empiler (Stack, f1) - Res-form := Res-Form U {f1} - suppr (m@,f); - si la ième ligne la supprimer, si la colonne indicée par f est vide la supprimer Satis : Tant que Stack pile- vide faire : - soit f1 = depiler (Stack) ; - si f1E Fs alors form (f) est vérifiée à l'état etat(/) Toute modification à la portée de l'homme du métier fait partie de l'esprit de l'invention. ANNEXE Annexe 1 {op = connection , result = failed ,...} et plus tard {op = connection , result = succes ,...} Annexe 2 E1 : {op = connection , result = failed , subject = machin } E2 : {op = connection , result = succès , subject = machin , date = 14 : 99 } E3 : {op = exec , result = succes , object = emacs , mode = : tex , subject = machin } Annexe 3 FA 0 H où F et H sont des formules atomiques de détection d'évènement exprimée en logique temporelle à partir de formules atomiques. E1 : {F} E2 : {H} E3 : {G} Annexe 4 ETATS F H E1 1 0 R2 0 1 R3 0 0 Tables de vérité des formules atomiques Annexe 5 ETATS # H F # # H E1 1 1 1 E2 1 0 E3 0 0 Tables de vérité des formules non atomiques Annexe 7 ETATS Formules et sous-formules Clauses- engendrées E1 F # # H (f1) (/1) : F (.f2) (Ïz) 0 H (13) (f2) A (13) ( /1) (13) H ,14) (/4)->FALSE E2 F A 0 H (/6) (/3) OH (/7) J 7)(J 3) (17): H (fa) (fa) (/6) : F (f 9) (/6)( 17) (f6)#FALSE E3 F A 0 H (/10) (f7) 0 H (f11) (/11)(h) (/11) : H (f 12) (f 12) --->FALSE (/10) : F (f13) (f11) FALSE Annexe 6 ETATS Formules et sous-formules Clauses engendrées El FAO 0 H (f 1) (f1) : F (f2) (f2) 0 H (f3) (f2) A (f3) i (f1) (J 3) H V 0 (0 H) (J;4) (f4) --) (/3) (f4) H (f5) (fs) --)(f4) (f5) FALSE O ( 0 H) (f6) (Ïs) --)(f4) E2 F A 0 H (17) (f6) (0 H) (fa) (f8) --) (f6) (Îe) : H V O (0 H) (fg) (f9)--)(f8) (f 9) : H (f 10) (f 10) --) (f 9) (f1O) (f)- 0 (0 H) (fIl) (f 1)--) (f ) (f7) (fI2) (fil2)--> FALSE (0 H) (f13) (f,2)-> FALSE (f13) : H V 0 (0 H) (fI1:) (f12) 1\ (/13)--) (17) Uts) H V 0 (0 H) (fl4) (fl4)--> (fl3) (f 14) H (f 15) (f14)--) (f13) (fl4) (fl5) (f1S)--) (f14) (f1S) 0(OH) (f 16) (f16) --)( f14) E3 F A 0 H (f17) (fil) 0 H (fl8) (f18) --)(fII) (f18) : H V O (0 H) (f,9) (f19) --)(f18) (/19) H (f2O) (f20) --)(f19) (/2o) FALSE 0(0 H) (f2l (f21) --)(fI9) (/16) (0 H) (f22) (f) --)(fI6) (f22) : H V O (0 H (f23) (123) --)(122) (f23) H (f24) (f24)#(f23) (f24) # FALSE 0 (0 H) (f25) (f25) #(f23) (f25)#FALSE (f1O F (f2s) (f26) --->FALSE 0 H (f27) (f2s) n (/27)-"(/17) (7): Hv 0 (0 H) (f28) (f28)--)(h7) (/28): H (/29) (f29)#(f28) (f29)#FALSE (f30)#(f28) O 0 H) (f30) (f30) FALSE REVENDICATIONS 1. Procédé performant de résolution de spécifications caractérisé en ce qu'il comporte : a) une étape de formulation des conditions d'audit que l'on veut détecter à l'aide de formules de spécification, exprimant des schémas d'attaque ou d'introduction frauduleuse, ou encore d'anomalies, ceci n'étant pas limitatif, à vérifier par l'examen des enregistrements du fichier compterendu du système informatique ; b) une étape d'expansion par un algorithme des formules en sousformules; c) une étape de balayage par un interpréteur consistant à engendrer pour chaque formule expansée à chaque enregistrement des clauses de Horn à résoudre pour détecter si la formule est valide ou non à cet enregistrement, les clauses de Horn exprimant les implications résolvantes des sous-formules pour chaque enregistrement balayé, en clauses positives, c'est-à-dire ne comptant qu'un littéral positif, et en clauses non positives, c'est-à-dire comptant au moins un littéral négatif, lesquels littéraux négatifs forment la partie négative de la clause ; d) une étape de mémorisation des clauses de Horn positives dans une pile de sous-formules #uvrées et une étape de mémorisation dans un tableau comportant une représentation de la ou des sous-formules impliquantes constituant la partie négative de la clause et du lien avec la ou les sous-formules impliquées constituant la partie positive de la clause et mémorisation dans un compteur du nombre de formules ou sous-formules présentes dans la partie négative de la clause pour chaque sous-formule impliquée ; e) une étape de résolution du tableau à partir de chaque clause positive rencontrée pour générer soit un fichier de sortie, soit une action du système informatique ; f) une étape d'itération des étapes b) à e) jusqu'au parcours complet de tous les enregistrements du fichier compte-rendu. 2. Procédé selon la revendication 1, caractérisé par le fait que pour la formulation de la spécification, une logique temporelle est utilisée. 3. Procédé selon la revendication 1, caractérisé en ce que le tableau est matriciel et indexé en colonnes par les indices des formules apparaissant dans la partie négative des clauses de Horn et les lignes sont exactement les clauses de Horn. 4. Procédé selon la revendication 1, caractérisé en ce que le tableau est représenté sous forme de matrice creuse, les colonnes étant représentées au moyen de listes chaînées et les lignes demeurant implicites, est préférée 5. Procédé selon les revendications 1 ou 2, caractérisé en ce qu'une étape d'optimisation de l'expansion des formules est obtenue par une table de hachage dans le but d'assurer qu'une même formule n'est pas expansée plus d'une fois à chaque enregistrement. 6. Procédé selon la revendication 1, caractérisé en ce que le fichier compte-rendu n'est parcouru qu'une seule fois du début jusqu'à la fin. 7. Système informatique comportant des moyens de mémorisation et des moyens d'exécution de programmes permettant la mise en #uvre du procédé selon une des revendications 1 à 6, caractérisé en ce que le système comporte : - un moyen adaptateur permettant de traduire les informations du fichier compte-rendu formulées dans le langage spécifique de la machine en un langage compréhensible d'un moyen interpréteur ; - le moyen interpréteur recevant les informations de l'adaptateur et recevant la formulation de la spécification dans la logique temporelle en une formule de spécification pour expanser cette formule et remplir le tableau et la pile de sous-formules #uvrées mémorisées dans une mémoire du système informatique et résultant du balayage du fichier compte-rendu du système informatique ; - un algorithme de traitement de clauses exécuté par le système informatique permettant de résoudre les clauses de Horn utilisant les informations du tableau et de la pile de sous-formules #uvrées, cet algorithme de traitement de clauses générant un fichier de sortie ou générant une action.