Добірка наукової літератури з теми "Sécurité des systèmes – Méthodes formelles (informatique)"
Оформте джерело за APA, MLA, Chicago, Harvard та іншими стилями
Зміст
Ознайомтеся зі списками актуальних статей, книг, дисертацій, тез та інших наукових джерел на тему "Sécurité des systèmes – Méthodes formelles (informatique)".
Біля кожної праці в переліку літератури доступна кнопка «Додати до бібліографії». Скористайтеся нею – і ми автоматично оформимо бібліографічне посилання на обрану працю в потрібному вам стилі цитування: APA, MLA, «Гарвард», «Чикаго», «Ванкувер» тощо.
Також ви можете завантажити повний текст наукової публікації у форматі «.pdf» та прочитати онлайн анотацію до роботи, якщо відповідні параметри наявні в метаданих.
Дисертації з теми "Sécurité des systèmes – Méthodes formelles (informatique)"
Rauzy, Pablo. "Méthodes logicielles formelles pour la sécurité des implémentations de systèmes cryptographiques." Thesis, Paris, ENST, 2015. http://www.theses.fr/2015ENST0039/document.
Повний текст джерелаImplementations of cryptosystems are vulnerable to physical attacks, and thus need to be protected against them. Of course, malfunctioning protections are useless. Formal methods help to develop systems while assessing their conformity to a rigorous specification. The first goal of my thesis, and its innovative aspect, is to show that formal methods can be used to prove not only the principle of the countermeasures according to a model, but also their implementations, as it is where the physical vulnerabilities are exploited. My second goal is the proof and the automation of the protection techniques themselves, because handwritten security code is error-prone
Bursuc, Sergiu. "Contraintes de déductibilité dans une algèbre quotient : réduction de modèles et applications à la sécurité." Cachan, Ecole normale supérieure, 2009. http://www.theses.fr/2009DENS0055.
Повний текст джерелаTo enable formal and automated analysis of security protocols, one has to abstract implementations of cryptographic primitives by terms in a given algebra. However, the algebra can not be free, as cryptographic primitives have algebraic properties that are either relevant to their specification or else they can be simply observed in implementations at hand. These properties are sometimes essential for the execution of the protocol, but they also open the possibility for an attack, as they give to an intruder the means to deduce new information from the messages that he intercepts over the network. In consequence, there was much work over the last few years towards enriching the Dolev-Yao model, originally based on a free algebra, with algebraic properties, modelled by equational theories. In this thesis, driven by both practical and theoretical interests, we propose general decision procedures for the insecurity of protocols, that can be applied to several classes of equational theories
Masson, Lola. "Safety monitoring for autonomous systems : interactive elicitation of safety rules." Thesis, Toulouse 3, 2019. http://www.theses.fr/2019TOU30220.
Повний текст джерелаAn active safety monitor is an independent mechanism that is responsible for keeping the system in a safe state, should a hazardous situation occur. Is has observations (sensors) and interventions (actuators). Safety rules are synthesized from the results of the hazard analysis, using the tool SMOF (Safety MOnitoring Framework), in order to identify which interventions to apply for dangerous observations values. The safety rules enforce a safety property (the system remains in a safe state) and some permissiveness properties, ensuring that the system can still perform its tasks. This work focuses on solving cases where the synthesis fails to return a set of safe and permissive rules. To assist the user in these cases, three new features are introduced and developed. The first one addresses the diagnosis of why the rules fail to fulfill a permissiveness requirement. The second one suggests candidate safety interventions to inject into the synthesis process. The third one allows the tuning of the permissiveness requirements based on a set of essential functionalities to maintain. The use of these features is discussed and illustrated on two industrial case studies, a manufacturing robot from KUKA and a maintenance robot from Sterela
Konopacki, Pierre. "Modélisation de politiques de sécurité à l'aide de méthode de spécifications formelles." Phd thesis, Université Paris-Est, 2012. http://tel.archives-ouvertes.fr/tel-00786926.
Повний текст джерелаColange, Maximilien. "Symmetry reduction and symbolic data structures for model-checking of distributed systems." Paris 6, 2013. http://www.theses.fr/2013PA066724.
Повний текст джерелаDistributed systems are becoming omnipresent in our daily life, especially in critical domains, thus requiring a strong guarantee of reliability. Approaches like testing are inherently not exhaustive, so that formal methods are needed. Among those, we focus on model-checking, that consists in exploring exhaustively all the behaviors of a system to ensure that the specification is enforced. However, this approach faces the “combinatorial explosion” problem: the number behaviors of a distributed system increases exponentially with its number of components. To tackle this explosion, several approaches have been proposed. We focus on two of them:- symmetries to identify similar behaviors: they share similar properties, thus allowing to reduce the number of behaviors to explore;- symbolic compact data structures, namely decision diagrams (DD), to reduce the memory footprint of the explored behaviors. We propose three main contributions:- Symmetry reduction and DD are theoretically orthogonal techniques, but are not known to combine well in practice, because efficiency of DD heavily relies on the use of dedicated algorithms. We propose a novel algorithm to use symmetry reduction on DD, and demonstrate experimentally its efficiency. - Classical operations on DD are encoded using a pre-computation of all possible inputs. We offer a new mechanism of manipulation of DD, fully symbolic, that avoids such a pre-computation. We demonstrate its efficiency to encode a transition relation, and to improve our symmetry reduction algorithm- We show how to use the two previous contributions to model-check an existing class of models, the Symmetric Nets with Bags
El, Jamal Mohamad Hani. "Contribution à l'évolution des exigences et son impact sur la sécurité." Phd thesis, Université Paul Sabatier - Toulouse III, 2006. http://tel.archives-ouvertes.fr/tel-00139543.
Повний текст джерелаGuesmi, Asma. "Spécification et analyse formelles des politiques de sécurité dans un processus de courtage de l'informatique en nuage." Thesis, Orléans, 2016. http://www.theses.fr/2016ORLE2010/document.
Повний текст джерелаThe number of cloud offerings increases rapidly. Therefore, it is difficult for clients to select the adequate cloud providers which fit their needs. In this thesis, we introduce a cloud service brokerage mechanism that considers the client security requirements. We consider two types of the client requirements. The amount of resources is represented by the functional requirements. The non-functional requirements consist on security properties and placement constraints. The requirements and the offers are specified using the Alloy language. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required resources in the adequate cloud providers, in a way that fulfills all customer requirements, including security properties. The broker checks that the placement configuration ensures all the security requirements. All these steps are done before the resources deployment in the cloud computing. This allows to detect the conflicts and errors in the clients requirements, thus resources vulnerabilities can be avoided after the deployment
Robin, Ludovic. "Vérification formelle de protocoles basés sur de courtes chaines authentifiées." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0019/document.
Повний текст джерелаModern security protocols may involve humans in order to compare or copy short strings betweendifferent devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examplesof such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose asymbolic model which includes attacker capabilities for both guessing short strings, and producing collisions whenshort strings result from an application of weak hash functions. We propose a new decision procedure for analyzing(a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in theAKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standard
Filipiak, Alicia. "Conception et analyse formelle de protocoles de sécurité, une application au vote électronique et au paiement mobile." Thesis, Université de Lorraine, 2018. http://www.theses.fr/2018LORR0039/document.
Повний текст джерелаThe last decade has seen the massive democratization of smart devices such as phones, tablets, even watches. In the wealthiest societies of the world, not only do people have their personal computer at home, they now carry one in their pocket or around their wrist on a day to day basis. And those devices are no more used simply for communication through messaging or phone calls, they are now used to store personal photos or critical payment data, manage contacts and finances, connect to an e-mail box or a merchant website... Recent examples call for more complex tasks we ask to such devices: Estonia voting policy allows the use of smart ID cards and smartphones to participate to national elections. In 2017, Transport for London launched the TfL Oyster app to allow tube users to top up and manage their Oyster card from their smartphone. As services grow with more complexity, so do the trust users and businesses put in them. We focus our interest into cryptographic protocols which define the exchanges between devices and entities so that such interaction ensure some security guarantees such as authentication, integrity of messages, secrecy… Their design is known to be an error prone task. Thankfully, years of research gave us some tools to improve the design of security protocols, among them are the formal methods: we can model a cryptographic protocol as an abstract process that manipulates data and cryptographic function, also modeled as abstract terms and functions. The protocol is tested against an active adversary and the guarantees we would like a protocol to satisfy are modeled as security properties. The security of the protocol can then be mathematically proven. Such proofs can be automated with tools like ProVerif or Tamarin. One of the big challenge when it comes to designing and formally proving the security an “industrial- level” protocol lies in the fact that such protocols are usually heavier than academic protocols and that they aim at more complex security properties than the classical ones. With this thesis, we wanted to focus on two use cases: electronic voting and mobile payment. We designed two protocols, one for each respective use case and proved their security using automated prover tools. The first one, Belenios VS, is a variant of an existing voting scheme, Belenios RF. It specifies a voting ecosystem allowing a user to cast a ballot from a voting sheet by flashing a code. The protocol’s security has been proven using the ProVerif tool. It guarantees that the vote confidentiality cannot be broken and that the user is capable of verifying their vote is part of the final result by performing a simple task that requires no technical skills all of this even if the user’s device is compromised – by a malware for instance. The second protocol is a payment one that has been conceived in order to be fully scalable with the existing payment ecosystem while improving the security management and cost on the smartphone. Its security has been proven using the Tamarin prover and holds even if the user’s device is under an attacker’s control
Jacomme, Charlie. "Preuves de protocoles cryptographiques : méthodes symboliques et attaquants puissants." Electronic Thesis or Diss., université Paris-Saclay, 2020. http://www.theses.fr/2020UPASG005.
Повний текст джерелаThe use of communication protocols has become pervasive at all levels of our society. Yet, their uses come with risks, either about the security of the system or the privacy of the user. To mitigate those risks, we must provide the protocols with strong security guarantees: we need formal, extensive, modular and machine-checked proofs. However, such proofs are very difficult to obtain in practice. In this Thesis, we strive to ease this process in the case of cryptographic protocols and powerful attackers. The four main contributions of this Thesis, all based on symbolic methods, are 1) a methodology for extensive analyses via a case study of multi-factor authentication; 2) composition results to allow modular proofs of complex protocols in the computational model; 3) symbolic methods for deciding basic proof steps in computational proofs, formulated as problems on probabilistic programs; 4) a prototype of a mechanized prover in the Computationally Complete Symbolic Attacker model