An interesting project from Microsoft's Research Labs in Cambridge, UK - Project Samoa is exploring ways to use formal methods proofs to validate the security and integrity of Web Services protocols.
An XML web service is, to a first approximation, a wide-area RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. Applications exist on the internet (for programmatic access to search engines and retail), on intranets (for enterprise systems integration), and are emerging between intranets (for the e-science Grid and for e-business). Specifications (such as WS-Security, now at OASIS) and early toolkits (such as Microsoft's WSE product) exist for securing web services by applying cryptographic transforms to SOAP envelopes.
The underlying principles, and indeed the difficulties, of using cryptography to secure RPC protocols have been known for many years, and there has been a sustained and successful effort to devise formal methods for specifying and verifying the security goals of such protocols. One line of work, embodied in the spi calculus of Abadi and Gordon and the applied pi calculus of Abadi and Fournet, has been to represent protocols as symbolic processes, and to apply techniques from the theory of the pi calculus, including equational reasoning, type-checking, and resolution theorem-proving, to attempt to verify security properties such as confidentiality and authenticity, or to uncover bugs.
The goal of the Samoa Project is to exploit recent theoretical advances in the analysis of security protocols in the practical setting of XML web services. Some early outcomes of this research include an implementation of declarative security attributes for web services and the design of a logic-based approach to checking SOAP-based protocols.
This is yet another example of how Microsoft is trying really hard to increase the security of its software and products - in this case by investigating whether there are ways to detect security holes in the protocols and messages themselves.
All content is
Copyright (c) 2010 Jorgen Thelin. All rights reserved.
The opinions expressed here represent my own views and not necessarily those of my current, prior or future employer(s).
Content is provided "as-is", without any representations or warrenties of any kind.
Contents of the Weblog Feed are licensed under a Creative Commons License.