CVE-2026-31413-BPF-Container-Escape

CVE-2026-31413: BPF 검증기의 1바이트에서 컨테이너 탈출까지 리눅스 BPF 검증기에서 건전성 버그를 발견했습니다. pushstack 호출의 + 1로 인해 분기 경로에서 ALU 명령어 하나가 건너뛰어집니다. BPFOR의 경우, 검증기는 dst = 0으로 추적하지만 CPU는 0 | K = K를 계산합니다. 완전한 컨테이너 탈출을 작성했습니다: BPF 맵에서의 OOB 읽기/쓰기, vtable 하이재킹, modprobepath 덮어쓰기, 호스트에서 루트 획득. 이후 한 문자짜리 검증기 수정과 90줄의 selftest로...

lean-cve-poc

CVE-2026-72844: Lean 4 커널 건전성 버그 중첩 귀납 프로젝션 검증 우회를 통해0 = 1을 공리 없이 증명하기. Field| Value ---|--- CVE| CVE-2026-72844 Advisory| VulnCheck VCSA Bug report| leanprover/lean414576 Fix| leanprover/lean414577 Affected| Lean 4 ≤ v4.31.0 / nightly ≤ 2026-07-27 Fixed in| nightly 2026-07-29+ / v4.32.2 CVSS 4.0...

CVE-2026-48100

Payy is an Ethereum L2 zk-rollup for privacy preserving and regulatory compliant transactions. Prior to version 1.3.0, aggagg forwards the compacted message stream from its inner proofs into a public messages: Field; 1000 array, but it never checks that the unused tail of the outer array is zero....

CVE-2026-48100 Payy: agg_agg trailing message slots are unconstrained and allow forged burn messages

Payy is an Ethereum L2 zk-rollup for privacy preserving and regulatory compliant transactions. Prior to version 1.3.0, aggagg forwards the compacted message stream from its inner proofs into a public messages: Field; 1000 array, but it never checks that the unused tail of the outer array is zero....

CVE-2026-48100

Prior to version 1.3.0 , the Payy Ethereum L2 zk-rollup suffered from a circuit soundness failure in the agg_agg function. The system failed to verify that the unused tail of a public messages array was zero, allowing a registered prover to insert forged burn messages into a valid proof. This fla...

CVE-2026-48100 Payy: agg_agg trailing message slots are unconstrained and allow forged burn messages

Payy is an Ethereum L2 zk-rollup for privacy preserving and regulatory compliant transactions. Prior to version 1.3.0, aggagg forwards the compacted message stream from its inner proofs into a public messages: Field; 1000 array, but it never checks that the unused tail of the outer array is zero....

CVE-2026-48100: Acceptance of Extraneous Untrusted Data With Trusted Data

Payy is an Ethereum L2 zk-rollup for privacy preserving and regulatory compliant transactions. Prior to version 1.3.0, aggagg forwards the compacted message stream from its inner proofs into a public messages: Field; 1000 array, but it never checks that the unused tail of the outer array is zero....

CVE-2026-53671

PREVAIL is a Polynomial-Runtime EBPF Verifier using an Abstract Interpretation Layer. Prior to version 0.2.4, the abstract transformer in prevail treats writes through a TCTX-typed base register as a silent no-op: domemstore in src/crab/ebpftransformer.cpp only models TSTACK stores, and the...

Buffa has a Use-After-Free in OwnedView via Unsound 'static Lifetime Promotion in Deref

A soundness bug in buffa's OwnedView allowed safe Rust code to trigger a use-after-free. The OwnedView::decode constructor transmuted a borrowed slice to &'static u8, and the Deref implementation exposed the promoted 'static lifetime on borrowed view fields such as &'static str and &'static u8 to...

GHSA-9PWQ-GCRX-WGHH Buffa has a Use-After-Free in OwnedView via Unsound 'static Lifetime Promotion in Deref

A soundness bug in buffa's OwnedView allowed safe Rust code to trigger a use-after-free. The OwnedView::decode constructor transmuted a borrowed slice to &'static u8, and the Deref implementation exposed the promoted 'static lifetime on borrowed view fields such as &'static str and &'static u8 to...

CVE-2026-72705

A flaw was found in Rocq Prover. The guard checker component fails to properly track recursive calls when a fixpoint passes itself as a higher-order argument to another fixpoint. This oversight allows for the creation of a type that is logically equivalent to its own negation, which can lead to t...

CVE-2026-72703

A flaw was found in Rocq Prover. The guard checker incorrectly processes parameters of nested mutual fixpoints when cross-calls occur between different bodies of the fixpoint. This oversight allows the system to accept non-terminating definitions as structurally decreasing. This critical logical...

CVE-2020-37268

A flaw was found in Coq and Rocq provers. The Print Assumptions feature, which is used to audit the soundness of proofs, fails to report when a definition was created without proper "universe checking" a mechanism to ensure logical consistency. This occurs when the definition is incorporated...

CVE-2026-72703

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. finduniformparameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes th...

CVE-2026-72705

The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function t...

CVE-2026-72711

The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::addopaque omits the checknometavarnofvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A...

CVE-2020-37268

Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type. Applying a functor inlines the body of the parameter, and the inlining drops the record that the term was built...

CVE-2026-72714 Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close

Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps...

CVE-2026-72711 Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::addopaque omits the checknometavarnofvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A...

CVE-2026-72714 Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close

Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps...