Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
SEAL: a logic programming framework for specifying and verifying access control models

Prasad Naldurg and Raghavendra K R

Abstract

We present SEAL, a language for specification and analysis of safety properties for label-based access control systems. A SEAL program represents a possibly infinite-state non-deterministic transition system describing the dynamic behavior of entities and their relevant access control operations. The features of our language are derived directly from the need to model new access control features arising from state-of-the art models in Windows 7, Asbestos, HiStar and others. We show that the reachability problem for this class of models is undecidable even for simple SEAL programs, but a bounded model-checking algorithm is able to validate interesting properties and discover relevant attacks.

Details

Publication typeInproceedings
Published in16th ACM Symposium on Access Control Models and Technologies (SACMAT)
PublisherACM
> Publications > SEAL: a logic programming framework for specifying and verifying access control models