A Practical Formal Model for Safety Analysis in Capability-Based Systems

  • Fred Spiessens
  • Peter Van Roy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3705)


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.


Model Checker Safety Analysis Expressive Power Safety Property Horn Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Boe84]
    Boebert, W.E.: On the inability of an unmodified capability machine to enforce the *-property. In: Proceedings of 7th DoD/NBS Computer Security Conference, September 1984, pp. 45–54 (1984),
  2. [BS79]
    Bishop, M., Snyder, L.: The transfer of information and authority in a protection system. In: Proceedings of the seventh ACM symposium on Operating systems principles, pp. 45–54. ACM Press, New York (1979)Google Scholar
  3. [DH65]
    Dennis, J.B., Van Horn, E.C.: Programming semantics for multiprogrammed computations. Technical Report MIT/LCS/TR-23, M.I.T. Laboratory for Computer Science (1965)Google Scholar
  4. [FB96]
    Frank, J., Bishop, M.: Extending the take-grant protection system (December 1996), Available at:
  5. [Har89]
    Hardy, N.: The confused deputy. ACM SIGOPS Oper. Syst. Rev 22(4), 36–38 (1989), CrossRefMathSciNetGoogle Scholar
  6. [Hol97]
    Holzmann, G.J.: The model checker spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  7. [HRU76]
    Harrison, M.A., Ruzzo, W.L., Ullman, J.D.: Protection in operating systems. Commun. ACM 19(8), 461–471 (1976)CrossRefzbMATHMathSciNetGoogle Scholar
  8. [HS73]
    Salzer, J.H., Schroeder, M.D.: The protection of information in computer systems. In: Fourth ACM Symposium on Operating System Principles (March 1973)Google Scholar
  9. [J0̈5]
    Jürjens, J.: Secure Systems Development with UML. Springer, Berlin (2005)zbMATHGoogle Scholar
  10. [Jos]
    Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming cryptographic protocols. Technical report, The MITRE Corporation. Availalbe, at
  11. [KL87]
    Kain, R.Y., Landwehr, C.E.: On access checking in capability-based systems. IEEE Trans. Softw. Eng. 13(2), 202–207 (1987)CrossRefGoogle Scholar
  12. [LS77]
    Lipton, R.J., Snyder, L.: A linear time algorithm for deciding subject security. J. ACM 24(3), 455–464 (1977)CrossRefzbMATHMathSciNetGoogle Scholar
  13. [MS03]
    Miller, M.S., Shapiro, J.: Paradigm regained: Abstraction mechanisms for access control. In: Saraswat, V.A. (ed.) ASIAN 2003. LNCS, vol. 2896, pp. 224–242. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  14. [MSC+01]
    Miller, M., Stiegler, M., Close, T., Frantz, B., Yee, K.-P., Morningstar, C., Shapiro, J., Hardy, N., Tribble, E.D., Barnes, D., Bornstien, D., Wilcox-O’Hearn, B., Stanley, T., Reid, K., Bacon, D.: E: Open source distributed capabilities (2001), Available at
  15. [MTS05]
    Miller, M.S., Tulloh, B., Shapiro, J.S.: The structure of authority: Why security is not a separable concern. In: Van Roy, P. (ed.) MOZ 2004. LNCS, vol. 3389, pp. 2–20. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. [NPV02]
    Nielsen, M., Palamidessi, C., Valencia, F.D.: Temporal concurrent constraint programming: denotation, logic and applications. Nordic J. of Computing 9(2), 145–188 (2002)zbMATHMathSciNetGoogle Scholar
  17. [QVD05]
    Quesada, L., Van Roy, P., Deville, Y.: The reachability propagator. Research Report INFO-2005-07, Université catholique de Louvain, Louvain-la-Neuve, Belgium (2005)Google Scholar
  18. [Rei03]
    Reich, S.: Escape from mutlithreaded hell. concurrency in the language “e” (March 2003), Presentation available at:
  19. [Sar93]
    Saraswat, V.A.: Concurrent Constraint Programming. MIT Press, Cambridge (1993)Google Scholar
  20. [SJG95]
    Saraswat, V.A., Jagadeesan, R., Gupta, V.: Default timed concurrent constraint programming. In: POPL 1995: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 272–285. ACM Press, New York (1995)CrossRefGoogle Scholar
  21. [SMRS04]
    Spiessens, F., Miller, M., Van Roy, P., Shapiro, J.: Authority Reduction in Protection Systems. Available at (2004),
  22. [SV05a]
    Spiessens, F., Van Roy, P.: The oz-E project: Design guidelines for a secure multiparadigm programming language. In: Van Roy, P. (ed.) MOZ 2004. LNCS, vol. 3389, pp. 21–40. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. [SV05b]
    Spiessens, F., Van Roy, P.: A practical formal model for safety analysis in Capability-Based systems. LNCS. Springer, Heidelberg (2005) Available at, Presentation available at Google Scholar
  24. [VH04]
    Van Roy, P., Haridi, S.: Concepts, Techniques, and Models of Computer Programming. MIT Press, Cambridge (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Fred Spiessens
    • 1
  • Peter Van Roy
    • 1
  1. 1.Université catholique de LouvainLouvain-la-NeuveBelgium

Personalised recommendations