Project Description

BPF verifier plays a crucial role in securing the system (though less so now that unprivileged BPF is disabled by default in both upstream and SLES), and bugs in the verifier has lead to privilege escalation vulnerabilities in the past (e.g. CVE-2021-3490).

One way to check whether the verifer has bugs to use model checking (a formal verification technique), in other words, build a abstract model of how the verifier operates, and then see if certain condition can occur (e.g. incorrect calculation during value tracking of registers) by giving both the model and condition to a solver.

For the solver I will be using the Z3 SMT solver to do the checking since it provide a Python binding that's relatively easy to use.

Goal for this Hackweek

Learn how to use the Z3 Python binding (i.e. Z3Py) to build a model of (part of) the BPF verifier, probably the part that's related to value tracking using tristate numbers (aka tnum), and then check that the algorithm work as intended.

Resources

Looking for hackers with the skills:

bpf ebpf formalverification modelchecking kernel security

This project is part of:

Hack Week 21 Hack Week 23 Hack Week 24

Activity

  • about 1 year ago: janvhs liked this project.
  • about 1 year ago: flonnegren liked this project.
  • about 1 year ago: vliaskovitis liked this project.
  • about 1 year ago: r1chard-lyu liked this project.
  • almost 2 years ago: moio liked this project.
  • over 3 years ago: dsterba liked this project.
  • over 3 years ago: mbrugger liked this project.
  • over 3 years ago: jzerebecki left this project.
  • over 3 years ago: jzerebecki added keyword "security" to this project.
  • over 3 years ago: jzerebecki joined this project.
  • over 3 years ago: jzerebecki liked this project.
  • over 3 years ago: ailiopoulos liked this project.
  • over 3 years ago: shunghsiyu started this project.
  • over 3 years ago: shunghsiyu added keyword "kernel" to this project.
  • over 3 years ago: shunghsiyu added keyword "bpf" to this project.
  • over 3 years ago: shunghsiyu added keyword "ebpf" to this project.
  • over 3 years ago: shunghsiyu added keyword "formalverification" to this project.
  • over 3 years ago: shunghsiyu added keyword "modelchecking" to this project.
  • over 3 years ago: shunghsiyu originated this project.

  • Comments

    • shunghsiyu
      over 3 years ago by shunghsiyu | Reply

      I've uploaded the jupyter notebook on GitHub that contains a minimal model of tnum along with tnum_add(), as well as the prove that it works.

    • shunghsiyu
      over 3 years ago by shunghsiyu | Reply

      The slides used for lightning talk can be found here

      While I'd like to achieve much more, I think what I've done during hack week is suffice to be called a complete project, so I'm marking this as complete

    • shunghsiyu
      about 2 years ago by shunghsiyu | Reply

      I'm restarting this project to model check the range tracking (minimal and maximal value possible in s32/u32/u64/s64 range) done in BPF verifier.

      In addition to that I hope to unify signed and unsigned range tracking based on previously posted idea and the "Interval Analysis and Machine Arithmetic: Why Signedness Ignorance Is Bliss" paper for simpler range tracking code.

    Similar Projects

    bpftrace contribution by mkoutny

    Description

    bpftrace is a great tool, no need to sing odes to it here. It can access any kernel data and process them in real time. It provides helpers for some common Linux kernel structures but not all.

    Goals

    • set up bpftrace toolchain
    • learn about bpftrace implementation and internals
    • implement support for percpu_counters
    • look into some of the first issues
    • send a refined PR (on Thu)

    Resources


    MCP Trace Suite by r1chard-lyu

    Description

    MCP Trace Suite is an AI-native Linux tracing and diagnostics framework built on the Model Context Protocol (MCP). It provides a secure and extensible interface that allows AI agents and LLMs to execute kernel-level and userspace tracing through eBPF, bpftrace, perf, ftrace, and syscall instrumentation.

    By bridging MCP with Linux observability tools, MCP Trace Suite enables autonomous debugging, profiling, and performance analysis without requiring direct system access.

    Github: https://github.com/r1chard-lyu/tracium

    Goals

    1. Build an MCP Server that can integrate various Linux debugging and tracing tools, including bpftrace, perf, ftrace, strace, and others, with support for future expansion of additional tools.

    2. Perform testing by intentionally creating bugs or issues that impact system performance, allowing an AI agent to analyze the root cause and identify the underlying problem.

    Resources

    • Gemini CLI: https://geminicli.com/
    • eBPF: https://ebpf.io/
    • bpftrace: https://github.com/bpftrace/bpftrace/
    • perf: https://perfwiki.github.io/main/
    • ftrace: https://github.com/r1chard-lyu/tracium/


    Add Qualcomm Snapdragon 765G (SM7250) basic device tree to mainline linux kernel by pvorel

    Qualcomm Snapdragon 765G (SM7250) (smartphone SoC) has no support in the linux kernel, nor in u-boot. Try to add basic device tree support. The hardest part will be to create boot.img which will be accepted by phone.

    UART is available for smartphone :).


    Improve UML page fault handler by ptesarik

    Description

    Improve UML handling of segmentation faults in kernel mode. Although such page faults are generally caused by a kernel bug, it is annoying if they cause an infinite loop, or panic the kernel. More importantly, a robust implementation allows to write KUnit tests for various guard pages, preventing potential kernel self-protection regressions.

    Goals

    Convert the UML page fault handler to use oops_* helpers, go through a few review rounds and finally get my patch series merged in 6.14.

    Resources

    Wrong initial attempt: https://lore.kernel.org/lkml/20231215121431.680-1-petrtesarik@huaweicloud.com/T/


    early stage kdump support by mbrugger

    Project Description

    When we experience a early boot crash, we are not able to analyze the kernel dump, as user-space wasn't able to load the crash system. The idea is to make the crash system compiled into the host kernel (think of initramfs) so that we can create a kernel dump really early in the boot process.

    Goal for the Hackweeks

    1. Investigate if this is possible and the implications it would have (done in HW21)
    2. Hack up a PoC (done in HW22 and HW23)
    3. Prepare RFC series (giving it's only one week, we are entering wishful thinking territory here).

    update HW23

    • I was able to include the crash kernel into the kernel Image.
    • I'll need to find a way to load that from init/main.c:start_kernel() probably after kcsan_init()
    • I workaround for a smoke test was to hack kexec_file_load() systemcall which has two problems:
      1. My initramfs in the porduction kernel does not have a new enough kexec version, that's not a blocker but where the week ended
      2. As the crash kernel is part of init.data it will be already stale once I can call kexec_file_load() from user-space.

    The solution is probably to rewrite the POC so that the invocation can be done from init.text (that's my theory) but I'm not sure if I can reuse the kexec infrastructure in the kernel from there, which I rely on heavily.

    update HW24

    • Day1
      • rebased on v6.12 with no problems others then me breaking the config
      • setting up a new compilation and qemu/virtme env
      • getting desperate as nothing works that used to work
    • Day 2
      • getting to call the invocation of loading the early kernel from __init after kcsan_init()
    • Day 3

      • fix problem of memdup not being able to alloc so much memory... use 64K page sizes for now
      • code refactoring
      • I'm now able to load the crash kernel
      • When using virtme I can boot into the crash kernel, also it doesn't boot completely (major milestone!), crash in elfcorehdr_read_notes()
    • Day 4

      • crash systems crashes (no pun intended) in copy_old_mempage() link; will need to understand elfcorehdr...
      • call path vmcore_init() -> parse_crash_elf_headers() -> elfcorehdr_read() -> read_from_oldmem() -> copy_oldmem_page() -> copy_to_iter()
    • Day 5

      • hacking arch/arm64/kernel/crash_dump.c:copy_old_mempage() to see if crash system really starts. It does.
      • fun fact: retested with more reserved memory and with UEFI FW, host kernel crashes in init but directly starts the crash kernel, so it works (somehow) \o/

    update HW25

    • Day 1
      • rebased crash-kernel on v6.12.59 (for now), still crashing


    bpftrace contribution by mkoutny

    Description

    bpftrace is a great tool, no need to sing odes to it here. It can access any kernel data and process them in real time. It provides helpers for some common Linux kernel structures but not all.

    Goals

    • set up bpftrace toolchain
    • learn about bpftrace implementation and internals
    • implement support for percpu_counters
    • look into some of the first issues
    • send a refined PR (on Thu)

    Resources


    pudc - A PID 1 process that barks to the internet by mssola

    Description

    As a fun exercise in order to dig deeper into the Linux kernel, its interfaces, the RISC-V architecture, and all the dragons in between; I'm building a blog site cooked like this:

    • The backend is written in a mixture of C and RISC-V assembly.
    • The backend is actually PID1 (for real, not within a container).
    • We poll and parse incoming HTTP requests ourselves.
    • The frontend is a mere HTML page with htmx.

    The project is meant to be Linux-specific, so I'm going to use io_uring, pidfs, namespaces, and Linux-specific features in order to drive all of this.

    I'm open for suggestions and so on, but this is meant to be a solo project, as this is more of a learning exercise for me than anything else.

    Goals

    • Have a better understanding of different Linux features from user space down to the kernel internals.
    • Most importantly: have fun.

    Resources


    Exploring Rust's potential: from basics to security by sferracci

    Description

    This project aims to conduct a focused investigation and practical application of the Rust programming language, with a specific emphasis on its security model. A key component will be identifying and understanding the most common vulnerabilities that can be found in Rust code.

    Goals

    Achieve a beginner/intermediate level of proficiency in writing Rust code. This will be measured by trying to solve LeetCode problems focusing on common data structures and algorithms. Study Rust vulnerabilities and learning best practices to avoid them.

    Resources

    Rust book: https://doc.rust-lang.org/book/


    vex8s-controller: a kubernetes controller to automatically generate VEX documents of your running workloads by agreggi

    Description

    vex8s-controller is an add-on for SBOMscanner project. Its purpose is to automatically generate VEX documents based on the workloads running in a kubernetes cluster. It integrates directly with SBOMscanner by monitoring VulnerabilityReports created for container images and producing corresponding VEX documents that reflect each workload’s SecurityContext.

    vex8s-controller workflow

    Here's the workflow explained:

    1. sbomscanner scans for images in registry
    2. generates a VulnerabilityReport with the image CVEs
    3. vex8s-controller triggers when a workload is scheduled on the cluster and generates a VEX document based on the workload SecurityContext configuration
    4. the VEX document is provided by vex8s-controller using a VEX Hub repository
    5. sbomscanner configure the VEXHub CRD to point to the internal vex8s-controller VEX Hub repository

    Goals

    The objective is to build a kubernetes controller that uses the vex8s mitigation rules engine to generate VEX documents and serve them through an internal VEX Hub repository within the cluster. SBOMscanner can then be configured to consume VEX data directly from this in-cluster repository managed by vex8s-controller.

    Resources


    Looking at Rust if it could be an interesting programming language by jsmeix

    Get some basic understanding of Rust security related features from a general point of view.

    This Hack Week project is not to learn Rust to become a Rust programmer. This might happen later but it is not the goal of this Hack Week project.

    The goal of this Hack Week project is to evaluate if Rust could be an interesting programming language.

    An interesting programming language must make it easier to write code that is correct and stays correct when over time others maintain and enhance it than the opposite.


    Help Create A Chat Control Resistant Turnkey Chatmail/Deltachat Relay Stack - Rootless Podman Compose, OpenSUSE BCI, Hardened, & SELinux by 3nd5h1771fy

    Description

    The Mission: Decentralized & Sovereign Messaging

    FYI: If you have never heard of "Chatmail", you can visit their site here, but simply put it can be thought of as the underlying protocol/platform decentralized messengers like DeltaChat use for their communications. Do not confuse it with the honeypot looking non-opensource paid for prodect with better seo that directs you to chatmailsecure(dot)com

    In an era of increasing centralized surveillance by unaccountable bad actors (aka BigTech), "Chat Control," and the erosion of digital privacy, the need for sovereign communication infrastructure is critical. Chatmail is a pioneering initiative that bridges the gap between classic email and modern instant messaging, offering metadata-minimized, end-to-end encrypted (E2EE) communication that is interoperable and open.

    However, unless you are a seasoned sysadmin, the current recommended deployment method of a Chatmail relay is rigid, fragile, difficult to properly secure, and effectively takes over the entire host the "relay" is deployed on.

    Why This Matters

    A simple, host agnostic, reproducible deployment lowers the entry cost for anyone wanting to run a privacy‑preserving, decentralized messaging relay. In an era of perpetually resurrected chat‑control legislation threats, EU digital‑sovereignty drives, and many dangers of using big‑tech messaging platforms (Apple iMessage, WhatsApp, FB Messenger, Instagram, SMS, Google Messages, etc...) for any type of communication, providing an easy‑to‑use alternative empowers:

    • Censorship resistance - No single entity controls the relay; operators can spin up new nodes quickly.
    • Surveillance mitigation - End‑to‑end OpenPGP encryption ensures relay operators never see plaintext.
    • Digital sovereignty - Communities can host their own infrastructure under local jurisdiction, aligning with national data‑policy goals.

    By turning the Chatmail relay into a plug‑and‑play container stack, we enable broader adoption, foster a resilient messaging fabric, and give developers, activists, and hobbyists a concrete tool to defend privacy online.

    Goals

    As I indicated earlier, this project aims to drastically simplify the deployment of Chatmail relay. By converting this architecture into a portable, containerized stack using Podman and OpenSUSE base container images, we can allow anyone to deploy their own censorship-resistant, privacy-preserving communications node in minutes.

    Our goal for Hack Week: package every component into containers built on openSUSE/MicroOS base images, initially orchestrated with a single container-compose.yml (podman-compose compatible). The stack will:

    • Run on any host that supports Podman (including optimizations and enhancements for SELinux‑enabled systems).
    • Allow network decoupling by refactoring configurations to move from file-system constrained Unix sockets to internal TCP networking, allowing containers achieve stricter isolation.
    • Utilize Enhanced Security with SELinux by using purpose built utilities such as udica we can quickly generate custom SELinux policies for the container stack, ensuring strict confinement superior to standard/typical Docker deployments.
    • Allow the use of bind or remote mounted volumes for shared data (/var/vmail, DKIM keys, TLS certs, etc.).
    • Replace the local DNS server requirement with a remote DNS‑provider API for DKIM/TXT record publishing.

    By delivering a turnkey, host agnostic, reproducible deployment, we lower the barrier for individuals and small communities to launch their own chatmail relays, fostering a decentralized, censorship‑resistant messaging ecosystem that can serve DeltaChat users and/or future services adopting this protocol

    Resources