비탈릭: 이더리움 다음 단계의 핵심은 무엇인가요?

저자：Vitalik Buterin

편집: 가환, ChainCatcher

특별히 Yoichi Hirai, Justin Drake, Nadim Kobeissi, Alex Hicks의 피드백과 검토에 감사드립니다.

지난 몇 달 동안, 새로운 프로그래밍 패러다임이 이더리움의 최전선 연구 커뮤니티와 컴퓨팅 분야의 많은 다른 구석에서 빠르게 인기를 얻고 있습니다: 매우 저수준의 언어(예: EVM 바이트코드, 어셈블리 언어) 또는 Lean을 사용하여 코드를 작성하고, Lean으로 작성된 자동 검증 가능한 수학적 증명을 사용하여 그 정확성을 검증하는 것입니다.

적절히 수행된다면, 이는 극도로 효율적인 코드를 출력할 수 있을 뿐만 아니라, 이전의 프로그래밍 방식보다 훨씬 안전할 수 있습니다. Yoichi Hirai는 이를 "소프트웨어 개발의 궁극적인 형태"라고 부릅니다.

이 글은 그 기본 원리를 밝히고, 소프트웨어의 형식적 검증이 무엇을 할 수 있는지, 그리고 이더리움 및 기타 분야에서 그 약점과 한계가 어디에 있는지를 탐구하려고 합니다.

형식적 검증이란 무엇인가?

형식적 검증은 자동으로 검사할 수 있는 방식으로 수학 정리에 대한 증명을 작성하는 것을 의미합니다. 상대적으로 간단하지만 여전히 흥미로운 예를 들어보겠습니다. 피보나치 수열에 대한 기본 정리: 매 세 번째 숫자는 짝수이고 나머지는 홀수입니다.

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

이를 증명하는 간단한 방법은 수학적 귀납법을 사용하는 것입니다. 매번 세 걸음 앞으로 나아갑니다.

첫 번째는 기본 경우입니다. F1 = F2 = 1, F3 = 2로 설정합니다. 관찰을 통해 우리는 이 진술("Fi는 3의 배수일 때 짝수, 그렇지 않으면 홀수")이 x = 3 이전에 성립함을 알 수 있습니다.

다음은 귀납적 경우입니다. 이 진술이 3k+3 이전에 성립한다고 가정합니다. 즉, 우리는 이미 F3k+1, F3k+2, F3k+3의 홀짝성을 각각 홀수, 홀수, 짝수로 알고 있습니다. 우리는 다음 세 숫자의 홀짝성을 계산할 수 있습니다:

F3k+4 = F3k+2 + F3k+3 = 홀수 + 짝수 = 홀수 F3k+5 = F3k+3 + F3k+4 = 짝수 + 홀수 = 홀수 F3k+6 = F3k+4 + F3k+5 = 홀수 + 홀수 = 짝수

따라서 우리는 이 진술이 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년 동안 존재했음에도 불구하고 이 분야가 여전히 소수에 불과한 이유를 설명하는 데 큰 역할을 합니다. 하지만 반면에 인공지능의 빠른 발전으로 인해 이전에는 불가능했던 많은 것들이 지금 빠르게 가능해지고 있습니다.

수학적 증명이 코드의 수호자가 되기 시작할 때

지금까지 당신은 아마 이렇게 생각할 것입니다: 좋습니다, 컴퓨터가 수학 정리의 증명을 검증할 수 있으니, 우리는 드디어 소수와 같은 미친 새로운 결론 중에서 어떤 것이 진짜인지, 어떤 것이 백 페이지 PDF 논문 속의 오류인지 확실히 알 수 있게 되었습니다.

어쩌면 우리는 와카모리 신이 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이 그 의미를 요약한 것입니다:

passivesecrecyle_ddh 정리는 X3DH의 수동 메시지 비밀성이 무작위 예언 모델 하의 DDH 가정과 최소한 같은 정도로 어렵다는 것을 나타내는 간결한 축약입니다. 만약 공격자가 X3DH의 수동 메시지 비밀성을 해독할 수 있다면, 그들은 DDH도 해독할 수 있습니다.

우리가 DDH가 해독하기 어렵다고 가정하므로, X3DH는 수동 공격에 대해서도 안전합니다. 이 정리는 공격자가 Signal의 키 교환 메시지를 수동적으로 관찰할 수 있다면, 그들이 생성한 세션 키를 무작위 키와 구별할 수 있는 확률이 무시할 수 있는 수준보다 높지 않다는 것을 증명합니다.

