Assurance of eBPF security with the eBPF verifier

Thumbnail Image

Files

URL

Journal Title

Journal ISSN

Volume Title

Perustieteiden korkeakoulu | Bachelor's thesis
Electronic archive copy is available locally at the Harald Herlin Learning Centre. The staff of Aalto University has access to the electronic bachelor's theses by logging into Aaltodoc with their personal Aalto user ID. Read more about the availability of the bachelor's theses.
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.

Authors

Date

2025-05-23

Department

Major/Subject

Tietotekniikka

Mcode

SCI3027

Degree programme

Teknistieteellinen kandidaattiohjelma

Language

en

Pages

26

Series

Abstract

The Linux eBPF subsystem is a framework that enables running custom programs inside of the kernel. It allows users to add functionality to the kernel, securing the programs with a verifier to the kernel. This thesis specifically focuses on the security of the eBPF programs and specifically the verifier that is the component providing the security. It discusses whether or not the verifier provides sufficient security for the eBPF subsystem. The security is assessed from three different perspectives: vulnerabilities found in the eBPF verifier, techniques to find vulnerabilities in the verifier and prove the correctness of the verifier and verifier compared to other approaches. This thesis studies eBPF documentation to explain how eBPF verifier works. Common Vulnerabilities and Exposures (CVE) are utilized in the analysis of vulnerabilities and each vulnerability is categorized with Microsoft STRIDE model and Common Weakness Enumeration (CWE). For the latter two perspectives, different studies and research in the field will be examined. The results show that significant amount of vulnerabilities have been discovered in the verifier, most of them found in the last five years. Found vulnerabilities are diverse and may result in attacks such as denial of service, privilege escalation or compromising integrity of kernel memory. One of the most used techniques to find vulnerabilities is fuzzing. Fuzzers can reach high code coverage but can not be trusted to prove the correctness of the verifier code. To prove the correctness, formal verification is used. However, as the verifier is complex, completely proving its correctness is almost impossible with formal verification. Furthermore, verifier compared to other approaches focuses on performance more than security and does not address the functional security of the programs. A significant amount of vulnerabilities have been found on the verifier and therefore unprivileged use of eBPF is not popular. Another possible reason for that is the difficulty of proving the correctness of the verifier. This leads to the conclusion that the current verifier approach to eBPF security is not sufficient for untrusted use but it provides enough security for privileged use.

Linuxin eBPF-alijärjestelmä on kehys, joka mahdollistaa mukautettujen ohjelmien suorittamisen kernelin sisällä. Se mahdollistaa käyttäjän määrittelemän toiminnallisuuden, jonka turvallisuuden eBPF todentaja on todentanut, lisäämisen kerneliin. Tämä opinnäytetyö keskittyy erityisesti eBPF-ohjelmien turvallisuuteen ja erityisesti todentajaan, joka on komponentti, joka vastaa turvallisuuden toteutumisesta. Työssä tarkastellaan, tarjoaako todentaja riittävän turvallisuustason eBPF-alijärjestelmälle. Turvallisuutta arvioidaan kolmesta näkökulmasta: tarkastajasta löydetyt haavoittuvuudet, haavoittuvuuksien löytämiseen ja todentajan oikeellisuuden todistamiseen käytetyt menetelmät sekä tarkastajan vertaaminen muihin lähestymistapoihin. Opinnäytetyö tutkii eBPF-dokumentaatiota todentajan toiminnan selittämiseksi. Haavoittuvuuksien analysoinnissa hyödynnetään CVE-tietokantaa, ja jokainen haavoittuvuus luokitellaan Microsoftin STRIDE-mallin ja CWE-luokituksen avulla. Kahta jälkimmäistä näkökulmaa varten tutkitaan alalla tehtyjä tutkimuksia ja julkaisuja. Tulokset osoittavat, että tarkastajasta on löytynyt huomattava määrä haavoittuvuuksia, joista suurin osa on löydetty viimeisen viiden vuoden aikana. Löydetyt haavoittuvuudet ovat monipuolisia ja voivat mahdollistaa esimerkiksi palvelunestohyökkäyksiä, oikeuksien laajentamista tai kernelin muistin turvallisuuden rikkomisen. Yksi yleisimmistä haavoittuvuuksien löytämismenetelmistä on fuzzaus. Fuzzereilla saavutetaan laaja koodikattavuus, mutta niihin ei voida luottaa todentajan koodin oikeellisuuden todistamisessa. Oikeellisuuden todistamisessa käytetään muodollista verifiointia. Todentaja on kuitenkin niin monimutkainen, että sen täydellinen muodollinen todistaminen on lähes mahdotonta. Lisäksi todentaja keskittyy enemmän suorituskykyyn kuin turvallisuuteen, eikä se takaa ohjelmien toiminnallista turvallisuutta. Opinnäytetyössä todetaan myös, että eBPF:n käyttö ilman erityisoikeuksia ei ole yleistä. Toinen mahdollinen syy tähän on todentajan oikeellisuuden todistamisen vaikeus. Tästä voidaan päätellä, että nykyinen todentajaapohjainen lähestymistapa eBPF:n turvallisuuteen ei ole riittävä ei-luotetun käytön kannalta, mutta se tarjoaa riittävän turvallisuuden, kun käyttö tapahtuu erityisoikeuksilla.

Description

Supervisor

Savioja, Lauri

Thesis advisor

Gunn, Lachlan

Keywords

Linux, kernel, eBPF, security

Other note

Citation

Permanent link to this item

https://urn.fi/URN:NBN:fi:aalto-202512099004

Collections

[kand] Perustieteiden korkeakoulu / SCI