SEAL: a logic programming framework for specifying and verifying access control models

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.

sacmat08m-naldurg.pdf
PDF file

In  16th ACM Symposium on Access Control Models and Technologies (SACMAT)

Publisher  ACM

Details

TypeInproceedings
> Publications > SEAL: a logic programming framework for specifying and verifying access control models