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.
FS2PV is a verification tool that compiles cryptographic-protocol implementations in a first-order subset of F# to a formal pi-calculus model. This pi-calculus model then can be analyzed using ProVerif to prove the desired security properties or to find security flaws. A blog entry explains the results of running FS2PV on a sample protocol.
Policy Advisor is a security tool shipped in November 2005 as part of Web Services Enhancements 3.0 for Microsoft .NET (WSE 3.0). See the WSE 3.0 readme, the Policy Advisor documentation, and the Microsoft patterns and practices guide Web Service Security: Scenarios, Patterns, and Implementation Patterns for Web Services Enhancements 3.0. Policy Advisor examines the configuration and policy files for one or more WSE endpoints, highlights typical security risks, and provides some remedial advice. Moreover, it summarizes the associated trace files (when present), showing message flows between endpoints. This version is implemented as an XSL transform. Jason Hogg discusses and demonstrates the WSE 3.0 and the Policy Advisor in his MSDN Architecture Webcast on Web Services Security Patterns, (March 16, 2006).
WSE Policy Advisor is a security plug-in for Web Services Enhancements 2.0 for Microsoft .NET (WSE). It can be invoked either from the WSE Configuration Editor or as a stand-alone tool. It examines the policy files that configure WSE, summarizes their security properties, highlights typical security risks, and provides some remedial advice. Ensure you have installed SP2 or SP3 of WSE 2.0 before attempting to install WSE Policy Advisor. A paper listed in the next section describes the advisor in detail.
TulaFale is a new specification language for writing machine-checkable descriptions of SOAP-based security protocols and their properties. TulaFale is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs Blanchet's resolution-based protocol verifier. Hence, we can automatically verify authentication and secrecy properties of SOAP protocols.
|
|