원문 제목: 형식 검증의 얕은 탐구

원문 저자: Vitalik

번역: Peggy, BlockBeats

편집자 주: AI 프로그래밍 능력이 급속히 향상되는 가운데, 소프트웨어 보안은 새로운 역설에 직면하고 있습니다: AI가 코드를 더 효율적으로 생성할 수도 있지만 취약점을 더 효과적으로 발견할 수도 있습니다. 암호화폐 산업에 있어 이 문제는 특히 중요합니다. 스마트 계약, ZK 증명, 합의 알고리즘 및 온체인 자산 시스템에 결함이 발생할 경우, 일반적인 소프트웨어 오류가 아닌 돌이킬 수 없는 자금 손실과 신뢰 붕괴가 발생할 수 있습니다.

Vitalik이 이 글에서 논의한 것은 바로 AI 시대의 코드 보안에 대한 또 다른 접근 방식인 형식 검증입니다. 간단히 말해, 이는 인간 감사자가 코드를 한 줄씩 검토하는 것이 아니라 프로그램이 충족해야 하는 속성을 수학적 명제로 작성하고, 그러한 속성이 성립하는지를 기계가 확인 가능한 증명으로 검증하는 것입니다. 과거에는 형식 검증이 임계가 높고 프로세스가 복잡하여 상대적으로 소규모의 연구 및 엔지니어링 분야에 투입되어 왔지만, AI가 코드 및 증명 작성을 보조할 수 있게 되면서 이러한 방법론이 다시 현실적인 의미를 찾고 있습니다.

본문의 핵심 주장은 "형식 검증이 모든 보안 문제를 해결할 수 있다"는 것이 아닙니다. 반면, Vitalik은 "증명 가능한 안전"이 절대적으로 안전을 의미하지 않는 다수 차례 강조했습니다: 증명은 중요한 가정을 놓칠 수 있으며, 명세가 잘못 기술될 수 있으며, 검증되지 않은 코드, 하드웨어 경계 및 사이드 채널 공격 또한 새로운 위험 요소가 될 수 있습니다. 하지만 이는 더 신뢰할 수 있는 보안 패러다임을 제공합니다. 개발자의 의도를 다양한 방식으로 표현하고, 시스템이 이러한 표현이 서로 호환되는지 자동으로 확인하게 합니다.

이는 이더리움에게 매우 중요합니다. 미래의 이더리움은 STARK, ZK-EVM, 양자 내성 서명, 합의 알고리즘 및 고성능 EVM 구현을 포함한 복잡한 하위 시스템에 점점 더 의존하게 될 것입니다. 이러한 시스템의 구현은 매우 복잡하지만 핵심 보안 목표는 상대적으로 명확하게 형식화될 수 있습니다. 이러한 시나리오에서, AI 보조 형식 검증이 최대 가치를 발휘할 수 있습니다: AI가 효율적인 코드 및 증명 작성을 맡고, 인간이 최종으로 증명된 명제가 실제 보안 목표와 일치하는지 확인합니다.

보다 광범위한 시각에서 볼 때, 이 글은 Vitalik이 AI 시대의 네트워크 보안에 대한 한 번의 대답이기도 합니다. 더 강력한 AI 공격자에 직면했을 때, 해답은 오픈 소스를 포기하거나 스마트 계약을 포기하거나 소수의 중앙화된 기관에 재의존하는 것이 아니라 핵심 시스템을 더 작고 더 검증 가능하며 더 신뢰할 수 있는 "안전한 코어"로 압축하는 것입니다. AI는 부정확한 코드를 대량으로 증가시킬 수 있지만, 과거보다 더 중요한 코드가 실제로 더 안전해질 수도 있습니다.

다음은 원문입니다:

특별히, Yoichi Hirai, Justin Drake, Nadim Kobeissi, 그리고 Alex Hicks에게 이 글을 리뷰하고 피드백을 제공해준 데 대해 진심으로 감사드립니다.

지난 몇 달 동안, 이더리움 프론트엔드 연구 그룹과 컴퓨팅 분야의 많은 다른 곳에서 새로운 프로그래밍 패러다임이 급속히 등장하고 있습니다: 개발자들이 직접 매우 하위 수준의 언어로 코드를 작성하는 것, 예를 들어 EVM 바이트코드, 어셈블리어, 또는 Lean을 사용하여 코드를 작성하고 Lean에서 자동으로 검사 가능한 수학적 증명을 작성하여 그 정확성을 검증합니다.

적절히 활용할 경우, 이러한 방식은 매우 효율적인 코드를 생성할 수도 있고, 과거의 소프트웨어 개발 방식보다 훨씬 더 안전할 수도 있습니다. Yoichi Hirai는 이를 "소프트웨어 개발의 최종 형태"라고 칭합니다. 본문은 이 접근 방식 뒤에 있는 핵심 논리를 설명하려고 합니다: 소프트웨어의 형식적 검증이 정확히 무엇을 할 수 있는지, 그 한계와 경계는 무엇인지——이더리움 문맥에서든 더 넓은 소프트웨어 개발 분야에서든.

형식적 검증이란?

형식적 검증은 기계가 자동으로 확인할 수 있는 방식으로 수학적 정리의 증명을 작성하는 것을 말합니다.

비교적 간단하지만 여전히 흥미로운 예로, 우리는 피보나치 수열에 관한 기본 정리를 볼 수 있습니다: 세 수 중에 하나는 짝수이며 나머지 두 수는 홀수입니다.

