Advertisement

Secure Service Orchestration

  • Massimo Bartoletti
  • Pierpaolo Degano
  • Gian Luigi Ferrari
  • Roberto Zunino
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4677)

Abstract

We present a framework for designing and composing services in a secure manner. Services can enforce security policies locally, and can invoke other services in a “call-by-contract” fashion. This mechanism offers a significant set of opportunities, each driving secure ways to compose services. We discuss how to correctly plan service orchestrations in some relevant classes of services and security properties. To this aim, we propose both a core functional calculus for services and a graphical design language. The core calculus is called λ req  [10]. It features primitives for selecting and invoking services that respect given behavioural requirements. Critical code can be enclosed in security framings, with a possibly nested, local scope. These framings enforce safety properties on execution histories. A type and effect system over-approximates the actual run-time behaviour of services. Effects include the actions with possible security concerns, as well as information about which services may be selected at run-time. A verification step on these effects allows for detecting the viable plans that drive the selection of those services that match the security requirements on demand.

Keywords

Security Policy Finite State Automaton Typing Judgment Type Safety Request Type 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abadi, M., Fournet, C.: Access control based on execution history. In: Proc. 10th Annual Network and Distributed System Security Symposium (2003)Google Scholar
  2. 2.
    Atkinson, B., et al.: Web Services Security (WS-Security) (2002), http://www.oasis-open.org
  3. 3.
    Banerjee, A., Naumann, D.A.: History-based access control and secure information flow. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, Springer, Heidelberg (2005)Google Scholar
  4. 4.
    Barendregt, H.P., et al.: Term graph rewriting. In: Parallel Languages on PARLE: Parallel Architectures and Languages Europe (1987)Google Scholar
  5. 5.
    Bartoletti, M., Degano, P., Ferrari, G.L.: History based access control with local policies. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, Springer, Heidelberg (2005)Google Scholar
  6. 6.
    Bartoletti, M., Degano, P., Ferrari, G.L.: Planning and verifying service composition. Technical Report TR-07-02, Dip. Informatica, Univ. of Pisa. (to appear in Journal of Computer Security, 2007), http://compass2.di.unipi.it/TR/Files/TR-07-02.pdf.gz
  7. 7.
    Bartoletti, M., Degano, P., Ferrari, G.L., Zunino, R.: Types and effects for resource usage analysis. In: Proc. Foundations of Software Science and Computation Structures (Fossacs) (to appear, 2007)Google Scholar
  8. 8.
    Bartoletti, M., Degano, P., Ferrari, G.L.: Enforcing secure service composition. In: Proc. 18th Computer Security Foundations Workshop (CSFW) (2005)Google Scholar
  9. 9.
    Bartoletti, M., Degano, P., Ferrari, G.L.: Plans for service composition. In: Workshop on Issues in the Theory of Security (WITS) (2006)Google Scholar
  10. 10.
    Bartoletti, M., Degano, P., Ferrari, G.L.: Types and effects for secure service orchestration. In: Proc. 19th Computer Security Foundations Workshop (CSFW) (2006)Google Scholar
  11. 11.
    Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science, 37 (1985)Google Scholar
  12. 12.
    Besson, F., de Grenier de Latour, T., Jensen, T.: Interfaces for stack inspection. Journal of Functional Programming 15(2) (2005)Google Scholar
  13. 13.
    Bhargavan, K., Corin, R., Fournet, C., Gordon, A.D.: Secure sessions for web services. In: Proc. ACM Workshop on Secure Web Services (2004)Google Scholar
  14. 14.
    Bhargavan, K., Fournet, C., Gordon, A.D.: A semantics for web services authentication. In: Proc. ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2004)Google Scholar
  15. 15.
    Bhargavan, K., Fournet, C., Gordon, A.D.: Verified reference implementations of WS-security protocols. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Computer Security Foundations Workshop (CSFW) (2001)Google Scholar
  17. 17.
    Bonelli, E., Compagnoni, A., Gunter, E.: Typechecking safe process synchronization. In: Proc. Foundations of Global Ubiquitous Computing. ENTCS, vol. 138(1) (2005)Google Scholar
  18. 18.
    Boreale, M., et al.: SCC: a service centered calculus. In: Bravetti, M., Núñez, M., Zavattaro, G. (eds.) WS-FM 2006. LNCS, vol. 4184, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Brogi, A., Canal, C., Pimentel, E.: Behavioural types and component adaptation. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, Springer, Heidelberg (2004)Google Scholar
  20. 20.
    Bruni, R., Melgratti, H., Montanari, U.: Theoretical foundations for compensations in flow composition languages. In: Proc. of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of programming languages (POPL) (2005)Google Scholar
  21. 21.
    Carbone, M., Honda, K., Yoshida, N.: Structured global programming for communicating behaviour. In: European Symposium in Programming Languages (ESOP) (to appear, 2007)Google Scholar
  22. 22.
    Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proc. 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2000)Google Scholar
  23. 23.
    Van der Aalst, W., ter Hofstede, A., Kiepuszewski, B., Barros, A.: Workflow patterns. Distributed and Parallel Databases 14(1) (2003)Google Scholar
  24. 24.
    Edjlali, G., Acharya, A., Chaudhary, V.: History-based access control for mobile code. In: Vitek, J. (ed.) Secure Internet Programming. LNCS, vol. 1603, Springer, Heidelberg (1999)CrossRefGoogle Scholar
  25. 25.
    Esparza, J.: On the decidability of model checking for several μ-calculi and Petri nets. In: Tison, S. (ed.) CAAP 1994. LNCS, vol. 787, Springer, Heidelberg (1994)CrossRefGoogle Scholar
  26. 26.
    Ferrari, G.L., Guanciale, R., Strollo, D.: JSCL: A middleware for service coordination. In: Najm, E., Pradat-Peyre, J.F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  27. 27.
    Fong, P.W.: Access control by tracking shallow execution history. In: IEEE Symposium on Security and Privacy (2004)Google Scholar
  28. 28.
    Garcia-Molina, H., Salem, K.: Sagas. In: Proc. ACM SIGMOD, ACM Press, New York (1987)Google Scholar
  29. 29.
    Gifford, D.K., Lucassen, J.M.: Integrating functional and imperative programming. In: ACM Conference on LISP and Functional Programming (1986)Google Scholar
  30. 30.
    Gordon, A., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: Proc. IEEE Computer Security Foundations Workshop (CSFW) (2002)Google Scholar
  31. 31.
    Gorla, D., Hennessy, M., Sassone, V.: Security policies as membranes in systems for global computing. Logical Methods in Computer Science 1(3) (2005)Google Scholar
  32. 32.
    Guidi, C., Lucchi, R., Gorrieri, R., Busi, N., Zavattaro, G.: SOCK: A calculus for service oriented computing. In: Dan, A., Lamersdorf, W. (eds.) ICSOC 2006. LNCS, vol. 4294, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  33. 33.
    Honda, K., Vansconcelos, V., Kubo, M.: Language primitives and type discipline for structures communication-based programming. In: Hankin, C. (ed.) ESOP 1998 and ETAPS 1998. LNCS, vol. 1381, Springer, Heidelberg (1998)CrossRefGoogle Scholar
  34. 34.
    Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2002)Google Scholar
  35. 35.
    Lapadula, A., Pugliese, R., Tiezzi, F.: A calculus for orchestration of web services. In: European Symposium in Programming Languages (ESOP) (to appear, 2007)Google Scholar
  36. 36.
    Lazovik, A., Aiello, M., Gennari, R.: Encoding requests to web service compositions as constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, Springer, Heidelberg (2005)CrossRefGoogle Scholar
  37. 37.
    Marriott, K., Stuckey, P.J., Sulzmann, M.: Resource usage verification. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, Springer, Heidelberg (2003)Google Scholar
  38. 38.
    Misra, J.: A programming model for the orchestration of web services. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004) (2004)Google Scholar
  39. 39.
    Nielson, F., Nielson, H.R.: Type and effect systems. In: Correct System Design (1999)Google Scholar
  40. 40.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)zbMATHGoogle Scholar
  41. 41.
    Schneider, F.B.: Enforceable security policies. ACM Transactions on Information and System Security (TISSEC) 3(1) (2000)Google Scholar
  42. 42.
    Sewell, P., Vitek, J.: Secure composition of untrusted code: box-π, wrappers and causality types. Journal of Computer Security 11(2) (2003)Google Scholar
  43. 43.
    Skalka, C., Smith, S.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, Springer, Heidelberg (2004)Google Scholar
  44. 44.
    Talpin, J.P., Jouvelot, P.: The type and effect discipline. Information and Computation 2(111) (1994)Google Scholar
  45. 45.
    Toma, I., Foxvog, D.: Non-functional properties in Web Services. WSMO Deliverable (2006)Google Scholar
  46. 46.
    Vallecillo, A., Vansconcelos, V., Ravara, A.: Typing the behaviours of objects and components using session types. In: Proc. of FOCLASA (2002)Google Scholar
  47. 47.
    Winskel, G.: The Formal Semantics of Programming Languages. The MIT Press, Cambridge (1993)zbMATHGoogle Scholar
  48. 48.
    Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: IEEE Symposium on Security and Privacy (1993)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Massimo Bartoletti
    • 1
  • Pierpaolo Degano
    • 1
  • Gian Luigi Ferrari
    • 1
  • Roberto Zunino
    • 1
  1. 1.Dipartimento di Informatica, Università di Pisa 

Personalised recommendations