Abstract
Service Oriented Computing (SOC) is a programming paradigm aiming at characterising Service Networks. Services are entities waiting for clients requests and they often result from the composition of many services.
We address here the problem of statically guaranteeing security of open services, i.e. services with unknown components. Security constraints are expressed by local policies that service components must obey.
We present here a type and effect system that safely over-approximates, in the form of history expressions, the possible run-time behaviour of open services, collecting partial information on the behaviours of their components. From a history expression, we then extract a plan that drives executions that never rise security violations.
Finally, we show how partial plans satisfying security requirements can be put together to obtain a safe orchestration plan.
Work partially supported by EU-funded project ‘‘SENSORIA”, by EU-funded project ‘‘CONSEQUENCE” and by EU-funded project ‘‘CONNECT”.
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
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Fournet, C.: Access control based on execution history. In: NDSS (2003)
Bartoletti, M., Costa, G., Degano, P., Martinelli, F., Zunino, R.: Securing Java with local policies. Journal of Object Technology (JOT) (2008)
Bartolett, M., Degano, P., Ferrari, G.L.: History-based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 316–332. Springer, Heidelberg (2005)
Bartoletti, M., Degano, P., Ferrari, G.L.: Planning and verifying service composition. Journal of Computer Security (JCS) 17(5), 799–837 (2009); Abridged version In: Proc. 18th Computer Security Foundations Workshop (CSFW) (2005)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Secure service orchestration. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2007. LNCS, vol. 4677, pp. 24–74. Springer, Heidelberg (2007)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 32–47. Springer, Heidelberg (2007)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Local policies for resource usage analysis. ACM Trans. Program. Lang. Syst. 31(6), 1–43 (2009)
Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Model checking usage policies. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 19–35. Springer, Heidelberg (2009)
Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77–121 (1985)
Besson, F., Jensen, T.P., Le Métayer, D.: Model checking security properties of control flow graphs. Journal of Computer Security 9(3), 217–250 (2001)
Boreale, M., De Nicola, R.: A symbolic semantics for the pi-calculus. Inf. Comput. 126(1), 34–52 (1996)
Bravetti, M., Lanese, I., Zavattaro, G.: Contract-driven implementation of choreographies. In: Kaklamanis, C., Nielson, F. (eds.) TGC 2008. LNCS, vol. 5474, pp. 1–18. Springer, Heidelberg (2009)
Busi, N., Gorrieri, R., Guidi, C., Lucchi, R., Zavattaro, G.: Choreography and orchestration: A synergic approach for system design. In: Benatallah, B., Casati, F., Traverso, P. (eds.) ICSOC 2005. LNCS, vol. 3826, pp. 228–240. Springer, Heidelberg (2005)
Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5) (2009)
Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Sec. 4(1-2), 2–16 (2005)
Martinelli, F., Matteucci, I.: Synthesis of web services orchestrators in a timed setting. In: Dumas, M., Heckel, R. (eds.) WS-FM 2007. LNCS, vol. 4937, pp. 124–138. Springer, Heidelberg (2008)
Martinelli, F., Matteucci, I.: Synthesis of local controller programs for enforcing global security properties. In: ARES, pp. 1120–1127 (2008)
De Nicola, R., Hennessy, M.: Ccs without tau’s. In: Ehrig, H., Levi, G., Montanari, U. (eds.) TAPSOFT 1987. LNCS, vol. 249, Springer, Heidelberg (1987)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)
Skalka, C., Smith, S.F.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 107–128. Springer, Heidelberg (2004)
Winskel, G.: The formal semantics of programming languages. MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Costa, G., Degano, P., Martinelli, F. (2010). Modular Plans for Secure Service Composition. In: Armando, A., Lowe, G. (eds) Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security. ARSPA-WITS 2010. Lecture Notes in Computer Science, vol 6186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16074-5_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-16074-5_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16073-8
Online ISBN: 978-3-642-16074-5
eBook Packages: Computer ScienceComputer Science (R0)