DocumentCode
2367022
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
fYear
2010
fDate
13-15 Dec. 2010
Firstpage
235
Lastpage
236
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/PRDC.2010.31
Filename
5703254
Link To Document