Computer Science and Engineering
The seL4 Core Platform (seL4CP) supports statically-architected systems on seL4 and is designed to serve the needs of embedded and cyberphysical systems. However, some of such systems need the ability to load applications whose resource needs and access rights are not known at system-configuration time.
To support such applications, this project is to provide a notion of protection domain (PD) templates, which are configured for maximum access and can be loaded with actual application code that is not part of the original system configuration. The template is initialised with a trusted loader, which is pointed at the actual app to be loaded. The app contains a signed header that specifies its authorised access. The trusted loader interprets that section, removes non-authorised access rights, and then loads and executes the actual target app. When the app exits, the template is re-set to its original state.
School
Research Area
Operating systems
- 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.
- Investigation of design options and trade-offs, as well as functionality to be added to the seL4CCP to support it;
- Implementation and evaluation of the design;
- Report describing the outcomes.
