Halmos를 사용한 상징적 테스트: 형식 검증을 위한 기존 테스트 활용

수학적 방법을 사용하여 여러 입력에 걸쳐 프로그램 또는 스마트 계약을 "검사"하는 프로세스인 공식 검증은 일반적으로 고품질의 안전한 코드를 작성하기 위한 기존 테스트에 대한 보다 간결하고 포괄적인 대안으로 간주됩니다. 그러나 실제로 공식 검증은 제한이 없고 상호 작용이 가능한 프로세스입니다. 단위 테스트와 마찬가지로 개발자는 공식 사양을 동적으로 정의하고 계층화하여 코드와 분석이 발전함에 따라 접근 방식을 반복해야 합니다. 또한 공식 검증은 작성하는 데 시간이 많이 걸릴 수 있는 사양만큼만 효과적입니다(종종 가파른 학습 곡선이 수반됨). 

프로세스가 어렵다고 생각하는 많은 개발자에게 단위 테스트는 종종 프로그램의 정확성을 확인하는 더 비용 효율적이고 시간 효율적인 방법입니다. 실제로 공식 검증은 단위 테스트에 대한 보다 포괄적인 대안이 아니라 보완적인 대안입니다. 이러한 프로세스는 서로 다른 강점과 한계를 가지고 있어 함께 사용할 때 훨씬 더 큰 확신을 제공합니다. 개발자는 항상 단위 테스트를 작성해야 합니다. 그렇다면 정식 검증을 위해 동일한 속성을 사용할 수 있다면 어떨까요?

할모스, 오픈 소스 정식 검증 도구를 사용하면 개발자가 다음을 수행할 수 있습니다. 재사용 기호 테스트를 통해 형식 사양에 대한 단위 테스트용으로 작성된 동일한 속성입니다. 개발자는 처음부터 강력한 속성 집합을 만들지 않고 중복 작업을 피하고 처음부터 시작하지 않고도 한 번에 몇 가지 사양으로 테스트를 개선할 수 있습니다. 우리는 이 도구를 공식 검증 프로세스의 다른 도구와 함께 공식 검증으로의 진입로로 사용하도록 설계했습니다. 개발자는 프로세스 후반에 추가하기 전에 최소한의 노력으로 몇 가지 분석으로 시작할 수 있습니다.

이 게시물에서는 공식 검증의 문제와 기호 테스트를 통해 단위 테스트와 공식 검증 사이의 격차를 해소할 수 있는 가능성을 다룹니다. 그런 다음 기존 스마트 계약 코드를 사용하여 Halmos의 데모를 살펴보고 개발자가 사용할 수 있는 다른 공식 검증 도구(많은 오픈 소스)를 간단히 살펴봅니다.

공식 검증 대 테스트

공식 검증 — 엄격함과 포괄성 때문에 블록체인 개발자들이 일반적으로 선호하는 — 프로그램이 특정 정확성 속성을 충족하는지 확인하여 프로그램의 정확성을 증명하는 프로세스입니다. 프로그램 고유의 속성은 일반적으로 외부에서 제공되며 사용 중인 확인 도구에서 지원하는 공식 언어 또는 표기법을 사용하여 표현됩니다. 개발자는 종종 형식 검증을 가능한 모든 시나리오에서 속성을 자동으로 테스트하기 위한 푸시 버튼 솔루션으로 인식하지만 실제로 형식 검증은 노동 집약적이고 고도의 대화형 프로세스가 될 수 있습니다.

정식 검증과 마찬가지로 단위 테스트에는 프로그램이 예상대로 작동하는지 평가하는 작업이 포함됩니다. 그러나 테스트는 다음에 대한 프로그램의 동작만 확인합니다. 일부 공식 인증을 통해 입력을 확인할 수 있습니다. 모든 가능한 입력. 테스트와 공식 검증 모두 프로그램의 예상 동작에 대한 설명이 필요합니다(테스트에 사용되는 테스트 케이스와 공식 검증에 사용되는 공식 사양 포함). 그러나 함께 사용하면 프로그램을 보다 철저하게 검사할 수 있습니다. 예를 들어 테스트는 간단한 버그와 실수를 찾는 데 효과적이지만 일반적으로 더 빠르고 쉽게 수행할 수 있습니다. 공식 확인은 사용하기 번거롭지만 오류가 없음을 증명하거나 테스트 또는 코드 검토에서 놓치기 쉬운 미묘한 버그를 드러낼 만큼 충분히 강력합니다.