이것을 AES 암호화 구현의 정확한 증명과 결합하면, Signal 프로토콜의 암호화가 수동 공격자에게 안전하다는 증명을 얻게 됩니다.

유사한 프로젝트는 TLS와 브라우저 내 암호학의 다른 부분 구현이 안전하다는 것을 증명했습니다.

완전한 엔드 투 엔드 형식적 검증을 수행하면, 당신이 증명하는 것은 단순히 프로토콜의 어떤 이론적 설명이 안전하다는 것이 아니라, 사용자가 실행하는 구체적인 코드가 실제로 안전하다는 것입니다.

사용자의 관점에서 볼 때, 이는 신뢰를 필요로 하지 않는 것을 크게 향상시킵니다: 코드를 완전히 신뢰하기 위해 전체 코드베이스를 검토할 필요가 없으며, 단지 그것이 증명된 그 진술에 대해서만 검토하면 됩니다.

이제 "안전"이라는 이 중요한 단어가 정확히 무엇을 의미하는지에 대한 몇 가지 중요한 전제가 필요합니다.

사람들은 정말 중요한 진술을 증명하는 것을 잊기 쉽습니다. 때때로 증명해야 할 진술은 코드 자체보다 더 간단한 설명 방식이 없다는 것을 발견하기도 쉽습니다.

증명에서 최종적으로 성립하지 않는 가정을 몰래 도입하기도 쉽습니다. 시스템에서 형식적 증명이 실제로 필요한 부분이 하나뿐이라고 결정했지만, 결과적으로 다른 부분(심지어 하드웨어)에서 심각한 결함에 직면하게 될 수도 있습니다.

Lean 구현 자체에도 버그가 있을 수 있습니다. 하지만 이러한 성가신 세부 사항을 논의하기 전에, 형식적 검증을 올바르고 이상적으로 완료했을 때 가져올 수 있는 유토피아에 대해 먼저 깊이 탐구해 보겠습니다.

안전을 위한 형식적 검증

컴퓨터 코드의 버그는 무섭습니다.

당신이 암호화폐를 불변의 체인 상 스마트 계약에 넣고, 북한이 코드에 버그가 발생했을 때 당신의 모든 자금을 자동으로 빼낼 수 있으며, 당신은 이의를 제기할 수 없을 때, 코드의 버그는 더욱 무섭습니다.

이 모든 것이 제로 지식 증명으로 포장될 때, 버그는 더욱 무섭습니다. 누군가 제로 지식 증명 시스템을 해킹하는 데 성공하면, 그들은 모든 돈을 추출할 수 있으며, 우리는 무슨 문제가 발생했는지 전혀 알지 못합니다(더 나쁜 것은, 언제 문제가 발생했는지조차 모른다는 것입니다).

우리가 강력한 AI 모델을 갖게 되었을 때, 예를 들어 2년 후의 Claude Mythos와 같은 모델이 이러한 버그를 자동으로 발견할 수 있다면, 코드의 버그는 더욱 더 무섭습니다.

이 현실에 대한 일부 사람들의 반응은 스마트 계약의 기본 개념을 포기하자는 것이며, 심지어 네트워크 분야는 방어자가 공격자에 대해 비대칭적 우위를 가질 수 없는 분야라고 주장합니다.

몇 가지 인용문:

시스템을 강화하려면 공격자가 취약점을 이용하는 데 사용하는 것보다 더 많은 토큰을 사용해야 합니다.

그리고:

우리 산업은 결정론적 코드에 기반하고 있습니다. 그것을 작성하고, 테스트하고, 배포하고, 그것이 작동한다고 확신하지만, 제 경험상 이러한 계약은 깨지고 있습니다.

진정한 AI 원주율 회사의 최고의 운영자들 사이에서, 코드베이스는 당신이 그것이 작동한다고 "믿는" 것에 불과하며, 그것의 성공 확률을 정확히 설명할 수 없습니다.

더 나쁜 것은, 일부 사람들은 유일한 해결책이 오픈 소스를 포기하는 것이라고 생각합니다.

사이버 보안에 있어, 이는 어두운 미래가 될 것입니다. 특히 인터넷의 탈중앙화와 자유를 걱정하는 우리에게는 극히 비관적인 전망입니다.

전체 암호 해적 정신은 근본적으로 다음과 같은 이념에 기반하고 있습니다: 인터넷에서 방어자는 우위를 가지며, 디지털 "성"을 구축하는 것은 파괴하는 것보다 훨씬 쉽습니다(암호화, 서명 또는 증명).

