BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Using the Cambridge ARM model to verify the concrete machine code 
 of seL4 - Magnus Myreen (University of Cambridge)
DTSTART:20110428T121500Z
DTEND:20110428T130000Z
UID:TALK31068@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:The L4.verified project has proved functional correctness of C
  code\nwhich implements a general-purpose operating system. The C code is\
 nabout 10\,000 lines long and is designed to run on ARM processors. The\n2
 00\,000-line L4.verified proof currently bottoms out at the level of C\nco
 de\, i.e. the C compiler is currently a trusted component in the\nintended
  workflow.\n\nIn this talk\, we will describe how we are using the Cambrid
 ge model of\nthe ARM instruction set architecture (ISA) to remove the C co
 mpiler\nfrom the trusted computing base. That is\, we are extending the\ne
 xisting L4.verified proof downwards so that it bottoms out at a much\nlowe
 r level\, namely\, the concrete ARM machine code which runs directly\non A
 RM hardware.\n\nThe L4.verified project and the Cambridge ARM project have
  for years\nbeen developed independently of one another. The main challeng
 e is\nnow: how do we bridge the gap between these separate projects? Our\n
 solution is to apply a technology\, which we call\, decompilation into\nlo
 gic. Our tool\, a decompiler\, translates ARM machine code into\nfunctiona
 l programs that are automatically verified to be functionally\nequivalent 
 with respect to the Cambridge model of the ARM ISA. We\napply our decompil
 er to the output of the C compiler to turn the seL4\nbinary into a large f
 unctional program. A connection can then be\nproved semi-automatically bet
 ween this functional program and the\nsemantics of the C code used in the 
 L4.verified proof.\n\nThis talk describes ongoing work which\, when comple
 te\, will remove the\nneed to trust the C compiler and the C semantics. Th
 e new proof will\ninstead have the Cambridge ARM model as a trusted compon
 ent.\n\nThis is joint work with Thomas Sewell\, Michael Norrish and Gerwin
 \nKlein of NICTA\, Australia.\n
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR