A Language for Safe Capability Based Collaboration
Yves Jaradin, Fred Spiessens, Peter Van Roy · 2005
In capability secure systems it is important to understand the restrictive influence programmed entities (e.g. procedures, objects, modules, components) have on the propagation of influence in a program. We explain why Take-Grant systems are not sufficiently expressive for this task, and we provide a new formalism – Authority Reduction systems (AR-systems) – to model collaborative propagation. AR-systems provide safe and tractable approximations of adequate precision for the confinement properties in configurations of collaborating entities. We propose a domain specific declarative language – SCOLL (Safe COLlaboration Language) – to express the collaborative behavior of subjects, the initial conditions in a configuration, and the requirements about confinement and liveness that are to be ensured. We provide the syntactic structure and an operational and denotational semantics for the language. From experiments with a first implementation, we provide a preliminary result and show how patterns for capability based collaboration can be analyzed and generated.