endrazine/rocq-cve-poc-21683CVE-2026-72705 — Rocq Guard Checker가 고차 인수로 전달된 Fixpoint를 허용함
가드 검사기 fixpoint 우회를 통한 러셀의 역설로 0 = 1을 공리 없이 증명.
Claude Opus 4.6 (Anthropic)에 의해 자율적으로 발견됨.
| 필드 | 값 |
|---|---|
| 버그 보고서 | rocq-prover/rocq#21683 |
| 수정 | PR #21684 |
| 영향받는 버전 | Rocq ≤ 9.1.0 / 가드 검사기가 있는 모든 Coq 버전 |
| 수정된 버전 | 9.2.0 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-670 (항상 잘못된 제어 흐름 구현) |
| CVE | CVE-2026-72705 |
가드 검사기는 자신을 다른 fixpoint의 고차 인수로 전달하는 fixpoint를 허용하며, 그 다른 fixpoint는 구조적 인수의 비부분항(non-subterm)에 대해 이를 호출합니다. 재귀 함수를 Definition(비-fixpoint 상수)에 전달하는 것은 올바르게 거부됩니다 — 가드 검사기가 이를 전개하여 문제가 되는 호출을 확인하기 때문입니다. 그러나 Fixpoint에 전달하는 것은 잘못 허용됩니다.
이는 4줄로 러셀 스타일의 역설을 만들어냅니다:
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
여기서 russell 1은 정의상 russell 1 -> False와 동일합니다. 즉, 자기 자신의 부정인 타입입니다. 자기 적용은 곧바로 False를 도출합니다.
이 익스플로잇은:
Print Assumptions는 **"Closed under the global context"**를 보고합니다False의 전체 증명은 4줄의 함수형 코드입니다Qed도 없이 순전히 정의에 의한 것입니다docker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
Rocq의 커널 검증 증명을 신뢰하는 모든 시스템이 영향을 받습니다:
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
가드 검사기는 russell을 거부해야 합니다. 왜냐하면 russell은 자신을 iterate_to_neg에 고차 인자로 전달하고, iterate_to_neg는 이를 S m(n의 부분항이 아님)에 대해 호출하기 때문입니다. 그러나 검사기는 직접적인 재귀 호출만 추적할 뿐, 고차 고정점 인자를 통한 호출은 추적하지 않습니다.
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
따라서 russell 1 ≡ russell 1 -> False이다. 이것은 고전적인 러셀 집합이다: 자신을 포함하지 않는 모든 집합의 집합. 자기 적용은 다음을 낳는다:
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
이 버그는 Tristan Stérin(@tcosmo)이 준비한 야간 퍼징 실행 중에 Claude Opus 4.6이 자율적으로 발견했으며, 가드 검사기에 관한 Yannick Forster(@yforster)의 조언을 바탕으로 했습니다. AI는 고차 고정점 우회 패턴을 식별하고 최소한의 iterate_to_neg/russell 익스플로잇을 구성했습니다.
참조: Zulip 스레드