CVE-2020-8835 PoC — Linux kernel 缓冲区错误漏洞

Source

Associated Vulnerability

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

Remarks