사양 오버헤드

공식 검증의 주요 과제 중 하나는 공식 사양을 작성하고 유지 관리하는 오버헤드입니다. 이 프로세스에는 특수 언어(많은 개발자가 먼저 배워야 하는 언어)를 사용하여 사양을 수동으로 작성하는 시간 소모적인 작업이 포함됩니다. 또한 이 프로세스는 일반적으로 간단한 속성을 작성하고 먼저 검증한 다음 점차적으로 더 복잡한 속성을 맨 위에 추가하는 증분식입니다. 테스트와 마찬가지로 명확한 중지 지점이 없는 개방형 프로세스이며 사용 가능한 시간 프레임 내에서 가능한 한 많은 속성만 추가할 수 있습니다. 또한 개발자가 확인 중인 코드를 변경할 때 기존 사양도 업데이트해야 하므로 추가 유지 관리 노력이 필요합니다. 이러한 요인으로 인해 추가 오버헤드를 감수하는 것을 주저하는 일부 개발자에게는 공식적인 검증이 어려운 작업이 될 수 있습니다.

그리고 테스팅과 공식적인 검증이 함께 사용될 때 코드 품질을 향상시킬 수 있지만, 두 가지 모두 서로 다른 언어와 형식으로 프로그램의 예상 동작에 대한 설명이 필요합니다(때로는 유사함). 이러한 설명을 작성하고 유지하는 것은 노동 집약적이며 동일한 설명의 두 가지 다른 형식을 유지하는 것은 중복된 노력처럼 느껴질 수 있습니다. 이로 인해 다음과 같은 질문이 제기됩니다. 개발자가 테스트와 확인에 모두 사용할 수 있는 방식으로 예상되는 동작을 설명할 수 있습니까?

상징적 테스트와 Halmos로 테스트와 공식 검증 사이의 격차 해소

기호 입력으로 테스트를 실행하는 방법인 기호 테스트는 사양 오버헤드를 줄이는 효과적인 공식 검증 방법입니다. 이 접근 방식을 사용하면 테스트 및 형식 검증 모두에 대해 동일한 테스트 사례를 사용할 수 있습니다. 프로그램이 제한된 입력 세트에 대해 올바르게 작동하는지 확인하는 기존 테스트와 달리 기호 테스트는 가능한 모든 입력에 대해 프로그램을 확인하므로 기호 테스트를 통과하는 프로그램은 공식적으로 검증된 것으로 간주할 수 있습니다.

Halmos는 기호 테스트를 위해 설계된 공식 검증 도구입니다. 별도의 사양을 요구하거나 새로운 언어를 배우는 대신 Halmos는 기존 테스트를 정식 사양으로 사용합니다. Halmos를 통해 테스트를 실행하면 가능한 모든 입력을 통과하는지 자동으로 확인하거나 반례를 제공합니다. 이렇게 하면 추가 사양 작성이 필요하지 않을 뿐만 아니라 정식 검증 목적으로 단위 테스트 또는 퍼징용으로 작성된 테스트를 재사용할 수 있습니다.

따라서 개발자는 현재 요구 사항에 따라 단위 테스트, 퍼징 및 형식 검증을 포함한 다양한 품질 보증 옵션 중에서 선택할 수 있는 유연성이 더 커집니다. 예를 들어 테스트는 임의의 입력을 생성하는 fuzzer의 도움으로 간단한 실수를 신속하게 식별할 수 있으며 Halmos는 모든 입력에서 프로그램의 정확성에 대한 신뢰를 더욱 높일 수 있습니다.

