LionsOS is a new seL4-based OS for embedded systems under development at TS. LionsOS isolates programs more than conventional Operating Systems and relies a lot more on asynchronous communication. Current tools used for debugging on conventional OSes are more limited for our use case. Current tools such as GDB are not equipped to debug our kind of architecture and so certain bugs that happen between process boundaries or rely on the scheduling of a system can be difficult to catch and fix. This project is to explore other ways of debugging system-wide execution such as scheduling and inter-process communication. This will involve looking at more modern tools such as rr as well as tracing infrastructure available in other OSes.
School
Computer Science and Engineering
Research Area
Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- 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.
- Port of an existing or development of a new tracing framework to give us more introspection into systems built on LionsOS.
- Evaluation of the feasibility of a record-and-replay debugger, such as RR.
