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

F. Spiessens, P. Van Roy

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    13 Citations (Scopus)


    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.
    Original languageEnglish
    Title of host publicationTrustworthy Global Computing
    Subtitle of host publicationInternational Symposium, TGC 2005, Edinburgh, UK, April 7-9, 2005. Revised Selected Papers
    EditorsR. De Nicola, D. Sangiorgi
    Place of PublicationBerlin
    Number of pages31
    ISBN (Electronic)978-3-540-31483-7
    ISBN (Print)3-540-30007-4, 978-3-540-30007-6
    Publication statusPublished - 2005

    Publication series

    NameLecture Notes in Computer Science (LNCS)
    ISSN (Print)0302-9743


    Dive into the research topics of 'A practical formal model for safety analysis in capability-based systems'. Together they form a unique fingerprint.

    Cite this