Security analysis of role-based access control through program verification

Anna Lisa Ferrara, P. Madhusudan, Gennaro Parlato

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We propose a novel scheme for proving administrative role-based access control (ARBAC) policies correct with respect to security properties using the powerful abstraction-based tools available for program verification. Our scheme uses a combination of abstraction and reduction to program verification to perform security analysis. We convert ARBAC policies to imperative programs that simulate the policy abstractly, and then utilize further abstract- interpretation techniques from program analysis to analyze the programs in order to prove the policies secure. We argue that the aggressive set-abstractions and numerical-abstractions we use are natural and appropriate in the access control setting. We implement our scheme using a tool called VAC that translates ARBAC policies to imperative programs followed by an interval-based static analysis of the program, and show that we can effectively prove access control policies correct. The salient feature of our approach are the abstraction schemes we develop and the reduction of role-based access control security (which has nothing to do with programs) to program verification problems.

Original languageEnglish (US)
Title of host publicationProceedings - 2012 IEEE 25th Computer Security Foundations Symposium, CSF 2012
Pages113-125
Number of pages13
DOIs
StatePublished - Oct 5 2012
Event2012 IEEE 25th Computer Security Foundations Symposium, CSF 2012 - Cambridge, MA, United States
Duration: Jun 25 2012Jun 27 2012

Publication series

NameProceedings of the Computer Security Foundations Workshop
ISSN (Print)1063-6900

Other

Other2012 IEEE 25th Computer Security Foundations Symposium, CSF 2012
Country/TerritoryUnited States
CityCambridge, MA
Period6/25/126/27/12

Keywords

  • Access control
  • Formal methods for security

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Security analysis of role-based access control through program verification'. Together they form a unique fingerprint.

Cite this