예: 테스트 isPowerOfTwo() 기능

예를 들어 다음을 고려하십시오. isPowerOfTwo() 주어진 숫자가 XNUMX의 거듭제곱인지 여부를 결정하는 함수입니다. 이 함수는 비트 조작 알고리즘 그러나 특히 입력이 XNUMX의 거듭제곱이 아닌 경우 정확성을 증명하기 어려울 수 있습니다.

다음에 대한 테스트를 상상해보십시오. isPowerOfTwo() 함수: 함수의 실제 출력과 주어진 입력에 대한 예상 출력을 비교합니다. 이는 매개 변수화된 테스트(속성 기반 테스트라고도 함)이므로 Foundry와 같은 퍼징 도구를 사용하여 다양한 입력 값으로 쉽게 실행할 수 있습니다.

이 테스트를 사용하여 다음을 검사할 수 있습니다. isPowerOfTwo() 단위 테스트 또는 퍼지 테스트를 통해 기능을 선택하고 입력을 선택하여 실행합니다. 이와 같은 테스트는 가능한 모든 입력에 대해 테스트를 실행하는 것이 계산상 불가능하기 때문에 함수의 정확성을 공식적으로 증명할 수 없습니다.

그러나 Halmos를 사용하면 개발자가 약간의 추가 노력만으로 공식 검증을 위해 이러한 기존 테스트를 재사용할 수 있습니다. 도구는 테스트의 기호 실행을 수행한 다음 어설션이 위반되지 않았는지 확인하여 가능한 모든 입력에 대해 테스트가 통과하는지 확인합니다. is 위반 한, 반례를 제공함으로써). 즉, 테스트가 Halmos를 통과하면 함수의 정확성이 공식적으로 검증됩니다. 즉, 알고리즘이 올바르게 구현되고 컴파일러에 의해 바이트코드로 정확하게 변환되었음을 의미합니다.

제한 사항: 제한된 기호 실행

일반적으로 완전히 자동으로 완전한 기호 테스트를 수행하는 것은 불가능합니다. 정지 문제, 이는 결정할 수없는. 이에 대한 한 가지 이유는 루프가 상징적으로 반복되어야 하는 횟수를 자동으로 결정하는 것이 종종 불가능하기 때문입니다. 결과적으로 완전 자동 형식 검증은 일반적으로 결정할 수 없습니다.

이러한 근본적인 한계를 감안할 때 Halmos는 완전성보다 자동화를 우선시합니다. 이를 위해 Halmos는 무제한 루프(반복 횟수가 프로그램 입력에 따라 다름) 또는 가변 길이 배열(문자열 포함)에 대해 제한된 기호 추론을 수행하도록 설계되었습니다. 이는 일부 완전성을 희생하지만 Halmos는 사용자가 루프 불변량과 같은 추가 주석을 제공하도록 요구하지 않도록 합니다.

예를 들어 다음과 같은 반복 버전을 고려하십시오. isPowerOfTwo() 루프 반복 횟수가 입력 수를 나타내는 데 필요한 최소 비트 수에 의해 결정되는 제한 없는 while 루프를 특징으로 하는 함수.

Halmos는 이 무제한 루프를 지정된 범위까지만 상징적으로 반복합니다. 예를 들어 경계가 3으로 설정되면 Halmos는 루프를 최대 3번 반복하고 루프가 3번 이상 반복되는 입력 값(예: 2^3보다 크거나 같은 값)을 고려하지 않습니다. ). 이 특별한 경우 경계를 256 이상으로 설정하면 Halmos가 완료될 수 있습니다.

데모: Halmos로 ERC721A의 공식 검증

