| Author | Martinoia, Diego |
| Title | Proving Correctness within an Access Control Evaluation Framework |
| URL | http://hdl.handle.net/10027/10132  |
| Publication Date | 2013 |
| Date Accessioned | 2013-10-24 20:33:03 |
| University/Publisher | University of Illinois – Chicago |
| Abstract | This thesis presents the proofs developed to demonstrate correctness of a case study within the Access Control Evaluation Framework (ACEF). ACEF is a theoretical framework developed at the University of Illinois at Chicago, aimed at creating application-sensitive implementations of access control policies, using well-known access control systems, while preserving some desirable properties. As the formal proof of these properties, including correctness, is usually a tedious process prone to error, a mixed approach was used, which relies on both human high-level abstraction and insight for the outlining of the proof sketches, and then verifies their formal correctness using a formal prover system. To achieve this, a generic template for ACEF for the Prototype Verification System formal prover was developed. The process of generating the proofs for this specific case study was also a benchmark for the validity of the template, as a first step towards the realization of a more automated approach to ACEF. In the conclusions, the validity of the approach is analyzed and possible future steps to improve it are outlined. |
| Subjects/Keywords | Access Control; Formal Methods; Correctness; PVS; Verification |
| Contributors | Zuck, Lenore (advisor); Hinrichs, Timothy (committee member); Lanzi, Pier Luca (committee member) |
| Language | en |
| Rights | Copyright 2013 Diego Martinoia |
| Country of Publication | us |
| Record ID | handle:10027/10132 |
| Repository | uic |
| Date Retrieved | 2019-12-17 |
| Date Indexed | 2019-12-17 |
| Issued Date | 2013-10-24 00:00:00 |
Sample Search Hits | Sample Images
…representation of a state, we have methods that expose information about the state to the outside. We are going to refer to these methods as queries. Queries and states are elements of any generic FSA. Since we are representing systems related to access control…
…queries in the typical subject-object-right fashion. Below are given some definition that will be useful in explaining the rest of the theory. 2.1 Access Control Model Definition 1 (Access Control Model). An Access Control Model (ACM…
…type A Model). Access Matrix type A (AMa ) is the simplest type of access control scheme in the Access Matrix (AM) family. It only consists of a matrix recording triplets that directly represent the authorization policies. So…
…represent how actions affect the states. 2.2 Access Control System Definition 2 (Access Control System). An ACS Y is a tuple M, L, next such that: • M : an ACM, as defined in the previous paragraph. • L: a finite set of labels (also called…
…for a formalized version of one of the well-known Access Matrix ACS’s and the so-called “dynamic coalitions” scenario, described in the next chapter, which was one of the driving needs for the development of ACEF. As we’ll see, the component of…
…queries q ∈ Q true for a given s ∈ S (i.e. s |= q ), and Auth(s) is the set of all the authorization queries r ∈ R such that s |= r (note that Auth(s) ⊆ T h(s), as R ⊆ Q). Example 1 (Access Matrix…
…if we let U denote the set of all possible strings, one possible representation in ACEF of the ACM for AMa would be: • States: The states are composed only from the access matrix, which is a subset of U 3 . Each s ∈ States(A) is a possible…
…state of the access matrix. For brevity, I’ll refer to the access matrix of state s using s.m 8 • Queries: The only available query is whether or not a triplet belongs to the matrix. Note that the presence of a triplet in the matrix also means that…
