The Third Microsoft Research Security Workshop will be held in Hamburg, Germany on the 15th and 16th of March, 2006. Following in the tradition of previous workshops [1, 2], the goal of this workshop is to bring together security experts from Microsoft Research, Microsoft Corporation and leading experts from academia and industry to discuss and debate future areas of security research and application.

Overview

The workshop will focus on current developments in the design and analysis of IT systems and applications intended to meet higher levels of security assurance. This agenda has been put forward as early as 1972 (in the Anderson report) and has been a challenge to the developers of IT systems ever since. While the challenge may thus be an old one, its nature keeps changing with the applications IT systems are expected to support. The talks in this workshop will cast light on current security challenges, on methodologies being developed to address those challenges, and on the transfer of concepts from security research to concrete applications.

Program chair

Dieter Gollmann, Hamburg University of Technology

Speakers

• Tuomas Aura, Microsoft Research
• Karthik Bhargavan, Microsoft Research
• Andrew Birrell, Microsoft Research
• Manuel Costa, Microsoft Research
• Caspar Bowden, Microsoft
• Cedric Fournet, Microsoft Research
• Brian LaMacchia, Microsoft
• John Manferdelli, Microsoft
• Wolfram Schulte, Microsoft Research

Agenda

14th March (Tuesday)

15th March (Wednesday)

16th March (Thursday)

Abstracts

Detecting personally identifiable information (PII) leaks in electronic documents

Sometimes, it is necessary to remove author names and other personally identifiable information (PII) from documents before publication. In this talk, I will describe a novel defensive tool for detecting such data. I will also explain the lessons we learned about where PII may be stored in documents and how it is put there. A key observation is that user and machine identifiers are not embedded in documents only by a single piece of software, such as a word processor, but various tools used at different stages of the document authoring process. Thus, control of the entire document lifecycle is needed to ensure that no private data is leaked.

Singularity

Singularity is a research project focused on the construction of dependable systems through innovation in the areas of systems, languages, and tools. We are building a research operating system prototype (called Singularity), extending programming languages, and developing new techniques and tools for specifying and verifying program behaviour. Advances in languages, compilers, and tools open the possibility of significantly improving software. For example, Singularity uses type-safe languages and an abstract instruction set to enable what we call Software Isolated Processes (SIPs). SIPs provide the strong isolation guarantees of OS processes (isolated object space, separate GCs, separate runtimes) without the overhead of hardware-enforced protection domains. In the current Singularity prototype SIPs are extremely cheap; they run in ring 0 in the kernel’s address space. Singularity uses these advances to build more reliable systems and applications. For example, because SIPs are so cheap to create and enforce, Singularity runs each program, device driver, or system extension in its own SIP. SIPs are not allowed to share memory or modify their own code. As a result, we can make strong reliability guarantees about the code running in a SIP. We can verify much broader properties about a SIP at compile or install time than can be done for code running in traditional OS processes. Broader application of static verification is critical to predicting system behaviour and providing users with strong guarantees about reliability.

Dependable system programming in Sing#

Sing# is the source language and compiler for the Singularity project. Singularity focuses on the construction of dependable operating systems and applications through innovation in the areas of operating systems, programming languages, and tools. Sing# is an experimental extension of C# (in fact of Spec#) that supports features required for writing operating systems code as well as application code running on Singularity. The main novel feature of Sing# is support for message passing in the form of channel contracts and channel operations, such as blocking message receipt patterns. Additionally, the language supports explicit, but compile-time checked, memory management. This enables efficient transfer of data between communicating processes without copying, yet without the drawbacks or errors associated with shared memory. For more information consult the Singularity project website.

Design rationale behind the Identity Metasystem architecture

Many of the problems facing the Internet today stem from the lack of a widely deployed, easily understood, secure identity solution. Microsoft’s “InfoCard” project and the Identity Metasystem vision underlying it are aimed at filling this gap using technology all can adopt and solutions all can endorse, putting users in control of their identity interactions on the Internet. The design decisions presented in this paper are intended to result in a widely accepted, broadly applicable, inclusive, comprehensible, privacy-enhancing, security-enhancing identity solution for the Internet. We present them and the rationale behind them to facilitate review of these design decisions by the security, privacy, and policy communities, so that people will better understand Microsoft’s implementations, and to help guide others when building interoperating implementations.

Verified interoperable implementations of security protocols

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# and verify them by compilation to ProVerif. We establish the correctness of our approach for a range of security properties, illustrated on simple protocol examples.

Verifying web services security

Based on joint work with K. Bhargavan and C. Fournet Microsoft Research, Cambridge.
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 standardized at OASIS) and toolkits (such as Microsoft’s WSE product and the upcoming Windows Communication Foundation) exist for securing web services by applying cryptographic transforms to SOAP envelopes.
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. This talk will present some important web services security protocols and discuss both their traditional and novel aspects that make them an interesting and challenging target for formal verification.