우리가 이것을 잃는다면, 인터넷 보안은 규모의 경제에서, 전 세계적으로 잠재적인 공격자를 추적하는 것에서만 올 수 있으며, 더 넓은 의미에서 지배와 파괴 사이에서 선택해야만 합니다.

나는 동의하지 않으며, 사이버 보안의 미래에 대해 더 낙관적인 비전을 가지고 있습니다.

나는 강력한 AI의 취약점 탐지 능력이 가져오는 도전이 심각하다고 생각하지만, 그것은 과도기적 도전입니다. 일단 먼지가 가라앉고 새로운 균형점에 도달하면, 우리는 과거보다 방어자에게 더 유리한 환경을 얻게 될 것입니다.

Mozilla는 내 의견에 동의합니다. 그들의 말을 인용하자면:

당신은 모든 다른 업무의 우선 순위를 재조정하고 이 작업에 지속적이고 집중적인 노력을 기울여야 할 수도 있지만, 터널의 끝에는 빛이 있습니다.

우리는 우리 팀이 이 도전에 어떻게 대응하는지에 대해 매우 자랑스럽게 생각하며, 다른 사람들도 그렇게 할 수 있습니다. 우리의 작업은 아직 끝나지 않았지만, 우리는 어려운 시기를 극복했으며, 단지 간신히 따라가는 것이 아니라 훨씬 더 나은 미래를 엿볼 수 있습니다.

방어자는 마침내 결정적으로 승리할 기회를 가집니다. … 결함은 한정적이며, 우리는 마침내 그것들을 모두 찾아낼 수 있는 세계로 들어가고 있습니다.

이제, 만약 당신이 Mozilla의 게시물에서 "형식적"과 "검증"이라는 두 단어를 Ctrl+F로 검색한다면, 당신은 일치하는 항목이 전혀 없다는 것을 발견할 것입니다. 사이버 보안의 긍정적인 미래는 형식적 검증이나 다른 어떤 단일 기술에 전적으로 의존하지 않습니다.

그것은 무엇에 달려 있을까요? 기본적으로 이 차트에 달려 있습니다:

CVE 취약점 수의 시간에 따른 감소 추세

수십 년 동안, 많은 기술이 취약점 수의 감소에 기여했습니다:

• 타입 시스템
• 메모리 안전 언어
• 소프트웨어 아키텍처의 개선(샌드박스화, 권한 제어 및 "신뢰할 수 있는 컴퓨팅 기반"과 "기타 코드"를 명확히 구분하는 것 포함)
• 더 나은 테스트 방법
• 보안 및 비보안 코딩 패턴에 대한 지식 체계의 지속적인 풍부화
• 사전 작성되고 감사된 소프트웨어 라이브러리의 지속적인 증가

AI 지원 형식적 검증은 새로운 패러다임으로 간주되어서는 안 되며, 오히려 이미 발전하고 있는 경향과 패러다임의 강력한 가속기로 여겨져야 합니다.

형식적 검증은 만능이 아닙니다. 그러나 그것은 목표가 구현보다 훨씬 간단한 경우에 특히 적합합니다. 이는 우리가 이더리움의 다음 주요 반복에서 배포해야 할 극도로 복잡한 기술들, 즉 양자 저항 서명, STARKs, 합의 알고리즘 및 ZK-EVMs에서 특히 사실입니다.

STARK는 매우 복잡한 소프트웨어입니다. 그러나 그것이 구현하는 핵심 보안 속성은 이해하고 형식화하기가 쉽습니다: 프로그램 P를 가리키는 해시 H, 입력 x 및 출력 y의 증명을 본다면, (i) STARK에서 사용되는 해시 알고리즘이 공격받았거나, (ii) P(x) = y입니다.

따라서 우리는 Arklib 프로젝트를 갖게 되었으며, 이는 완전히 형식적 검증된 STARK 구현을 만들려고 합니다(VCV-io를 참조하십시오. 이는 다양한 다른 암호 프로토콜의 형식적 검증에 사용할 수 있는 기본 예언자 계산 인프라를 제공합니다. 그 중 많은 것이 STARK의 의존성입니다).

더 야심찬 것은 evm-asm입니다: 완전히 형식적 검증된 전체 EVM 구현을 구축하는 프로젝트입니다.

