Model-Driven Information Flow Security for Component-Based Systems

  • Najah Ben Said
  • Takoua Abdellatif
  • Saddek Bensalem
  • Marius Bozga
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8415)


This paper proposes a formal framework for studying information flow security in component-based systems. The security policy is defined and verified from the early steps of the system design. Two kinds of non-interference properties are formally introduced and for both of them, sufficient conditions that ensures and simplifies the automated verification are proposed. The verification is compositional, first locally, by checking the behavior of every atomic component and then globally, by checking the inter-components communication and coordination. The potential benefits are illustrated on a concrete case study about constructing secure heterogeneous distributed systems.


component-based systems information flow security noninterference unwinding conditions automated verification 


  1. [AL12]
    Accorsi, R., Lehmann, A.: Automatic information flow analysis of business process models. In: Barros, A., Gal, A., Kindler, E. (eds.) BPM 2012. LNCS, vol. 7481, pp. 172–187. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. [ASRL11]
    Abdellatif, T., Sfaxi, L., Robbana, R., Lakhnech, Y.: Automating information flow control in component-based distributed systems. In: 14th International ACM Sigsoft Symposium on Component Based Software Engineering (CBSE 2011), pp. 73–82. ACM (2011)Google Scholar
  3. [AWD11]
    Accorsi, R., Wonnemann, C., Dochow, S.: Swat: A security workflow analysis toolkit for reliably secure process-aware information systems. In: Sixth International Conference on Availability, Reliability and Security, ARES 2011, pp. 692–697. IEEE (2011)Google Scholar
  4. [BBB+11]
    Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based design using the BIP framework. IEEE Software, Special Edition – Software Components beyond Programming – from Routines to Services 28(3), 41–48 (2011)Google Scholar
  5. [BBMP08]
    Bartolini, C., Bertolino, A., Marchetti, E., Parissis, I.: Data Flow-Based Validation of Web Services Compositions: Perspectives and Examples. In: de Lemos, R., Di Giandomenico, F., Gacek, C., Muccini, H., Vieira, M. (eds.) Architecting Dependable Systems V. LNCS, vol. 5135, pp. 298–325. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. [BBS06]
    Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), pp. 3–12. IEEE Computer Society Press (2006)Google Scholar
  7. [BDL06]
    Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from uml models to access control infrastructures. ACM Transactions on Software Engineering and Methodology 15, 39–91 (2006)CrossRefGoogle Scholar
  8. [BLP76]
    Bell, E.D., La Padula, J.L.: Secure computer system: Unified exposition and Multics interpretation (1976)Google Scholar
  9. [DD77]
    Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Communications of the ACM, 504–513 (1977)CrossRefGoogle Scholar
  10. [EKV+05]
    Efstathopoulos, P., Krohn, M., VanDeBogart, S., Frey, C., Ziegler, D., Kohler, E., Mazières, D., Kaashoek, F., Morris, R.: Labels and Event Processes in the Asbestos Operating System. SIGOPS Operating Systems Review 39(5), 17–30 (2005)CrossRefGoogle Scholar
  11. [FG01]
    Focardi, R., Gorrieri, R.: Classification of Security Properties (Part I: Information Flow). In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  12. [FGF09]
    Frau, S., Gorrieri, R., Ferigato, C.: Petri net security checker: Structural non-interference at work. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 210–225. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  13. [FRS05]
    Focardi, R., Rossi, S., Sabelfeld, A.: Bridging language-based and process calculi security. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 299–315. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. [GM82]
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)Google Scholar
  15. [HV06]
    Hutter, D., Volkamer, M.: Information flow control to secure dynamic web service composition. In: Clark, J.A., Paige, R.F., Polack, F.A.C., Brooke, P.J. (eds.) SPC 2006. LNCS, vol. 3934, pp. 196–210. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. [jif]
  17. [Kuh98]
    Richard Kuhn, D.: Role Based Access Control on MLS Systems without Kernel Changes. In: ACM Workshop on Role Based Access Control (RBAC 1998), pp. 25–32. ACM (1998)Google Scholar
  18. [KYB+07]
    Krohn, M., Yip, A., Brodsky, M., Cliffer, N., Frans Kaashoek, M., Kohler, E., Morris, R.: Information Flow Control for Standard OS Abstractions. SIGOPS Operating Systems Review 41(6), 321–334 (2007)CrossRefGoogle Scholar
  19. [Man00]
    Mantel, H.: Possibilistic Definitions of Security - An Assembly Kit. In: 13th IEEE Workshop on Computer Security Foundations (CSFW 2000), p. 185. IEEE Computer Society (2000)Google Scholar
  20. [McC88]
    McCullough, D.: Noninterference and the composability of security properties. In: Security and Privacy (SP 1988), pp. 177–186. IEEE Computer Society (1988)Google Scholar
  21. [McL94]
    McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Security and Privacy (SP 1994), p. 79. IEEE Computer Society (1994)Google Scholar
  22. [Rus92]
    Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical Report CSL-92-2, SRI International (1992)Google Scholar
  23. [SM03]
    Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1) (2003)CrossRefGoogle Scholar
  24. [SQSL05]
    Shen, J., Qing, S., Shen, Q., Li, L.: Covert channel identification founded on information flow analysis. In: Hao, Y., Liu, J., Wang, Y.-P., Cheung, Y.-M., Yin, H., Jiao, L., Ma, J., Jiao, Y.-C. (eds.) CIS 2005. LNCS (LNAI), vol. 3802, pp. 381–387. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  25. [SS01]
    Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher Order Symbolic Computation 14(1), 59–91 (2001)CrossRefGoogle Scholar
  26. [SS12]
    Seehusen, F., Stølen, K.: A Method for Model-driven Information Flow Security. In: Dependability and Computer Engineering: Concepts for Software-Intensive Systems, pp. 199–229. IGI Global (2012)Google Scholar
  27. [SSM98]
    Sandhu, R., Ravi, S., Munawer, Q.: How to do discretionary access control using roles. In: ACM Workshop on Role-Based Access Control (RBAC 1998), pp. 47–54. ACM (1998)Google Scholar
  28. [SV98]
    Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Symposium on Principles of Programming Languages (POPL 1998), pp. 355–364. ACM (1998)Google Scholar
  29. [ZBWM08]
    Zeldovich, N., Boyd-Wickizer, S., Mazières, D.: Securing distributed systems with information flow control. In: 5th USENIX Symposium on Networked Systems Design and Implementation (NSDI 2008), pp. 293–308. USENIX Association (2008)Google Scholar
  30. [Zda04]
    Zdancewic, S.: Challenges for information-flow security. In: Programming Language Interference and Dependence, PLID 2004 (2004)Google Scholar
  31. [ZL97]
    Zakinthinos, A., Lee, E.S.: A general theory of security properties. In: Security and Privacy (SP 1997), pp. 94–102. IEEE Computer Society (1997)Google Scholar
  32. [ZZNM02]
    Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Secure program partitioning. ACM Transactions on Computer Systems 20(3), 283–328 (2002)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Najah Ben Said
    • 1
  • Takoua Abdellatif
    • 2
  • Saddek Bensalem
    • 1
  • Marius Bozga
    • 1
  1. 1.UJF-Grenoble 1/CNRS, VERIMAG UMR 5104GrenobleFrance
  2. 2.ESSTHSSousse UniversityHammam SousseTunisia

Personalised recommendations