간단한 증명 방법은 수학적 귀납법을 사용하여 세 개의 수를 한 번에 이동하는 것입니다.

먼저 초기 경우를 살펴봅니다. F1 = F2 = 1, F3 = 2 라고 가정합니다. 직접 관찰하면, 이 명제 - "i가 3의 배수일 때 Fi가 짝수이고, 그렇지 않으면 Fi가 홀수임" - 이 x = 3까지 유효함을 알 수 있습니다.

다음은 귀납 단계입니다. 이 명제가 3k+3 이전에 유효하다고 가정하면, 즉, 우리는 이미 F3k+1, F3k+2, F3k+3의 홀짝성이 각각 홀수, 홀수, 짝수임을 알고 있습니다. 따라서 다음 세 숫자의 홀짝성을 계산할 수 있습니다:

이를 통해, "3k+3 이전에 알려진 명제"에서부터 "3k+6 이전에도 명제가 성립함을 확인"하는 것으로 진행됩니다. 계속해서 이러한 추론을 반복하면, 모든 정수에 대해이 규칙이 성립한다는 것을 확신할 수 있습니다.

이 논증은 인간에게 설득력이 있습니다. 그러나 만약 당신이 증명하고 싶은 것이 100배나 복잡하고, 정말로 자신이 잘못을 범하지 않았다는 것을 확인하고 싶다면 어떻게 해야 할까요? 그럴 때는 컴퓨터도 믿을 수 있는 증명을 구성할 수 있습니다.

대략적으로 다음과 같을 것입니다:

이것은 동일한 추론이지만 Lean으로 표현된 것입니다. Lean은 수학적 증명을 작성하고 검증하는 데 자주 사용되는 프로그래밍 언어입니다.

이는 위에서 제공한 "인간판" 증명과 매우 다르게 보입니다. 이러한 이유가 있습니다: 컴퓨터에게 직관적인 것과 인간에게 직관적인 것은 완전히 다릅니다. 여기서 말하는 컴퓨터는 예전의 "컴퓨터"를 의미하며 if/then 문으로 이루어진 "결정론적" 프로그램을 가리킵니다. 이는 대형 언어 모델을 의미하지 않습니다.

위 증명에서 당신은 fib(3k+4) = fib(3k+3) + fib(3k+2)이 사실을 강조하는 것이 아닙니다. 당신이 강조하는 것은 fib(3k+3) + fib(3k+2)가 홀수임을, 그리고 Lean에서 fib(3k+4)에 대한 정의를 이해하기 위해 그것을 자동으로 결합해주는 omega 태크틱이라는 매우 큰 이름의 것입니다.

보다 복잡한 증명에서는 때로 각 단계에서 명확히 밝혀야 할 수도 있습니다: 어떤 수학적 법칙이 이 단계를 따라가게 하는지, 때로는 그러한 법칙들은 Prod.mk.inj와 같이 몇몇 암호화된 이름을 가지기도 합니다. 그러나 반면에, 여러분은 매우 큰 다항식 표현식을 풀기 위해 한 줄의 omega 또는 ring과 같은 식만 작성하면 증명을 완료할 수도 있습니다.

이러한 비직관성과 번잡함이 기계로 검증 가능한 증명이 거의 60년에 걸쳐 존재했음에도 불구하고 계속해서 소수 분야에 머물러 있는 중요한 이유입니다. 그러나 동시에, 많은 과거에는 거의 불가능한 일들이 AI의 급속한 발전으로 인해 현재 가능해지고 있습니다.

컴퓨터 프로그램 검증

여기까지 오면 아마도 여러분은 생각할 것입니다: 그래서 우리는 컴퓨터가 수학 정리를 증명하도록 할 수 있으니, 이제 우리는 소수에 관한 그런 엉뚱한 새로운 발견들 중에 어떤 것이 진실이고, 어떤 것이 백 페이지 PDF 논문에 감춰진 오류인지 확실히 할 수 있게 됩니다. 아마도 우리는 아랍 마사르에 대한 ABC 가설에 대한 증명이 정확한지 조차 알 수 있을 것입니다! 그러나 호기심을 충족시키는 것 외에도, 이 일에는 무슨 실익이 있을까요?

대답은 많을 수 있습니다. 그리고 제게 있어서 매우 중요한 한 가지 대답은: 컴퓨터 프로그램의 정확성을 검증하는 것, 특히 암호학이나 보안과 관련된 프로그램들을 포함할 때입니다. 결국, 컴퓨터 프로그램 자체가 수학 객체이기 때문에, 컴퓨터 프로그램이 어떤 방식으로 작동할 것인지를 증명하는 것은 본질적으로 수학 정리를 증명하는 것입니다.

예를 들어, Signal과 같은 암호화 통신 소프트웨어가 실제로 안전한지를 증명하고 싶다고 가정해 봅시다. 먼저 수학적으로 명확하게 설명하고, 이 맥락에서 "안전"이란 정확히 무엇을 의미하는지 작성할 수 있습니다. 일반적으로 증명해야 하는 것은: 특정 암호학 가정이 성립할 때, 개인 키를 소유한 사람만이 메시지 내용을 알 수 있다는 것입니다. 현실에서, 진정 중요한 보안 속성은 물론 여러 가지가 있습니다.

사실, 이미 이 문제를 명쾌히 이해하려는 팀이 존재함이 밝혀졌습니다. 그들이 제시한 안전 정리 중 하나는 대략 다음과 같습니다:

다음은 Leanstral이 이 정리의 의미에 대한 요약입니다:

passive_secrecy_le_ddh 정리는 콤팩트 리덕션으로, 무작위 오라클 모델(Random Oracle Model)에서, X3DH의 수동 메시지 비밀성이 DDH 가정만큼 공격하기 어려움을 보여줍니다.

다시 말해, 만약 공격자가 X3DH의 수동 메시지 비밀성을 공격해 성공한다면, 그들은 DDH도 공격할 수 있습니다. DDH는 일반적으로 어려운 문제로 간주되므로, X3DH도 수동 공격에 대항할 수 있다고 볼 수 있습니다.

이 정리는, 만약 공격자가 Signal의 키파괴 메시지를 수동으로 관찰한다면, 최종적으로 생성된 세션 키를 무작위 키와 구별할 수 있는 이점을 무시할 확률을 넘지 못함을 증명합니다.

또한 AES 암호화가 올바르게 구현되었음을 증명하는 증명과 결합하면, Signal 프로토콜의 암호화 메커니즘이 수동 공격에 남아 있는 유용성이 있습니다.

이와 유사한 검증 프로젝트는 이미 존재하며, TLS 및 다른 브라우저 내 암호화 구성 요소의 안전한 구현을 증명하는 데 사용됩니다.

만약 당신이 엔드 투 엔드 형식의 형식적 검증을 수행할 수 있다면, 증명하는 것은 단순히 어떤 프로토콜 설명이 이론적으로 안전한지가 아닌 사용자가 실제로 실행하는 구체적인 코드가 실제로 안전하다는 것입니다. 사용자 관점에서, 이는 "신뢰 없이도"의 수준을 크게 향상시킵니다:이 코드를 완전히 신뢰하기 위해 전체 코드베이스를 행 단위로 확인할 필요 없이 이미 증명된 몇 가지 주장을 확인하면 됩니다.

물론, 여기에는 매우 중요한 성격이 있다는 것을 상기할 필요가 있습니다, 특히 "안전"이란 키워드가 정확히 무엇을 의미하는지에 대해. 사람들은 종종 실제로 중요한 주장을 증명하는 것을 잊어버리기 쉽습니다; 또한 증명이 필요한 주장이 코드 그 자체보다 간결한 설명이 없을 수 있으며, 증명에 최종적으로 부합되지 않은 가정을 몰래 삽입하기 쉽습니다. 어떤 시스템의 일부분 만 실제로 형식적인 증명이 필요하다고 판단할 수 있으나 결국 그 다른 부분에서 심지어 하드웨어 수준에서 핵심적 결함을 당할 수 있습니다. Lean 자체의 구현도 버그가 존재할 수 있습니다. 그러나 이러한 귀찮은 세부사항을 논의하기 전에, 우리는 실현에 거의 이상적인 면모를 가져올 수도 있는 형식적 검증이 어떤 식의 거의 유토피아적 전망을 가져올 수 있는지에 대해 조금 더 살펴보겠습니다.

보안 지향 형식 검증

컴퓨터 코드에서의 버그는 원래부터 걱정스러운 문제였습니다.

암호화폐를 변경할 수 없는 블록체인 스마트 계약에 넣을 때, 코드 버그는 더욱 두려워집니다. 왜냐하면 코드에 오류가 있을 경우, 북한 해커가 자동으로 당신의 자금을 모두 가져갈 수 있고, 여러분은 거의 손쓸 수 있는 방법이 없을 것입니다.

그 모든 것이 제로 지식 증명으로 감싸졌을 때, 코드 버그는 더욱 두려워집니다. 왜냐하면 누군가가 제로 지식 증명 시스템을 성공적으로 침투하면, 그들은 모든 자금을 인출할 수 있으며, 우리는 무엇이 문제인지 전혀 알 수 없을 것입니다. 더 나쁜 경우에는, 우리는 문제가 발생했다는 것조차 전혀 모를 수도 있습니다.

강력한 AI 모델을 보유한 경우, 코드 버그는 더욱 두려워집니다. 예를 들어 Claude Mythos와 같은 모델은 2년간의 개선을 거쳐 이러한 취약점을 자동으로 발견할 수도 있습니다.

어떤 사람들은 이 현실을 직면하면서, 스마트 계약이라는 기본 개념을 포기하고 네트워크 공간이 실질적으로 공격자에 비해 방어자가 비대칭적 우위를 가질 수 없는 분야가 될 수 있다고 주장하기 시작했습니다.

다음은 몇 가지 인용문입니다:

시스템을 강화하기 위해 버그를 찾는 데 사용하는 토큰이, 공격자가 그 버그를 악용하는 데 사용하는 토큰보다 더 많이 필요합니다.

그리고:

우리 산업은 결정론적 코드를 중심으로 구축되었습니다. 코드 작성, 테스트, 배포하고, 그 코드가 제대로 작동한다는 것을 알 수 있습니다. 그러나 내 경험상, 이러한 계약은 점점 무효화되고 있습니다. 진정한 AI 네이티브 회사의 최고 수준 운영자들 사이에서, 코드 라이브러리는 이미 어떤 면에서는 "작동한다고 믿는" 것으로 변모하고 있으며, 이에 상응하는 믿음의 확률은 더 이상 정확하게 설명될 수 없습니다.

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