Halmos의 기능을 입증하기 위해 상징적으로 테스트하고 공식적으로 검증하는 데 사용했습니다. ERC721A, 단일 발행과 거의 동일한 비용으로 배치 발행을 허용하는 ERC721 표준의 고도로 가스 최적화된 구현입니다. ERC721A에는 몇 가지 혁신적인 기능이 포함되어 있습니다. 최적화 이 효율성을 달성하기 위해; 예를 들어 발행 시점이 아니라 토큰이 전송될 때까지 토큰 소유권 데이터에 대한 업데이트를 지연하여 가스를 절약할 수 있습니다. 이를 위해서는 게으른 데이터 구조에서 소유권 정보를 효율적으로 검색하기 위해 복잡한 데이터 구조와 알고리즘을 사용해야 합니다. 이 최적화는 가스 효율성을 향상시키지만 코드 복잡성도 증가시키고 구현의 정확성을 증명하기 어렵게 만듭니다. 따라서 ERC721A는 구현에 대한 신뢰를 높이고 잠재적 사용자에게 혜택을 줄 수 있으므로 공식 검증을 위한 좋은 후보가 됩니다.

기호 테스트 속성

ERC721A에 대한 기존 테스트는 Hardhat(현재 Halmos에서 지원하지 않음)을 사용하여 JavaScript로 작성되었으므로 기본 진입점 기능에 대해 Solidity에서 새로운 테스트를 작성했습니다. mint(), burn()및 transfer(). 이 테스트는 각 기능이 토큰 소유권과 잔액을 올바르게 업데이트하고 다른 사용자의 잔액이나 소유권을 변경하지 않고 관련 사용자에게만 영향을 미치는지 확인했습니다. 후자는 ERC721A에서 게으른 데이터 구조 알고리즘을 사용하기 때문에 증명하기 쉽지 않습니다. 예를 들어, 다음 테스트는 transfer() 함수는 지정된 토큰의 소유권을 올바르게 업데이트합니다.

또 다른 테스트는 다음을 확인합니다. transfer() 함수는 앞에서 언급한 것처럼 증명하기 어려운 다른 주소의 잔액을 변경하지 않습니다.

검증 결과

ERC721A 스마트 컨트랙트에 Halmos를 이용하여 총 19 테스트. 테스트는 완료하는 데 3분이 걸린 루프 언롤링 바운드 16으로 Halmos를 통해 실행되었습니다. 확인 시간의 내역은 아래 표에서 확인할 수 있습니다. 실험은 M1 Pro 칩과 16GB 메모리가 장착된 MacBook Pro에서 진행되었습니다.

Test	시간
테스트굽기균형업데이트	6.67
testBurnNextTokenId변경되지 않음	1.40
테스트화상기타균형보존	5.69
testBurnOtherOwnership보존	189.70
testBurn소유권업데이트	3.81
테스트 굽기 요구 사항	71.95
테스트민트밸런스업데이트	0.20
testMintNextTokenId업데이트	0.18
테스트민트기타균형보존	0.26
testMint기타소유권보존	5.74
testMint소유권업데이트	1.38
testMint요구 사항	0.09
testTransferBalance변경되지 않음	9.03
testTransferBalance업데이트	53.53
testTransferNextTokenId변경되지 않음	4.47
testTransferOtherBalance보존	19.57
testTransferOtherOwnership보존	430.61
테스트 소유권 이전업데이트	18.71
테스트전송요구사항	149.18

대부분의 테스트는 몇 초 만에 완료되었지만 일부 테스트는 몇 분이 걸렸습니다. 이러한 시간 소모적인 테스트는 고려해야 할 사례의 복잡한 특성으로 인해 확인하기 어려웠으며 지연 데이터 구조 알고리즘의 정확성과 밀접한 관련이 있습니다.

전반적으로 이 실험의 결과는 Halmos가 스마트 계약 코드의 정확성을 효과적으로 검증할 수 있음을 나타냅니다. 스마트 계약의 복잡성과 잠재적인 에지 케이스에도 불구하고 코드의 무결성에 대한 신뢰도를 높입니다.

주입된 버그로 실험

