Ph.D. Preliminary Exam - Ryan Michael Babbitt

Date: 09 Jun, 2009
Time: 10:00 AM
Location: 223 Atanasoff Hall
Topic: VER-SEC: A Model-based Framework for the Managed Verification of Security Properties in Distributed Access Control Infrastructures
Major Professor(s): Johnny S. Wong


Abstract:

Engineering verifiably secure systems presents several challenges to the typical security analyst, such as what parts of the system should be modeled, how they should be modeled, and what verification paradigm/tool should be used to conduct the verification. Traditional approaches directly using individual verification tools may require expert knowledge of the tool under consideration and as a result may lead to a significant amount of error-prone manual interaction/interpretation. The Model-Based Security Engineering (MBSE) paradigm has emerged as a promising approach to counter this problem. Typically, MBSE relies on a high-level modeling language, e.g. UML,  to express the system components and behaviors. Security properties over the system can then be expressed in a related constraint language, e.g. OCL, and the model and its properties automatically translated to the input language of a verification tool and checked. The MBSE paradigm has begun to leverage the popularity and usability of UML with the power of formal methods to make engineering verifiably secure systems easier. However, existing approaches still have several limitations, such as 1) lack of capability to analyze and verify critical security properties, e.g. availability, 2) inadequate conflict analysis among security properties,  3) not incorporating some important access control concepts, e.g. session management and access request evaluation, 4) not utilizing formal specification techniques to heir fullest, and finally, 5) still requiring significant manual interaction. In this proposal, we describe our vision for VER-SEC, a model-based framework, founded on Role-Based Access Control (RBAC) and infused with concepts from the XACML reference architecture, for the managed verification of security properties in distributed access control infrastructures. We claim that our framework will significantly improve the expressive power and capability of existing MBSE approaches, while introducing a greater level of automation, and making them more useful for application in non-academic settings.