여기서 보안 속성은 그렇게 간단하고 명확하지 않습니다: 기본적으로 목표는 Lean으로 작성된 다른 EVM 구현과 동등하다는 것을 증명하는 것입니다. 그러나 그 구현은 최대한 직관성과 가독성을 위해 작성되었으며, 특정 실행 효율성을 고려할 필요가 없습니다.

우리는 동등하게 증명할 수 있는 열 개의 EVM 구현을 얻을 수 있으며, 그들은 우연히도 동일한 치명적인 결함을 포함하고 있어 공격자가 권한이 없는 주소에서 모든 ETH를 빼낼 수 있습니다.

하지만 이는 현재 어떤 EVM 구현이 이러한 결함을 가지고 있을 가능성보다 훨씬 적습니다. 그리고 우리가 고통스러운 교훈을 겪은 후 그 중요성을 이해하게 된 또 다른 보안 속성인 DoS 공격 저항 능력은 쉽게 규정할 수 있습니다.

또한 두 가지 중요한 분야는 다음과 같습니다:

• 비잔틴 내결함성 합의. 여기서는 모든 기대되는 보안 속성을 형식적으로 규정하는 것이 마찬가지로 어렵지만, 버그가 그렇게 흔했던 것을 고려할 때 시도할 가치가 있습니다. 따라서 우리는 Lean에서 진행 중인 합의 프로토콜의 Lean 구현 및 증명을 가지고 있습니다.
• 스마트 계약 프로그래밍 언어: Vyper 및 Verity의 형식적 검증을 참조하십시오.

이 모든 경우에서 형식적 검증이 제공하는 엄청난 부가 가치 중 하나는 이러한 증명이 실제로 엔드 투 엔드라는 것입니다. 일반적으로 가장 성가신 버그는 상호작용 버그로, 두 개의 독립적으로 고려된 하위 시스템의 경계에 숨어 있습니다.

인간에게는 전체 시스템을 엔드 투 엔드로 추론하는 것이 너무 어렵습니다. 그러나 자동화된 규칙 검사 시스템은 이를 수행할 수 있습니다.

효율성을 위한 형식적 검증

evm-asm을 다시 살펴보겠습니다. 이것은 EVM 구현입니다. 그러나 RISC-V 어셈블리로 직접 작성된 EVM 구현입니다.

진짜로.

다음은 ADD 연산 코드입니다:

import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64

/-- 256-bit EVM ADD: 이진, 2개 팝, 1개 푸시.
    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 노트북도 있습니다).

물론, 진정한 엔드 투 엔드를 구현하기 위해서는 RISC-V의 구현(또는 증명기의 산술화) 자체를 형식적으로 검증해야 하지만, 걱정하지 마십시오. 이 분야의 작업도 이미 존재합니다.

어셈블리로 직접 코드를 작성하는 것은 우리가 50년 전 자주 하던 일입니다. 그때부터 우리는 이러한 관행을 포기하고 고급 언어로 코드를 작성하기 시작했습니다.

고급 언어는 효율성에서妥協를 하지만, 그 대가로 코드를 작성하는 속도가 훨씬 빨라지고, 더 중요한 것은 다른 사람의 코드를 이해하는 속도도 훨씬 빨라지며, 이는 보안에 필수적입니다.

형식적 검증과 인공지능의 결합 덕분에 우리는 "미래로 돌아가는" 기회를 갖게 되었습니다.

구체적으로 말하자면, 우리는 인공지능이 어셈블리 코드를 작성하게 하고, 그 어셈블리 코드가 필요한 속성을 갖추었다는 것을 검증하는 형식적 증명을 작성할 수 있습니다.

최소한, 필요한 속성은 가독성을 높이기 위해 최적화된 구현과 완벽하게 동등해야 합니다.

우리는 더 이상 단일 코드 객체가 가독성과 효율성 사이에서 균형을 맞출 필요가 없으며, 두 개의 독립적인 객체를 갖게 됩니다: 하나는(어셈블리 구현) 효율성을 최적화하고, 다른 하나는(안전 선언 또는 고급 언어 구현) 가독성을 최적화하며, 그 후 우리는 수학적 증명을 통해 두者之间의 동등성을 증명합니다.

사용자는(자동으로) 한 번 그 증명을 검증할 수 있으며, 그 이후에는 빠른 버전을 실행하기만 하면 됩니다.

이 방법은 매우 강력하며, Yoichi Hirai가 "소프트웨어 개발의 궁극적인 형태"라고 부른 이유가 있습니다.

형식적 검증은 만병통치약이 아니다