이는 네트워크 보안에 대해 어두운 미래가 될 것입니다. 특히 인터넷의 탈중앙화와 자유에 관심이 있는 사람들에게는 매우 어두운 미래가 될 것입니다. 전체 암호핑크 정신은 결국 다음을 기반으로 하고 있습니다: 인터넷에서, 방어자는 우위를 가집니다. 디지털 "성을 짓는" 것은 파괴하는 것보다 쉽습니다. 우리가 이를 잃게 되면, 인터넷 보안은 규모의 경제, 잠재적 공격자를 세계적으로 추적함으로써 비롯되는 것에서만 나올 수밖에 없으며, 더 넓은 의미로 말하자면, 하나를 선택하려고 할 때: 모든 것을 지배하거나 파멸로 향하는 두 가지 중 하나를 택해야 합니다.

나는 이 판단에 동의하지 않습니다. 네트워크 보안의 미래에 대해서는 훨씬 낙관적인 비전을 갖고 있습니다.

강력한 AI 취약성 발견 능력에 따른 도전은 실제로 심각하지만, 이는 과도기적인 도전입니다. 모든 것이 정리되고 우리가 새로운 균형에 진입한 후에, 우리는 지난 세월보다 방어쪽에 유리한 상태에 도달할 것입니다.

모질라도 이를 인정합니다. 그들의 말을 인용하면 다음과 같습니다:

이 작업에 지속적이고 집중적인 방식으로 노력하기 위해 다른 모든 것의 우선순위를 다시 조정해야 할 수도 있습니다. 그러나 터널 끝에는 빛이 있습니다. 이 도전에 대응하기 위해 팀이 어떻게 일어섰는지 우리는 매우 자랑스럽게 생각하며, 다른 사람들도 그렇게 할 것입니다. 우리의 작업은 아직 끝나지 않았지만, 우리는 기로를 지나며「따라 잡기만 하는」 것 이상의, 더 나은 미래를 보이기 시작했습니다. 방어쪽은 드디어 결정적인 승리의 기회를 갖게 되었습니다.

……

결함의 수는 제한되어 있으며, 우리는 그들을 모두 찾아낼 수 있는 세계로 진입하고 있습니다.

지금, 만약 모질라의 이 기사에서「formal」과「verification」을 Ctrl+F로 검색하면 두 단어가 나오지 않음을 알게 될 것입니다. 네트워크 보안의 긍정적인 미래는 엄격히 형식적 검증이나 그 밖의 어떤 단일 기술에 의존하지 않습니다.

그럼 무엇에 의지하는 것일까요? 기본적으로, 아래 그림에 나온 것처럼:

지난 수십 년 동안 많은 기술들이「취약성 감소」 추세를 밀어주었습니다:

유형 시스템;

메모리 보안 언어;

소프트웨어 아키텍쳐 개선, 인클루딩 샌드박스, 퍼미션 메커니즘, 그리고 보다 일반적으로「신뢰할 수 있는 컴퓨팅 기반」과「기타 코드」를 명시적으로 구분;

더 나은 테스트 방법;

안전 및 불안전 코딩 패턴에 대한 지식 쌓이기;

더욱 많은 사전 작성 및 감사된 소프트웨어 라이브러리.

AI 지원의 형식적 검증은 신뢰할 만한 새로운 패러다임으로 보아서는 안 됩니다. 대신, 이는 이미 전진 중인 추세와 패러다임을 가속하는 강력한 가속기로서 바라봐야 합니다.

형식적 검증은 만병통치약이 아닙니다. 그러나 특정 시나리오에서는 특히 유용합니다: 구체적인 구현보다는 목표가 훨씬 간단한 경우에 말이죠. 이는 이더리움 다음 주요 업그레이드에서 배포해야 할 몇 가지 가장 복잡한 기술들에 대해 뚜렷하게 나타납니다, 예를 들어 양자 내성 서명, STARK, 합의 알고리즘, 그리고 ZK-EVM를 포함한 것들.

STARK은 매우 복잡한 소프트웨어 세트입니다. 그러나 실현하는 핵심 보안 속성은 이해하기 매우 쉽고 형식화하기도 쉽습니다. 증명이 프로그램 P, 입력 x 및 출력 y의 해시 H를 가리킬 때, 사용된 해시 알고리즘이 깨졌다는 것이나 P(x) = y임을 의미합니다. 따라서 우리는 Arklib 프로젝트를 갖게 되었으며, 이 프로젝트는 완전한 형식화 검증이 수행된 STARK 구현을 만들고자 합니다. 다른 관련 프로젝트로는 VCV-io가 있으며, 이 프로젝트는 다양한 암호학 프로토콜에 대한 형식화 검증을 수행할 수 있는 기본적인 오라클 계산 인프라를 제공하며, 이러한 프로토콜 중 많은 것들이 STARK의 종속 구성 요소입니다.

보다 야심찬 것은 evm-asm입니다. 이 프로젝트는 완벽한 EVM 구현을 구축하고 형식화 검증하려는 시도입니다. 이 곳에서 보안 속성은 그리 명확하지 않습니다. 간단히 말해, 이 프로젝트의 목표는 해당 구현이 Lean으로 작성된 다른 EVM 구현과 동등함을 증명하는 것입니다. 후자는 구체적인 실행 효율성을 고려하지 않고 직관성과 가독성을 최대한으로 추구합니다.

물론, 이론적으로 여전히 다음과 같은 상황이 발생할 수 있습니다. 우리에게는 서로 동등하다고 증명된 열 개의 EVM 구현이 있지만, 모두 동일한 치명적 결함을 공유하며이 결함은 어떠한 방식으로든 공격자가 권한이 없는 주소에서 모든 ETH를 이체할 수 있게 합니다. 그러나 특정 EVM 구현이 이러한 결함을 가질 가능성에 비하면 이러한 상황이 발생할 확률은 훨씬 낮습니다. 우리는 변수명 증명을 통해 실제로 중요한 보안 속성 인 DoS 내성의 중요성을 이후에야 진정으로 깨닫게 되었습니다.

