Nik Swamy, Synthesizing Verified Implementations of Web Services Security
Windows Communication Foundation (WCF) is a set of .NET technologies for building and running connected systems with a communications infrastructure built using web services. (In the most common case, you can think of web services as remote procedure calls over HTTP using XML as a message format.) In WCF, a web service can publish security policies which clients are expected to comply with in order to access the service. These security policies are inherently compositional and can rely on policies published by other services. The flexibility afforded by this facility, however, complicates both the intended meaning of a policy as well as the high-level security goals that a service wishes to enforce.
This talk presents work in progress to automatically synthesize verified client implemenations that comply with the security policies published by a service. The talk focuses primarily on giving a formal semantics to security policies in the style of a protocol narration. The semantics is given inductively to capture the compositional nature of policy. I will also describe ongoing work to state and verify security properties of the generated clients in the presence of an active attacker.