암호학 및 컴퓨터 과학 분야에는 형식적 방법(또는 더 넓게는 "증명"에 대한 의존성)을 비판하는 전통이 있습니다. 이 전통은 형식적 방법 자체의 역사만큼이나 오래되었습니다.

이 문헌은 실제 사례로 가득 차 있습니다. 초기 간단한 암호학 시대의 손으로 쓴 증명에서 시작하겠습니다. 여기서 인용된 것은 Menezes와 Koblitz의 2004년 비판입니다:

1979년, Rabin은 어떤 의미에서 "증명 가능한" 안전성을 가진 암호 함수 하나를 제안했습니다. 즉, 그것은 어떤 환원주의적 안전 속성을 가지고 있습니다.

환원주의 안전 진술은 암호문 y에서 메시지 m을 찾을 수 있는 사람은 n을 분해할 수 있어야 한다고 말합니다. … Rabin이 그의 암호화 방안을 제안한 직후, Rivest는 아이러니하게도, 그에게 추가적인 안전성을 부여하는 이 특성이 "선택 암호문"이라는 공격자에 직면했을 때 전체가 무너질 것이라고 지적했습니다.

즉, 공격자가 어떤 방식으로든 Alice가 선택한 암호문을 해독하도록 속일 수 있다면, 공격자는 Sam이 n을 분해하는 데 사용한 것과 동일한 단계를 따를 수 있습니다.

Menezes와 Koblitz는 더 많은 예를 제시합니다. 일반적인 경향은 암호 프로토콜을 더 "증명 가능"하게 만들기 위한 설계가 종종 그것들을 더 "자연스럽지 않게" 만들어, 설계자가 고려하지 않은 상황에서 무너질 가능성이 더 높아진다는 것입니다.

이제 기계 검증 가능한 증명과 코드로 돌아가 보겠습니다. 이는 2011년에 발견된 형식적 검증된 C 컴파일러에서의 취약점에 대한 논문입니다:

우리가 발견한 두 번째 CompCert 문제는 다음과 같은 코드를 생성하는 두 개의 버그에 나타납니다: stwu r1, -44432(r1) 여기서 대형 PowerPC 스택 프레임이 할당되고 있습니다.

문제는 16비트의 비트 이동 필드가 오버플로우되었습니다. CompCert의 PPC 의미는 이 즉시 수의 너비에 대한 제한을 규정하지 않았으며, 그들은 어셈블러가 범위를 초과한 값을 포착할 것이라고 가정했습니다.

또 다른 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 작업을 구현한 vxarqu64 내부 포장 함수에 존재합니다. 백업 메커니즘이 이동 작업에 잘못된 매개변수를 전달하여 하드웨어 SHA-3 지원이 없는 ARM64 플랫폼에서 SHA-3 해시가 손상되었습니다.

이는 유형 I 결함에 해당합니다: 이 내부 함수는 마킹되었지만 전체 NEON 백엔드는 런타임 안전성이나 정확성에 대한 증명을 완료하지 않았습니다.

또한:

libcrux-psq 라이브러리는 후량자 사전 공유 키 프로토콜을 구현합니다. decrypt_out 메서드에서 AES-GCM 128 복호화 경로는 복호화 결과에 대해 .unwrap()을 호출하고 오류를 전파하지 않습니다. 형식이 잘못된 암호문은 프로세스를 충돌시킬 수 있습니다.

위의 네 가지 문제는 다음 두 가지 유형 중 하나에 해당합니다:

• 코드의 일부만 검증된 경우(나머지를 검증하기에는 너무 어려워서), 결과적으로 검증되지 않은 코드가 저자 예상보다 더 많은 취약점을 가지고 있음을 발견했습니다(그리고 그 방식이 더 치명적입니다).
• 저자가 증명해야 할 핵심 속성을 규정하는 것을 잊은 경우입니다.

Nadim의 글에는 형식적 검증 실패 패턴에 대한 분류가 포함되어 있으며, 그는 다른 유형의 실패 패턴(예: 또 다른 주요 경우는 "형식적 규범 자체가 잘못되었거나 증명에 구축 시스템이 조용히 수용한 허위 진술이 포함된 경우")도 제시합니다.

마지막으로, 소프트웨어와 하드웨어 경계에서의 형식적 검증 실패를 살펴보겠습니다. 여기서 흔한 문제 중 하나는 사이드 채널 공격에 대한 저항력을 검증하는 것입니다.