또 다른 두 가지 중요한 방향은 다음과 같습니다:

비잔틴 장애 허용 합의. 이 방향에서는 모든 기대되는 보안 속성을 형식적으로 정의하는 것 또한 쉽지 않습니다. 그러나 해당 버그가 아직도 매우 흔하기 때문에 형식적 검증 시도는 여전히 가치가 있습니다. 따라서 Lean 합의 구현 및 해당 증명에 대한 몇 가지 현재 진행 중인 작업이 있습니다.

스마트 계약 프로그래밍 언어. Vyper 및 Verity에서의 형식적 검증 작업이 포함됩니다.

이러한 모든 사례에서 형식적 검증이 가져오는 엄청난 가치 증대는 다음과 같습니다: 이러한 증명이 실제로 엔드 투 엔드입니다. 가장 어려운 버그 중 많은 것들은 종종 상호 작용 버그로서, 이러한 버그들은 따로 고려되는 두 하위 시스템의 경계에 발생합니다. 인간에게는 전체 시스템을 논리적으로 추론하는 것이 너무 어려우나, 자동 규칙 검사 시스템은 이를 수행할 수 있습니다.

효율성 중심의 형식적 검증

우리는 다시 evm-asm을 살펴보겠습니다. 이는 EVM 구현입니다.

그것은 RISC-V 어셈블리 언어로 직접 작성된 EVM 구현체입니다.

그것은 말 그대로 어셈블리입니다.

다음은 ADD 작업 코드입니다:

RISC-V를 선택한 이유는 현재 구축 중인 ZK-EVM 증명자가 일반적으로 RISC-V를 증명하고 이더리움 클라이언트를 RISC-V로 컴파일하여 작동하기 때문입니다. 따라서 RISC-V로 EVM 구현을 직접 작성하면 이론적으로 달성 가능한 가장 빠른 구현이어야 합니다. RISC-V는 일반 컴퓨터에서 매우 효율적으로 시뮬레이션되며, RISC-V 노트북도 이미 존재합니다. 물론, 완전한 엔드 투 엔드를 달성하려면 RISC-V 구현 자체나 증명자의 산술 표현에 대해 형식적 검증을 수행해야 합니다. 하지만 걱정할 필요는 없습니다. 이미 이러한 종류의 작업이 존재합니다.

직접 어셈블리로 코드를 작성하는 것은 50년 전에 우리가 자주했던 일입니다. 그 이후로 우리는 점차 고수준 언어로 코드를 작성하도록 전환해 왔습니다. 고수준 언어는 일정한 효율성을 희생하지만, 그 대가로 코드 작성 속도가 훨씬 빠르며, 더 중요한 것은 남의 코드를 이해하는 데 훨씬 빠릅니다. 이는 보안에 있어 필수적인 요건입니다.

형식적 검증과 AI를 결합함으로써 우리는 「미래로 돌아가는」 기회를 갖게 됩니다. 구체적으로 말하면, AI가 어셈블리 코드를 작성하고, 그런 다음 형식적으로 증명을 쓰고, 이러한 어셈블리 코드가 우리가 원하는 특성을 갖추었음을 검증합니다. 적어도 이 목표 특성은 다음과 같을 수 있습니다: 가독성을 위해 최적화되고, 어떤 사람이 친숙한 고수준 언어로 작성된 구현과 완전히 동등합니다.

이렇게 하면 더 이상 코드가 가독성과 효율성 사이에서 균형을 이룰 필요가 없어집니다. 우리는 두 가지 분리된 객체를 갖게 됩니다: 효율성을 위해 최적화된 어셈블리 구현체 및 특정 실행 환경의 요구에 따라 조정된 것; 그리고 가독성을 위해 최적화된 보안 주장 또는 고수준 언어 구현입니다. 그런 다음, 두 객체 간의 동치성을 증명하는 수학적 증명을 통해 두 번째 버전만 실행하면 됩니다.

이것은 매우 강력합니다. 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에서 commit e2618b31은 버그 하나를 수정했다: 'nand' 명령은 'and'로 출력되며, 'nand'는 흔하지 않은 ~(a & b) 모드에서만 선택된다. 이 버그는 무작위로 생성된 프로그램을 컴파일하여 발견되었다.

오늘날, 즉 2026 년에는 Nadim Kobeissi가 Cryspen에서 소프트웨어의 형식적 검증 취약점을 설명하면서 다음과 같이 언급했습니다:

2025 년 11 월, Filippo Valsorda는 libcrux-ml-dsa v0.0.3가 동일한 결정론적 입력에서 다른 플랫폼에서 서로 다른 공개 키와 서명을 생성하는 버그를 독립적으로 보고했습니다. 이 버그는 _vxarq_u64 내장 함수 래퍼에 발생했는데, 이 래퍼는 XAR 작업을 사용하는 SHA-3의 Keccak-f 치환에서 사용됩니다. 대체 경로는 잘못된 인수를 이동 작업에 전달하여 ARM64 플랫폼에서 하드웨어 SHA-3 지원이 없는 경우 SHA-3 요약이 손상되도록 합니다. 이것은 I 형 오류입니다: 이 내장 함수는 확인되었으며, NEON 백엔드 전체에 대한 런타임 안전성이나 정확성 증명이 완료되지 않았습니다.

그리고 다음 것도 있습니다:

