LionsOS is a new seL4-based OS for embedded systems under development at TS. It uses a modular device-driver model that passes I/O data via shared-memory, zero-copy data structures. LionsOS I/O outperforms Linux.

USB is an important functionality for most systems, including embedded, and is often performance-critical. This project is to develop a USB driver and port a USB protocol stack to LionsOS.

School

Computer Science and Engineering

Research Area

Operating systems

Suitable for recognition of Work Integrated Learning (industrial training)? 

Yes

The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.

  • USB working natively on LionsOS;
  • Report describing the approach, lessons learned and presenting a performance analysis.