Full Record

New Search | Similar Records

Title Proving Correctness within an Access Control Evaluation Framework
Publication Date
Date Accessioned
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
Date Indexed 2019-12-17
Issued Date 2013-10-24 00:00:00

Sample Images