당신이 메시지를 보호하기 위해 완벽하게 안전한 암호 형식을 가지고 있다 하더라도, 몇 미터 떨어진 사람이 전기 신호의 변화를 포착하고 수십만 번의 암호화 후에 당신의 개인 키를 추출할 수 있다면, 당신은 여전히 안전하지 않습니다.

이는 "차분 전력 분석"에 대한 기사로, 현재 충분히 이해된 이러한 기술의 예입니다.

차분 전력 분석은 사이드 채널 공격의 일반적인 유형입니다. 출처: 위키백과

사람들은 이러한 공격자에 대한 저항력을 증명하려고 시도해왔습니다. 그러나 그러한 증명은 특정 공격자의 수학적 모델이 필요하며, 이를 통해 증명할 수 있습니다.

때때로 "d 탐지 모델"이 사용됩니다: 우리는 공격자가 회로에서 쿼리할 수 있는 위치 수에 대해 알려진 제한이 있다고 가정합니다. 그러나 일부 누출 형태는 이러한 모델로 포착할 수 없습니다.

이 기사에서 관찰된 바와 같이, 흔한 문제는 과도기적 누출입니다: 만약 당신이 특정 위치의 값뿐만 아니라 그 값의 변화에 따라 달라지는 신호를 관찰할 수 있다면, 이는 일반적으로 두 값(새로운 값과 이전 값)에서 필요한 정보를 복원하는 데 충분합니다.

이 기사는 다른 형태의 누출에 대한 분류를 제공합니다.

수십 년 동안, 이러한 형식적 검증에 대한 비판은 형식적 검증을 개선하는 데 도움이 되었습니다. 과거에 비해 우리는 이제 이러한 문제를 예방하는 데 더 능숙합니다. 그러나 오늘날에도 여전히 완벽하지 않습니다.

전반적으로, 여기에는 하나의 주요 실마리가 있습니다. 형식적 검증은 강력합니다.

그러나 마케팅 용어가 형식적 검증을 "증명 가능한 정확성"을 제공하는 것처럼 들리게 하더라도, 이른바 "증명 가능한 정확성"은 본질적으로 소프트웨어(또는 하드웨어)가 "정확하다"고 증명하지 않습니다.

대부분의 인간 이해에 따르면, "정확하다"는 것은 "사물의 행동이 사용자에 대한 개발자의 의도와 일치한다"는 의미입니다.

그리고 "안전하다"는 것은 "사물의 행동이 사용자의 기대를 위반하지 않고, 사용자에게 불리한 행동을 하지 않는다"는 의미입니다.

이 두 경우 모두, 정확성과 안전성은 수학적 객체와 인간의 의도 또는 기대 간의 비교로 귀결됩니다.

인간의 의도와 기대는 기술적으로도 수학적 객체입니다. 결국 인간의 뇌도 우주의 일부이며, 충분한 계산 능력이 있다면 시뮬레이션할 수 있는 물리 법칙을 따릅니다.

그러나 그것들은 믿을 수 없을 만큼 복잡한 수학적 객체이며, 컴퓨터와 우리 자신도 이해하거나 읽을 수 없습니다.

모든 실제 의도와 목적에 대해, 그것들은 블랙 박스입니다. 우리가 자신의 의도와 기대에 대해 어떤 이해를 갖는 것은 단지 우리가 각자 수년간 자신의 생각을 관찰하고 타인의 생각을 추론한 경험 덕분입니다.

그리고 우리는 원래의 인간 의도를 컴퓨터에 넣을 수 없기 때문에, 형식적 검증은 인간 의도와의 비교를 증명할 수 없습니다.

따라서 "증명 가능한 정확성"과 "증명 가능한 안전성"은 실제로 우리가 인간이 이해하는 "정확성"과 "안전성"을 증명하지 못합니다. 우리가 인간의 뇌를 완전히 시뮬레이션할 수 없는 한, 어떤 것도 할 수 없습니다.

그럼 도대체 무엇에 쓰일까요?

나는 테스트 스위트, 타입 시스템 및 형식적 검증을 모두 프로그래밍 언어의 안전성을 위한 동일한 기본 방법의 다양한 구현으로 보는 경향이 있습니다(이것이 유일하게 합리적인 방법일 수도 있습니다).

이들은 모두 우리의 의도를 다양한 방식으로 중복적으로 규정하고, 그런 다음 이러한 다양한 규정이 서로 호환되는지를 자동으로 검사하는 것입니다.

이 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)

여기서 당신은 세 가지 다른 방식으로 당신의 의도를 표현합니다:

