View Proposal

---

Proposer

Adam Sampson

Title

Model-check Linux's BPF verifier

Goal

Use model-checking (or other formal techniques) to improve the safety of Linux's BPF verifier

Description

BPF is a virtual machine architecture that is used for various "programmability" tasks inside the Linux kernel - for example, you can use it to specify custom firewall rules or custom scheduling conditions. It's important that BPF is *not* a general-purpose architecture, since BPF programs must execute within a fixed amount of time and resources - the BPF verifier is responsible for checking BPF programs to make sure they meet these rules. Since the BPF verifier is just a bit of code written in C, it's had several bugs where harmful BPF programs are incorrectly validated. This seems like an ideal application for some formal reasoning - can you come up with a way of making the BPF verifier itself verifiably safe, so you can prove that it can't validate an unsafe program? I'm imagining using model-checking techniques for this, but I'm sure there are other ways you could attack this problem as well.

Resources

Background

Url

Difficulty Level

Challenging

Ethical Approval

None

Number Of Students

1

Supervisor

Adam Sampson

Keywords

model checking, bpf, linux, kernel, security

Degrees

Bachelor of Science in Computer Science
Bachelor of Science in Computer Systems
Master of Engineering in Software Engineering
Master of Science in Computer Science for Cyber Security
Master of Science in Computing (2 Years)
Master of Science in Information Technology (Software Systems)
Master of Science in Network Security
Master of Science in Software Engineering
Bachelor of Science in Computing Science
Bachelor of Engineering in Robotics
Bachelor of Science in Computer Science (Cyber Security)