Cryptographically verified implementations for TLS. With R. Corin, C. Fournet, and E. Zalinescu. In 15th ACM Conference on Computer and Communications Security (CCS'08), pages 459-468, Alexandria, Virginia, October 2008. ACM Press. Earlier versions of this work appeared at FCC 2007 and FCC 2008.

We intend to narrow the gap between concrete implementations of cryptographic protocols and their verified models. We develop and verify a small functional implementation of the Transport Layer Security protocol (\tls). We make use of the same executable code for interoperability testing against mainstream implementations, for automated symbolic cryptographic verification, and for automated computational cryptographic verification. We rely on a combination of recent tools, and we also develop a new tool for extracting computational models from executable code. We obtain strong security guarantees for TLS as used in typical deployments.

Refinement types for secure implementations. With J. Bengtson, C. Fournet, A.D. Gordon, and S. Maffeis. In 20th IEEE Computer Security Foundations Symposium (CSF 2008), pages 17-32, Pittsburgh, Pennsylvania, June 2008. IEEE Computer Society. An extended version of this paper appears as Technical Report MSR-TR-2008-118, Microsoft Research, September 2008.

We present the design and implementation of a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.

Service combinators for farming virtual machines. With A.D. Gordon and I. Narasamdya. In COORDINATION 2008, Oslo, June 4-6, 2008. Springer LNCS 5052:33-49. An extended version of this paper appears as Technical Report MSR-TR-2007-165, Microsoft Research, December 2007.

Management is one of the main expenses of running the server farms that implement enterprise services, and operator errors can be costly. Our goal is to develop type-safe programming mechanisms for combining and managing enterprise services, and we achieve this goal in the particular setting of farms of virtual machines. We assume each server is service-oriented, in the sense that the services it provides, and the external services it depends upon, are explicitly described in metadata. We describe the design, implementation, and formal semantics of a library of combinators whose types record and respect server metadata. We describe a series of programming examples run on our implementation, based on existing server code for order processing, a typical data centre workload.

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. With C. Fournet, A.D. Gordon, and N. Swamy.

We describe reference implementations for selected configurations of the user authentication protocol defined by the Information Card Profile V1.0. Our code can interoperate with existing implementations of the client, identity provider, and relying party roles of the protocol. We derive formal proofs of security properties for our code using an automated theorem prover. Hence, we obtain the most substantial examples of verified implementations of cryptographic protocols to date, and the first for any federated identity-management protocols. Moreover, we present a tool that downloads security policies from services and token servers and compiles them to a verifiably secure client proxy.

Secure Implementations of Typed Session Abstractions. With R. Corin, P-M. Deniélou, C. Fournet, and J.J. Leifer, in 20th IEEE Computer Security Foundations Symposium (CSF20), pages 170--186. July 2007.

Distributed applications can be structured as parties that exchange messages according to some pre-arranged communication patterns. These sessions (or contracts, or protocols) simplify distributed programming: when coding a role for a given session, each party just has to follow the intended message flow, under the assumption that the other parties are also compliant. In an adversarial setting, remote parties may not be trusted to play their role. Hence, defensive implementations also have to monitor one another, in order to detect any deviation from the assigned roles of a session. This task involves low-level coding below session abstractions, thus giving up most of their benefits. We explore language-based support for sessions. We extend the ML language with session types that express flows of messages between roles, such that well-typed programs always play their roles. We compile session type declarations to cryptographic communication protocols that can shield programs from any low-level attempt by coalitions of remote peers to deviate from their roles. Our main result is that, when reasoning about programs that use our session implementation, one can safely assume that all session peers comply with their roles---without trusting their remote implementations.

Getting operations logic right: types, service-orientation, and static analysis. With A.D. Gordon. Position paper for the Workshop on The Rise and Rise of the Declarative Datacentre, MSR Cambridge, May 12-13, 2008.

The human operators of datacentres work from a manual, sometimes known as the run book, that lists how to perform operating procedures such as the provisioning, deployment, monitoring, and upgrading of servers. To improve failure and recovery rates, it is attractive to replace human intervention by software, known as operations logic, that automates such operating procedures. We advocate a declarative programming model for operations logic, and the use of static analysis to detect programming errors, such as the potential for misconfiguration.

The Rise and Rise of the Declarative Datacentre. Co-editor with A.D. Gordon, T. Harris, and P. Toft. Appears as Technical Report TR-2008-61, Microsoft Research, May 2008. Position Papers from the Workshop on The Rise and Rise of the Declarative Datacentre, MSR Cambridge, May 12-13, 2008.

Verified reference implementations of WS-Security protocols. With C. Fournet and A.D. Gordon. In 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006), Vienna, September 8-9, 2006.  Springer LNCS 4184:88-106.

We describe a new reference implementation of the web services security specifications. The implementation is structured as a library in the functional programming language F#. Applications written using this library can interoperate with other compliant web services, such as those written using Microsoft WSE and WCF frameworks. Moreover, the security of such applications can be automatically verified by translating them to the applied pi calculus and using an automated theorem prover. We illustrate the use of our reference implementation through examples drawn from the sample applications included with WSE and WCF. We formally verify their security properties. We also experimentally evaluate their interoperability and performance.

Verified interoperable implementations of security protocols. With C. Fournet, A.D. Gordon, and S. Tse. In 19th IEEE Computer Security Foundations Workshop (CSFW 2006), pages 139-152, Venice, July 5-7, 2006. IEEE Computer Society. An extended version of this paper appears as Technical Report MSR-TR-2006-46, Microsoft Research, September 2007.

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic cryptographic libraries. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.