Halmos의 제한된 추론의 효율성을 입증하기 위해 이전 버전의 ERC721A 계약에서 버그를 탐지하는 데 사용했습니다. 이 버전에는 산술 오버플로를 잘못 처리하고 잠재적으로 많은 수의 토큰을 일괄 발행할 수 있는 문제가 있었습니다. 이로 인해 게으른 데이터 구조의 무결성이 손상되고 일부 사용자가 토큰 소유권을 잃을 수 있습니다(문제 해결 현재 버전에서). 우리는 버그가 있는 버전에서 ERC19A에 대해 동일한 721개 테스트 세트를 실행했으며 Halmos는 mint() 기능. 특히 Halmos는 위에서 설명한 익스플로잇 시나리오로 이어지는 입력 값을 제공했습니다. 이 실험의 결과는 불완전함에도 불구하고 Halmos의 제한된 추론이 스마트 계약에서 악용 가능한 버그를 탐지하고 방지하는 효과적인 방법이 될 수 있음을 나타냅니다.

관련된 일

이더리움 스마트 계약 바이트코드에 대한 정식 검증 도구는 다양한 팀에서 개발되었습니다. Halmos를 포함한 이러한 도구는 스마트 계약의 보안 및 정확성을 보장하는 데 사용할 수 있습니다. 이러한 도구의 다양한 기능, 기능 및 제한 사항을 비교하고 이해하면 개발자가 고유한 요구 사항에 가장 적합한 도구를 선택하는 데 도움이 될 수 있습니다.

Halmos는 스마트 계약 검증에 사용할 수 있는 도구 세트에 귀중한 추가 기능이지만 기존 도구를 보완(대체하지 않음)하기 위한 것입니다. 개발자는 Halmos를 다른 도구와 결합하여 계약에서 더 높은 수준의 보증을 달성할 수 있습니다. 아래에서는 Halmos를 EVM 바이트코드를 지원하는 몇 가지 선택된 공식 도구와 비교합니다.

• K 연역적 검증 및 대화형 정리 증명을 가능하게 하는 강력한 공식 검증 프레임워크입니다. 기본 이론 및 구현은 높은 수준의 표현력을 제공하므로 복잡한 프로그램 및 알고리즘을 검증하는 데 적합합니다. 그러나 K는 자동 검증에 중점을 두고 설계되지 않았으며 검증 프로세스 중에 더 많은 수동 작업이 필요할 수 있는 특정 자동화 기능이 부족하다는 점에 유의해야 합니다. K 프레임워크를 사용하기 위해서는 K 언어로 공식 스펙을 작성해야 하며, 사용하기 전에 이를 학습해야 합니다. 그 강점은 자동화된 추론을 사용하여 분석하기 어려울 수 있는 복잡한 시스템을 검증하는 데 특히 유용합니다.
• 체르토라 Halmos와 유사하게 자동화된 검증에 중점을 두고 제한된 모델 확인을 지원하는 스마트 계약용 공식 검증 도구입니다. Certora를 사용하려면 개발자는 새로운 언어를 배워야 합니다. CVL, 사양을 작성하기 위해. 이 언어는 Halmos가 현재 지원하지 않는 기능인 계약 불변성을 통해 많은 중요한 속성에 대한 간결한 설명을 허용합니다. 비공개 소스의 독점 도구임에도 불구하고 Certora는 지속적인 개발과 우수한 사용자 지원을 통해 강력한 공식 검증 도구를 제공합니다.
  
  반면에 Halmos는 규모가 더 작은 오픈 소스 도구이며 현재 Certora에서 제공하는 일부 기능이 부족하지만 공공재 역할을 하기 위한 것이며 광범위한 설정 및 유지 관리가 필요합니다.
