소개
비트코인 및 Liquid와 같은 다른 블록체인의 보안은 ECDSA 및 Schnorr 서명과 같은 디지털 서명 알고리즘의 사용에 달려 있습니다. 이 라이브러리가 작동하는 타원 곡선의 이름을 따서 명명된 libsecp256k1라는 C 라이브러리는 비트코인 코어와 Liquid 모두에서 이러한 디지털 서명 알고리즘을 제공하는 데 사용됩니다. 이러한 알고리즘은 모듈러 역수라는 수학적 계산을 사용하며, 이는 계산의 상대적으로 비싼 구성 요소입니다.
“빠른 상수 시간 gcd 계산 및 모듈러 역수”에서 Daniel J. Bernstein과 Bo-Yin Yang은 새로운 모듈러 역수 알고리즘을 개발합니다. 2021년, 이 알고리즘은 “safegcd”라고 불리며 Peter Dettman에 의해 libsecp256k1에 구현되었습니다. 이 새로운 알고리즘의 검증 과정의 일환으로 Blockstream Research는 Coq 증명 보조 도구를 사용하여 알고리즘이 실제로 256비트 입력에서 올바른 모듈러 역수 결과로 종료됨을 형식적으로 검증한 최초의 기관이었습니다.
알고리즘과 구현 간의 간극
2021년의 형식화 노력은 Bernstein과 Yang이 설계한 알고리즘이 올바르게 작동함을 보여주었습니다. 그러나 libsecp256k1에서 해당 알고리즘을 사용하려면 safegcd 알고리즘의 수학적 설명을 C 프로그래밍 언어로 구현해야 합니다. 예를 들어, 알고리즘의 수학적 설명은 256비트 부호 있는 정수만큼 넓을 수 있는 벡터의 행렬 곱셈을 수행하지만, C 프로그래밍 언어는 기본적으로 64비트(또는 일부 언어 확장을 통해 128비트)까지의 정수만 제공합니다.
safegcd 알고리즘을 구현하려면 C의 64비트 정수를 사용하여 행렬 곱셈 및 기타 계산을 프로그래밍해야 합니다. 또한 구현을 빠르게 만들기 위해 많은 다른 최적화가 추가되었습니다. 결국 libsecp256k1에는 safegcd 알고리즘의 네 가지 별도의 구현이 있습니다: 서명 생성을 위한 두 개의 상수 시간 알고리즘, 32비트 시스템에 최적화된 것과 64비트 시스템에 최적화된 것, 그리고 서명 검증을 위한 두 개의 가변 시간 알고리즘, 다시 32비트 시스템과 64비트 시스템 각각에 대한 것입니다.
검증 가능한 C
safegcd 알고리즘이 올바르게 구현되었는지 확인하기 위해 모든 구현 세부 사항을 확인해야 합니다. 우리는 Coq 정리 증명기를 사용하여 C 코드에 대한 추론을 위한 Verified Software Toolchain의 일부인 Verifiable C를 사용합니다.
검증은 각 검증 대상 함수에 대해 분리 논리를 사용하여 전제 조건과 후제 조건을 지정함으로써 진행됩니다. 분리 논리는 서브루틴, 메모리 할당, 동시성 등에 대한 추론을 전문으로 하는 논리입니다.
각 함수에 사양이 주어지면, 검증은 함수의 전제 조건에서 시작하여 함수 본문의 각 문장 후에 새로운 불변식을 설정하고, 마지막으로 함수 본문 끝이나 각 반환 문장 끝에서 후제 조건을 설정합니다. 대부분의 형식화 노력은 코드의 “사이”에서 불변식을 사용하여 각 C 표현식의 원시 작업을 조작되는 데이터 구조가 수학적으로 무엇을 나타내는지에 대한 더 높은 수준의 진술로 변환하는 데 사용됩니다. 예를 들어, C 언어가 64비트 정수 배열로 간주하는 것은 실제로 256비트 정수의 표현일 수 있습니다.
최종 결과는 libsecp256k1의 64비트 가변 시간 safegcd 모듈러 역수 알고리즘 구현이 기능적으로 올바르다는 것을 Coq 증명 보조 도구가 검증한 형식적 증명입니다.
검증의 한계
기능적 정확성 증명에는 몇 가지 한계가 있습니다. Verifiable C에서 사용되는 분리 논리는 부분 정확성으로 알려진 것을 구현합니다. 즉, C 코드가 올바른 결과로 반환되는 것을 보장하지만, 종료 자체를 증명하지는 않습니다. 우리는 safegcd 알고리즘의 경계에 대한 이전 Coq 증명을 사용하여 주요 루프의 루프 카운터 값이 실제로 11회 초과하지 않음을 증명함으로써 이 한계를 완화합니다.
또 다른 문제는 C 언어 자체에 형식적 사양이 없다는 것입니다. 대신 Verifiable C 프로젝트는 CompCert 컴파일러 프로젝트를 사용하여 C 언어의 형식적 사양을 제공합니다. 이는 검증된 C 프로그램이 CompCert 컴파일러로 컴파일될 때 결과 조립 코드가 그 사양을 충족함을 보장합니다(위의 한계에 따라). 그러나 이는 GCC, clang 또는 다른 컴파일러가 생성한 코드가 반드시 작동할 것이라는 보장을 제공하지 않습니다. 예를 들어, C 컴파일러는 함수 호출 내 인수에 대해 서로 다른 평가 순서를 가질 수 있습니다. 그리고 C 언어에 형식적 사양이 있다고 하더라도, 형식적으로 검증되지 않은 컴파일러는 여전히 프로그램을 잘못 컴파일할 수 있습니다. 이는 실제로 발생합니다.
마지막으로, Verifiable C는 구조체를 전달하거나 반환하거나 할당하는 것을 지원하지 않습니다. libsecp256k1에서는 구조체가 항상 포인터로 전달되지만(이는 Verifiable C에서 허용됨), 구조체 할당이 사용되는 경우가 몇 가지 있습니다. 모듈러 역수 정확성 증명을 위해, 3개의 할당이 필드별로 구조체 할당을 수행하는 특수 함수 호출로 대체해야 했습니다.
요약
Blockstream Research는 libsecp256k1의 모듈러 역수 함수의 정확성을 형식적으로 검증했습니다. 이 작업은 C 코드의 검증이 실제로 가능하다는 추가 증거를 제공합니다. 일반 목적의 증명 보조 도구를 사용하면 복잡한 수학적 주장을 기반으로 구축된 소프트웨어를 검증할 수 있습니다.
libsecp256k1에 구현된 나머지 함수들도 검증될 수 있는 것을 막는 것은 없습니다. 따라서 libsecp256k1는 가능한 가장 높은 소프트웨어 정확성 보장을 얻을 수 있습니다.
