The TS group has just developed a proof-of-concept of a secure network firewall running on the verified seL4 microkernel and LionsOS. Currently the firewall supports the transmission of traffic between two network interfaces, and is able to apply simple filtering rules to a subset of IP traffic (TCP, UDP, ICMP). Filtering rules and forwarding routes may be viewed and updated through a rudimentary web interface. Presently it has a number of missing features that prevent its practical use, with each feature requiring a varying degree of work to implement. While we are happy to leave most of them to the open-source community, we are looking for interns for the higher priority ones. These are:
- Support for IPv6, as well as more IP protocols and ethernet types
- A collection of optimised, concurrency-safe data structures which can be used by firewall components for reading and updating shared network state (e.g. NAT port mappings, TCP connection)
If there is sufficient time left after the above, the rest can be spent on improvements to existing features or adding further functionality, with the ultimate aim of enabling the firewall to be deployed on the TS network.
School
Computer Science and Engineering
Research Area
Operating systems | Networking
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.
- Functional firewall that can be deployed
- Report describing design and implementation
