When & Where: 12:30pm, Wednesday, Nov 20, 2002, Room 400 AKW
Abstract:
With system security and robustness becoming ever more problematic and critical throughout the computing universe, formalized operating systems built from formalized components is the only viable long-term OS strategy - however remote this dream may appear now. The language, compiler, and formal reasoning tools needed to accomplish this goal are mostly here. Two critical problems remain, however. The first problem is managing the sheer size and complexity of real operating systems: how to modularize and formally validate OS components separately, and then build them into a larger system in a formally verifiable manner. PCC and proof-generating compilers provide an important tool toward addressing this problem, but are only part of the story. The second critical problem is the enormous cultural gap between the people who write operating systems and the people who write proofs about systems. These two problems are in fact closely related, and in this talk I will discuss these problems and possible approaches toward solving them, from the perspective of an OS hacker who has dabbled a bit in formal methods.