libcrux-psq 크레이트는 후양자 사전 공유 키 프로토콜을 구현했습니다. decrypt_out 메서드에서는 AES-GCM 128 복호화 경로가 복호화 결과에 .unwrap()을 호출하고 오류를 계속 전달하지 않습니다. 비정상적인 암호문 하나로도 프로세스를 충돌시킬 수 있습니다.

위 네 가지 문제는 두 가지 유형으로 분류할 수 있습니다:

첫 번째 유형은 일부 코드만 확인되었으며 나머지 확인하기가 너무 어려운 경우입니다. 결과적으로 확인되지 않은 코드가 작성자가 상상한 것보다 더 쉽게 버그를 일으키며 이러한 버그는 종종 더 중요합니다.

두 번째 유형은 작성자가 특정 중요한 속성을 명시하는 것을 잊어버렸고 해당 속성은 원래 증명되어야 했던 것입니다.

Nadim의 논문은 형식적 검증의 실패 모델을 분류했습니다. 그는 다른 실패 유형도 나열했습니다. 예를 들어, 또 다른 주요 유형은 형식적 명세 자체가 잘못된 경우이거나 증명에 오류 주장이 포함된 경우이지만 시스템이 이를 무시합니다.

마지막으로, 소프트웨어와 하드웨어 경계에서 발생하는 형식적 검증 실패를 살펴볼 수 있습니다. 여기에서 흔한 문제 중 하나는 시스템이 부측청단 공격에 저항할 수 있는지 확인하는 것입니다. 메시지를 이론적으로 완전히 안전한 방법으로 보호했더라도 몇 미터 떨어진 누군가가 전기 변동을 캡처하고 수십만 번의 암호화 후에 개인 키를 추출할 수 있다면 여전히 안전하지 않습니다.

「차분 전력 분석」(differential power analysis)은 이러한 기술 중 요즘에는 충분히 이해된 예입니다.

차분 전력 분석은 일반적인 부측청단 공격입니다. 출처: 위키피디아

과거에도 누군가는 시스템이 이러한 공격자에 저항할 수 있음을 증명하려고 노력했습니다. 그러나 이러한 증명은 공격자에 대한 수학적 모델링을 필요로하며 그러한 모델링 아래에서 보안을 증명해야 합니다. 때때로 사람들은 「d-탐지 모델」을 사용할 수 있습니다. 즉, 공격자가 위치를 탐지할 수 있는 회로의 수에는 알려진 상한이 존재한다는 가정입니다. 그러나 문제는 이러한 모델이 일부 유출 형식을 포착하지 못할 수 있다는 것입니다.

이 논문에서 지적한 흔한 문제는 전환성 유출(transitional leakage)입니다. 만약 당신이 관찰 중인 신호가 특정 위치의 구체적인 값에 의존하는 것이 아니라 그 값의 변화에 따라 달라진다면 종종 두 값을 - 이전 값과 새 값 - 사이에서 필요한 정보를 회복할 수 있습니다. 그 값만이 아니라 두 값에 의존할 수 있습니다. 이 논문은 다른 유출 형식에 대해도 분류합니다.

수십 년 동안 이러한 형식 검증에 대한 비판은 다시 형식 검토를 더 나아지게 했습니다. 과거와 비교했을 때, 우리는 이제 이러한 문제에 대해 더 경계심이 있다. 그러나 오늘날까지도 완벽하지는 않습니다.

전체적인 시각에서 본다면, 여기엔 실제로 공통적인 선이 있습니다: 형식 검증은 매우 강력합니다. 그러나 시장 홍보가 이를 “증명 가능한 올바름”을 가져다 줄 수 있다고 포장하더라도, 이를테면 “증명 가능한 올바름”은 본질적으로 소프트웨어나 하드웨어가 실제로 “정확한”임을 증명할 수 없습니다.

대다수 사람들에게 있어서 “정확함”은 대략 다음을 의미합니다: 이것이 목적을 개발자가 의도한 사용자의 이해와 일치한다는 것.

그리고 “안전함”은 대략 다음을 의미합니다: 이것이 사용자 이익을 손상시키지 않고, 사용자의 기대에서 벗어나지 않는 방식으로 작동하는 것.

이 두 경우 모두, 정확성과 안전성은 최종적으로 비교로 귀결됩니다: 한 쪽은 수학 객체이고, 다른 한 쪽은 인간의 의도나 기대입니다. 엄밀히 말하면, 인간의 의도와 기대 자체도 수학 객체입니다—결국, 인간의 두뇌도 우주의 일부이며, 우주는 물리 법칙을 따릅니다; 충분한 계산 능력이 있다면, 원칙적으로 그것들을 시뮬레이션할 수 있습니다. 그러나 이들은 매우 복잡한 수학 객체이며, 컴퓨터든 우리든, 진정으로 이해하지 못하거나 심지어 읽을 수 없습니다. 실용적인 목적을 위해 우리는 그것들을 블랙박스로 간주할 수 있습니다. 우리가 자신의 의도와 기대를 어느 정도 이해할 수 있는 유일한 이유는 각 사람이 자신의 아이디어를 수년 동안 지켜보고 남의 생각을 추론해야 했기 때문입니다.

우리가 원시적인 인간의 의도를 직접적으로 컴퓨터에 넣을 방법이 없기 때문에, 형식 검증은 시스템이 인간의 의도와 비교되는 것을 증명할 방법이 없습니다. 따라서, “증명 가능한 정확성”과 “증명 가능한 안전성”은 실제로 인간이 이해하는 “정확성”과 “안전성”을 증명하지 못합니다—우리가 뇌를 모방할 수 있을 때까지, 이러한 점을 진정으로 실현할 방법이 없습니다.

