Computer Science & Engineering
Making Operating Systems Fault Free
Prof. Wolfgang J. Paul
Computer Science Department, University of the
Friday, November 12, 2004, †††3:30-4:30 p.m.
Refreshments will be served in front of the Forum from 3:00 to 3:30 pm.
Abstract: The development of computer systems is becoming increasingly prone to faults. This is mostly due to growing complexities combined with shorter development cycles and the use of testing methodologies that are insufficient to show correct operation. For current operating systems this problem can be frequently experienced by the occurrences of system crashes, hang-ups and the vulnerability by viruses.
It is the goal of our current efforts to enable computer systems that are free of design errors. This is done by showing their correctness using formal methods. Our ultimate goal is the formal verification of entire computer systems consisting of hardware, system software, communication system and applications. The focus of this talk is the correctness of an operating system which is a difficult problem in itself. We explain our approach to make operating systems fault free. We outline the paper and pencil correctness proof for an operating system microkernel written in C. The key ingredients of the proof are:
1) a simulation of virtual machines by physical processors with swap memory. Here physical memory serves as a cache for virtual memory. In the correctness proof one argues simultaneously about hardware (memory management units) and low level software (page fault handlers).
†2) semantics and provably correct compiler for an appropriate subset of C. One needs small steps semantics resp. structured operational semantics, because the computations of the kernel needs to be interleaved with computations of the users. One needs also to consider in line assembler code, because the variables of an abstract C machine do not show the user processes. The correctness proof for the compiler is nontrivial, because the recursion of small steps semantics does not match the recursion for the code generation very well.
†3) the definition of an abstract machine model for an operating system kernel providing multiprocessing and virtual memory. In this model interrupt handling and function calls can be treated in a very uniform way. The simulation of this model by a physical machine combines the techniques from the first two parts.
This is joint work with M. Gargano, M. Hillebrand and D. Leinenbach. It is part of a large project funded by the German national government, which aims at the formal verification of entire computer systems consisting of hardware, system software, communication system and applications.
Biography: Prof. Paul has received his PhD in Computer
Science from the University of the
Hosted by CSE Dept.††††††† ††††††††††Everyone invited!