The Trustworthy Systems (TS) group has just developed a proof-of-concept of a secure network firewall running on the verified seL4 microkernel and LionsOS. It presently has a number of limitations that prevent is practical use, including no support for IPv6, network address translation, connection tracking, filter rule chaining and a number of protocols.
This project is to add the missing functionality, with the aim of deploying the firewall to protect the TS network.
School
Computer Science and Engineering
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.
- fully functional firewall that can be deployed
- report describing design and implementation