그렇다면, 형식 검증의 실질적인 가치는 무엇인가요?

저는 테스트 슈트, 유형 시스템 및 형식 검증을 하나의 공통된 프로그래밍 언어 보안 메커니즘의 다른 구현 형태로 간주하는 것을 선호합니다—아마도 이것이 정말로 설득력 있는 유일한 방법일 것입니다. 이들의 공통점은: 서로 다른 방식으로 우리의 의도를 중복해서 설명하고, 그 다른 설명 사이의 상호 호환성을 자동으로 확인한다는 점입니다.

예를 들어, 다음은 Python 코드를 살펴봅시다:

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

첫째, 직접적 표현: 피보나치 공식을 코드로 구현.

둘째, 간접적 표현: 입력, 출력 및 재귀 프로세스 중간 단계가 모두 정수임을 유형 시스템을 통해 설명합니다.

셋째, "케이스 패키지" 방식 도입: 즉, 테스트 케이스입니다.

이 파일을 실행하면 시스템은 이러한 예제를 사용하여 공식이 유효한지 확인합니다. 유형 검사기는 유형 간의 호환 여부를 확인할 수 있습니다: 두 정수를 더하는 것은 유효한 작업이며 다른 정수를 얻게 됩니다. 유형 시스템은 물리적 계산에서도 종종 유용합니다: 가속도를 계산 중이면서 결과의 단위가 m/s이 아닌 m/s² 인 경우, 어디에서 잘못 계산했는지 파악할 수 있습니다. 그리고 "케이스 패키지" 스타일의 정의는 테스트 케이스가 그 중 하나이지만 종종 직접적이고 명시적인 정의보다는 인간이 개념을 다루는 방식에 더 적합합니다.

자신의 의도를 표현하는 방법이 다양할수록 좋습니다. 이상적인 상황에서는 이러한 방법들이 서로 충분히 다르기 때문에 동일한 문제를 처리하는 데 다양한 사고 방식을 사용해야 합니다. 따라서 이러한 모든 표현이 결국 서로 호환되면, 실제로 의도를 가장 잘 나타낼 가능성이 높아집니다.

안전 프로그래밍의 핵심은 여러 다양한 방식으로 의도를 표현한 다음 이러한 표현이 서로 호환되는지 자동으로 검증하는 것입니다.

형식적 검증은 이러한 접근 방식을 더 나아가게 합니다. 형식적 검증을 사용하면 거의 무제한으로 자신의 의도를 설명할 수 있으며, 이러한 설명이 서로 호환될 때에만 프로그램이 검증됩니다.

최적화된 구현과 인간이 읽기 쉽지만 효율성이 떨어지는 구현을 동시에 작성하고 둘 사이의 일치성을 확인할 수 있습니다. 또한 이 프로그램이 만족해야 하는 수학적 속성을 친구 10명에게 각각 작성하도록 요청한 다음 모든 속성을 만족하는지 확인할 수 있습니다. 만일 만족하지 않으면, 프로그램에 문제가 있는지 아니면 해당 수학적 속성에 문제가 있는지 추가적으로 판단할 수 있습니다. AI 는 위의 모든 작업을 매우 효율적으로 수행하게 할 수 있습니다.

어떻게 시작해야 할까요?

솔직히 말해서, 직접 증명을 작성할 가능성은 거의 없습니다. 형식적 메소드가 실제로 보급되지 못한 이유는 대부분의 사람들이 이 빌어먹을 증명을 어떻게 작성해야 하는지 이해하기 어렵기 때문입니다.

아래 코드 조각이 무슨 의미인지 말해 줄 수 있나요?

(원하신다면, 이것은 특정 SPHINCS 서명 변형의 특정 보안 주장을 위한 몇 가지 보조 보조 정리 중 하나입니다. 이 주장은 어떤 다른 메시지에 대한 서명과 비교하여 특정 메시지에 대한 서명을 생성하는 경우, 해시 충돌이 없는 한 해당 메시지에 대한 서명이 하나의 해시 체인에서 더 높은 위치 값을 사용해야한다는 것입니다. 따라서 해당 정보는 다른 서명에서 계산할 수 없습니다.)

코드를 직접 작성하고 증명할 필요 없이, AI 가 도와줄 수 있습니다 — Lean 을 사용하여 바로 코딩할 수도 있고, 속도를 추구하고 싶다면 어셈블리어로도 코딩할 수 있습니다 — 그리고 그 과정에서 원하는 여러 가지 속성을 증명할 수 있습니다.

이 작업의 장점 중 하나는 자가 검증적이라는 점이기 때문에 항상 관찰할 필요가 없습니다. AI 가 몇 시간 동안 계속 실행되도록 할 수 있습니다. 최악의 경우에는 그냥 제자리걸음을 하거나 계속 진전이 없을 수 있고요; 또는 제 Leanstral 이 한 번 했던 것처럼, 스스로의 작업을 더 쉽게 하기 위해 바로 증명해야 하는 명제를 바꾸는 일이 있을 수도 있습니다.

최종적으로 확인해야 하는 것은: 증명된 명제가 실제로 증명하려고 했던 것인지 입니다.

이 SPHINCS 서명 변형에서 최종 명제는 다음과 같습니다:

이것은 실제로 거의 "가독성"에 가까워졌습니다:

