CVE-2020-8835 PoC — Linux kernel bpf verifier vulnerability

Source

https://github.com/digamma-ai/CVE-2020-8835-verification

Associated Vulnerability

Title:Linux kernel bpf verifier vulnerability (CVE-2020-8835)
Description:In the Linux kernel 5.5.0 and newer, the bpf verifier (kernel/bpf/verifier.c) did not properly restrict the register bounds for 32-bit operations, leading to out-of-bounds reads and writes in kernel memory. The vulnerability also affects the Linux 5.4 stable series, starting with v5.4.7, as the introducing commit was backported to that branch. This vulnerability was fixed in 5.6.1, 5.5.14, and 5.4.29. (issue is aka ZDI-CAN-10780)

Description

Formal verification example for CVE-2020-8835

Readme

Formal vefication of [CVE-2021-31440](https://www.zerodayinitiative.com/blog/2021/5/26/cve-2021-31440-an-incorrect-bounds-calculation-in-the-linux-kernel-ebpf-verifier)

## Set up environment

- Install Linux headers: `sudo apt install linux-headers-$(uname -r)`
- Install coq-config: `pip install coq-config`
- Install OPAM: `apt-get install opam`
- Initialize switch: `coq-config`
- Switch to the new OPAM switch: `opam switch ebpf_bug` (you may need to
  re-open your shell after that)

## Compile Project

- `make`

## Contact and further info

-  [Digamma.ai](http://digamma.ai)

File Snapshot


 [4.0K]  /data/pocs/f76a90ae09f2dad95bed636343831fc6435c7310
├── [6.7K]  common.v
├── [ 334]  coq_config.yaml
├── [  28]  _CoqProject
├── [1.3K]  demo.c
├── [ 830]  ebpf_bug.c
├── [ 831]  ebpf_fix.c
├── [4.1K]  ebpf_proof_bug.v
├── [3.4K]  ebpf_proof.v
├── [1.0K]  Makefile
└── [ 584]  README.md

0 directories, 10 files

Shenlong Bot has cached this for you

Remarks

1. It is advised to access via the original source first.

2. Local POC snapshots are reserved for subscribers — if the original source is unavailable, the local mirror is part of the paid plan.

View subscription plans →

Goal Reached Thanks to every supporter — we hit 100%!