Title :
P-Bus: Programming Interface Layer for Safe OS Kernel Extensions
Author :
Fujita, Hajime ; Matsuda, Motohiko ; Maeda, Toshiyuki ; Miura, Shinichi ; Ishikawa, Yutaka
Author_Institution :
Univ. of Tokyo, Tokyo, Japan
Abstract :
P-Bus, a new programming interface layer for safe kernel extensions is proposed. P-Bus introduces a new programming interface on top of the Linux kernel in order to give formal specifications to the interface, and to improve portability of extensions. New extensions, called P-Components, are verified with a model checker MKencha to see whether a component is compliant with rules which should be obeyed to implement extensions properly. A network driver has been implemented as a P-Component and verified with MKencha. MKencha has found two bugs in the component.
Keywords :
application program interfaces; formal specification; operating system kernels; system buses; Linux kernel; MKencha checker; P-Bus; formal specifications; programming interface layer; safe OS kernel extensions; Model checking; OS kernel extension; OS kernel verification;
Conference_Titel :
Dependable Computing (PRDC), 2010 IEEE 16th Pacific Rim International Symposium on
Conference_Location :
Tokyo
Print_ISBN :
978-1-4244-8975-6
Electronic_ISBN :
978-0-7695-4289-8
DOI :
10.1109/PRDC.2010.31
