trailofbits/break-golf암호분석 골프: 스킴을 깨고 Lean 4로 증명하세요. 개념 증명 보드.
실행되는 것이 아니라 증명된 암호분석 결과를 위한 보드입니다.
챌린지는 두 개의 세계와 당신이 증명해야 할 명제를 고정합니다. 당신은 적대자와 그것이 두 세계를 구별한다는 증명을 작성합니다. 승리는 그 증명입니다. 아무것도 실행되거나, 샘플링되거나, 재생되지 않으며, 어떤 사람도 제출물을 읽고 그것이 인정되는지 판단하지 않습니다.
상태: 검증기가 실행됩니다. verify: 이슈는 챌린지에 고정된 타입에 대해 CI에서 정교화(elaborate)되고 #print axioms로 감사되며, 판정은 댓글로 돌아옵니다. 기록은 여전히 수동으로 scoring/ledger.json에 추가됩니다.
이것은 독립적인 Lake 프로젝트입니다. 수학을 리비전에 고정된 git 의존성으로 가져오므로, 보드는 모드의 고정된 명제에 대해 검증합니다:
require RandomSystems from git
"https://github.com/MarcIlunga/random-systems.git" @ "08aec7a7"
빌드 시간은 캐시일 뿐 문제가 아닙니다. Mathlib의 olean은 lake exe cache get을 통해 CDN에서 가져오며, 고정 리비전과 챌린지 olean 약 400 MB는 매니페스트와 자체 소스를 키로 하는 Actions 캐시에 저장됩니다.
| 경로 | 설명 |
|---|---|
challenges/<name>/Challenge.lean | 신뢰됨. 제출물이 반드시 구현해야 하는 정확한 타입을 고정합니다. 어떤 업로드에도 포함되지 않습니다. |
challenges/<name>/Cost.lean | 양식의 수치를 바탕으로 제출물마다 플랫폼이 생성합니다. |
challenges/<name>/config.json | 점수, par, 허용 공리, 타임아웃. 챌린지를 추가할 때 편집하는 유일한 파일입니다. |
challenges/<name>/Solve.template.lean | 제출자가 채우는 골격입니다. |
tools/manifest.py | challenges/에서 docs/data/manifest.json을 도출합니다. |
tools/ledger.py | scoring/ledger.json에서 docs/data/ledger.json을 도출하며, 레코드의 점수를 매기고 정렬합니다. |
tools/record.py | 검증된 제출물을 원장에 추가합니다. proved가 아닌 것은 거부합니다. |
tools/verify.py | 제출물 하나를 검증합니다. 챌린지 id는 argv[1], 본문은 stdin, JSON 판정은 stdout으로 받습니다. lean-golf와 동일한 인터페이스입니다. |
tools/lint_challenges.py | 모든 챌린지 설정이 보드와 검증기에 필요한 것을 갖추고 있는지 확인합니다. |
tools/check_site.py | 정적 사이트가 자체 생성 데이터를 로드하고 렌더링할 수 있는지 확인합니다. |
scoring/ledger.json | 레코드 집합입니다. |
docs/ | GitHub Pages 사이트입니다. 정적이며, 생성된 두 파일만 읽습니다. |
examples/ | 테스트 픽스처: 검증은 통과하지만 아무것도 획득하지 못하는 제출물과, 이를 과대 주장하는 쌍둥이 제출물입니다. |
python3 tools/manifest.py # rewrite the manifest
python3 tools/manifest.py --check # fail if stale
python3 tools/ledger.py # rescore and sort the records
python3 tools/lint_challenges.py # configs are complete
python3 tools/check_site.py # the site can render what the tools generate
printf '%s' "$BODY" | python3 tools/verify.py spoc128 # one submission
verify.yml는 push와 pull request에서 실행됩니다: --check 게이트, config lint, 사이트 검사, 그리고 검증기가 반드시 수용해야 하고 반드시 거부해야 하는 일련의 제출물들 — sorry, native_decide, 알 수 없는 챌린지, 0인 advantage, Lean 블록이 없는 본문 — 입니다. workflow_dispatch는 이슈를 열지 않고 필요할 때 하나의 제출물을 검증합니다.
submission.yml은 두 개의 job으로 verify: 이슈를 처리합니다. 첫 번째는 신뢰할 수 없는 입력을 파싱하며 쓰기 권한이 없습니다; 두 번째는 그 판정을 다운로드하여 댓글을 게시합니다. 이 분리는 lean-golf의 방식이며, 이슈 본문이 토큰에 도달할 수 없는 이유입니다.
제출물은 챌린지가 고정한 타입을 채우는 하나의 선언입니다:
-- Challenge.lean, trusted. The verifier builds its own copy.
def score : Golf.Score := ⟨budget, advNum, advDen⟩ -- from the submission form
structure Solution where
strategy : game.Param → PFunDDS.DDE game.Query game.Response
verdict : List (game.Query × Option game.Response) → Bool
wins : Golf.Attack.Wins (G := game) ⟨strategy, verdict⟩ score.budget score.advantage
-- Solve.lean, the upload.
def solution : Challenge.SpoC128.Solution where
strategy := …
verdict := …
wins := …
세 개의 느슨한 이름 대신 하나의 구조를 사용하는 이유는, 느슨한 이름들이 충돌하기 때문입니다:
strategy/verdict/attackWins를 이미 선언한 Challenge.lean을 임포트하는 Solve.lean은 "has already been declared" 오류로 실패합니다.
제출물을 신뢰된 타입의 값으로 만들면 충돌이 제거되고
검증기의 타입 검사가 단일 #check로 축소됩니다.
두 가지가 성립해야 하며, 어느 것도 신뢰에 기대지 않습니다.
숫자는 명제의 일부입니다. 플랫폼이 숫자를 Cost.lean에 기록하고, Challenge.lean이 그로부터 score를 구성하며, score는 Solution.wins의 타입 안에 나타납니다. 숫자를 바꾸면 증명해야 할 대상이 바뀝니다.
제출물은 우리의 타입에 속해야 합니다. 감사 단계는 신뢰된 챌린지를 제출물과 함께 임포트하고 다음을 정교화합니다
example : Challenge.SpoC128.Solution := Solution.SpoC128.solution
자체 Challenge.SpoC128.Solution을 선언하는 제출물은 우리의 것과 충돌하며, 다른 타입을 사용하는 제출물은 타입 검사를 통과하지 못합니다. 이 단계가 없으면 챌린지를 전혀 import하지 않는 제출물이 같은 이름의 자명한 구조체를 정의하고 0비트에서 "증명"될 수 있습니다 — 그 구멍은 실제로 존재했으며, 두 공격 모두 이제 CI 케이스입니다.
쿼리 횟수에는 별도의 증명이 필요하지 않습니다. 그것은 완성된 적대자에 대한 주장이 아니라 생성자 인자입니다. Attack.distinguisher q는 DDD.ofDDE strategy q verdict이며, 구성상 q에서 잘리고, Attack.silent_past는 그것이 그 이상을 발행하지 않음을 증명합니다. 예산을 초과 지출할 방법이 없으므로 검사할 것도 없습니다.
budget, advNum, advDen은 제출 양식에서 오며, 신뢰되지 않습니다. 그럴 필요도 없습니다: 플랫폼이 이들을 Cost.lean에 대입하고, Challenge.lean이 이들로부터 score를 구성하며, score는 Solution.wins 내부에 나타납니다. 따라서 이 숫자들은 명제에 대한 주장이 아니라 명제의 일부입니다.
실제 SpoC-128 공격에 대해 검사한 결과:
| 주장 | 결과 |
|---|---|
budget = 3, advantage 1 | 컴파일됨 — 정직한 주장 |
budget = 1, advantage 1 | 실패 — Wins 1 1은 다른, 더 강한 정리 |
budget = 3, advantage 2 | 실패 — advantage 1을 초과할 수 있는 것은 없음 |
그리고 축소할 유인도 없습니다: score = log₂(budget / advantage^e)이므로, 더 작게 주장한 advantage나 더 크게 주장한 budget은 score를 높입니다. 양방향 모두 불리합니다. 유일한 수는 실제로 증명할 수 있는 가장 타이트한 주장입니다.
검증기가 아무것도 읽지 않고 내리는 네 가지 추가 거부:
| 속임수 | 판정 |
|---|---|
| 주장 약화 | 고정된 Solution에 대한 타입 불일치 |
| 편리한 가설 추가 | 동일 |
증명에 sorry 사용 | sorryAx는 permitted_axioms에 없음 |
native_decide / maxHeartbeats 상향 | 즉시 거부 |
미리 고정된 것은 없습니다. 아무도 연구하지 않은 스킴에서 어떤 비용으로 어떤 advantage에 도달할 수 있는지는 연구 질문이므로, 어떤 목표든 추측입니다 — 그리고 너무 높게 설정된 목표는 진짜 2⁻³⁰ 구별자를 0으로 채점합니다. 대신 보드는 결과를 측정합니다:
score = log₂( budget / advantage^e )
단위당 쿼리 이점이며, 그 밑이 2인 로그는 공격이 반박하는 보안 수준(비트)이다. 낮을수록 좋다. 자신의 이점을 낮게 말하면 점수가 올라가므로, 증명할 수 있는 것보다 적게 주장해서 얻을 것은 없다.
e는 챌린지마다 정해지며 기본값이 없다. 결정 게임에서는 e = 2이고 — 이점 α를 증폭하려면 약 α⁻²회의 반복이 필요하다 — 탐색 성격의 게임에서는 e = 1이다. 두 관례 모두 문헌에 존재하며 그 불일치는 알려져 있으므로(Micciancio–Walter, On the Bit Security of Cryptographic Primitives), 각 챌린지는 어느 쪽을 쓰는지 명시한다.
파(par)는 설계자 자신의 주장이며 명세에서 가져온 것이므로, 공격 난이도에 대한 추측은 어디에도 등장하지 않는다. 파 미만은 그 주장에 대한 돌파다.
기록은 최고 점수 순으로 나열된다. 그것이 순위의 전부다.