A practical formal model for safety analysis in capability-based systems

We present a formal system that models programmable abstractions for access control. Composite abstractions and patterns of arbitrary complexity are modeled as a configuration of communicating subjects. The subjects in the model can express behavior that corresponds to how information and authority are propagated in capability systems.The formalism is designed to be useful for analyzing how information and authority are confined in arbitrary configurations, but it will also be useful in the reverse sense, to calculate the necessary restrictions in a subject’s behavior when a global confinement policy is given.We introduce a subclass of these systems we call ”saturated”, that can provide safe and tractable approximations for the safety properties in arbitrary configurations of collaborating entities