Policy Advisor for WSE 3.0. With C. Fournet and A.D. Gordon. In Web Service Security: Scenarios, patterns, and implementation guidance for Web Services Enhancements (WSE) 3.0. Pages 324-330.  Microsoft Press, 2006. [Amazon] [MSDN]

An advisor for web services security policies. With C. Fournet, A.D. Gordon, and G. O'Shea. In 2005 ACM Workshop on Secure Web Services (SWS 2005), Fairfax, VA, USA.  Pages 1-9.  ACM Press, 2005.

We identify common security vulnerabilities found during security reviews of web services with policy-driven security. We describe the design of an advisor for web services security configurations, the first tool both to identify such vulnerabilities automatically and to offer remedial advice. We report on its implementation as a plugin for Microsoft Web Services Enhancements (WSE).

Secure sessions for web services. With R. Corin, C. Fournet, and A.D. Gordon. In 2004 ACM Workshop on Secure Web Services (SWS 2004), Washington DC. ACM Press, 2004.

WS-Security provides basic means to secure SOAP traffic, one envelope at a time. For typical web services, however, using WS-Security independently for each message is rather inefficient; besides, it is often important to secure the integrity of a whole session, as well as each message.  To these ends, recent specifications provide further SOAP-level mechanisms. WS-SecureConversation introduces security contexts, which can be used to secure sessions between two parties.  WS-Trust specifies how security contexts are issued and obtained.  We develop a semantics for the main mechanisms of WS-Trust and WS-SecureConversation, expressed as a library for TulaFale, a formal scripting language for security protocols.  We model typical protocols relying on these mechanisms, and automatically prove their main security properties.  We also informally discuss some limitations of these specifications.

Verifying policy-based security for web services. With C. Fournet and A.D. Gordon. In 2004 ACM Conference on Computer and Communication Security (CCS 2004), pages 268-277, Washington DC. ACM Press, 2004.  An extended version of this paper appears as Technical Report MSR-TR-2004-84, Microsoft Research, November 2005.

WS-SecurityPolicy is a declarative configuration language for driving web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy, and propose a more abstract link language for specifying the security goals of web services and their clients. Hence, we present the architecture and implementation of fully automatic tools that (1) compile policy files from link specifications, and (2) verify by invoking a theorem prover whether a set of policy files run by any number of senders and receivers correctly implements the goals of a link specification, in spite of active attackers. Policy-driven web services implementations are prone to the usual subtle vulnerabilities associated with cryptographic protocols; our tools help prevent such vulnerabilities, as we can verify policies when first compiled from link specifications, and also re-verify policies against their original goals after any modifications during deployment.

A formalism for consistency and partial replication. With M. Shapiro, Y. Chong, and Y. Hamadi. Technical Report MSR-TR-2004-58, Microsoft Research, June 2004.

Replication protocols are complex and it is difficult to compare their consistency properties. To this effect, we propose a formalism where a replica executes actions subject to constraints in its local view or multilog. Schedules are selected non-deterministically from the set of sound schedules. This set grows with the number of actions and shrinks as the number of constraints increases. If the size of the set is one, the site has converged; if the size becomes zero, the site has detected an unrecoverable conflict. If every site runs the same schedule, they are consistent. We formalise this intuitive concept of consistency in four different ways, which generalise classical consistency criteria and which expose different aspects of consistency protocols. We prove them equivalent. We provide the first formal definition of consistency for partially replicated data. In general, achieving consistency entails global consensus; we exhibit sufficient conditions for deciding locally and derive a new decentralised protocol. In a separate technical report we prove the consistency of some published consistency protocols; this underscores the deep commonalities between them.

The Actions-Constraints approach to replication: Definitions and proofs. With M. Shapiro. Technical Report MSR-TR-2004-14, Microsoft Research, March 2004.

Replicated information raises the major issue of consistency. We have developped a simple, formal framework, in order to better understand and compare consistency properties of replication protocols. The framework is both formal and implementable. Our language is simple enough to prove interesting properties, yet sufficiently powerful to specify diverse systems. In our model, each site maintains its local view of data, of actions to execute, and of the constraints that define legal execution schedules. Adding actions increases the number of possible schedules; adding constraints reduces scheduling non-determinism. We exhibit significant subsets of actions that are progressively more determined and show a number of useful properties. The system is consistent if every action is eventually scheduled and local executions converge. We compare different possible formulations of the consistency property and prove them to be mutually equivalent. This underscores the deep commonalities between diverse protocols. One of our formulations can be used to characterise consistency in partially replicated systems, i.e., where a site has visibility of only a subset of data, actions and constraints. Finally, we show how a number of protocols from the literature are modeled in the action-constraint framework.

TulaFale: A security tool for web services. With C. Fournet, A.D. Gordon, and R. Pucella. In Formal Methods for Components and Objects (FMCO 2003), Springer LNCS 3188:197-222, 2004.

Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for writing complementary machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language 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 properties of SOAP protocols.

A semantics for web services authentication. With C. Fournet and A.D. Gordon. In Conference Record of POPL 2004 The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 198-209, ACM Press, 2004.  An extended version of this paper appears 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).

We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Security describes a range of XML security tokens, such as username tokens, public-key certificates, and digital signature blocks, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these tokens, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security tokens and of sample protocols distributed with the WSE implementation of WS-Security.  By embedding our data model within Abadi and Fournet's applied pi calculus, we formulate and prove security properties with respect to the standard Dolev-Yao threat model.  Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format.