Workshop meeting schedule, 9 May 2008

• 9:00–9:30 Introduction (Andrew Myers, Carl Landwehr)
• 9:30–9:45 Discussion

• The goal of this session is to learn about how the government currently certifies different kinds of software, and how current efforts are attempting to improve this.

  10:00–12:00 Current certification processes.

  • 10:05–10:30 High-assurance (Type 1) certification processes (Mike Dransfield)
    
  • 10:30–10:55 Measuring software assurance properties: Thoughts on the future (Kris Britton, CAS)
    
  • 10:55–11:20 Accreditation (TBA)
    
  • 11:20–11:45 CAS certification efforts (Konrad Vesey)
    
  • 11:45–12:00 Discussion
    

• 12:00–1:00 Lunch

• What is the state of the art in program analysis and program verification relevant to this study? Are fundamental limits to what can be achieved? How should these methods be used as part of a larger assurance mechanism?

  1:00–2:15 Analysis and verification.

  • Tom Ball, Microsoft Research
  • Peter Lee, CMU
  • Benjamin Pierce, U. Penn
  • Discussion

• This session examines how methods for annotating programs with types, specifications, or other annotations can be used to obtain assurance. Again, we want to understand the limits and potential synergies of such methods.

  2:30–3:55 Exploiting annotations and specifications

  • An ultimate type system. Greg Morrisett, Harvard
  • Generation of not only code but also certification evidence from formal specifications. Alessandro Coglio, Kestrel
  • Building secure web applications with SELinks. Mike Hicks, U. Maryland, College Park
  • Software assurance. Joe Hurd, Galois
  • Discussion

• The plan is to talk about more dynamic methods that involve running program code to obtain added assurance, such as testing and model checking, and other program transformations that add assurance.

  4:10–5:00 Model checking, transformation and monitoring

  • Securing real applications. Saman Amarasinghe, MIT
  • Retrofitting legacy code for security. Somesh Jha, UW Madison
  • Secure Virtual Architecture: a framework for certifying commodity software. Vikram Adve, UIUC

• 5:00–5:30 Wrap-up 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.