On the Evolution of Adversary Models - from the Beginning to Sensor Networks

Invariably, new technologies introduce new vulnerabilities which often enable new attacks by increasingly potent adversaries. Yet new systems are more adept at handling well-known attacks by old adversaries than anticipating new ones. Our adversary models seem to be perpetually out of date: often they do not capture adversary attacks and sometimes they address attacks rendered impractical by new technologies.
In this talk, I provide a brief overview of adversary models beginning with those required by program and data sharing technologies ('60-'70s), continuing with those required by computer communication and networking technologies ('70s-'90s), and ending with those required by and sensor network technologies ('00s ->). I argue that sensor, ad-hoc, and mesh networks require new models, different from those in common use, namely those of the Dolev-Yao and Byzantine adversaries. I illustrate this with adversaries that attack perfectly sensible and otherwise correct protocols of sensor networks. These attacks cannot be countered with traditional security protocols using end-to-end design arguments and require emergent security properties as countermeasures.

Moore's Law, thermodynamics and security

Computer hardware will change over the next 5 years with the advent of many-core CPU’s in traditional PCs client and sever form factors as well as a proliferation of many “cool” distributed, programmable devices. I will talk about the programming challenges of the new environment and the implications for security including device security, intra-machine isolation, “high MIPs” applications like grids and “low MIPS” handheld devices. I’ll talk about additional potential vulnerabilities introduced by asynchrony and delegation models on these devices.

.NET Framework Security: Lessons learned from 5 years of shipping partially-trusted code

A little over five years ago Microsoft introduced the .NET Framework, a cross-language programming environment that includes a constrained execution model for mobile code (a.k.a "partially-trusted code"). In this talk I'll share some of the lessons we learned since then by observing developers, administrator and end-users working with partially-trusted code. I'll also discuss new language features and code analysis tools for partial-trust development that were added to the most recent version of the .NET Framework based on feedback from version 1 customers. Although developed in the context of the .NET Framework, our observations are applicable to other execution environments that depend on type safety, stack inspection and trust management systems for enforcing isolation and security policies.

Vigilante: End-to-end containment of internet worms

Worm containment must be automatic because worms can spread too fast for humans to respond. Recent work has proposed network-level techniques to automate worm containment; these techniques have limitations because there is no information about the vulnerabilities exploited by worms at the network level. We propose Vigilante, a new end-to-end approach to contain worms automatically that addresses these limitations. Vigilante relies on collaborative worm detection at end hosts, but does not require hosts to trust each other. Hosts run instrumented software to detect worms and broadcast self-certifying alerts (SCAs) upon worm detection. SCAs are proofs of vulnerability that can be inexpensively verified by any vulnerable host. When hosts receive an SCA, they generate filters that block infection by analysing the SCA-guided execution of the vulnerable software. We show that Vigilante can automatically contain fast-spreading worms that exploit unknown vulnerabilities without blocking innocuous traffic.

Participation

Participation is by invitation only and will be limited to approximately 100 academics to maintain the quality of the interaction. An important part of the workshop is the opportunity to meet in an informal setting with ample time for discussion and debate. If you are interested in attending, please contact Dieter Gollmann (diego ‘at’ tu-harburg.de) with a short position statement connecting your research interests with the major topics of the workshop. Places will be allocated on a first come first served basis until exhausted or the 1st March, 2006.

Participants have to cover the cost of their own travel and hotel expenses (some hotel rooms in central Hamburg will be reserved. Journey time from the central railway station to Harburg Rathaus is 15 minutes with trains every 10 minutes).

There is no charge for attending the workshop and its social functions.

Venue

The workshop will be hosted in the Audimax II, located in Building I on the campus of the Hamburg University of Technology. Hamburg is a major commercial centre in Northern Europe, with a flourishing container port at its core. Hamburg University of Technology is a young academic institution founded in 1978, located in Hamburg-Harburg across the estuary from the city centre.

The conference reception will be held at the Museum für Völkerkunde Hamburg, Rothenbaumchaussee 64, 20148 Hamburg.

Hamburg international airport, located in the north-west of Hamburg, has direct connections to most major European cities. The city centre and Harburg can be reached by public transport. Flights with RyanAir service Lübeck airport, about 60 km from Hamburg. There is a bus shuttle from Lübeck airport to the central bus terminal (ZOB) in Hamburg, connecting directly with arriving and departing flights. Hamburg-Harburg has its own railway station on the German Intercity network.

Previous Security Workshops

• Cambridge, UK: 4–6 November 2002
• Cologne, Germany: 2–4 June 2004

The presentations from the previous workshops are available at these URLs.