1,721,024 research outputs found
A Certified Core Policy Language
No full textWe present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown access-control policy languages such as eXtensible Access Control Markup Language (XACML) [OAS13] already exist, because access rules in such languages are often expressed in a declarative manner using fragments of a natural language like English, it isn’t alwaysclear what the intended behaviour of the system encoded in these access rules should be. To remedy this ambiguity, formal specification of how an access-control mechanism should behave, is typically given in some sort of logic, often a subset of first order logic. To show that an access-control system actually behaves correctly with respect to its specification,
proofs are needed, however the proofs that are often presented in the literature are hard or impossible to formally verify. The verification difficulty is partly due to the fact that the language used to do the proofs while mathematical in nature, utilizes intuitive justifications to derive the proofs. Intuitive language in proofs means that the proofs could be incomplete and/or contain subtle errors.
ACCPL is small by design. By small we refer to the size of the language; the syntax,
auxiliary definitions and the semantics of ACCPL only take a few pages to describe. This compactness allows us to concentrate on the main goal of this thesis which is the ability to reason about the policies written in ACCPL with respect to specific questions. By making the language compact, we have stayed away from completeness and expressive power in several directions. For example, ACCPL uses only a single policy combinator, the conjunction policy combinator. The design of ACCPL is therefore a trade-off between ease of formal proof of correctness and expressive power. We also consider ACCPL a core policy access-control language since we have retained the core features of many access-control policy languages. For instance ACCPL employs a single condition type called a “prerequisite” where other languages may have very expressive and rich sets of conditions
Proving properties of programs using automatically generated models.
No full textThis thesis describes a method for automatically generating theories in a first order logic with arithmetic for the purpose of proving properties about the programs. We build the logic and define the syntactic model generation algorithm. The models can be used to prove a substantial class of properties that are true of the programs they are generated from. Here, a model is a set of formulas of the logic that are interpreted as mathematical function definitions. These functions describe the computation steps of the algorithm
A Certified Core Policy Language
No full textWe present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control rules and policies. Although full-blown access-control policy languages such as eXtensible Access Control Markup Language (XACML) [OAS13] already exist, because access rules in such languages are often expressed in a declarative manner using fragments of a natural language like English, it isn’t alwaysclear what the intended behaviour of the system encoded in these access rules should be. To remedy this ambiguity, formal specification of how an access-control mechanism should behave, is typically given in some sort of logic, often a subset of first order logic. To show that an access-control system actually behaves correctly with respect to its specification,\ud
proofs are needed, however the proofs that are often presented in the literature are hard or impossible to formally verify. The verification difficulty is partly due to the fact that the language used to do the proofs while mathematical in nature, utilizes intuitive justifications to derive the proofs. Intuitive language in proofs means that the proofs could be incomplete and/or contain subtle errors.\ud
ACCPL is small by design. By small we refer to the size of the language; the syntax,\ud
auxiliary definitions and the semantics of ACCPL only take a few pages to describe. This compactness allows us to concentrate on the main goal of this thesis which is the ability to reason about the policies written in ACCPL with respect to specific questions. By making the language compact, we have stayed away from completeness and expressive power in several directions. For example, ACCPL uses only a single policy combinator, the conjunction policy combinator. The design of ACCPL is therefore a trade-off between ease of formal proof of correctness and expressive power. We also consider ACCPL a core policy access-control language since we have retained the core features of many access-control policy languages. For instance ACCPL employs a single condition type called a “prerequisite” where other languages may have very expressive and rich sets of conditions
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
No full textThe goal of this thesis is to find provably correct methods for detecting conflicts between XACML rules. A conflict occurs when one rule permits a request and another denies that same request. As XACML deals with access control, we can help prevent unwanted access by verifying that it contains rules that do not have unintended conflicts. In order to help with this, we propose an algorithm to find these conflicts then use the Coq Proof Assistant to prove correctness of this algorithm. The algorithm takes a rule set specified in XACML and returns a list of pairs of indices denoting which rules conflict. It is then up to the policy writer to see if the conflicts are intended, or if they need modifying. Since we will prove that this algorithm is sound and complete, we can be assured that the list we obtain is complete and only contains true conflicts
The Logic of Hereditary Harrop Formulas as a Specification Logic for Hybrid
No full textHybrid is a two-level logical framework that supports higher-order abstract syntax\ud
(HOAS), where a specification logic (SL) extends the class of object logics (OLs) we\ud
can reason about. We develop a new Hybrid SL and formalize its metatheory, proving weakening, contraction, exchange, and cut admissibility; results that greatly simplify reasoning about OLs in systems providing HOAS. The SL is a sequent calculus defined as an inductive type in Coq and we prove properties by structural induction over SL sequents. We also present a generalized SL and metatheory statement, allowing us to prove many cases of such theorems in a general way and understand how to identify and prove the difficult cases. We make a concrete and measurable improvement to Hybrid with the new SL formalization and provide a technique for abstracting such proofs, leading to a condensed presentation, greater understanding, and a generalization that may be instantiated to other logics
A Verified Algorithm for Detecting Conflicts in XACML Access Control Rules
No full textThe goal of this thesis is to find provably correct methods for detecting conflicts between XACML rules. A conflict occurs when one rule permits a request and another denies that same request. As XACML deals with access control, we can help prevent unwanted access by verifying that it contains rules that do not have unintended conflicts. In order to help with this, we propose an algorithm to find these conflicts then use the Coq Proof Assistant to prove correctness of this algorithm. The algorithm takes a rule set specified in XACML and returns a list of pairs of indices denoting which rules conflict. It is then up to the policy writer to see if the conflicts are intended, or if they need modifying. Since we will prove that this algorithm is sound and complete, we can be assured that the list we obtain is complete and only contains true conflicts
TEpla: A Certified Type Enforcement Access-Control Policy Language
No full textIn 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
Reasoning Using Higher-Order Abstract Syntax in a Higher-Order Logic Proof Environment: Improvements to Hybrid and a Case Study
No full textWe present a series of improvements to the Hybrid system, a formal theory implemented in Isabelle/HOL to support specifying and reasoning about formal systems using higher-order abstract syntax (HOAS). We modify Hybrid's type of terms, which is built definitionally in terms of de Bruijn indices, to exclude at the type level terms with `dangling' indices. We strengthen the injectivity property for Hybrid's variable-binding operator, and develop rules for compositional proof of its side condition, avoiding conversion from HOAS to de Bruijn indices. We prove representational adequacy of Hybrid (with these improvements) for a lambda-calculus-like subset of Isabelle/HOL syntax, at the level of set-theoretic semantics and without unfolding Hybrid's definition in terms of de Bruijn indices. In further work, we prove an induction principle that maintains some of the benefits of HOAS even for open terms. We also present a case study of the formalization in Hybrid of a small programming language, Mini-ML with mutable references, including its operational semantics and a type-safety property. This is the largest case study in Hybrid to date, and the first to formalize a language with mutable references. We compare four variants of this formalization based on the two-level approach adopted by Felty and Momigliano in other recent work on Hybrid, with various specification logics (SLs), including substructural logics, formalized in Isabelle/HOL and used in turn to encode judgments of the object language. We also compare these with a variant that does not use an intermediate SL layer. In the course of the case study, we explore and develop new proof techniques, particularly in connection with context invariants and induction on SL statements
Coercive Subtyping in Lambda-Free Logical Frameworks
Get PDFWe show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF
Proving properties of programs using automatically generated models.
No full textThis thesis describes a method for automatically generating theories in a first order logic with arithmetic for the purpose of proving properties about the programs. We build the logic and define the syntactic model generation algorithm. The models can be used to prove a substantial class of properties that are true of the programs they are generated from. Here, a model is a set of formulas of the logic that are interpreted as mathematical function definitions. These functions describe the computation steps of the algorithm
- …
