비탈릭: 이더리움의 다음 단계에서 핵심은 무엇인가?
번역 및 편집: 자후안(Jiahuan), ChainCatcher
요이치 히라이(Yoichi Hirai), 저스틴 드레이크(Justin Drake), 나딤 코베이시(Nadim Kobeissi), 알렉스 힉스(Alex Hicks)가 피드백과 검토를 제공해 주셔서 특별히 감사드립니다.
지난 몇 달간, 이더리움의 선두 연구 커뮤니티뿐 아니라 전산학 전반의 여러 분야에서 새로운 프로그래밍 패러다임이 급속도로 인기를 끌고 있습니다. 바로 EVM 바이트코드나 어셈블리어와 같은 극도로 저수준의 언어 또는 Lean을 직접 사용해 코드를 작성하고, Lean으로 작성된 자동 검증 가능한 수학적 증명을 이용해 그 정확성을 검증하는 방식입니다.
적절히 수행된다면, 이 방법은 단순히 매우 효율적인 코드를 생성할 뿐만 아니라 기존의 어떤 프로그래밍 방식보다 훨씬 더 안전한 코드를 산출할 가능성이 있습니다. 요이치 히라이는 이를 “소프트웨어 개발의 궁극적 형태”라고 명명했습니다.
본 글은 이러한 접근법의 기본 원리를 밝히고, 소프트웨어의 형식적 검증(formal verification)이 무엇을 할 수 있는지, 그리고 이더리움 및 기타 분야에서 그 한계와 약점이 어디에 있는지를 탐구하려 합니다.
형식적 검증이란 무엇인가?
형식적 검증이란, 컴퓨터가 자동으로 검사할 수 있는 방식으로 수학 정리에 대한 증명을 작성하는 것을 말합니다. 비교적 단순하지만 여전히 흥미로운 예시를 들어보겠습니다. 피보나치 수열에 관한 기본 정리 하나를 살펴보죠: 세 번째 항부터 시작해 매 세 번째 숫자는 짝수이며, 나머지는 홀수입니다.
1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 ...
이 사실을 증명하는 간단한 방법은 수학적 귀납법이며, 매번 세 단계씩 전진합니다.
우선 기초 사례(base case)를 살펴봅시다. F₁ = F₂ = 1, F₃ = 2라 하겠습니다. 관찰을 통해, 해당 명제(“Fᵢ는 i가 3의 배수일 때 짝수이고, 그렇지 않으면 홀수이다”)가 x = 3 이전까지는 성립함을 확인할 수 있습니다.
다음은 귀납 단계(inductive step)입니다. 명제가 3k+3 이전까지 성립한다고 가정합니다. 즉, F₃ₖ₊₁, F₃ₖ₊₂, F₃ₖ₊₃의 홀짝성 각각이 홀수, 홀수, 짝수임을 이미 알고 있습니다. 이제 다음 세 항의 홀짝성을 계산할 수 있습니다:
F₃ₖ₊₄ = F₃ₖ₊₂ + F₃ₖ₊₃ = 홀수 + 짝수 = 홀수
F₃ₖ₊₅ = F₃ₖ₊₃ + F₃ₖ₊₄ = 짝수 + 홀수 = 홀수
F₃ₖ₊₆ = F₃ₖ₊₄ + F₃ₖ₊₅ = 홀수 + 홀수 = 짝수
따라서 우리는 명제가 3k+3 이전까지 성립한다는 가정에서, 명제가 3k+6 이전까지 성립함을 도출하였습니다. 이 추론을 반복적으로 적용함으로써, 해당 규칙이 모든 정수에 대해 성립함을 확신할 수 있습니다.
이 논거는 인간에게는 충분히 설득력이 있습니다. 그러나 만일 복잡도가 백 배 이상인 것을 증명해야 하고, 자신이 실수를 전혀 범하지 않았다는 점을 철저히 확신하고 싶다면 어떨까요? 이때에는 컴퓨터가 납득할 수 있는 증명을 제공하면 됩니다.
그 구체적인 모습은 다음과 같습니다:
-- 피보나치 수열: fib 0 = 0, fib 1 = 1, fib 2 = 1 (인덱스가 1만큼 오프셋됨)
def fib : Nat → Nat
| 0 => 0
| 1 => 1
| n + 2 => fib (n + 1) + fib n
-- 주장: fib (3k+1)은 홀수, fib (3k+2)는 홀수, fib (3k+3)은 짝수.
-- 동등하게 표현하면: fib 3부터 시작해 매 세 번째 피보나치 수는 짝수.
-- 우리는 k에 대한 귀납법을 사용해 세 가지 모두를 동시에 증명합니다. 왜냐하면 다음 블록의 각 경우가 이전 블록을 기반으로 구성되기 때문입니다.
theorem fib_triple (k : Nat) :
fib (3 * k + 1) % 2 = 1 ∧
fib (3 * k + 2) % 2 = 1 ∧
fib (3 * k + 3) % 2 = 0 := by
induction k with
| zero => decide
| succ k ih =>
-- 새 인덱스를 (무언가) + 2 형태로 다시 쓰면 fib가 풀립니다.
refine ⟨?_, ?_, ?_⟩
· show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1
omega
· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1
omega
· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)
+ (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0
omega
이것은 위에서 제시한 ‘인간용’ 증명과 동일한 추론 논리를 Lean 언어로 표현한 것입니다. Lean은 수학적 증명을 작성하고 검증하는 데 널리 사용되는 프로그래밍 언어입니다.
이 표현은 위의 인간용 증명과 달라 보이는데, 그 이유는 매우 타당합니다. 즉, 컴퓨터(전통적인 의미에서, if/then 문으로 구성된 ‘결정론적’ 프로그램, 대규모 언어 모델이 아닌)에게 직관적인 것과 인간에게 직관적인 것은 근본적으로 다릅니다.
위 증명에서는 fib(3k+4) = fib(3k+3) + fib(3k+2)라는 사실을 강조하지 않고, 오히려 fib(3k+3) + fib(3k+2)가 홀수임을 강조합니다. 그리고 Lean 내부에서 이름이 상당히 거창한 ‘omega’ 전략이, fib(3k+4)에 대한 정의 지식과 자동으로 연결됩니다.
더 복잡한 증명에서는 단계마다 어떤 수학 법칙이 현재 단계를 허용하는지를 명시적으로 지정해야 하며, 때로는 Prod.mk.inj처럼 난해한 이름의 규칙을 활용해야 합니다.
반면, 거대한 다항식 표현식을 한 번에 펼쳐내고, 단순히 "omega"나 "ring" 같은 한 줄 명령어만으로도 그것이 타당함을 증명할 수 있습니다.
이런 비직관성과 번거로움은, 기계 검증 가능한 증명이 약 60년 전부터 존재했음에도 불구하고 이 분야가 여전히 소수파에 머물러 있는 주된 이유를 설명해 줍니다. 하지만 한편으로는 인공지능의 급속한 발전 덕분에, 과거에는 불가능했던 많은 일이 지금 당장 가능해지고 있습니다.
수학 증명이 코드를 지키기 시작할 때
지금까지 읽으신 분이라면 아마 이렇게 생각하실지도 모릅니다: “좋아요, 컴퓨터는 이제 수학 정리의 증명을 검증할 수 있게 되었군요. 그러면 마침내 소수(prime number) 등에 관한 광활한 신규 결론 중 어느 것이 진짜이고, 어느 것이 수백 페이지 분량의 PDF 논문 속 오류인지 확실히 알 수 있겠네요!”
혹은, 무야카즈 히로오(Shinichi Mochizuki)의 ABC 추측 관련 주장을 정확히 검증해 볼 수도 있을지도 모르겠습니다!
하지만 호기심을 떠나, 그렇다고 해서 어쩌면요?
이에 대한 답은 여러 가지가 있습니다. 하지만 저에게 특히 중요한 답은, 특히 암호화 또는 보안 관련 작업을 수행하는 컴퓨터 프로그램의 정확성을 검증하는 데 그 응용 가능성이 있다는 점입니다.
결국 컴퓨터 프로그램 자체가 수학적 객체이므로, 프로그램이 특정 방식으로 작동한다는 것을 증명하는 것 역시 수학 정리입니다.
예를 들어, Signal과 같은 암호화 통신 소프트웨어가 실제로 안전한지 검증하고 싶다고 가정해 봅시다. 그런 맥락에서 ‘안전함’이 수학적으로 무엇을 의미하는지를 정의할 수 있습니다.
고차원적으로 보면, 우리가 증명해야 할 것은, 특정 암호학적 가정이 성립한다고 가정할 때, 오직 개인 키를 소유한 사람만 메시지 내용에 대한 어떤 정보도 얻을 수 있다는 것입니다. 현실에서는 다양한 보안 속성이 모두 매우 중요합니다.
흥미롭게도, 바로 이런 문제를 해결하려는 팀이 실제로 존재합니다! 그들의 보안 정리 중 하나는 다음과 같습니다:
theorem passive_secrecy_le_ddh
(g : G)
(adv : PassiveAdversary G SK) :
passiveSecrecyAdvantage (F := F) g adv ≤
ProbComp.boolDistAdvantage
(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))
(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))
Leanstral이 이 정리의 의미를 요약한 내용은 다음과 같습니다:
‘passive_secrecy_le_ddh’ 정리는 X3DH의 수동적 메시지 비밀 유지성(passive message secrecy)이 랜덤 오라클 모델 하의 DDH 가정만큼 어려움을 갖는다는 것을 보여주는 압축된 귀납(reduction)입니다. 공격자가 X3DH의 수동적 메시지 비밀 유지성을 깨뜨릴 수 있다면, DDH도 깨뜨릴 수 있습니다.
우리는 DDH가 깨지기 어렵다고 가정하므로, X3DH는 수동적 공격에도 안전합니다. 이 정리는, 공격자가 Signal의 키 교환 메시지를 수동적으로 관찰하더라도, 생성된 세션 키를 임의의 키와 구분할 수 있는 확률이 무시할 수 있을 정도로 낮다는 것을 보장합니다.
이 정리와 AES 암호화 구현의 정확성 증명을 결합하면, Signal 프로토콜이 수동적 공격자에 대해 암호학적으로 안전하다는 결론을 도출할 수 있습니다.
유사한 프로젝트들은 TLS 및 브라우저 내 암호학의 다른 부분 구현 역시 안전하다는 것을 입증했습니다.
단말 간(end-to-end) 완전한 형식적 검증을 수행한다면, 단순히 프로토콜의 이론적 설명이 안전하다는 것만이 아니라, 실제 사용자가 실행하는 구체적인 코드가 실제로 안전하다는 것도 증명하게 됩니다.
사용자 입장에서는, 이는 신뢰성(trustworthiness)을 크게 향상시킵니다. 코드 전체를 검토할 필요 없이, 증명된 명제들만 확인하면 코드를 완전히 신뢰할 수 있습니다.
그러나 ‘안전함(safety)’이라는 핵심 용어가 실제로 무엇을 의미하는지에 대해 기억해야 할 중요한 전제들이 있습니다.
사람들은 종종 정말 중요한 명제를 증명하는 것을 잊어버리기 쉽습니다. 또, 증명하려는 명제가 코드 자체보다 더 간단한 설명을 갖지 못하는 경우도 흔합니다.
증명 과정에서 결국 성립하지 않는 가정을 은근슬쩍 도입하기도 쉽고, 시스템 중 단 하나의 부분만 형식적 검증이 필요하다고 판단했다가, 다른 부분(심지어 하드웨어)에 존재하는 심각한 취약점에 의해 무너질 수도 있습니다.
Lean 자체 구현에도 버그가 있을 수 있습니다. 그러나 이러한 성가신 세부사항들을 논의하기 전에, 먼저 형식적 검증이 올바르고 이상적으로 수행될 경우 도달할 수 있는 유토피아적 미래를 심층적으로 탐구해 보겠습니다.
보안을 위해 고안된 형식적 검증
컴퓨터 코드의 버그는 끔찍합니다.
암호화폐를 변경 불가능한 블록체인 상의 스마트 계약에 넣고, 북한이 코드 버그를 발견하자마자 자동으로 당신의 자금을 모두 빼돌리고 이에 대해 이의 제기조차 불가능하다면, 코드 버그는 더욱 끔찍해집니다.
이 모든 것이 영지식 증명(zero-knowledge proof)으로 포장되면, 버그는 더욱 끔찍해집니다. 누군가 영지식 증명 시스템을 해킹하면, 돈을 전부 빼돌릴 수 있으며, 우리는 도대체 무슨 일이 일어났는지 전혀 알지 못할 것입니다(더 나쁜 건, 언제 문제가 발생했는지도 모른다는 점입니다).
클로드 마이토스(Claude Mythos)와 같은 강력한 AI 모델이 두 차례의 추가 반복 후에 버그를 자동으로 탐지할 수 있게 된다면, 코드 버그는 더욱더 끔찍해질 것입니다.
일부 사람들은 이러한 현실에 대해, 스마트 계약의 기본 개념 자체를 포기하자는 주장을 펼치거나, 사이버 공간이 방어자가 공격자보다 비대칭적 우위를 가질 수 있는 영역이 될 수 없다고 믿기도 합니다.
몇 가지 인용문을 소개합니다:
시스템을 강화하려면, 공격자가 취약점을 악용하는 데 쓰는 것보다 더 많은 리소스를 취약점을 발견하는 데 투입해야 합니다.
그리고:
우리 산업은 결정론적 코드(deterministic code)를 기반으로 구축되어 있습니다. 코드를 작성하고, 테스트하고, 출시하고, 그것이 제대로 작동한다고 확신합니다. 그러나 제 경험상, 이 신뢰의 약속은 이미 붕괴되고 있습니다.
정말 AI-네이티브 회사의 최고 운영자들 사이에서는, 코드베이스가 이제 ‘작동한다고 믿는’ 대상이 되었으며, 그 성공 확률을 더 이상 정확히 설명할 수 없게 되었습니다.
더 나쁜 것은, 일부 사람들이 유일한 해결책으로 오픈소스 포기를 제안한다는 점입니다.
사이버 보안 측면에서는 이것이 어두운 미래입니다. 특히 인터넷의 탈중앙화와 자유를 중시하는 우리에게는, 극도로 비관적인 전망입니다.
전체 암호 펑크(cypherpunk) 정신은 근본적으로 다음과 같은 아이디어에 기반합니다: 인터넷에서는 방어자가 우위를 점하며, 암호화, 서명, 혹은 증명과 같은 디지털 ‘성채(castle)’를 구축하는 것이 그것을 파괴하는 것보다 훨씬 쉽다는 것입니다.
이 우위를 잃어버린다면, 인터넷 보안은 규모의 경제(economies of scale)에서만 나오게 되고, 전 세계적으로 잠재적 공격자를 추적해야 하며, 더 넓은 의미에서 통치와 파괴 사이에서 선택해야만 하게 될 것입니다.
저는 이 견해에 동의하지 않으며, 사이버 보안의 미래에 대해 훨씬 낙관적인 비전을 가지고 있습니다.
강력한 AI의 버그 탐지 능력이 가져올 도전은 엄청나지만, 그것은 일시적인 도전입니다. 일단 혼란이 가라앉고 새로운 균형점에 도달하면, 우리는 과거보다 훨씬 방어자에게 유리한 환경을 얻게 될 것입니다.
모질라(Mozilla) 역시 저의 견해에 동의합니다. 그들의 말을 인용하자면:
당신은 다른 모든 일을 재조정하고, 이 작업에 지속적이고 집중적인 노력을 기울여야 할 수도 있습니다. 그러나 터널 끝에는 빛이 있습니다.
우리는 우리 팀이 이 도전에 어떻게 대응했는지 매우 자랑스럽게 생각하며, 다른 이들도 그렇게 할 수 있을 것이라고 믿습니다. 우리의 작업은 아직 끝나지 않았지만, 우리는 가장 어려운 고비를 넘겼으며, 겨우 따라가는 수준을 넘어 훨씬 더 아름다운 미래를 엿볼 수 있습니다.
방어자는 마침내 결정적인 승리를 거둘 기회를 얻었습니다. … 결함은 유한하며, 우리는 이제 그것들을 모두 찾아낼 수 있는 세상에 진입하고 있습니다.
현재 Mozilla 게시물에서 Ctrl+F로 ‘형식적(formal)’과 ‘검증(verification)’이라는 단어를 검색하면, 결과는 없습니다. 사이버 보안의 긍정적 미래는 형식적 검증이나 어떤 단일 기술에만 의존하지 않습니다.
그렇다면 무엇에 의존할까요? 기본적으로 다음 차트에 요약되어 있습니다:
CVE 취약점 수의 시간 경과에 따른 감소 추세
수십 년간, 여러 기술이 취약점 수 감소에 기여해 왔습니다:
- 타입 시스템(type system)
- 메모리 안전 언어(memory-safe language)
- 소프트웨어 아키텍처 개선(샌드박싱, 권한 제어 포함; 더 넓은 의미로는 ‘신뢰할 수 있는 컴퓨팅 기반(Trusted Computing Base)’과 ‘그 외 코드’를 명확히 구분하는 것)
- 개선된 테스트 방법
- 안전/비안전 코딩 패턴에 대한 지식 체계의 지속적 확장
- 사전 작성 및 감사된 소프트웨어 라이브러리의 지속적 증가
AI 보조 형식적 검증은 완전히 새로운 패러다임으로 보기보다는, 이미 진행 중인 추세와 패러다임을 강력하게 가속화하는 기술로 보는 것이 적절합니다.
형식적 검증은 만능이 아닙니다. 그러나 구현보다 목표가 훨씬 단순한 경우에 특히 효과적입니다. 이는 이더리움의 다음 주요 반복판에서 배포될 예정인, 극도로 복잡하고 난해한 기술들—양자 저항성 서명(quantum-resistant signature), STARK, 합의 알고리즘, ZK-EVM—에 특히 해당합니다.
STARK는 매우 복잡한 소프트웨어입니다. 그러나 그것이 구현하는 핵심 보안 속성은 이해하고 형식화하기 매우 쉽습니다: 프로그램 P, 입력 x, 출력 y에 대한 해시 H를 가리키는 증명을 본다면, (i) STARK에서 사용된 해시 알고리즘이 해킹되었거나, (ii) P(x) = y입니다.
따라서 Arklib 프로젝트는 완전히 형식적으로 검증된 STARK 구현을 만들려는 시도를 하고 있습니다(VCV-io 참조: 이는 다양한 다른 암호 프로토콜의 형식적 검증을 위한 기초 오라클 계산 인프라를 제공하며, 이 중 많은 것이 STARK의 종속성입니다).
그보다 더 야심 찬 프로젝트는 evm-asm입니다: 완전히 형식적으로 검증된 전체 EVM 구현을 구축하려는 프로젝트입니다.
여기서의 보안 속성은 훨씬 단순하지 않습니다: 기본적으로 목표는 Lean으로 작성된 다른 EVM 구현과의 동등성을 증명하는 것이며, 이 다른 구현은 실행 효율을 전혀 고려하지 않고, 최대한 직관적이고 가독성 있게 작성될 수 있습니다.
우리는 열 개의 EVM 구현을 얻을 수 있고, 이들 모두가 서로 동등하다는 것을 증명할 수 있지만, 우연히도 이들 모두가 공격자가 권한 없는 주소의 ETH를 모두 탈취할 수 있는 치명적인 결함을 포함할 가능성도 있습니다.
하지만 현재 어느 하나의 EVM 구현에 이런 결함이 존재할 가능성보다는 훨씬 낮습니다. 또 다른, 우리가 고통스러운 교훈을 통해 그 중요성을 깨달은 보안 속성은 DoS 공격에 대한 저항력인데, 이는 규격화하기가 훨씬 쉽습니다.
또 다른 두 가지 중요한 분야는 다음과 같습니다:
- 비잔틴 장애 허용 합의(Byzantine Fault Tolerant Consensus): 여기서는 기대되는 모든 보안 속성을 형식적으로 규격화하는 것이 어렵지만, 버그가 너무 흔했기에 시도해 볼 가치가 있습니다. 따라서 우리는 Lean에서 진행 중인 합의 프로토콜의 Lean 구현 및 증명을 보유하고 있습니다.
- 스마트 계약 프로그래밍 언어: Vyper 및 Verity에서의 형식적 검증을 참고하세요.
이 모든 경우에서, 형식적 검증이 제공하는 거대한 부가 가치 중 하나는 이러한 증명이 진정으로 단말 간(end-to-end)이라는 점입니다. 일반적으로 가장 골치 아픈 버그는 두 개의 독립적으로 고려된 하위 시스템의 접점에 숨어 있는 상호작용 버그(interaction bug)입니다.
인간은 전체 시스템을 단말 간으로 추론하기에는 너무 어렵습니다. 그러나 자동화된 규칙 검사 시스템은 이를 수행할 수 있습니다.
효율성을 위해 고안된 형식적 검증
evm-asm을 다시 살펴보겠습니다. 이것은 EVM 구현입니다. 하지만 이는 RISC-V 어셈블리어로 직접 작성된 EVM 구현입니다.
정말 그렇습니다.
ADD 연산 코드는 다음과 같습니다:
import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64
/-- 256비트 EVM ADD: 이진 연산, 스택에서 2개를 pop, 1개를 push.
Limb 0: LD, LD, ADD, SLTU (캐리), SD (5개 명령어).
Limbs 1-3: LD, LD, ADD, SLTU (캐리1), ADD (캐리인), SLTU (캐리2), OR (캐리아웃), SD (각 8개 명령어).
그 다음 ADDI sp, sp, 32.
레지스터: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/
def evm_add : Program :=
-- Limb 0 (5개 명령어)
LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;
-- Limb 1 (8개 명령어)
LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;
-- Limb 2 (8개 명령어)
LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;
-- Limb 3 (8개 명령어)
LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;
-- sp 조정
ADDI .x12 .x12 32
end EvmAsm.Evm64
RISC-V가 선택된 이유는, 현재 개발 중인 ZK-EVM 증명기는 일반적으로 RISC-V를 증명하고 이더리움 클라이언트를 RISC-V로 컴파일함으로써 작동하기 때문입니다. 따라서 RISC-V로 직접 작성된 EVM 구현을 사용한다면, 이는 가능한 가장 빠른 구현이 될 것입니다.
RISC-V는 일반 컴퓨터 내에서도 매우 효율적으로 시뮬레이션할 수 있으며(실제로 RISC-V 노트북도 시장에 나와 있습니다).
물론, 진정한 단말 간(end-to-end)을 위해서는 RISC-V 구현 자체(또는 증명기의 산술화)도 형식적으로 검증해야 하지만, 걱정하지 마세요. 이에 대한 작업도 이미 진행 중입니다.
어셈블리어로 직접 코드를 작성하는 것은 50년 전에 흔히 행하던 일이었습니다. 그 이후 우리는 고급 언어로 코드를 작성하도록 전환했습니다.
고급 언어는 효율성 면에서 타협을 하지만, 그 대가로 코드를 훨씬 빠르게 작성할 수 있고, 무엇보다도 타인의 코드를 이해하는 속도도 훨씬 빨라집니다. 이는 보안 측면에서 필수적입니다.
형식적 검증과 인공지능의 결합을 통해 우리는 ‘미래로 돌아가기(back to the future)’할 기회를 얻게 됩니다.
구체적으로는, 인공지능이 어셈블리 코드를 작성하고, 그 어셈블리 코드가 요구되는 속성을 갖는다는 형식적 증명을 작성할 수 있습니다.
적어도, 요구되는 속성은 단순히 가독성을 위해 최적화된, 인간 친화적인 고급 언어로 작성된 구현과 완벽히 동등하다는 것일 수 있습니다.
우리는 더 이상 가독성과 효율성 사이에서 균형을 맞춰야 하는 단일 코드 객체를 필요로 하지 않으며, 두 개의 독립된 객체를 갖게 됩니다: 하나는(어셈블리 구현) 특정 실행 환경의 요구 사항을 고려하여 오직 효율성만을 최적화하고, 다른 하나는(보안 선언 또는 고급 언어 구현) 오직 가독성만을 최적화하며, 수학적 증명을 통해 이 둘 사이의 동등성을 입증합니다.
사용자는 이 증명을 한 번 자동으로 검증한 후, 그 이후부터는 빠른 버전만 실행하면 됩니다.
이 방법은 매우 강력하며, 요이치 히라이는 이를 ‘소프트웨어 개발의 궁극적 형태’라고 명명한 데에는 이유가 있습니다.
형식적 검증은 만병통치약이 아니다
암호학 및 컴퓨터 과학 분야에는 형식적 방법 자체의 역사만큼 오래된 전통이 하나 있습니다. 바로 형식적 방법(또는 더 넓은 의미에서 ‘증명’에 대한 의존성)을 비판하는 전통입니다.
이 문헌에는 실제 사례가 가득합니다. 초기 수작업 증명 시대의 간단한 암호학을 예로 들어, 메네즈(Menezes)와 콜비츠(Koblitz)가 2004년에 한 비판을 인용하겠습니다:
1979년, 라빈(Rabin)은 일종의 ‘증명 가능’ 보안을 갖는 암호화 함수를 제안했습니다. 즉, 이는 귀납적 보안 속성을 갖습니다.
귀납적 보안 선언은, 암호문 y로부터 메시지 m을 찾을 수 있는 사람은 반드시 n을 소인수 분해할 수 있어야 한다는 것입니다. … 라빈의 암호화 방안이 제안된 직후, 리베스트(Rivest)는 풍자적으로, 이 추가적인 보안을 부여하는 특성 자체가 ‘선택 암호문 공격(chosen-ciphertext attack)’이라는 또 다른 유형의 공격자에 직면했을 때 전체 시스템을 무너뜨린다고 지적했습니다.
즉, 공격자가 앨리스(Alice)가 자신의 선택한 암호문을 해독하도록 속일 수 있다고 가정할 경우, 공격자는 위 문단에서 샘(Sam)이 n을 소인수 분해하기 위해 사용한 것과 동일한 단계를 따를 수 있습니다.
메네즈와 콜비츠는 이어 더 많은 사례를 제시합니다. 흔히 나타나는 패턴은, 암호 프로토콜을 더 ‘증명 가능’하게 하려는 설계가 종종 그것들을 더 ‘비자연스럽게’ 만들고, 설계자조차 고려하지 못한 방식으로 붕괴될 가능성을 높인다는 점입니다.
이제 기계 검증 가능한 증명과 코드로 돌아갑시다. 2011년, 형식적으로 검증된 C 컴파일러에서 버그가 발견되었다는 논문이 있습니다(링크):
우리가 발견한 CompCert의 두 번째 문제는 두 개의 버그로 인해 다음과 같은 코드가 생성되는 현상에 있습니다: stwu r1, -44432(r1). 여기서는 대규모 PowerPC 스택 프레임이 할당되고 있습니다.
문제는 16비트 이동(offset) 필드가 오버플로우한다는 점입니다. CompCert의 PPC 의미론은 이 즉시수(immediate) 너비에 대한 제한을 규정하지 않았고, 어셈블러가 범위를 벗어난 값을 포착할 것이라고 가정했습니다.
또 다른 2022년 논문(링크)도 있습니다:
CompCert-KVX에서, 커밋 e2618b31은 ‘nand’ 명령어가 ‘and’로 인쇄되는 버그를 수정했습니다. ‘nand’는 극히 드문 ~(a & b) 패턴에서만 사용됩니다. 이 버그는 무작위로 생성된 프로그램을 컴파일함으로써 발견되었습니다.
그리고 오늘날, 2026년, 나딤 코베이시(Nadim Kobeissi)는 Cryspen에서 형식적으로 검증된 소프트웨어의 버그를 다음과 같이 설명합니다:
2025년 11월, 필리포 발소르다(Filippo Valsorda)가 독자적으로 libcrux-ml-dsa v0.0.3이 동일한 결정론적 입력을 주었을 때, 서로 다른 플랫폼에서 서로 다른 공개 키와 서명을 생성한다는 사실을 보고했습니다.
이 버그는 SHA-3의 Keccak-f 치환에서 사용되는 XAR 연산을 구현하는 _vxarq_u64 내부 래퍼 함수에 있습니다. 하위 호환 메커니즘이 시프트 연산에 잘못된 인수를 전달했으며, 하드웨어 SHA-3 지원이 없는 ARM64 플랫폼에서 SHA-3 해시값이 손상되었습니다.
이것은 유형 I 결함(Type I fault)입니다: 해당 내부 함수는 표시되었지만, 전체 NEON 백엔드는 런타임 보안성 또는 정확성에 대한 증명이 완료되지 않았습니다.
그리고:
libcrux-psq 라이브러리는 양자 저항성 사전 공유 키 프로토콜을 구현합니다. decrypt_out 메서드에서, AES-GCM 128 복호화 경로가 복호화 결과에 대해 .unwrap()을 호출하여 오류를 전파하지 않았습니다. 형식이 잘못된 암호문 하나로 프로세스가 충돌합니다.
위의 네 가지 문제는 모두 다음 두 유형 중 하나에 속합니다:
- 검증이 부분 코드에만 수행된 경우(나머지 부분을 검증하기가 너무 어렵기 때문에), 결과적으로 검증되지 않은 코드가 작성자의 예상보다 훨씬 더 많은 결함(그리고 훨씬 더 치명적인 방식의 결함)을 포함하는 경우.
- 필요한 증명의 핵심 속성을 명시하지 않은 경우.
나딤의 글에는 형식적 검증 실패 패턴의 분류가 포함되어 있으며, 다른 유형의 실패 패턴(예: ‘형식적 규격 자체가 틀렸거나, 증명에 시스템이 묵인하는 거짓 진술이 포함되어 있다’)도 제시합니다.
마지막으로, 소프트웨어와 하드웨어 경계에서의 형식적 검증 실패를 살펴볼 수 있습니다. 여기서 흔한 문제는 측면 채널 공격(side-channel attack)에 대한 저항력 검증입니다.
당신의 메시지를 보호하는 암호 형태가 완벽하게 안전하더라도, 몇 미터 떨어진 사람이 전기 신호의 변동을 포착해 수십만 차례의 암호화 후 당신의 개인 키를 추출할 수 있다면, 당신은 여전히 안전하지 않습니다.
‘차분 전력 분석(Differential Power Analysis)’에 관한 이 글(링크)은 현재 잘 알려진 그러한 기술의 예시입니다.
차분 전력 분석은 측면 채널 공격의 일반적인 유형입니다. 출처: 위키백과
측면 채널 공격자에 대한 저항력을 증명하려는 시도는 계속되고 있습니다. 그러나 그러한 증명은 공격자의 수학적 모델을 필요로 하며, 이를 기반으로 보안을 증명해야 합니다.
때때로 ‘d 탐지 모델(d-probe model)’이 사용됩니다: 우리는 공격자가 회로 내에서 쿼리할 수 있는 위치 수에 알려진 제한이 있다고 가정합니다. 그러나 일부 유출 형태는 이러한 모델이 포착할 수 없습니다.
이 글에서 관찰된 바에 따르면, 흔한 문제는 전이적 유출(transient leakage)입니다: 위치의 값뿐만 아니라 그 값의 변화를 반영하는 신호를 관찰할 수 있다면, 이는 일반적으로 하나의 값이 아니라 새 값과 이전 값이라는 두 개의 값에서 필요한 정보를 복구하기에 충분합니다.
이 글은 다른 형태의 유출에 대한 분류도 제시합니다.
수십 년간, 형식적 검증에 대한 이러한 비판은 형식적 검증 기술을 더 나아지게 했습니다. 과거보다 우리는 이제 그러한 문제를 더 잘 방지할 수 있습니다. 그러나 오늘날에도 이 기술은 완벽하지 않습니다.
전체 맥락에서, 하나의 주요 단서가 있습니다. 형식적 검증은 강력합니다.
하지만 마케팅 용어가 형식적 검증을 ‘증명 가능한 정확성(provable correctness)’을 제공하는 것으로 보이게 만들더라도, 이 ‘증명 가능한 정확성’은 근본적으로 소프트웨어(또는 하드웨어)가 ‘정확하다’는 것을 증명하지는 못합니다.
대부분의 인간이 이해하는 ‘정확함(correctness)’의 의미는 다음과 같습니다: “사물의 동작이 개발자의 의도에 대한 사용자의 이해와 일치한다.”
그리고 ‘안전함(safety)’의 의미는 다음과 같습니다: “사물의 동작이 사용자의 기대를 위반하지 않으며, 사용자의 이익에 해로운 일을 하지 않는다.”
이 두 경우 모두, 정확성과 안전성은 수학적 객체와 인간의 의도 또는 기대 사이의 비교로 귀결됩니다.
인간의 의도와 기대도 기술적으로는 수학적 객체입니다. 결국 인간의 뇌 역시 우주의 일부이며, 충분한 계산 능력이 있다면 시뮬레이션할 수 있는 물리 법칙을 따릅니다.
그러나 이들은 믿을 수 없을 정도로 복잡한 수학적 객체이며, 컴퓨터도 우리 자신도 이해하거나 심지어 읽을 수 없습니다.
실제 목적과 의도에 비추어 볼 때, 이들은 흑상자(black box)입니다. 우리가 자신의 의도와 기대에 대해 어느 정도 이해할 수 있는 이유는, 우리 각자가 수년간 자신의 생각을 관찰하고 타인의 생각을 추론해 온 경험 때문입니다.
그리고 우리가 원시적인 인간 의도를 컴퓨터에 직접 집어넣을 수 없기 때문에, 형식적 검증은 인간의 의도와의 비교를 증명할 수 없습니다.
따라서 ‘증명 가능한 정확성’과 ‘증명 가능한 안전성’은 인간이 이해하는 ‘정확성’과 ‘안전성’을 실제로 증명하지 않습니다. 인간의 뇌를 완전히 시뮬레이션할 수 있게 되기 전까지는 어떤 것도 이를 증명할 수 없습니다.
그럼 이 기술은 도대체 무엇에 쓰는가?
저는 테스트 스위트, 타입 시스템, 형식적 검증을 모두 프로그래밍 언어의 보안성을 위한 동일한 근본적 방법의 서로 다른 구현으로 간주합니다(이것이 유일하게 합리적인 방법일 수도 있습니다).
이들은 모두 우리의 의도를 서로 다른 방식으로 중복해서 규격화하고, 자동으로 이 다양한 규격화가 서로 호환되는지 검사하는 데 관한 것입니다.
다음 Python 코드를 예로 들어보겠습니다:
def fib(n: int) -> int:
if n < 0:
raise Exception("Negative values not supported")
elif 0 <= n < 2:
return n
else:
return fib(n-1) + fib(n-2)
if __name__ == '__main__':
assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
assert fib(15) == 610
여기서 당신은 세 가지 다른 방식으로 자신의 의도를 표현합니다:
- 명시적으로, 코드 내에서 피보나치 공식을 구현함으로써
- 암시적으로, 타입 시스템을 통해(입력, 출력, 재귀 중간 단계가 모두 정수임을 지정함)
- ‘샘플 패키지(sample pack)’ 방식을 통해: 테스트 케이스
파일을 실행하면 공식과 예시가 비교됩니다. 타입 검사기는 타입 호환성을 검증합니다: 두 정수를 더하는 것은 허용되는 연산이며, 또 다른 정수를 생성합니다.
타입 시스템은 물리학에서 과제를 검사하는 좋은 방법입니다: 가속도를 계산했는데 단위가 m/s²가 아니라 m/s가 나온다면, 분명 잘못 계산한 것입니다.
테스트 케이스는 ‘샘플 패키지’ 정의의 한 인스턴스이며, 인간이 개념을 처리할 때 이 방식이 직접적인 명시적 정의보다 훨씬 자연스럽습니다.
당신의 의도를 표현하는 방식이 다양할수록, 이상적으로는 서로 다른 사고방식을 요구하는 방식일수록, 이 모든 표현이 서로 호환됨이 입증될 때, 당신이 실제로 원하던 것을 표현해냈다는 확신이 커집니다.
안전한 프로그래밍은 자신의 의도를 여러 가지 서로 다른 방식으로 표현하고, 자동으로 이 표현들이 모두 서로 호환되는지 검증하는 것입니다.
형식적 검증은 이 방법을 한층 더 확장할 수 있게 해줍니다. 형식적 검증을 통해, 당신은 거의 무한한 수의 서로 다른 중복 방식으로 자신의 의도를 규격화할 수 있으며, 프로그램은 이 모든 방식이 호환될 때만 검증을 통과합니다.
고도로 최적화된 구현과, 효율성은 극도로 낮지만 인간이 읽기 쉬운 구현을 모두 규격화하고, 이 둘이 일치함을 검증할 수 있습니다. 당신의 열 명의 친구에게 당신의 프로그램이 가져야 한다고 생각하는 수학적 속성 목록을 요청한 후, 그것들이 모두 통과하는지 확인할 수도 있습니다.
통과하지 못한다면, 프로그램이 틀렸는지, 아니면 수학적 속성이 잘못 정의되었는지를 찾아냅니다. 또한, 인공지능을 활용해 이 모든 작업을 극도로 효율적으로 수행할 수 있습니다.
그럼 나는 어떻게 시작해야 하나?
현실적으로 말하면, 당신이 직접 증명을 작성하지는 않을 것입니다. 형식적 방법이 널리 퍼지지 못한 이유는 대부분의 사람들이 이러한 난해한 내용을 어떻게 작성해야 할지 모르기 때문입니다. 아래 코드의 의미를 설명할 수 있습니까?
/-- Helper: foldl 수준에서 누산기(acc)와 함께 점별(pointwise) ≤.
private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : Nat) (hAcc : a ≤ b)
(hLE : Forall₂ (· ≤ ·) ds1 ds2) :
List.foldl (λ acc d => acc * w + d) a ds1 ≤
List.foldl (λ acc d => acc * w + d) b ds2 := by
match ds1, ds2, hLE with
| [], [], .nil => exact hAcc
| d1::ds1', d2::ds2', .cons hd htl =>
simp [List.foldl]
refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl
exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd
(궁금하시다면, 이것은 SPHINCS 서명 변형의 특정 보안 선언을 증명하는 과정에서 등장하는 여러 보조 정리(sub-lemma) 중 하나입니다.
구체적으로, 이 선언은 다음과 같습니다: 해시 충돌이 발생하지 않는 한, 어떤 메시지의 서명은 다른 어떤 메시지의 서명보다도 최소한 하나의 해시 계단에서 더 높은 값을 필요로 하며, 따라서 다른 서명에서 계산할 수 없는 정보를 포함한다는 것입니다.)
수동으로 코드와 증명을 작성할 필요는 없습니다. 인공지능이 당신을 대신해 프로그램을 작성해 줄 수 있습니다(Lean으로 직접 작성하거나, 속도를 위해 어셈블리어로 작성하든 상관없이), 그리고 그 과정에서 기대되는 어떤 속성도 자동으로 증명해 줄 수 있습니다.
이 작업은 자기 검증(self-verifying)이라는 장점이 있어, 당신이 직접 감독할 필요가 없습니다. 그냥 인공지능을 몇 시간 동안 계속 실행시키면 됩니다.
가장 나쁜 경우는 아무런 진전 없이 제자리걸음만 하거나(또는 제가 사용한 leanstral이 한 것처럼, 자신의 작업 부담을 줄이기 위해 요청된 증명 대상을 스스로 바꿔치기하는 경우)입니다.
당신이 마지막에 확인해야 할 유일한 것은, 인공지능이 증명한 선언이 당신의 요구에 부합하는지 여부입니다.
SPHINCS 서명 변형에서, 최종 선언은 다음과 같습니다:
theorem wots_fullDigits_incomparable
{dig1 dig2 : List Nat} {w l1 l2 : Nat}
(hw : 0 < w)
(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)
(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)
(hL2suff : l1 * (w - 1) < w ^ l2)
(hNeq : dig1 ≠ dig2) :
¬ Forall₂ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧
¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)
이것은 사실상 겨우 읽을 수 있는 수준에 있습니다:
하나의 해시 요약(dig1)에서 생성된 숫자가 다른 해시 요약(dig2)에서 생성된 숫자와 같지 않다면,
다음 두 경우는 모두 성립하지 않습니다:
- 모든 숫자에 대해, dig1의 숫자 ≤ dig2의 숫자
- 모든 숫자에 대해, dig2의 숫자 ≤ dig1의 숫자
이것은 체크섬을 추가해 생성된 ‘확장된 숫자(wotsFullDigits)’에도 동일하게 적용됩니다. 즉, dig1의 확장 버전에서는 어딘가의 숫자가 더 높을 수밖에 없고, dig2의 확장 버전에서는 다른 곳에서 숫자가 더 높을 수밖에 없습니다.
증명 작성에 있어서 대규모 언어 모델(Large Language Model)을 사용해 본 결과, 클로드(Claude)와 딥시크 4 프로(Deepseek 4 Pro) 모두 잘 작동합니다. Leanstral은 Lean 작성을 위해 특별히 미세 조정된 작은 오픈소스 웨이트 모델로서, 매우 유망한 대안입니다.
이 모델은 119B 파라미터를 가지며, 토큰당 6B가 활성화되며, 로컬에서 실행할 수 있습니다(제 노트북에서는 약 15토큰/초의 속도로 실행됨). 벤치마크에 따르면, Leanstral은 훨씬 더 큰 일반 모델보다 우수합니다:
제 현재 개인 경험에 따르면, Deepseek 4 Pro보다 약간 뒤처지긴 하지만, 여전히 매우 효과적입니다.
형식적 검증은 우리 문제의 전부를 해결해주지는 않습니다.
하지만 인터넷 보안 모델이 소수의 강력한 조직을 모두 신뢰하는 데 기반을 두지 않도록 하려면, 우리는 코드를 신뢰해야 하며, 이는 강력한 인공지능 공격자에 대해서도 코드를 신뢰해야 함을 의미합니다.
AI 보조 형식적 검증은 이 목표를 달성하는 데 확고한 한 걸음을 내딛게 해줍니다.
블록체인과 ZK-SNARK처럼, 인공지능과 형식적 검증은 매우 보완적인 기술입니다.
블록체인은 프라이버시와 확장성을 희생하면서 개방적 검증성과 검열 저항성을 부여하고, ZK-SNARK는 다시 프라이버시와 확장성을 돌려줍니다(사실상 이전보다 훨씬 더 많이).
인공지능은 정확성을 희생하면서 대량의 코드 작성을 가능하게 하며, 형식적 검증은 다시 정확성을 돌려줍니다(사실상 이전보다 훨씬 더 높은 수준의 정확성).
기본 설정(default) 상태에서 인공지능은 극도로 부주의한 코드를 대량으로 생산할 것이며, 버그 수는 증가할 것입니다.
사실, 어떤 경우에는 버그 증가를 용인하는 것이 올바른 균형일 수도 있습니다: 버그가 경
TechFlow 공식 커뮤니티에 오신 것을 환영합니다
Telegram 구독 그룹:https://t.me/TechFlowDaily
트위터 공식 계정:https://x.com/TechFlowPost
트위터 영어 계정:https://x.com/BlockFlow_News
@VitalikButerin