• HEVM Halmos와 유사한 또 다른 공식 검증 도구입니다. 이전에는 Foundry의 선구자인 DappTools의 일부였습니다. HEVM과 Halmos 모두 별도의 명세를 요구하지 않는 특징이 있으며 기존 테스트를 상징적으로 실행하여 어설션 위반을 식별할 수 있습니다. 이를 통해 사용자는 두 도구를 상호 교환적으로 사용하거나 동일한 테스트에 대해 병렬로 실행하여 기호 테스트를 위한 여러 옵션을 제공할 수 있습니다.
  
  유사성에도 불구하고 HEVM과 Halmos는 독립적으로 개발되었으며 구현 세부 사항이 다릅니다. 특히 최적화 및 상징적 추론 전략 측면에서 그렇습니다. 또한 HEVM은 Haskell로 작성되고 Halmos는 Python으로 작성되어 풍부한 Python 생태계에 대한 노출을 제공합니다. 두 도구를 모두 사용할 수 있는 기능을 통해 사용자는 스마트 계약의 보안과 정확성을 보장할 수 있는 더 많은 유연성과 옵션을 얻을 수 있습니다.

할모스 오픈 소스이며 현재 베타 단계에 있습니다. 신규사업에 적극 나서고 있습니다 풍모 Foundry 치트 코드 및 기타 몇 가지 주요 유용성 기능을 포함한 기능. 어떤 기능이 가장 중요한지에 대한 귀하의 의견에 진심으로 감사드리며 Halmos를 모두를 위한 더 나은 도구로 만들기 위한 피드백, 제안 및 기여를 환영합니다.

**

여기에 표현된 견해는 인용된 개별 AH Capital Management, LLC("a16z") 직원의 견해이며 16z 또는 그 계열사의 견해가 아닙니다. 여기에 포함된 특정 정보는 16z가 관리하는 펀드의 포트폴리오 회사를 포함하여 제16자 출처에서 얻은 것입니다. 신뢰할 수 있는 출처에서 가져왔지만 16z는 이러한 정보를 독립적으로 확인하지 않았으며 정보의 현재 또는 지속적인 정확성 또는 주어진 상황에 대한 적절성에 대해 어떠한 진술도 하지 않습니다. 또한 이 콘텐츠에는 타사 광고가 포함될 수 있습니다. XNUMXz는 그러한 광고를 검토하지 않았으며 여기에 포함된 광고 콘텐츠를 보증하지 않습니다.

이 콘텐츠는 정보 제공의 목적으로만 제공되며 법률, 비즈니스, 투자 또는 세금 관련 조언에 의존해서는 안 됩니다. 그러한 문제에 관해서는 자신의 고문과 상의해야 합니다. 증권 또는 디지털 자산에 대한 언급은 설명을 위한 것일 뿐이며 투자 추천이나 투자 자문 서비스 제공을 의미하지 않습니다. 또한, 이 콘텐츠는 투자자 또는 예비 투자자를 대상으로 하거나 사용하도록 의도되지 않았으며, 어떤 상황에서도 a16z가 관리하는 펀드에 투자하기로 결정할 때 의존할 수 없습니다. (16z 펀드에 대한 투자 제안은 사모 투자 각서, 청약 계약서 및 해당 펀드의 기타 관련 문서에 의해서만 이루어지며 전체 내용을 읽어야 합니다.) 언급되거나 언급된 모든 투자 또는 포트폴리오 회사 설명된 내용은 16z가 관리하는 차량에 대한 모든 투자를 대표하는 것은 아니며 투자가 수익성이 있거나 미래에 수행되는 다른 투자가 유사한 특성 또는 결과를 가질 것이라는 보장이 없습니다. Andreessen Horowitz가 관리하는 펀드의 투자 목록(발행자가 16z가 공개적으로 공개하도록 허가하지 않은 투자 및 공개적으로 거래되는 디지털 자산에 대한 미고지 투자 제외)은 https://a16z.com/investments에서 볼 수 있습니다. /.

내부에 제공된 차트와 그래프는 정보 제공의 목적으로만 사용되며 투자 결정을 내릴 때 의존해서는 안 됩니다. 과거의 성과는 미래의 결과를 나타내지 않습니다. 내용은 표시된 날짜 현재만 말합니다. 이 자료에 표현된 모든 예측, 추정, 예측, 목표, 전망 및/또는 의견은 예고 없이 변경될 수 있으며 다른 사람이 표현한 의견과 다르거나 반대될 수 있습니다. 추가 중요 정보는 https://a16z.com/disclosures를 참조하십시오.