CSAIL Event Calendar

On the Use of Model Checking for the Verification and Testing of Access Control Systems

Abstract: Access control deals with regulating the accesses principals
have to resources, and is an important aspect of security. In this talk,
I will discuss my work (with collaborators) on verification and testing
of access control systems. Verification problems of interest arise as a
consequence of delegation, a feature with which a trusted administrator
is able to allow other semi-trusted administrators to change the
authorization state. Such problems are often intractable (NP-hard). I
will discuss the utility of, and challenges we faced with a
model-checker to address a basic verification problem in this context.
With testing, we seek to establish that an access control implementation
has properties of interest. In this context, I will discuss our work
with two commercial systems. I will articulate properties of interest,
justify the use of model-checking, our translation of declarative
properties to traces that we seek to exercise in the system under test,
and our use of a model-checker as a trace-generator. Our work in this
context has exposed heretofore unknown issues in a well-known commercial
system.

Bio: Mahesh Tripunitara is an assistant professor in the ECE department
at the University of Waterloo in Canada, where he had been since 2009.
He works mostly in information security, on problems in access control,
conditional payments, cryptographic key transport and more recently,
computer hardware. He has a PhD in computer science from Purdue
University, and about 9 years of industry-experience.

See other events happening in March 2013