Languages

Certified OS Kernel

strict warning: Only variables should be passed by reference in /var/www/drupal/modules/book/book.module on line 559.

Background

While dependability certification is becoming increasingly important for many high level applications, the operating system kernel is often assumed to be "correct". This represents a weak link in today’s safety-critical systems since operating systems today are often extremely complex and may contain many subtle bugs. Even "bug fixes" distributed by the OS vendors may introduce new vulnerabilities or corrupt other system components.

Certified Software

One promising solution to establish true dependability is to use formal certification and insist that the kernel executable always comes with a rigorous mathematical proof. The proof is checkable by computer and states that the kernel is free of bugs with respect to a particular specification. Certified kernels provide the high assurance required by systems in the embedded application domain ranging from PDA, medical devices, to automobiles.

certified software

There exists a significant semantic gap between the formal certification and the user’s view of correctness. Therefore, it is important to specify clear and understandable definitions, which formalize the OS properties that users are concerned, such as safety, security and robustness. Moreover, the proper, precise and formal specifications of the code inside OS kernels are prerequisite for proving their correctness.

On the other hand, formal certification of large low-level implementations (especially OS) has so far been considered prohibitively expensive. Recently, the research progress in theorem proving and certifying compilation makes the view changing. The tools, known as proof assistants, provide explicit machine-checkable proofs and facilitate automation. Using certifying compilers, the proof constructed by higher level program verifiers can be propagated down to the machine-code level to reduce the certification cost. Besides, we concentrate on the modularity of proof construction, which is the key technique for make formal certification practical and scalable.

Certification Framework

It is a common practice for modern operating system kernels to employ different language features and various abstraction levels, such as dynamic code loading (e.g. boot-loader, programs loader), concurrency (thread scheduling), interrupt handlers (device drivers). A key step making certified operating system kernels possible is to actually demonstrate the feasibility of certifying the complete software system with all these diverse features.

kernel modules

Due to the fact that kernel developers never use a universal logic to design, the difficulty of certifying the whole system in single program logic is self-evident. An alternative is to divide-and-conquer, that is, to decompose the kernels into several parts, which renders specialized domain-specific logics certifying individual kernel parts a natural solution. To allow certifying the interactions of kernel parts and build complete certified operating system kernels, we need to also support the interoperability of different logics.

The most important research topic of us is to design a certification framework, where the kernels can be certified modularly and at the same time linked together to form complete certified OS kernels.

certification-framework

The framework is essentially Hoare-style program logic system over the lowest programming language level (raw machine language) so as to link the different binary object modules and prove the correctness of the linkage simultaneously. On the other hand, the framework has to support heterogeneous program specification languages and existing various verification systems for the kernel parts with domain-specific logics.

It is justified that the framework is sophisticated and its soundness should be also proved strictly. We build the certification framework upon a mechanized meta logic, which is expressive enough to construct logics, formal proofs and specifications yet simple so that the proof checker can be hand-verified for its correctness.

What we have done

  • AIM: A minimal kernel protocol, including interrupts and synchronization
  • Swap: A logic for certifying context switching

Related Projects