Djawula is an seL4-based fully dynamic, general-purpose operating system under development at TS. Unlike the reasonably mature LionsOS, which has a static architecture, Djawula supports the security policy and system architecture to evolve at runtime. This requires support for enabling, disabling and configuring device drivers at runtime.
The aim of this project is to develop a device manager, similar to the one of Haiku OS, for dynamically managing seL4 device drivers. It needs to be integrated with Djawula's security enforcement and dynamically connect and disconnect clients to drivers.
School
Computer Science & Engineering
Research Area
Operating Systems and Secure Systems
Suitable for recognition of Work Integrated Learning (industrial training)?
TBC
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
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.
- Design, implementation and evaluation of a device manager for seL4 device drivers in Djawula;
- report describing the above.
Please check with project lead.