• 코드에서 피보나치 공식을 구현하여 명시적으로
• 타입 시스템을 통해 암묵적으로(입력, 출력 및 재귀 중간 단계가 모두 정수임을 지정)
• "샘플 패키지" 방법: 테스트 케이스

파일을 실행하면 공식이 샘플과 대조됩니다. 타입 검사기는 타입이 호환되는지를 검증할 수 있습니다: 두 개의 정수를 더하는 것은 유효한 작업이며, 또 다른 정수를 생성합니다.

타입 시스템은 물리학에서 작업을 검사하는 좋은 방법입니다: 만약 당신이 가속도를 계산하고, 미터/초가 아니라 미터/초²라는 단위를 얻었다면, 당신은 잘못된 것입니다.

테스트 케이스는 "샘플 패키지" 정의의 한 예입니다. 인간이 개념을 처리할 때, 이러한 방식은 종종 직접적인 명시적 정의보다 더 자연스럽습니다.

당신이 당신의 의도를 다양한 방식으로 규정할수록, 이상적으로는 문제를 해결하기 위해 서로 다른 사고 방식을 요구하는 전혀 다른 방식으로, 이러한 모든 표현 방식이 서로 호환된다는 것이 증명되면, 당신은 실제로 당신이 진정으로 원하는 것을 표현했을 가능성이 더 높습니다.

안전한 프로그래밍은 당신의 의도를 다양한 방식으로 표현하고, 그런 다음 이러한 표현이 모두 서로 호환되는지를 자동으로 검증하는 것입니다.

형식적 검증은 이 방법을 더욱 확장할 수 있게 해줍니다. 형식적 검증을 통해 거의 무한한 수의 다양한 중복 방식으로 당신의 의도를 규정할 수 있으며, 프로그램은 이 모든 것이 호환될 때만 검증을 통과할 수 있습니다.

당신은 고도로 최적화된 구현과 효율성이 극히 낮지만 인간이 읽기 쉬운 구현을 규정할 수 있으며, 두 구현이 일치하는지를 검증할 수 있습니다. 당신은 당신의 열 명의 친구에게 당신의 프로그램이 가져야 할 수학적 속성 목록을 제공하도록 요청할 수 있으며, 그것이 모두 통과하는지를 확인할 수 있습니다.

만약 통과하지 못한다면, 프로그램이 잘못되었는지 아니면 수학적 속성이 잘못되었는지를 찾아낼 수 있습니다. 그리고 당신은 인공지능을 사용하여 이러한 모든 작업을 매우 효율적으로 수행할 수 있습니다.

그럼 어떻게 시작해야 할까요?

현실적으로 말하자면, 당신은 스스로 증명을 작성하지 않을 것입니다. 형식적 방법이 유행하지 않은 이유는 대부분의 사람들이 이러한 난해한 내용을 작성하는 방법을 이해하지 못하기 때문입니다. 당신은 아래의 코드가 무엇을 의미하는지 말해줄 수 있습니까?

  /-- Helper: foldl 수준에서 누산기를 가진 점진적 ≤ -/
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 서명 변형에 대한 특정 안전 진술의 증명에서 수많은 하위 보조 정리 중 하나입니다.

구체적으로, 그 진술은: 해시 충돌이 발생하지 않는 한, 어떤 메시지의 서명은 해시 단계의 어느 지점에서든 다른 메시지의 서명보다 더 높은 값을 필요로 하며, 따라서 그것은 다른 서명에서 계산할 수 없는 정보를 포함합니다.)

수동으로 코드를 작성하고 증명을 작성할 필요 없이, 당신은 인공지능에게 프로그램을 작성하게 할 수 있습니다(직접 Lean으로 작성하든, 속도를 위해 어셈블리 언어로 작성하든), 그리고 과정에서 어떤 기대 속성을 증명하게 할 수 있습니다.

이 작업의 장점은 그것 자체가 자기 검증적이라는 것입니다. 따라서 당신은 감독할 필요가 없으며, 단지 인공지능이 몇 시간 동안 연속적으로 잘 작동하도록 하면 됩니다.

