The TS group has a simple point-of-sale system implemented on top of LionsOS. This project is to revisit its architecture from the security point-of-view, including minimising the trusted computing base (TCB) and investigate feasibility of verifying the TCB. Options to investigate include implementing the business/accounting logic in a verification-friendly language (Pancake or CakeML) and using scalable verification approaches under investigation in TS.
School
Computer Science & Engineering
Research Area
Secure Systems | Operating Systems | Formal Verification
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.
- Report describing the evaluation, proposed design/implementation and take-aways;
- any design, implementation and verification artefacts resulting from the above.
Please check with project lead.