In today's information era, the security of computer systems as resources of invaluable information is of crucial importance not just to security administrators but also to users of these systems. Access control is an information security process which guards protected resources against unauthorized access as specified by restrictions in security policies. One significant obstacle to regulate access in secure systems is the lack of formal semantics and specifications for the policy languages which are used in writing security policies. Expressing security policies that are implemented pursuant to required security goals and that accommodate security policy rules correctly is of high importance to the system's integrity, confidentiality, and availability. The semantics of the most widely used policy languages such as SELinux is expressed in a declarative manner using a colloquial natural language (e.g., English), which leads to ambiguity in the interpretation of the policy statements. For this reason, both the development and the analysis of security policies are generally imprecise and based on cognitive concepts; that is to say, they are not conducted in a mathematically-precise and verifiable way. Type Enforcement (TE) is a MAC (Mandatory Access Control) access control mechanism that is used in the SELinux security module. Type Enforcement (TE) is implemented based on the type/domain field of security contexts. TE allows the creation of different domains in the system by assigning subjects to domains and subsequently associating them with objects. TE mandates a central policy-driven approach to access control. We propose a small and certifiably correct TE policy language, TEpla, as an appropriate candidate for the primary access control feature of SELinux, Type Enforcement. TEpla can provide ease of use, analysis, and verification of its properties. TEpla is a certified policy language with formal semantics, exposing ease of reasoning and allowing verification. We use the Coq proof assistant to mechanize semantics and to machine-check the proofs of TEpla, ensuring correctness guarantees are provided. Having a certified semantics simplifies and fosters the development of certified tools for policy-related tasks such as automating various kind of policy analyses.

Sécuriser des systèmes industriels, et en particulier des systèmes intégrés au système d'information, devient l'une des préoccupations les plus urgentes qui inquiètent non seulement tous les acteurs industriels mais aussi les gouvernements. Un nombre très important d'entités industrielles et d'infrastructures sont si critiques que toute cyber attaque réussie contre ces entités peut causer d'énormes dégâts aux entreprises, à l'environnement et plus gravement à la sécurité nationale et à la sûreté des personnes. Cette thèse étudie l'intégration des systèmes ICS avec les systèmes d'entreprise d'un point de vue sécurité. Notre objectif est d'étudier les vulnérabilités de sécurité des systèmes industriels intégrés et de proposer des modèles et des mécanismes pour améliorer leur sécurité et les protéger contre les attaques complexes. Après avoir réalisé une étude approfondie sur les vulnérabilités des systèmes ICS intégrés (IICS) et les solutions de sécurité existantes, nous nous sommes concentrés sur l'étude de la technique de défense en profondeur et son applicabilité aux systèmes ICS intégrés. Nous avons alors défini une nouvelle méthode générique de segmentation pour les IICS, SONICS, qui permet de simplifier la segmentation des IICS en se concentrant uniquement sur les aspects qui sont réellement significatifs pour la segmentation. Nous avons ensuite développé une version améliorée de SONICS, RIICS, une méthode de segmentation pour les systèmes IICS qui comble les lacunes de SONICS en se concentrant sur le risque en plus des spécificités techniques et industrielles. Pour compléter la méthode de segmentation, nous avons étudié les solutions de ségrégation et de contrôle d'accès. Nous avons proposé un nouveau modèle de contrôle de flux basé sur DTE (Domain Type Enforcement) pour les systèmes ICS intégrés. / Securing ICS systems, and especially integrated ones, is becoming one of the most urgent issues that disquiets not only all industrial actors but also governments. Very important number of industrial entities and infrastructures are so critical that any non contained cyber attack on these entities can cause huge damage to business, to environment and more gravely to national security and people safety.This thesis studies the integration of ICS with Corporate systems from a security standpoint. Our goal is to study integrated ICS systems security vulnerabilities and suggest models and mechanisms to improve their security and protect them against ceyberattacks. After conducting a study on the vulnerabilities of integrated ICS systems (IICS) and the existing security solutions, we focused on the study of defence in depth technique and its applicability to integrated ICS systems. We defined a new generic segmentation method for IICS, SONICS, which simplifies the segmentation of IICS by focusing only on spects that are really significant for segmentation. We next developed an improved version of SONICS, RIICS (Risk based IICS Segmentation), a segmentation method for IICS systems that fills the SONICS gaps by focusing on risk on top of technical and industrial specifications. To complement the segmentation method, we studied segregation and access control solutions. We proposed a new DTE-based l (Domain Type Enforcement) flow control model for integrated ICS systems.

This work is engaged in access control mechanism in GNU/Linux operating systems. At first discretionary and mandatory access control are compared and examine basic technologies based on mandatory access control. More closely is focused on project SELinux, whose generation of new rules is explained. Within the thesis is made application for logging evaluation and for writing new Type Enforcement rules.

This master's thesis describes the problems of SELinux, and the methods of creation of a proper security policy with a focus on the SELinux reference policy and its mechanisms. It designs the methodics of formulation of specific security rules, supplemented with the practical example of its application. Furthermore, it describes the available security rules commonly used for http, ftp and ssh services securing, their modification and practical utilization. According to the proposed methodology, these services are protected with their own security rules and both security methods are mutually compared and evaluated.