ACE Seminar: Security Analysis of Self-Administrated Role-Based Access Control through Program Verification

Speaker: Dr Gennaro Parlato, University of Southampton
UCL Contact: Christophe Petit (Visitors from outside UCL please email in advance).
Date/Time: 02 Jul 15, 16:00 - 17:00
Venue: Galton LT

Abstract

Role-based Access Control (RBAC) has become an increasingly popular access control model, particularly suitable for large organizations, and it is implemented in several software systems. Automatic security analysis of administrative RBAC systems is recognized as an important problem, as an analysis tool can help designers check whether their policies meet expected security properties. We will present Vac, an automatic tool for verifying security properties of administrative RBAC. Vac converts administrative RBAC policies to imperative programs that simulate the policies both precisely and abstractly and supports several automatic verification back-ends to analyze the resulting programs. We will describe the architecture of Vac and give an overview of the analysis techniques we have designed and implemented in our tool. We will also report on experiments with several benchmarks from the literature.

Dr Gennaro Parlato

Gennaro Parlato is a Lecturer in Automated Verification in the School of Electronics and Computer Science at the University of Southampton (UoS) and a member of the Academic Centre of Excellence in Cybersecurity Southampton. Prior to joining UoS in 2011, he was a research associate in the Department of Computer Science at the University of Illinois at Urbana-Champaign, and a CNRS postdoc research associate in the Modeling and Verification research group at LIAFA laboratory in Paris. He obtained his Ph.D. in Computer Science at the University of Salerno in 2006. Gennaro is interested in software verification and in building reliable and secure software systems using formal correctness techniques.