AI 시대의 사이버보안, 형식 검증이 답이 될 수 있을까

[AI 시대의 사이버보안, 형식 검증이 답이 될 수 있을까] 지난 몇 달, 이더리움 리서처들 사이에서 새로운 프로그래밍 패러다임이 빠르게 자리잡고 있습니다. 매우 저수준 언어냐 Lean으로 직접 코드를 작성하고, 그 정확성을 기계가 자동 검증 가능한 수학적 증명으로 보장하는 방식이죠. 비탈릭이 오늘 ‘AI와 결합된 형식 검증(formal verification)이 사이버보안의 미래를 어떻게 바꿀 수 있는지’에 대한 글을 통해 이에 대해 알아보겠습니다. [형식 검증이란 무엇인가] 형식 검증은 수학적 정리를 컴퓨터가 자동 검증할 수 있는 형태로 증명하는 것입니다. 이는 60년 가까이 존재해왔지만, 작성이 까다로워 보안이 매우 중요한 영역에만 적용되어 왔었죠. 그런데 AI의 빠른 발전 덕분에, 그동안 불가능했던 많은 것들이 가능해지고 있습니다. 컴퓨터 프로그램 자체도 수학적 객체이기 때문에, 프로그램이 특정 방식으로 동작한다는 사실 역시 수학 정리로 증명할 수 있습니다. 실제로 Signal, TLS 같은 암호 프로토콜의 실제 구현 보안을 엔드 투 엔드로 증명하려는 프로젝트들이 진행 중이기도 합니다. 이렇게 수학적으로 코드가 형식 검증되면, 사용자나 개발자 입장에서는 코드 전체를 검토할 필요 없이 그 코드에 대해 증명된 명제만 확인하면 되니 신뢰 비용이 크게 줄어들죠. [AI 시대의 위기와 기회] 최근 다수의 디파이 해킹 사례들이 터지며, 스마트 컨트랙트와 영지식 증명에 AI 기반 버그 탐색까지 더해지면 공격자 우위가 압도적이 될 수 있다는 비관론이 증가하고 있습니다. 일부 사람들은 오픈소스 자체를 포기해야 한다고까지 주장하죠. 그러나 비탈릭은 이를 과도기적 도전이라고 이야기하며, 형식 검증을 사용하면 이를 해결할 수 있다고 주장합니다. [이더리움 적용 사례] • STARK: 소프트웨어 자체는 매우 복잡하지만, 보장하려는 보안 속성은 한 문장으로 정리됩니다. "어떤 증명이 프로그램 P, 입력 x, 출력 y에 대한 것이라면, 해시 알고리즘이 깨졌거나 실제로 P(x)=y이거나 둘 중 하나"라는 진술이죠. 목표가 이렇게 단순하기 때문에 형식 검증이 잘 들어맞습니다. 완전히 형식 검증된 STARK 구현을 만드는 Arklib 프로젝트가 진행 중입니다. • EVM: evm-asm은 EVM 전체를 RISC-V 어셈블리로 직접 작성하고, Lean으로 작성된 구현과의 동치성을 증명합니다. • 합의: 비잔틴 장애 허용 합의의 속성을 형식적으로 증명하려는 노력이 이어지고 있습니다. [보안과 효율을 동시에 잡는 것이 가능할까] 형식 검증과 AI의 결합은 "효율 전용 구현"과 "가독성 전용 구현"을 분리한 뒤, 둘의 동치성을 수학적으로 증명하는 길을 엽니다. AI가 어셈블리를 작성하고, 그것이 사람 친화적 고수준 구현과 일치한다는 사실을 증명하면 끝이죠. 이더리움의 전 형식 검증 엔지니어 Yoichi Hirai는 이를 "소프트웨어 개발의 최종 형태"라고 부르기도 합니다. [한계: 만병통치약은 아니다] 다만 형식 검증은 우리가 일상적으로 이해하는 "정확함"을 증명하지 않습니다. 정확성과 보안은 결국 코드와 인간 의도 사이의 비교인데, 인간의 의도 자체에 오류가 있을 수 있기 때문이죠. 코드의 일부만 검증되어 비검증 영역에서 치명적 버그가 터지거나, 명세 자체가 잘못되거나, 사이드 채널처럼 모델 밖 공격이 들어오는 실제 사례들도 존재합니다. [시사점] 비탈릭이 그리는 미래는 소프트웨어가 "안전한 핵(secure core)"과 "위험한 가장자리(insecure edge)"로 분화하는 모습입니다. 가장자리는 샌드박스에서 최소 권한으로 운영되고, 핵은 모든 것을 관할하는 형태입니다. 핵에는 AI의 추가 연산력 전부를 보안 강화에 투입하고, 그 크기는 작게 유지합니다. 운영체제 커널, 이더리움, IoT 등이 안전한 핵 후보입니다. 즉 AI와 형식 검증 두 기술은 상보적이며, 적어도 안전한 핵 안에서는 "버그는 불가피하다"는 옛 격언이 거짓이 되는 세계가 가능할 것이라는 게 비탈릭의 결론입니다. 출처