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:
- What are the limits of what security properties we can determine with high assurance, from programs in various executable representations (source, binary, scripts), possibly accompanied by additional artifacts of construction?
- What security properties can be enforced by running programs in environments that constrain or confine their behavior?
- Are there opportunities to combine techniques from different layers (specification, analysis, testing, confinement, monitoring) to really strengthen software assurance? How can techniques from different layers be used most effectively in combination?
- What kind of assurance improvements can we get in the relatively near term?
- What kinds of approaches appear most fruitful in the longer term, assuming research investment?
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:40 | Welcome (Carl Landwehr) |
8:40–9:25 | Preliminary study briefing (Andrew Myers) |
9:25–9:45 | Discussion |
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:15 | Singularity: Improving OS Architecture to improve Static Analysis (Galen Hunt) |
1:15–1:30 | Operating Systems & Confinement (Eddie Kohler) |
1:30–1:45 | Protection and Communication Abstractions for Web Browsers in MashupOS (Helen Wang) |
1:45–2:15 | Discussion |
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:00 | Windows Security Testing (Chris Walker) |
3:00–3:15 | Discussion |
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
- 3:30–3:45 Directed Testing of Sequential and Concurrent Programs (Koushik Sen)
- 3:45–4:00 BitBlaze: Binary Analysis for Computer Security (Dawn Song)
- 4:00–4:15 Rootkits (Scott Field)
- 4:15–4:55 Discussion
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