Securely Taking On New Executable Stuff Of Uncertain Provenance

Workshop meeting agenda, 20 June 2008

[Workshop location and logistics]

Recall that the goal is to study whether it is possible to securely run software of uncertain provenance, improving the assurance and substantially reducing the cost of certifying security properties of mission-critical software systems. Questions of interest include:

The day will be structured mostly as short position statements from participants (10 minutes plus time for short questions), followed by longer discussion periods. It's important to keep position statements short so we have time for substantive discussions. Also, please think about the questions above in preparing your position statement.

MSR is also organizing a pre-STONESOUP meeting on June 19, noon–5:30pm, for those who would like to hear about what is going on at MSR. [June 19 schedule here]

Schedule, June 20

8:30–9:45 Introduction

This session will give an overview of the study goals and progress made thus far, including a description of the software assurance problem from the perspective of the government. We'll discuss the goals of the study.

8:30–8:40Welcome (Carl Landwehr)
8:40–9:25Preliminary study briefing (Andrew Myers)

Can we use hardware mechanisms such as virtual machine monitors and trusted platform modules to provide assurance? Are there opportunities to strengthen this assurance by exploiting program analysis or transformation?

10:00–12:00 Confinement: VMMs and TPMs

10:00–10:15 Flicker: An Execution Infrastructure for TCB Minimization (Mike Reiter)
10:15–10:30 The Caernarvon Security Model: Confinement of Malicious Code and Downloading of Trusted Code (Paul Karger)
10:30–10:45 STONESOUP thoughts (Monica Lam)
10:45–11:00 A Formally Verified Hardware Separation Kernel (Matthew Wilding)
11:00–12:00 Discussion

12:00–1:00 Lunch

Can we use operating-system mechanisms such as dynamic information flow and (software) virtual machines to provide assurance, and what security properties are enforced? What is the right dividing line for obtaining this assurance here vs. by program analysis or transformation?

1:00–2:15 Confinement: OS

1:00–1:15Singularity: Improving OS Architecture to improve Static Analysis (Galen Hunt)
1:15–1:30Operating Systems & Confinement (Eddie Kohler)
1:30–1:45Protection and Communication Abstractions for Web Browsers in MashupOS (Helen Wang)

Current commercial tools for finding bugs and vulnerabilities have come a long way and have been integrated into industrial development processes. How far can current approaches be pushed? Can these tools rely on dynamic enforcement mechanisms to fill in holes in assurance?

2:30–3:15 Tools

2:30–2:45 Every Time You Say "Tool" Some Marketing Person Somewhere Cries Out In Pain (Brian Chess)
2:45–3:00Windows Security Testing (Chris Walker)

Program analysis and transformation are appealing ways to obtain assurance. However, there are many challenges, such as dealing with concurrency and binary program representations. How far can this approach be pushed? Can dynamic mechanisms be used to fill in holes in assurance?

3:30–4:45 Analysis and verification

In closing, we want to identify promising directions for improving software assurance. Are there underexplored ideas or synergies between existing approaches? We also want to discuss what related approaches we haven't spent enough time looking at yet.

5:00–5:30 Wrap-up discussion


Tom Ball (MSR), Brian Chess (Fortify), Dawson Engler (Stanford), John Farrell (IARPA), Scott Field (Microsoft), Galen Hunt (MSR), Eddie Kohler (UCLA), Monica Lam (Stanford), Carl Landwehr (IARPA), Paul Karger (IBM), Greg Morrisett (Harvard), Andrew Myers (Cornell), Mike Reiter (UNC), Koushik Sen (Berkeley), Dawn Song (Berkeley), John Steven (Cigital), Konrad Vesey (CAS), Chris Walker (Microsoft), Helen Wang (MSR), Matthew Wilding (Rockwell Collins)