Martinoia_Diego.pdf (482.28 kB)

Proving Correctness within an Access Control Evaluation Framework

Download (482.28 kB)
thesis
posted on 24.10.2013, 00:00 by Diego Martinoia
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.

History

Advisor

Zuck, Lenore

Department

Computer Science

Degree Grantor

University of Illinois at Chicago

Degree Level

Masters

Committee Member

Hinrichs, Timothy Lanzi, Pier Luca

Submitted date

2013-08

Language

en

Issue date

24/10/2013

Exports

Categories

Exports