University of Illinois at Chicago
Browse
Martinoia_Diego.pdf (482.28 kB)

Proving Correctness within an Access Control Evaluation Framework

Download (482.28 kB)
thesis
posted on 2013-10-24, 00:00 authored 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

2013-10-24

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC