Abstract
Within distributed systems with completely distributed interactions between parties with mutual distrust, it is hard to control the (illicit) flowing of private information to unintended parties. Unlike existing methods dealing with verification of low-level cryptographic protocols, we propose a novel model-based approach based on model transformations to build a secure-by-construction multiparty distributed system. First, starting from a component-based model of the system, the designer annotates different parts of it in order to define the security policy. Then, the security is checked and when valid, a secure distributed model, consistent with the desired security policy, is automatically generated. To illustrate the approach, we present a framework that implements our method and use it to secure an online social network application.
The research leading to these results has received funding from the European Community’s Seventh Framework Programme [FP7/2007-2013] under grant agreement ICT-318772 (D-MILS).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
no. TR-2014-6 on http://www-verimag.imag.fr/Rapports-Techniques,28.html.
- 2.
In general, a third conflict resolution layer is used, however, it has a confined impact on information flow and is ommited here for the sake of simplicity of the presentation.
References
Ben Said, N., Abdellatif, T., Bensalem, S., Bozga, M.: Model-driven information flow security for component-based systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) From Programs to Systems. LNCS, vol. 8415, pp. 1–20. Springer, Heidelberg (2014)
Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time systems in BIP. In: Proceedings of the SEFM 2006, pp. 3–12. IEEE Computer Society Press (2006)
Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: Automated conflict-free distributed implementation of component-based models. In: Proceedings of the SIES 2010, pp. 108–117. IEEE (2010)
Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Distrib. Comput. 25(5), 383–409 (2012)
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)
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)
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)
Basin, D.A., Doser, J., Lodderstedt, T.: Model driven security: from UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15(1), 39–91 (2006)
Chollet, S., Lalanda, P.: Security specification at process level. In: Proceedings of the SCC 2008, pp. 165–172. IEEE Computer Society (2008)
Accorsi, R., Wonnemann, C.: Static information flow analysis of workflow models. In: Proceedings of the ISSS and BPSC 2010, LNI, vol. 177, pp. 194–205 (2010)
Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20, 504–513 (1977)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, pp. 11–20. IEEE Computer Society (1982)
Heintze, N., Riecke, J.G.: The slam calculus: programming with secrecy and integrity. In: Proceedings of the POPL 1998, pp. 365–377. ACM (1998)
Volpano, D.M., Irvine, C.E., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4(2/3), 167–188 (1996)
Laud, Peeter: Semantics and program analysis of computationally secure information flow. In: Sands, David (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)
Adão, P., Fournet, C.: Cryptographically sound implementations for communicating processes. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 83–94. Springer, Heidelberg (2006)
Courant, J., Ene, C., Lakhnech, Y.: Computationally sound typing for non-interference: the case of deterministic encryption. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 364–375. Springer, Heidelberg (2007)
Laud, P.: On the computational soundness of cryptographically masked flows. In: Proceedings of the POPL 2008, pp. 337–348. ACM (2008)
Fournet, C., Rezk, T.: Cryptographically sound implementations for typed information-flow security. In: Proceedings of the POPL 2008, pp. 323–335. ACM (2008)
Zdancewic, S., Zheng, L., Nystrom, N., Myers, A.C.: Secure program partitioning. ACM Trans. Comput. Syst. 20, 283–328 (2002)
Fournet, C., Le Guernic, G., Rezk, T.: A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms. In: Proceedings of the CCS 2009, pp. 432–441. ACM (2009)
Krohn, M.N., Yip, A., Brodsky, M.Z., Cliffer, N., Kaashoek, M.F., Kohler, E., Morris, R.: Information flow control for standard OS abstractions. In: Proceedings of the SOSP 2007, pp. 321–334. ACM (2007)
Zeldovich, N., Boyd-Wickizer, S., Kohler, E., Mazières, D.: Making information flow explicit in HiStar. In: Proceedings of the OSDI 2006, pp. 263–278. Usenix Assoc. (2006)
Vandebogart, S., Efstathopoulos, P., Kohler, E., Krohn, M.N., Frey, C., Ziegler, D., Kaashoek, M.F., Morris, R., Mazières, D.: Labels and event processes in the Asbestos operating system. ACM Trans. Comput. Syst. 25(4), 1–11 (2007)
Zeldovich, N., Boyd-Wickizer, S., Mazières, D.: Securing distributed systems with information flow control. In: Proceedings of the NSDI 2008, pp. 293–308. Usenix Assoc. (2008)
Parrend, P., Frénot, S.: Security benchmarks of OSGi platforms: toward hardened OSGi. Softw. Pract. Exper. 39(5), 471–499 (2009)
Kuz, I., Liu, Y., Gorton, I., Heiser, G.: Camkes: a component model for secure microkernel-based embedded systems. J. Syst. Softw. 80(5), 687–699 (2007)
Abdellatif, T., Sfaxi, L., Robbana, R., Lakhnech, Y.: Automating information flow control in component-based distributed systems. In: Proceedings of the CBSE 2011, pp. 73–82. ACM (2011)
Ben Said, N., Abdellatif, T., Bensalem, S., Bozga, M.: A robust framework for securing composed web services. In: Braga, C., et al. (eds.) FACS 2015. LNCS, vol. 9539, pp. 105–122. Springer, Heidelberg (2016). doi:10.1007/978-3-319-28934-2_6
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Said, N.B., Abdellatif, T., Bensalem, S., Bozga, M. (2016). A Model-Based Approach to Secure Multiparty Distributed Systems. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science(), vol 9952. Springer, Cham. https://doi.org/10.1007/978-3-319-47166-2_62
Download citation
DOI: https://doi.org/10.1007/978-3-319-47166-2_62
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47165-5
Online ISBN: 978-3-319-47166-2
eBook Packages: Computer ScienceComputer Science (R0)