최악의 결과는 그것이 제자리에서 돌고 아무런 진전을 이루지 못하는 것입니다(또는, 내가 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의 확장에 있는 숫자가 더 높습니다.

대형 언어 모델을 사용하여 증명을 작성하는 데 있어, 나는 Claude와 Deepseek 4 Pro가 모두 능숙하다고 생각합니다. Leanstral은 Lean을 작성하기 위해 특별히 미세 조정된 작은 오픈 소스 가중치 모델로, 매우 유망한 대안입니다.

그것은 119B의 매개변수를 가지고 있으며, 각 토큰은 6B를 활성화합니다. 당신은 그것을 로컬에서 실행할 수 있지만, 속도가 느립니다(내 노트북에서 약 15 tok/sec 속도). 벤치마크에 따르면, Leanstral은 훨씬 더 큰 일반 모델보다 우수합니다:

현재 내 개인적인 경험에 따르면, 그것은 Deepseek 4 Pro보다 약간 떨어지지만 여전히 매우 효과적입니다.

형식적 검증은 우리의 모든 문제를 해결할 수 없습니다.

그러나 우리가 인터넷 보안 모델이 더 이상 몇몇 강력한 조직에 대한 신뢰에 기반하지 않기를 원한다면, 우리는 코드에 대한 신뢰로 전환할 필요가 있습니다. 이는 강력한 인공지능의 상대에 직면했을 때도 코드에 대한 신뢰를 포함합니다.

AI 지원 형식적 검증은 우리가 이 목표를 달성하는 길에서 확고한 발걸음을 내딛게 해줍니다.

블록체인과 ZK-SNARKs와 마찬가지로, 인공지능과 형식적 검증은 매우 상호 보완적인 기술입니다.

블록체인은 프라이버시와 확장성을 대가로 개방된 검증 가능성과 검열 저항성을 부여하며, ZK-SNARKs는 다시 프라이버시와 확장성을 되돌려줍니다(실제로 이전보다 더 많이).

인공지능은 정확성을 대가로 대량의 코드를 작성할 수 있는 능력을 부여하며, 형식적 검증은 다시 정확성을 되돌려줍니다(실제로 이전보다 더 높습니다).

기본적으로, 인공지능은 대량의 조잡한 코드를 생성할 것이며, 버그의 수는 증가할 것입니다.

사실, 어떤 경우에는 버그의 증가를 용인하는 것이 올바른 균형일 수 있습니다: 만약 버그가 경미하다면, 심지어 버그가 있는 소프트웨어조차도 없는 소프트웨어보다 낫습니다.

하지만 여기서 사이버 보안은 낙관적인 미래를 가지고 있습니다: 소프트웨어는(계속해서) "안전한 핵심" 주위에 "불안전한 주변 부분"으로 분열될 것입니다.

불안전한 주변 부분은 샌드박스에서 실행되며, 작업을 완료하는 데 필요한 최소한의 권한만 부여받습니다.

안전한 핵심은 모든 것을 관리합니다. 안전한 핵심이 무너진다면, 모든 것이 무너질 것입니다. 당신의 개인 데이터, 당신의 돈 등등. 그러나 만약 어떤 불안전한 주변 부분이 무너진다면, 안전한 핵심은 여전히 당신을 보호할 수 있습니다.

안전한 핵심에 관해서는, 우리는 버그가 있는 코드가 만연하는 것을 허용할 수 없습니다. 우리는 안전한 핵심의 규모를 작게 유지하기 위해 급진적인 조치를 취할 것입니다. 심지어 그것을 더 작게 만들 것입니다.

반대로, 우리는 인공지능이 가져오는 모든 추가 성능을 안전한 핵심을 더욱 안전하게 만드는 작업에 완전히 투입하여, 우리가 고도로 디지털화된 사회에서 부여한 극도의 신뢰 임무를 견딜 수 있도록 할 것입니다.

운영 체제의 커널(또는 적어도 그 일부)은 이러한 안전한 핵심이 될 것입니다.

이더리움은 또 다른 안전한 핵심이 될 것입니다.

적어도 성능 집약적이지 않은 모든 계산에 대해, 당신이 사용하는 하드웨어는 세 번째 안전한 핵심이 될 것입니다.

사물 인터넷 관련 시스템은 네 번째가 될 것입니다.

적어도 이러한 안전한 핵심들 사이에서, "버그는 불가피하며, 당신은 단지 공격자보다 먼저 그것들을 찾아내기 위해 노력해야 한다"는 오래된 격언은 반증될 것이며, 진정한 안전을 얻을 수 있는 더욱 희망적인 세계로 대체될 것입니다.

그러나 만약 당신이 형편없는 소프트웨어에 당신의 자산과 데이터를 맡기기로 결심한다면, 그 소프트웨어가 우연히 그것들을 블랙홀로 삼킬 수 있다면, 당신은 물론 그 자유를 가집니다.