Abstract.
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Szyperski, C.: Component Software — Beyond Object Oriented Programming. Addison-Wesley Longman, Amsterdam (1997)
Beugnard, A., Jézéquel, J.M., Plouzeau, N., Watkins, D.: Making Components Contract Aware. IEEE Computer 32, 38–45 (1999)
Lindqvist, U., Jonsson, E.: A Map of Security Risks Associated with Using COTS. IEEE Computer 31, 60–66 (1998)
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)
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)
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)
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)
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)
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)
ISO/IEC: Common Criteria for Information Technology Security Evaluation. International Standard ISO/IEC 15408 (1998)
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)
Herrmann, P., Krumm, H.: A Framework for Modeling Transfer Protocols. Computer Networks 34, 317–337 (2000)
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)
Back, R.J.R., Kurkio-Suonio, R.: Decentralization of process nets with a centralized control. Distributed Computing, 73–87 (1989)
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)
Herrmann, P., Krumm, H.: Modular Specification and Verification of XTP. Telecommunication Systems 9, 207–221 (1998)
Lamport, L.: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16, 872–923 (1994)
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21, 181–185 (1985)
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)
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)
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)
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)
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)
Schmitz, L.: The SalesPoint Framework — Technical Overview (1999), Available via WWW ist.unibw-muenchen.de/Lectures/SalesPoint/overview/english/TechDoc.htm
OBI Consortium: OBI Technical Specifications — Open Buying on the Internet. Draft release v2.1 edn. (1999)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Herrmann, P. (2003). Formal Security Policy Verification of Distributed Component-Structured Software. In: König, H., Heiner, M., Wolisz, A. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2003. FORTE 2003. Lecture Notes in Computer Science, vol 2767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39979-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-39979-7_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20175-5
Online ISBN: 978-3-540-39979-7
eBook Packages: Springer Book Archive