Issue No. 01 - January (2008 vol. 34)
We outline a methodology for designing and composing services in a secure manner. In particular, we are concerned with safety properties of service behaviour. Services can enforce security policies locally and can invoke other services respecting given security contracts. This call-by-contract mechanism offers a significant set of opportunities, each driving secure ways to compose services. We discuss how to correctly plan services compositions in several relevant classes of services and security properties. To this aim, we propose a graphical modelling framework, based on a foundational calculus called lambda-req. Our formalism features dynamic and static semantics, so allowing for formal reasoning about systems. Static analysis and model checking techniques provide the designer with useful information to assess and fix possible vulnerabilities.
Web services, call-by-contract, language-based security, static analysis, system verification
G. Ferrari, R. Zunino, P. Degano and M. Bartoletti, "Semantics-Based Design for Secure Web Services," in IEEE Transactions on Software Engineering, vol. 34, no. , pp. 33-49, 2007.