| 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 Images
