• ERTOS Home
•  
• News
• Events
• Jobs
• Research
  • seL4
  • L4.verified
  • Information Flow
  • CAmkES
  • Power Management
  • Device Drivers
    • Termite
    • Dingo
  • Virtualisation
  • Secure Access Controller
  • L4
  • Former Projects
• People
• Publications
• Software
• Hardware
• Education
• Collaboration and Commercialisation
• Contact
• Search

Research on Device Drivers

Overview

A fast and reliable operating system requires fast and reliable device drivers. Most current operating systems sacrifice reliability for speed by executing drivers in the kernel mode. Given that drivers account for 70% of the kernel code, and that driver developers are typically not kernel experts, it does not come as a surprise that the majority of OS failures nowadays are caused by bugs in device drivers.

At ERTOS, we attack the problem from two different angles in the context of two projects.

Termite

The Termite project is developing an approach to creating bug-free device drivers by generating them automatically from a formal specification of the device.

Dingo

The Dingo project investigates how existing operating systems, such as Linux, can be made more driver-friendly without radically changing their architecture.