Formal Security Policy Verification of Distributed Component-Structured Software

  • Peter Herrmann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


Component-structured software, which is coupled from independently developed software components, introduces new security problems. In particular, a component may attack components of its environment and, in consequence, spoil the application incorporating it. Therefore, to guard a system, we constrain the behavior of a component by ruling out the transmission of events between components which may cause harm. Security policies describing the behavior constraints are formally specified and, at runtime, so-called security wrappers monitor the interface traffic of components and check it for compliance with the specifications. Moreover, one can also use the specifications to prove formally that the combinations of the component security policies fulfill certain security properties of the complete component-structured application. A well-known method to express system security properties is access control which can be modelled by means of the popular Role Based Access Control (RBAC) method.

Below, we will introduce a specification framework facilitating the formal proof that component security policy specifications fulfill RBAC-based application access control policies. The specification framework is based on the specification technique cTLA. The design of state-based security policy specifications and of RBAC-models is supported by framework libraries of specification patterns which may be instantiated and composed to a specification. Moreover, the framework contains already proven theorems facilitating the formal reasoning since a deduction proof can be reduced to proof steps which correspond directly to the theorems. In particular, we introduce the specification framework and clarify its application by means of an e-commerce example.


Access Control Security Policy Process Type Process Instance Event Argument 
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.


  1. 1.
    Szyperski, C.: Component Software — Beyond Object Oriented Programming. Addison-Wesley Longman, Amsterdam (1997)Google Scholar
  2. 2.
    Beugnard, A., Jézéquel, J.M., Plouzeau, N., Watkins, D.: Making Components Contract Aware. IEEE Computer 32, 38–45 (1999)CrossRefGoogle Scholar
  3. 3.
    Lindqvist, U., Jonsson, E.: A Map of Security Risks Associated with Using COTS. IEEE Computer 31, 60–66 (1998)CrossRefGoogle Scholar
  4. 4.
    Herrmann, P.: Trust-Based Procurement Support for Software Components. In: Proceedings of the 4th International Conference on Electronic Commerce Research (ICECR-4), Dallas, ATSMA, IFIP, pp. 505–514 (2001)Google Scholar
  5. 5.
    Herrmann, P., Krumm, H.: Trust-adapted enforcement of security policies in distributed component-structured applications. In: Proceedings of the 6th IEEE Symposium on Computers and Communications, Hammamet, pp. 2–8. IEEE Computer Society Press, Los Alamitos (2001)CrossRefGoogle Scholar
  6. 6.
    Herrmann, P., Wiebusch, L., Krumm, H.: State-Based Security Policy Enforcement in Component-Based E-Commerce Applications. In: Proceedings of the 2nd IFIP Conference on E-Commerce, E-Business & E-Government (I3E), Lisbon, pp. 195–209. Kluwer Academic Publisher, Dordrecht (2002)Google Scholar
  7. 7.
    Fraser, T., Badger, L., Feldman, M.: Hardening COTS Software with Generic Software Wrappers. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy, pp. 2–16. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  8. 8.
    Herrmann, P.: Trust-Based Protection of Software Component Users and Designers. In: Nixon, P., Terzis, S. (eds.) iTrust 2003. LNCS, vol. 2692, pp. 75–90. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    Khan, K., Han, J., Zheng, Y.: A Framework for an Active Interface to Characterise Compositional Security Contracts of Software Components. In: Proceedings of the Australian Software Engineering Conference (ASWEC 2001), Canberra, pp. 117–126. IEEE Computer Society Press, Los Alamitos (2001)CrossRefGoogle Scholar
  10. 10.
    ISO/IEC: Common Criteria for Information Technology Security Evaluation. International Standard ISO/IEC 15408 (1998)Google Scholar
  11. 11.
    Ferraiolo, D.F., Sandhu, R., Gavrila, S., Kuhn, D.R., Chandramouli, R.: Proposed NIST Standard for Role-Based Access Control. ACM Transactions on Information and System Security 4, 224–274 (2001)CrossRefGoogle Scholar
  12. 12.
    Herrmann, P., Krumm, H.: A Framework for Modeling Transfer Protocols. Computer Networks 34, 317–337 (2000)CrossRefGoogle Scholar
  13. 13.
    Vissers, C.A., Scollo, G., van Sinderen, M.: Architecture and specification style in formal descriptions of distributed systems. In: Agarwal, S., Sabnani, K. (eds.) Protocol Specification, Testing and Verification, vol. VIII, pp. 189–204. Elsevier, IFIP, Amsterdam (1988)Google Scholar
  14. 14.
    Back, R.J.R., Kurkio-Suonio, R.: Decentralization of process nets with a centralized control. Distributed Computing, 73–87 (1989)Google Scholar
  15. 15.
    Herrmann, P., Krumm, H., Drögehorn, O., Geisselhardt, W.: Framework and Tool Support for Formal Verification of High Speed Transfer Protocol Designs. Telecommunication Systems 20, 291–310 (2002)CrossRefGoogle Scholar
  16. 16.
    Herrmann, P., Krumm, H.: Modular Specification and Verification of XTP. Telecommunication Systems 9, 207–221 (1998)CrossRefGoogle Scholar
  17. 17.
    Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16, 872–923 (1994)CrossRefGoogle Scholar
  18. 18.
    Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Heyl, C., Mester, A., Krumm, H.: ctc — A Tool Supporting the Construction of cTLA-Specifications. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 407–411. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  20. 20.
    Graw, G., Herrmann, P., Krumm, H.: Constraint-Oriented Formal Modelling of OO-Systems. In: Second IFIP WG 6.1 International Working Conference on Distributed Applications and Interoperable Systems (DAIS 1999), Helsinki, pp. 345–358. Kluwer Academic Publisher, Dordrecht (1999)CrossRefGoogle Scholar
  21. 21.
    Ferraiolo, D.F., Barkley, J.F., Kuhn, D.R.: A Role Based Access Control Model and Reference Implementation within a Corporate Intranet. ACM Transactions on Information Systems Security 1, 34–64 (1999)CrossRefGoogle Scholar
  22. 22.
    Osborn, S.L., Sandhu, R.S., Munawer, Q.: Configuring Role-Based Access Control to Enforce Mandatory and Discretionary Access Control Policies. ACM Transactions on Information and System Security 3, 85–106 (2000)CrossRefGoogle Scholar
  23. 23.
    Zöllner, J., Federrath, H., Klimant, H., Pfitzmann, A., Piotraschke, R., Westfeld, A., Wicke, G., Wolf, G.: Modeling the security of steganographic systems. In: Aucsmith, D. (ed.) IH 1998. LNCS, vol. 1525, pp. 345–355. Springer, Heidelberg (1998)Google Scholar
  24. 24.
    Schmitz, L.: The SalesPoint Framework — Technical Overview (1999), Available via WWW
  25. 25.
    OBI Consortium: OBI Technical Specifications — Open Buying on the Internet. Draft release v2.1 edn. (1999) Google Scholar
  26. 26.
    Ferrari, E., Samarati, P., Bertino, E., Jajodia, S.: Providing flexibility in information flow control for object-oriented systems. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, pp. 130–140 (1997)Google Scholar
  27. 27.
    Myers, A.C., Liskov, B.: Complete, Safe Information with Decentralized Labels. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, pp. 186–197 (1998)Google Scholar
  28. 28.
    Herrmann, P.: Information Flow Analysis of Component-Structured Applications. In: Proceedings of the 17th Annual Computer Security Applications Conference (ACSAC 2001), New Orleans. ACM SIGSAC, pp. 45–54. IEEE Computer Society Press, Los Alamitos (2001)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Peter Herrmann
    • 1
  1. 1.Computer Science DepartmentUniversity of DortmundDortmundGermany

Personalised recommendations