Titre de l'écran-titre (visionné le 12 février 2024) / Dans le paysage numérique actuel, la prévention des cyberattaques est devenue extrêmement cruciale. Cela est particulièrement vrai pour les systèmes critiques pour la sécurité, où la protection contre ces menaces est d'une importance primordiale. Pour répondre à cette préoccupation, MITRE Corporation a développé ATT&CK, un vaste cadre comprenant des matrices de données. Ce cadre a pour but d'évaluer l'état de préparation d'une entreprise en matière de sécurité et d'identifier les vulnérabilités qui peuvent exister au sein de son infrastructure. En tirant parti des capacités de MITRE ATT&CK, y compris ses tactiques et techniques, en conjonction avec l'outil LDA4CPS, nous avons conçu une nouvelle approche pour identifier les vulnérabilités les plus critiques dans un système sensible. De plus, nous avons également conçu une solution pour relever les défis associés à ces vulnérabilités. L'utilisation de LDA4CPS nous permet de résoudre efficacement le graphe AND-OR, offrant ainsi une résolution pratique. De plus, l'inclusion des atténuations MITRE ATT&CK fournit à l'équipe bleue (côté défensif) une meilleure connaissance de la situation et une compréhension plus approfondie des circonstances qui prévalent. Par conséquent, l'intégration de LDA4CPS et de MITRE ATT&CK fournit aux organisations des informations précieuses et des mesures pratiques pour renforcer leur posture de sécurité, renforçant ainsi leur capacité à lutter contre les cybermenaces. / In today's digital landscape, the prevention of cyber attacks has become exceptionally crucial. This is especially true for safety-critical systems, where safeguarding against these threats is of paramount importance. To address this concern, the MITRE Corporation has developed ATT&CK, an extensive framework comprising data matrices. This framework serves the purpose of assessing a company's security preparedness and pinpointing vulnerabilities that may exist within its infrastructure. By leveraging the capabilities of MITRE ATT&CK, including its tactics and techniques, in conjunction with the LDA4CPS tool, we have devised a novel approach to identify the most critical vulnerabilities in a susceptible system. Furthermore, we have also devised a solution to tackle the challenges associated with these vulnerabilities. Employing LDA4CPS enables us to effectively solve the AND-OR graph, thereby offering a practical resolution. Moreover, the inclusion of MITRE ATT&CK mitigations provides the blue team (defensive side) with enhanced situational awareness and a deeper understanding of the prevailing circumstances. Consequently, the integration of LDA4CPS and MITRE ATT&CK equips organizations with valuable insights and practical measures to bolster their security posture, thus reinforcing their ability to combat cyber threats.

.

.

.

.

Les travaux présentés dans ce mémoire sont relatifs à l'élaboration formelle de la commande d'un Système à Évènements Discrets (SED) logique à partir des exigences exprimées dans le cahier des charges. La méthode proposée est basée sur la résolution de manière littérale d'un système d'équations représentant ces exigences.<br />Le cadre mathématique, support de ces travaux, est l'algèbre de Boole des fonctions booléennes. Ce cadre mathématique a été retenu pour les raisons suivantes :<br />- Dans le cas particulier des SED logiques non temporisés, toute loi de commande peut être décrite à l'aide de fonctions booléennes.<br />- Les exigences exposées dans un cahier des charges peuvent être formalisées sous forme de relations entre des fonctions booléennes.<br />- Les résultats obtenus dans le cadre de cette thèse nous permettent de déterminer automatiquement quelles sont les fonctions booléennes qui satisfont le système d'équations entre fonctions booléennes représentant ces exigences.<br />La méthode proposée permet au concepteur d'exprimer les exigences dans des formalismes différents. Il a également la possibilité de fixer la forme de la solution qu'il souhaite obtenir ou de ne réaliser la synthèse que sur une partie du modèle.<br />Le chapitre 2 de ce mémoire est consacré à la présentation des résultats mathématiques que nous avons établis pour pouvoir résoudre un système d'équations à n inconnues dans toute structure d'algèbre de Boole. <br />L'approche de synthèse est détaillée au chapitre 3 au travers du traitement de 3 exemples de taille et de complexité croissantes. Nous montrons comment les exigences exprimées dans un cahier des charges peuvent être formalisées sous forme de relations entre des fonctions booléennes. La résolution du système d'équations est réalisée automatiquement grâce à une maquette informatique développée au LURPA.

.

En Génie Automatique, le GRAFCET [IEC 848] est couramment employé pour la modélisation de la dynamique des systèmes à événements discrets, en raison de ses capacités de modélisation et de son ergonomie. Cependant, il lui est reproché de ne pas être défini de manière suffisamment formelle pour que tous les grafcets établis soient sans ambigüité et puissent être validés. L'objectif des travaux est double : contribuer à la formalisation du GRAFCET de manière à renforcer ses fondements théoriques et offrir à tout analyste les moyens nécessaires pour valider une modélisation exprimée en GRAFCET en vérifiant les propriétés des modèles et leur comportement par rapport à leurs entrées/sorties. Le GRAFCET étant une machine d'état complexe - essentiellement à cause des parallélismes importants qu'il permet de décrire - nous proposons à l'analyste d'utiliser le graphe des situations accessibles, ou grafcet d'état équivalent pour valider sa spécification. Nous avons conçu une technique de génération automatique du graphe des situations accessibles d'un grafcet global (qui est un automate fini «équivalent»), de manière à pouvoir établir un ensemble de preuves et propriétés sur la cohérence intrinsèque du grafcet et sur sa pertinence par rapport au cahier des charges. Une algèbre de Boole, dans laquelle la notion de fronts a été formalisée par deux opérateurs unaires a été construite. Les 14 propriétés qui ont été démontrées ont permis d'établir un module de calcul symbolique utilisé pour tenir compte de l'historique des évolutions des entrées. Nos travaux intègrent les extensions du modèles GRAFCET. Pour valider notre approche, une maquette informatique en C a été développée et permet de calculer l'automate équivalent au grafcet à valider. Nous utilisons pour vérifier certaines propriétés l'outil MEC développé pour l'étude des systèmes de transitions. Deux exemples de validation de grafcets par analyse de leur automate sont donnés dans le mémoire.

Nous présentons les bases de Grobner, leur utilisation et la parallélisation des algorithmes qui les calculent dans le cas de polynômes booléens. Une première partie est consacrée à la présentation théorique des bases de Grobner dans le cas général. Cette présentation se veut accessible a des non-spécialistes. Une étude bibliographique de la complexité est faite. Une deuxième partie concerne les applications des bases de Grobner booléennes en calcul propositionnel et en preuve de circuits combinatoires. Nous proposons un algorithme de preuve formelle de circuits combinatoires hiérarchisés. Dans la troisième partie nous adaptons l'algorithme séquentiel au cas booléen et nous étudions plus en détail la normalisation. Nous proposons deux méthodes de parallélisation a granularité différentes. Nous analysons et comparons plusieurs implantations parallèles et présentons des résultats expérimentaux. Les algorithmes sont généralisables au cas des polynômes a coefficients rationnels. Nous soulignons l'influence de la répartition des données sur le temps d'exécution. Nous présentons une methode de répartition des polynômes basée sur la recherche de chemins de longueur donnée dans un graphe oriente. Cette répartition nous permet d'obtenir des résultats interpretables et de conclure sur les différents algorithmes

.