암호 명세 Lean 4 작성, 증명으로 검사하는 암호 규칙
Strawmap Hegotá (2027) · cryptography specs in Lean 4
합의층이 쓰는 암호 기술의 명세를 글 문서가 아니라 증명 도우미(proof assistant) Lean 4 코드로 적습니다. 명세에 틀린 곳이 없는지 컴퓨터가 검사할 수 있게 합니다.
왜 필요한가
이더리움 합의층은 서명과 해시 같은 암호 기술 위에서 돌아갑니다. 지금까지 이런 규칙은 주로 영어 문서와 파이썬 참조 코드로 정리해 왔습니다. 사람이 읽기에는 좋지만 명세에 모순이 없는지, 안전 성질을 정말 만족하는지는 눈으로 확인하는 데 그칩니다. 여러 클라이언트 팀이 같은 문장을 다르게 해석해 서로 다른 결과를 내는 일도 생길 수 있습니다. Lean 4 는 수학 증명을 컴퓨터가 한 줄씩 검사하는 증명 도우미(proof assistant)이자 프로그래밍 언어입니다. 암호 명세를 Lean 4 로 적으면 명세가 그대로 실행되는 코드가 되고 이 함수는 항상 이런 성질을 지킨다는 주장에 증명을 붙여 기계가 확인할 수 있습니다. 해석의 여지가 줄고 구현이 명세와 어긋나는지도 더 엄밀하게 대조할 수 있습니다. 같은 칸에 양자 내성 키 등록이 놓인 데서 보듯 합의층은 새 암호 기술을 들여올 준비를 하고 있습니다. 새 암호를 넣을 때 명세 단계의 실수는 네트워크 전체의 안전 문제가 되므로, 처음부터 기계가 검증할 수 있는 형태로 적어 두려는 것입니다. 이 항목은 체인 규칙을 직접 바꾸지 않는 프로토콜 밖 작업입니다. Hegotá 칸은 Strawmap 의 예상일 뿐 확정은 아닙니다.
어떻게 동작하나
- 명세를 Lean 4 코드로 적습니다 서명 검증이나 해시 계산 같은 암호 규칙을 문장이 아니라 Lean 4 함수로 정의합니다. 정의 자체가 실행되는 코드라서 입력을 넣어 결과를 바로 확인할 수 있습니다.
- 지켜야 할 성질을 증명합니다 올바른 서명은 항상 통과한다 같은 성질을 정리(theorem)로 적고 증명을 붙입니다. 증명에 빈틈이 있으면 Lean 4 가 받아 주지 않습니다.
- 구현이 명세와 맞는지 대조합니다 클라이언트 팀은 이 명세를 기준으로 삼아 각자의 구현이 같은 입력에 같은 결과를 내는지 확인합니다.