Samoa: Formal Tools for Securing Web Services

Established: May 16, 2003

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: A Cryptographic-Protocol Verifier for F#

    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 for WSE 3.0

    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 (for WSE 2.0)

    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.

    • Aaron Skonnard, PluralSight: “Very nice. We need more tools like this that facilitate authoring and analyzing service contracts, especially during design and development.”
    • Benjamin Mitchell, WSE expert: “In combination with the WSE Settings add-in the Policy Advisor provides a great service for anyone wanting to understand and apply policy files, without having to get too focused on the XML angle brackets.”
    • Savas Parastatidis, University of Newcastle “I too wanted to say how cool this tool is. I run it against a very old policy file I had written by hand for the secure version of the WS-GAF Registry service and it told me things that I had never imagined could have caused problems.”

    TulaFale: A Security Tool for Web Services

    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.

    • Bhargavan, C. Fournet, A. Gordon, and N. Swamy, Verified implementations of the Information Card federated identity-management protocol. In ACM Symposium on Information, Computer and Communication Security (ASIACCS’08), Tokyo, March 18-20, 2008.
    • Bhargavan, C. Fournet, and A. Gordon, Verified Reference Implementations of WS-Security Protocols. In 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006), pp88-106, Vienna, September 8-9, 2006. Volume 4184 of Springer LNCS, 2006.
    • Bhargavan, C. Fournet, A. Gordon, and S. Tse, Verified Interoperable Implementations of Security Protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW 2006), pp139-152, Venice, July 5-7, 2006. An extended version is available as Technical Report MSR-TR-2006-46, Microsoft Research, September 2007.
    • Bhargavan, C. Fournet, A. Gordon, and G. O’Shea, An Advisor for Web Services Security Policies. In 2005 ACM Workshop on Secure Web Services (SWS 2005), November 11, 2005.
    • Fournet, A. Gordon, and S. Maffeis, A Type Discipline for Authorization Policies. In 2005 European Symposium on Programming (ESOP 2005), pp141-156, April 6-8, 2005. An extended version is available as Technical Report MSR-TR-2005-01, Microsoft Research, September 2005.
    • Bhargavan, R. Corin, C. Fournet, and A. Gordon, Secure Sessions for Web Services. In 2004 ACM Workshop on Secure Web Services (SWS 2004), Washington DC, October 29, 2004.
    • Bhargavan, C. Fournet, and A. Gordon, Verifying Policy-Based Security for Web Services. In 2004 ACM Conference on Computer and Communications Security (CCS 2004), pp268-277, Washington DC, October 25-29, 2004. An extended version is available as Technical Report MSR-TR-2004-84, Microsoft Research, November 2005.
    • Bhargavan, C. Fournet, A. Gordon, and R. Pucella, TulaFale: A Security Tool for Web Services. In International Symposium on Formal Methods for Components and Objects (FMCO 2003), pp197-222, Leiden. Volume 3188 of Springer LNCS, Revised Lectures, 2004.
    • Bhargavan, C. Fournet, and A. Gordon, A Semantics for Web Services Authentication. In 2004 ACM Symposium on Principles of Programming Languages, pp198-209, Venice, January 14-16, 2004. An extended version is available as Technical Report MSR-TR-2003-83, Microsoft Research, February 2004. A journal version appears in Theoretical Computer Science 340(1):102-153 (June 2005).
    • Gordon and R. Pucella, Validating a web service security abstraction by typing. In 2002 ACM Workshop on XML Security, pp18-29, Fairfax VA, November 22, 2002. An extended version is available as Technical Report MSR-TR-2002-108, Microsoft Research, December 2002. A journal version appears in Formal Aspects of Computing 17:277-318, 2005.

  • Researchers

    • Karthik Bhargavan, Microsoft Research
    • Cédric Fournet, Microsoft Research

    Interns

  • Web Services and SOAP

    [2006-12-26] JSON vs XML as a data interchange format [2006-12-05] Lucovsky announces deprecation of Google’s SOAP Search API [2006-11-16] Amazon: utility computing power broker [2006-11-08] WS-Policy working draft [2006-05-04] Web Services for Management [2006-05-01] WS-I starts on Basic Profile 1.2, Basic Profile 2.0, and Reliable Secure Profile 1.0 [2006-03-15] Toward Converging Web Service Standards for Resources, Events, and Management [2006-02-16] Global Grid Forum and Enterprise Grid Alliance to merge [2005-12-31] Dilbert on Web services standards [2005-11-28] Paul Graham on Web 2.0 [2005-10-01] Slides from PDC 2005 [2005-09-26] Cool poster [2005-09-12] The LINQ Project [2005-08-22] Sabre replacing EDI with Web Services [2005-07-29] Garden Point Service Language GPSL [2005-07-28] UK ETF Report on GT4 [2005-07-26] Some EJB history from Ted Neward [2005-07-14] IDC: Web Services Consumption to Hit Stride [2005-06-23] Calling SOAP Servers from JS in Mozilla [2005-06-13] OC-SOAP – SOAP client for OCaml, using CDuce [2005-06-02] IBM, HP, CA: Management Using Web Services: A Proposed Architecture and Roadmap [2005-05-25] ICWS 2005 advance programme [2005-05-25] Web Services Competency Workshop in a Box [2005-04-27] Alternative software stacks for OGSA-based grids [2005-04-16] AJAX with J2EE [2005-02-10] Introducing Indigo: An Early Look [2005-02-04] Amazon Web Services in Scheme [2005-01-14] Real World Web Services [2004-12-08] W3C published WS-Addressing working draft [2004-12-07] Bosworth: Web services in the 21st century [2004-12-07] CNET: Web services patents fetch $15.5 million [2004-12-03] Don Box: a Universal Web Service [2004-12-03] The BPEL Book [2004-12-02] IBM CICS to support web services [2004-11-29] Sapir on the Personal Service Builder concept [2004-11-25] Web services patents for sale [2004-11-20] Bosworth talk on Collaboration, Customization, and Communication [2004-11-18] SoapMail refreshed for WSE2 [2004-11-16] Five New Financial Web Services [2004-11-11] Amazon offers WS-based message queues [2004-11-08] WS-Coordination, WS-AtomicTransaction, and WS-BusinessActivity specs refreshed [2004-11-04] NOAA’s National Weather Service [2004-11-01] Interview: Keith Ballinger on WSE [2004-10-13] LaMonica: EPL to complete with BPEL [2004-10-08] WS-Management [2004-09-18] Cabrera, Kurt, Box: “An Introduction to the Web Services Architecture and Its Specifications” [2004-09-15] WS-MetadataExchange [2004-09-08] SOAP-over-UDP [2004-09-03] WS-Policy refreshed [2004-08-31] WS-Eventing refreshed [2004-08-26] W3C CR Message Transmission Optimization Mechanism (MTOM) [2004-08-24] Amazon Web Services 4.0 [2004-08-24] WS-I Basic Profile 1.1 [2004-08-20] Devices Profile for Web Services refreshed [2004-08-10] WS-Addressing submitted to W3C [2004-07-26] Amazon: “We’ve just scratched the surface” [2004-07-06] WSJ: “SOA and Web Services Go Mobile, Nokia-Style” [2004-06-23] CNET: “eBay sold on web services” [2004-05-04] Jeff Schlimmer “A Technical Introduction to the Devices Profile for Web Services” [2004-04-05] Webber Parastatidis “Why WSDL Is Not Yet Another Object IDL” [2004-04-01] CNET: “Services-oriented architecture gains support” [2004-04-01] Pat Helland “Metropolis” [2004-03-30] WS-Addressing refreshed [2004-03-09] Reliable Messaging in a Service Oriented Architecture [2004-02-25] CNET: “Microsoft places bet on Whitehorse” [2004-02-17] Web Services Dynamic Discovery (WS-Discovery) Specification Released [2004-01-28] Coordinating Web Services Activities with WS-Coordination, WS-AtomicTransaction, and WS-BusinessActivity [2004-01-20] CNET: “Web services shakeout looming” [2004-01-20] Globus: “The WS-Resource Framework” [2004-01-14] Bob Sutor: “A Web services wish list” [2004-01-07] Forrester: “Ten tips for killer Web services” [2004-01-06] WS-Eventing: allows services to subscribe to or accept subscriptions for event notification messages [2003-12-31] CNET: “Web Services: 2003 in Review” [2003-12-22] BusinessWeek: “Reprogramming Amazon” [2003-12-19] CNET: “Amazon–the Web Services bellwether” [2003-12-08] CNET: “CA enters Web services management” [2003-11-20] MS & HP: slides for Gartner Application and Integration Conference [2003-11-18] OGSI.NET 2.0 announced [2003-11-07] MS & Vodafone: “Mobile Web Services Technical Roadmap” [2003-10-28] MIT ShuttleTrack web service [2003-10-27] Don Box: “A Guide to Developing and Running Connected Systems with Indigo” [2003-10-01] CACM 46(10) “Service Oriented Computing” [2003-09-30] Hao He: “What is Service-Oriented Architecture?” [2003-09-24] SOAP interface to microsoft.com [2003-08-26] Werner Vogels “Web Services are not Distributed Objects: Common Misconceptions about Service Oriented Architectures” [2003-08-12] Savas Parastatidis et al: “A Grid Application Framework based on Web Services Specifications and Practices (v1.0)” [2003-07-10] Applied XML Developers Conference 2003 West [2003-07-10] Panel: “Bill of Rights for Web Services” [2003-06-24] W3C: SOAP Version 1.2 [2003-06-17] WS-I testing tools for conformance to BP 1.0 [2003-06-09] Hull Benedikt Christophides Su “E-Services: A Look Behind the Curtain” [2003-05-22] CNET: Amazon updates Web services tool [2003-05-08] CNET: W3C brushes up SOAP standard [2003-04-01] Yasser Shohoud: “RPC/Literal and Freedom of Choice” [2003-03-01] ACM Queue: “A Conversation with Adam Bosworth” [2003-02-26] Frank Leymann: BTW2003 keynote [2003-02-05] Fifth Birthday of XML [2002-08-26] Serge Abiteboul: EDBT lectures [2002-07-15] W3C: WSDL Version 1.2 [2002-06-06] W3C: Web Service Description Usage Scenarios [2002-05-20] Sahai Graupner Kim “The Unfolding of the Web Services Paradigm ” [2002-04-30] Sam Ruby: “Google’s Genius” (on using SOAP) [2002-04-18] xmlhack: “Amazon goes REST, Google goes SOAP” [2001-04-04] Don Box: “A Brief History of SOAP” [2000-10-01] Steve Burbeck: “The Tao of e-business services” [2000-03-01] Don Box: “A Young Person’s Guide to SOAP” [1999-09-25] Dave Winer: “Dave’s History of SOAP” [1998-02-27] Dave Winer: “RPC over HTTP via XML”

    Web Services Security

    [2006-09-06] Invoking WSE 3.0 Secure Web Services from Windows Workflow Foundation [2006-06-19] Windows Live ID [2006-02-26] IBM/Novell pursuing Higgins Project as response to InfoCard [2006-02-20] OASIS members approve WS-Security 1.1 [2006-02-20] Security for REST Web Services [2006-02-16] CA address web services security [2006-01-23] WS authorization [2006-01-17] Policies in WSE3 [2006-01-09] Burton: Put Web services security on front burner [2005-12-22] PingSTS – An Early Preview [2005-12-20] Ping Identity has WS-Federation toolkit for Apache [2005-12-14] Scenarios, Patterns, and Implementation Guidance for Web Services Enhancements (WSE) 3.0 [2005-11-03] Sessions: Objects, Components, Web Services [2005-10-26] OASIS WS Secure Exchange TC formed [2005-10-05] WSE 3.0 October CTP released [2005-09-22] Kenai announce eXamineXT test tool for web services security [2005-09-09] MSN search APIs: can MS out-Google Google? [2005-09-06] IBM: securing SO apps [2005-08-01] Stamos/Stender: Attacking Web Services, Blackhat 2005 [2005-07-26] Black Hat edition of OWASP Guide [2005-07-26] Enterprise Grid Alliance identifies grid security risks [2005-07-14] Trust, SecureConversation, SecurityPolicy submitted to OASIS [2005-07-13] WS-SecurityPolicy (July 2005, version 1.1) [2005-07-11] DOS attack on web service [2005-07-11] Pen Test Tool – WSDigger [2005-06-27] RSS security? [2005-06-16] Securing Web Services with mod_security [2005-06-10] Vulnerability assessment tool for web services [2005-06-03] Microsoft WS-I Basic Security Profile 1.0 Sample Application [2005-06-03] WSE 3.0 June CTP [2005-06-01] UIUC AMPol project for web services security [2005-05-13] Web Single Sign-On Interoperability Profile [2005-05-12] Kim Cameron “Laws of Identity” [2005-05-12] Microsoft Identity Metasystem [2005-05-05] DIMACS Workshop on Security of Web Services and E-Commerce [2005-04-30] Vittorio Bertocci’s visual notation for WS-Security [2005-04-12] Liberty releases interfaces for ID-based web services [2005-03-28] Cisco planning XML device [2005-03-18] Routing Secured SOAP Messages Through Multiple SOAP Intermediaries Using WSE 2.0 [2005-03-15] OASIS ratifies long-awaited SAML 2.0 [2005-02-28] WS-SecureConversation refreshed [2005-02-28] WS-Trust refreshed [2005-02-26] SOAP is dead? [2005-02-17] XML Security Comes to the Fore at RSA [2005-02-11] Liberty Alliance Releases Second Version of Web Services Framework Specifications [2005-01-31] Securing the Username Token with WSE 2.0 [2004-12-24] Putting Policy in Charge [2004-12-06] OMII releases a web service infrastructure for building grid applications [2004-12-05] Sxip Networks: Reinventing Digital Identity [2004-12-03] WSE 2.0 SP2 Golden [2004-10-05] WS-SecureConversation/WS-Trust Interop Workshop [2004-09-17] SOAP inspection / tampering tools [2004-09-15] Nadalin: “WS-Security changing Web services landscape” ” [2004-09-02] ZDNet: “XML Web services security best practices” [2004-08-23] DDJ: “Web Services Ad Hoc Firewalls” [2004-08-18] Demchenko: “White collar” Attacks on Web Services and Grids [2004-08-13] New OASIS WSS TC draft profiles (SAML, REL, SwA, Kerberos, Minimalist) [2004-08-01] Don Smith: “WS-Security Drilldown in Web Services Enhancements 2.0” [2004-07-21] Kirk Allen Evans: “Using WSE 2.0 to Enable Interoperable Kerberos Authentication” [2004-07-20] O’Neill: “XML and Web Services: Are We Secure Yet?” [2004-07-19] eWeek: XML firewalls [2004-07-15] Web Services Firewall Forum XWall Released [2004-07-14] InternetNews: “Prevent a Web Services Insecurity Complex” [2004-07-02] ZapThink: “Implementing Secure Web Services in B2B Environments” [2004-06-24] Simon Johnston on model-driven security for SOA [2004-06-19] OWASP AppSec 2004 [2004-05-25] Bustamante: “Behold WSE 2.0: Removing Another Layer of WS-Pain” [2004-05-24] SOAP features added to MS ISA firewall [2004-05-03] PayPal releases Web Services APIs [2004-05-01] Forum XWALL for MS ISA Server datasheet [2004-04-07] OASIS Standardizes WS-Security [2004-03-29] CNET: “Extra headaches of securing XML” [2004-03-11] Teros: hardware support for WS-Security [2004-02-25] WS-I Publishes Web Services Security Interoperability Guidelines [2004-02-17] Line56: “Web Services Vulnerabilities” [2004-01-29] Panel at CMU West: “Web Services Security” [2004-01-27] OWASP Top Ten Vulnerabilities for 2004 [2004-01-19] Draft: Web Services Security: SOAP Message Security 1.0 [2004-01-04] ZapThink: “A Guide to Securing XML and Web Services” [2003-12-19] Web Services Security Kerberos Binding published [2003-11-26] eWeek: “Free Tools Speed Web-Services Security” [2003-11-24] NeSC: “Practical security for e-Science projects” [2003-11-20] WS-Trust/WS-SecureConversation Interop Workshop [2003-11-18] Faust: “SOAP Web Services Attacks – Introduction and Simple Injection” [2003-11-13] WS-Security from a SmartPhone [2003-11-12] CNET: “Liberty Alliance debuts new standard” [2003-10-31] 2003 ACM Workshop on XML Security [2003-10-01] Xiong, Helander, Forin, Yuval “Secure Invisible Computing” [2003-09-17] CNET: “Microsoft, IBM push Web services advances” [2003-09-17] IBM & MS: “Secure, Reliable, Transacted Web Services: Architecture and Composition” [2003-09-10] Forrester: “Web services standards to converge” [2003-08-27] OASIS: SOAP Message Security, Working Draft 17 [2003-07-16] CNET: “Microsoft bolsters Web services security” [2003-07-10] IBM & MS: “Federation of Identities in a Web Services World” [2003-05-03] CNET: “Passport to get Web services stamp” [2003-02-05] CNET: “Security key goal for Web services group” [2003-01-13] MSDN: “Securing Web Services with ISA Server” [2003-01-13] OWASP: “The Top Ten Web Application Security Vulnerabilities” [2003-01-01] White, Chon: “Wide Open on Port 80” [2002-12-16] InfoWorld: “Microsoft highlights security in Web services development pack” [2002-12-11] CNET: “XML encryption specs approved” [2002-11-22] 2002 ACM Workshop on XML Security [2002-10-15] Netegrity minding the Web services security store [2002-05-16] Slashdot: “XML Web Services & Security” [2002-04-07] IBM & MS: “Security in a Web Services World” [2002-03-16] Paul Prescod: “Some thoughts about SOAP versus REST on Security” [2001-12-28] Phrack: “RPC without borders (surfing USA …)” [2000-06-29] SOAP: “The future or a security nightmare” [2000-06-15] Bruce Schneier: “SOAP”

People

People

Portrait of Andy Gordon

Andy Gordon

Senior Principal Research Manager