하나의 해시 요약에 의해 생성된 숫자(디지1)가 다른 해시 요약에 의해 생성된 숫자(디지2)와 같지 않을 경우 다음 주장은 성립하지 않습니다:

모든 숫자에 대해, 디지1의 각 자릿수가 디지2의 해당 자릿수보다 작거나 같음;

모든 숫자에 대해, 디지2의 각 자릿수가 디지1의 해당 자릿수보다 작거나 같습니다.

여기 비교되는 것은 체크섬을 추가한 "확장 숫자"(wotsFullDigits)입니다. 즉, 어느 정도에서는 디지1의 확장 숫자가 더 높을 수밖에 없고, 다른 몇 군데에서는 디지2의 확장 숫자가 더 높을 수 있습니다.

증명을 위해 대형 언어 모델을 사용하는 경우, Claude 가 이미 충분히 잘 작동하고 있고, DeepSeek 4 Pro 역시 충분히 강력합니다. Leanstral 은 Lean 작성에 특화된 무겁지 않은, 오픈 소스 가중치 모델의 미래가 있습니다. 이것은 1,190 억 개의 매개변수를 보유하고 있지만, 각 토큰 당 60 억 개의 매개변수만 활성화되므로 로컬에서 실행할 수 있습니다. 다소 느릴 수는 있지만 — 제 노트북에서는 초당 약 15개의 토큰입니다.

벤치마크에 따르면, Leanstral 은 많은 대형 범용 모델보다 우수한 성능을 보여줍니다:

내 현재 개인적 경험에 따르면, DeepSeek 4 Pro 보다 약간 약하지만 여전히 효과적입니다.

형식 검증은 우리 모든 문제를 해결하지는 않을 것입니다. 그러나 우리가 모두가 소수의 강력한 조직을 신뢰하는 대신 인터넷 보안 모델을 구축하길 원한다면, 우리는 코드를 신뢰할 수 있는 방법으로 바꿀 수 있어야 합니다. 심지어 강력한 AI 상대에서도 코드를 신뢰할 수 있어야 합니다. AI 지원 형식 검증은 우리가 이 방향으로 한 걸음 응기하는 데 도움이 될 수 있습니다.

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

블록체인은 프라이버시와 확장 가능성을 희생함으로써 개방형 검증성과 검열 저항성을 가져왔으며, ZK-SNARKs는 프라이버시와 확장 가능성을 되찾아왔습니다. 사실, 이전보다 더 강하게.

AI는 대규모 코딩을 가능케하지만 정확성을 희생하게 합니다. 반면 형식 검증은 정확성을 되찾아왔습니다. 사실, 이전보다 더 강하게.

기본적으로 AI는 대량의 부정확한 코드를 생성하며 버그의 수도 증가합니다. 실제로 특정 시나리오에서는 버그를 증가시키는 것이 올바른 균형일 수도 있습니다. 이러한 버그가 경미한 영향을 미친다면 결함이 있는 소프트웨어가 전혀 없는 소프트웨어보다 낫습니다. 그러나 여기에서도 네트워크 보안에는 낙관적인 미래가 있습니다. 소프트웨어는 여전히 "보안 코어"를 중심으로 "보안되지 않은 주변 구성 요소"로 분화될 것입니다.

이러한 보안되지 않은 주변 구성 요소는 샌드박스에서 실행되며 수행하는 데 필요한 최소한의 권한만 할당됩니다. 보안 코어는 모든 것을 관리합니다. 보안 코어가 손상되면 모든 것이 손상됩니다. 당신의 개인 데이터, 당신의 자금 및 더 많은 것이 영향을 받게됩니다. 그러나 어떤 보안되지 않은 주변 구성 요소에 문제가 발생해도 보안 코어는 여전히 당신을 보호할 수 있습니다.

보안 코어에 관련된 경우 버그가 있는 코드가 계속 퍼져 가는 것을 방치하지 않을 것입니다. 우리는 보안 코어의 규모를 적극적으로 통제하여 충분히 작게 유지하고 심지어 더 줄일 것입니다. 반면 AI가 제공하는 모든 추가 기능을 보안 코어 자체의 안전성 향상에 투입하여 매우 디지털화된 사회에서 매우 높은 신뢰 부담을 지게 할 것입니다.

귀하의 운영 체제 커널 또는 적어도 일부는 이러한 보안 코어 중 하나가 될 것입니다. 이더리움은 또 다른 하나가 될 것입니다. 이상적인 상황에서는 고성능 컴퓨팅이 아닌 모든 계산에서 사용하는 하드웨어도 세 번째 보안 코어가 될 것입니다. 일부 사물 인터넷 관련 시스템은 네 번째가 될 것입니다.

적어도 이러한 보안 코어 중에서는 "버그는 피할 수 없으며, 공격자보다 빨리 발견해야 한다"는 구어가 더 이상 성립하지 않을 것입니다. 이것은 더 희망적인 세상에 밀려날 것입니다: 거기에서 우리는 진정한 보안을 얻을 수 있습니다.

물론, 당신이 자산과 데이터를 매우 엉망으로 작성되었고 심지어 그것을 모두 블랙홀에 넣어 버릴 수도 있는 소프트웨어에 맡기기를 원한다면, 여전히 이 자유를 가지고 계실 것입니다.

[원문 링크]

BlockBeats 공식 커뮤니티에 참여하세요:

Telegram 구독 그룹：https://t.me/theblockbeats

Telegram 토론 그룹：https://t.me/BlockBeats_App

Twitter 공식 계정：https://twitter.com/BlockBeatsAsia