핵심 요약
- 새로운 형태의 컴퓨팅. 영지식 증명을 사용하면 작업 부하를 실행하고 결과와 함께 프로그램이 올바르게 실행되었음을 보여주는 짧은 증명을 받을 수 있습니다. 누구나 프로그램을 다시 실행하지 않고, 실행한 사람을 신뢰하지 않고, 프로그램이 실행된 데이터에 접근할 필요 없이 밀리초 만에 증명을 확인할 수 있습니다.
- 광범위한 채택을 가로막아 온 세 가지 큰 과제가 있었습니다: 증명을 충분히 빠르게 생성할 수 있도록 하는 것, 암호학 전문 지식 없이도 일반 프로그램에서 증명을 사용할 수 있도록 하는 것, 그리고 수십 년 후에도 여전히 신뢰할 수 있는 암호학 위에 이를 구축하는 것입니다.
- Magnetar는 이 세 가지 과제 모두에서 큰 진전을 이루었습니다. Rust, Go 또는 C로 작성된 프로그램을 증명하고, 이전의 가장 빠른 유사 시스템보다 평균 10배에서 39배 빠르게 실행되며, 보안을 표준 해시 함수에만 의존합니다. 이는 Microsoft Research에서 영지식 증명을 실용화하기 위한 10년이 넘는 연구의 최신 성과입니다.
새로운 형태의 컴퓨팅
컴퓨터가 생성하는 모든 결과에는 암묵적인 질문이 따릅니다: 프로그램이 주장된 대로 실행되어 올바른 출력을 생성했는가? 오늘날 이 질문에 답하려면 검증과 함께 어느 정도의 신뢰가 필요한 경우가 많습니다. 우리는 운영자, 공급업체, 거래 상대방 또는 에이전트를 신뢰하며, 계약, 감사, 로그를 통해 그 신뢰를 확립합니다.
영지식 증명은 신뢰를 확립하는 근본적으로 다른 접근 방식을 제시합니다. 프로그램이 실행되면 출력과 함께 짧은 증명, 즉 이 프로그램이 이러한 입력에 대해 이 출력을 생성했음을 나타내는 암호학적 인증서를 생성합니다. 증명은 작고 확인이 빠릅니다. 증명을 받은 사람은 프로그램을 다시 실행하지 않고도 밀리초 만에 결과를 확인할 수 있으며, 동일한 보증이 필요한 다른 사람에게 증명을 전달할 수도 있습니다. 영지식 속성 덕분에 증명은 비공개로 유지되어야 하는 입력에 대한 어떠한 정보도 노출하지 않습니다.
이는 실제 세계에서 정확성이 의미하는 바를 바꿉니다. 결과를 누가 생성했는지 때문에 신뢰할 필요가 없어집니다. 결과에 무엇이 동반되는지를 근거로 검증할 수 있게 됩니다. 누군가를 대신해 행동하는 AI 에이전트는 각 행동이 주어진 정책을 준수했음을 증명하는 증명서를 첨부할 수 있습니다. 규제 대상 금융 기관은 거래 내역을 공개하지 않고도 거래가 올바르게 처리되었음을 증명할 수 있습니다. 증명 생성이 프로그램 실행만큼 일상적인 일이 되면 이 모든 것이 가능해집니다.
세 가지 큰 과제
영지식 증명은 1980년대에 발명되었으며, 프로그램 실행을 증명한다는 아이디어도 거의 같은 시기부터 존재해 왔습니다. 이를 범용 도구로 만들지 못하게 한 것은 동시에 해결하기 어려웠던 세 가지 과제입니다.
효율성. 역사적으로 증명 생성은 프로그램 자체를 실행하는 것보다 수백만 배 더 많은 연산을 필요로 했습니다. 수년간의 연구로 그 오버헤드가 줄어들었지만, 가장 빠른 시스템들은 다른 부분에서 타협을 함으로써 속도를 달성했습니다.
범용성과 사용 편의성. 많은 증명 시스템은 개발자가 프로그램을 암호학 회로, 즉 해당 연산의 고정된 산술적 표현으로 수동으로 다시 작성하도록 요구합니다. 이는 몇 달이 걸리는 작업입니다. 애플리케이션을 변경할 때마다 새 회로가 필요하며, 이 번역 과정 자체가 보안 버그의 잦은 원인이 됩니다. 범용적인 대안은 일반 프로세서의 실행을 증명하는 것으로, 이렇게 하면 컴파일된 모든 프로그램을 작성된 그대로 증명할 수 있습니다. 그러나 최근까지 이러한 범용성은 속도나 보안에서 큰 비용을 치러야 했습니다.
보안. 증명은 그 기반이 되는 암호학만큼만 강력합니다. 많은 증명 시스템은 충분히 강력한 양자 컴퓨터로 깨질 수 있는 타원 곡선에 기반합니다. Microsoft는 자사의 제품과 서비스를 양자 후 암호로 전환한다는 목표를 가진 Quantum Safe Program으로 이 문제를 해결하고 있으며, 이 목표는 최근 2029년으로 앞당겨졌습니다. 양자 후 증명 시스템은 이미 존재하지만, 일부는 격자 가정에 기반하고 대부분은 증명 비용을 줄이기 위해 고안된 새로운 암호학 함수에 기반합니다. 이러한 새로운 암호학 함수는 오늘날 인터넷을 보호하는 암호학이 받아온 수십 년간의 검증을 거치지 않았으며, 일부는 아직 증명되지 않은 오류 정정 부호에 관한 수학적 추측에 의존합니다. 이들은 강한 가정을 통해 속도를 얻은 것입니다.
PODCAST SERIES
The Shape of Things to Come
Microsoft의 Doug Burger와 게스트들이 AI에 대한 근본적인 진실과 AI가 미래를 어떻게 재편할 것인지에 대해 깊이 있게 이야기합니다.
지금 듣기10년이 넘는 연구의 결실
10년 넘게 Microsoft Research는 영지식 증명과 검증 가능 컴퓨팅을 실용적으로 만드는 연구를 해왔습니다. 초기 연구는 두 가지 접근 방식을 따랐는데, 둘 다 작은 프로그램에만 실용적이었습니다. 첫 번째 (새 탭에서 열림) (새 탭에서 열림)접근 방식은 sum-check라는 기법을 사용하여 검증자가 증명자와의 짧은 대화를 통해 긴 계산을 확인할 수 있게 해주는 sum-check 프로토콜(새 탭에서 열림)것이지만, 이는 특정한 계층 구조를 가진 계산에만 적용될 수 있었습니다. 두 번째 (새 탭에서 열림) (새 탭에서 열림)접근 방식은 타원곡선 암호학을 사용하여 거의 모든 계산에 대해 매우 작은 증명을 만들었습니다. 그러나 이는 비밀 정보가 포함된 일회성 신뢰 설정을 필요로 하며, 이 정보가 유출되면 누구나 증명을 위조할 수 있게 됩니다. 이 접근 방식은 양자 컴퓨터에도 취약합니다.
2019년에 Spartan 이라는 새로운 영지식 증명 시스템이 sum-check 접근 방식으로 돌아와 신뢰 설정 없이 범용 프로그램에 작동하도록 만들었습니다. Spartan은 서로 다른 암호학적 구성 요소로 인스턴스화될 수도 있습니다. 바로 이 유연성이 나중에 증명 시스템이 해시 함수만으로 구축될 수 있게 한 요인입니다. 이어진 일련의 연구 결과들이 남은 조각들을 채워 넣었습니다:
- Phalanx(새 탭에서 열림)은(는) 2021년에 프로세서가 모든 단계에서 동일한 명령어 사이클을 실행하는 것과 같은 반복을 활용하여 Spartan보다 한 자릿수 빠르게 계산을 증명하는 방법을 보여주었습니다. Magnetar의 프로세서 기술은 이 아이디어를 기반으로 합니다.
- Nova(새 탭에서 열림), HyperNova(새 탭에서 열림), NeutronNova(새 탭에서 열림), Neo 및 SuperNeo(새 탭에서 열림) 은(는) Spartan의 증명을 일찍 중단하고 부분 결과들을 접어서 결합하면 어떤 크기의 계산이든 훨씬 낮은 비용으로 실용적으로 증명할 수 있음을 보여주었습니다.
- Brakedown(새 탭에서 열림)은(는) 2021년에 빠른 해시 기반 커밋먼트 방식을 도입하고 이를 Spartan과 결합하여, 보안이 표준 해시 함수에 기반하는 최초의 Spartan 변형을 탄생시켰습니다.
- Spice(새 탭에서 열림), Lasso(새 탭에서 열림), Nebula(새 탭에서 열림), 그리고 Twist and Shout(새 탭에서 열림) 은(는) 범용 프로세서의 핵심인 메모리 연산을 저렴하게 증명할 수 있게 했고, Jolt(새 탭에서 열림) 은(는) 이를 Spartan과 결합하면 완전한 프로세서의 실행을 효율적으로 증명할 수 있음을 보여주었습니다.
- 올해 초, Vega(새 탭에서 열림) 은(는) 이 연구 흐름을 디지털 신원에 적용하여 정부 자격 증명으로부터의 사실을 증명했습니다. 10분의 1초 미만의 시간 안에.
- 최근에는, BinarySpartan (opens in new tab) 가 프로세서의 논리와 표준 해시 함수를 효율적으로 표현할 수 있는 이진 필드에 Spartan을 도입했습니다. BinarySpartan은 또한 Ligerito (opens in new tab)(훨씬 짧은 증명을 제공하는 Brakedown 방식의 커밋 스킴)에 의존하며, 또한 ring switching (opens in new tab)(비트 벡터에 대한 커밋을 효율적으로 만들어 주는 기술)에도 의존합니다.
이들 각각은 문제의 한 조각을 해결했습니다. Magnetar는 이 조각들이 하나로 모이는 지점입니다.
Magnetar
Magnetar 는 영지식 가상 머신(zkVM)이며, 세 가지 과제 모두에 대해 동시에 큰 진전을 이루어 냅니다.
범용입니다. Magnetar는 모든 주류 언어를 위한 성숙한 컴파일러를 갖춘 개방형 프로세서 아키텍처인 RISC-V의 실행을 증명합니다. 개발자가 Rust, Go 또는 C로 프로그램을 작성하고 평소처럼 컴파일하면, Magnetar는 작성된 그대로의 프로그램을 증명합니다. 이것이 실무에서 의미하는 바를 생각해 보십시오. 비즈니스 정책, 데이터 파이프라인, 또는 이더리움 가상 머신(EVM)용 인터프리터는 그저 하나의 프로그램일 뿐이며, 이미 이를 유지 보수하는 엔지니어들은 작성된 그대로의 실행을 증명할 수 있습니다. 그 결과, 증명은 더 이상 전문가만의 활동이 아닙니다.
이는 동급의 이전 시스템보다 빠릅니다. Magnetar는 노트북에서 초당 7.2에서 8.7백만 개의 프로세서 명령을 증명합니다. 암호화 해싱부터 작은 EVM 인터프리터 내부의 토큰 전송에 이르는 15개의 벤치마크 프로그램에서, 동일한 머신에서 가장 빠른 기존 zkVM보다 평균 10배에서 39배 빠르며, 토큰 전송 벤치마크에서는 다른 두 개보다 300배 이상 빠릅니다. 최적화된 Magnetar는 초당 9.5–12.8백만 사이클을 증명하며, 이는 여기서 보고된 각 속도 향상을 약 1.3배 증가시킵니다. 증명 검증은 약 12밀리초에 완료됩니다.
이 보안은 표준 암호화에 기반을 둡니다. Magnetar는 SHA-256이나 SHA-3 같은 표준 해시 함수에 의존하며, 이는 이미 모든 조직의 시스템을 보호하고 있는 동일한 기본 요소들입니다. 타원 곡선도, 격자도, 특수 목적 해시 함수도, 신뢰할 수 있는 초기 설정도, 그리고 오류 정정 부호에 관한 미증명 추측도 필요로 하지 않습니다. 해시 함수는 암호학 도구 상자에서 가장 철저히 연구된 기본 요소이며, NIST가 자체적으로 보수적인 포스트 양자 옵션으로 표준화한 상태 비저장 해시 기반 서명의 기반이기도 합니다. 수십 년 후에도 여전히 신뢰할 수 있어야 하는 시스템의 경우, 표준 해시 함수에만 의존하면 로드맵에서 암호학적 마이그레이션을 없앨 수 있습니다.
이 동일한 설계 결정은 또 한 번의 이점을 가져옵니다. Magnetar 증명 검증은 대부분 표준 해시 함수와 이진체 연산을 평가하는 것으로 구성되는데, 이는 바로 Magnetar가 효율적으로 증명하는 연산들입니다. 따라서 증명 검증은 Magnetar에게는 평범한 작업입니다. 이것이 Magnetar가 계산을 조각 단위로 증명한 후 그 조각들을 결합함으로써 어떤 크기의 계산이든 증명할 수 있게 해주는 이유입니다. 또한 이를 통해 Magnetar는 원장이나 블록체인 같은 장기 실행 시스템을 증명할 수 있습니다.
이 기술 논문 전체 설계, 보안 분석 및 측정 결과를 제시합니다.
앞으로의 전망
Magnetar는 영지식 증명과 검증 가능 컴퓨팅을, 조직들이 이미 신뢰하는 암호학 기반 위에서, 엔지니어가 일반적인 코드를 작성하듯 실제로 활용할 수 있는 속도로 발전시킵니다. Magnetar는 암호학적 증명이 계산의 일상적인 산출물이 되는 미래를 실현합니다. 우리는 기술 리더들이 더 이상 다음과 같이 묻지 않을 것이라고 기대합니다. 실행 증명이 실용적인지 여부 대신 다음에 초점을 맞춘다 결과적으로 것입니다 그들은 맹신하기보다 직접 검증하는 것을 선호한다.
영지식 증명이 귀하의 사용 사례를 어떻게 지원할 수 있는지 알아보고 싶으시다면, 저희는 기꺼이 여러분의 소식을 듣습니다 (새 탭에서 열림).