PropertyGPT는 대규모 언어 모델(LLM)을 활용하여 스마트 컨트랙트의 공식 검증을 위한 포괄적인 속성 생성을 자동화하는 엔드 투 엔드 시스템입니다. 백서의 저자는 Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, Yang Liu입니다. ^[1]

개요

PropertyGPT는 고급 자연어 처리, 특히 GPT 모델을 사용하여 검증 규칙 생성을 자동화함으로써 스마트 컨트랙트 보안 문제를 해결합니다. 이 기술은 복잡한 코드 기능을 이해하고 지식을 자동으로 이전하여 효율적이고 널리 적용 가능한 보안 규칙을 생성합니다. PropertyGPT는 이러한 규칙을 공식화하는 데 드는 비용과 시간을 줄여 보안 전문가에 대한 의존도를 낮춥니다. 이 접근 방식을 통해 PropertyGPT는 스마트 컨트랙트의 다양하고 복잡한 특성에 적응할 수 있는 수많은 불변 검증 규칙을 신속하게 생성하여 엄격한 보안 표준을 충족하는지 확인합니다. 규칙 생성을 자동화하면 보안 감사 프로세스가 간소화되고 전체 비용이 절감되어 더 많은 프로젝트가 개발 초기에 스마트 컨트랙트를 보호할 수 있습니다. ^[1][2]

이 시스템은 23개의 Certora 프로젝트에서 작성된 623개의 속성을 사용하여 구현 및 평가되었으며 80%의 재현율을 달성했습니다. PropertyGPT는 이러한 프로젝트 내에서 CVE, 공격 사건 및 제로 데이 취약점을 감지하여 버그 현상금 보상을 받았습니다. 전이 학습, 검색 증강 생성, 기호 실행, 모듈식 검증 및 경계 모델 검사를 포함하는 속성 검증 프로세스를 사용하여 광범위한 스마트 컨트랙트 취약점을 감지합니다. ^[1][2]

기술

벡터 데이터베이스

PropertyGPT의 벡터 데이터베이스는 유사한 코드를 검색하고 원래 참조 속성에 매핑하는 데 도움이 되는 중요한 구성 요소입니다. 참조 속성에 해당하는 중요한 코드를 숫자 표현(종종 벡터)으로 임베딩하여 구성됩니다.

• 벡터 데이터베이스 생성: 벡터 데이터베이스는 참조 속성과 관련된 코드의 필수 부분을 임베딩하여 형성됩니다. 이 프로세스는 코드를 숫자 표현 또는 벡터로 변환합니다.
• 유사한 코드 검색: PropertyGPT가 속성 생성을 위해 제목 코드를 수신하면 벡터 데이터베이스를 쿼리하여 특정 임계값 내에서 유사한 코드를 검색합니다. 유사성은 데이터베이스에 있는 코드의 숫자 표현을 기반으로 하며, 임계값은 유사하지 않은 코드를 필터링합니다.
• 참조 속성에 매핑: PropertyGPT는 벡터 데이터베이스에서 유사한 코드를 검색한 후 각 코드를 원래 참조 속성에 매핑합니다. 이 매핑은 생성된 속성이 기존의 관련 속성을 기반으로 하고, 더 정확하고 상황에 맞는 속성 생성을 위해 참조 속성에 인코딩된 지식을 활용하도록 보장합니다.

벡터 데이터베이스는 참조 속성의 본질을 캡처하는 코드 표현의 저장소 역할을 하여 PropertyGPT가 유사한 코드를 검색하고 참조 속성에 매핑하여 알 수 없는 코드에 대한 사용자 정의 속성을 생성할 수 있도록 합니다. 임베딩 및 유사성 계산 기술에 대한 특정 세부 사항은 PropertyGPT 배후의 연구자가 선택한 방법 및 알고리즘에 따라 다릅니다. ^[1][2]

반복적인 속성 생성

PropertyGPT의 반복적인 속성 생성에는 제목 코드에 대한 후보 속성을 생성하고 개선하여 정확성과 컴파일 가능성을 보장하는 작업이 포함됩니다. 이 프로세스는 벡터 데이터베이스에서 제목 코드와 유사한 참조 속성을 검색하는 것으로 시작됩니다. 이러한 참조 속성은 예시 역할을 하고 후보 속성 생성을 위한 시작점을 제공합니다. 그런 다음 생성 프롬프트는 특정 변수 또는 함수 이름이 아닌 구조적 및 구문적 측면에 초점을 맞춰 이러한 속성 생성을 안내합니다. ^[1]

후보 속성이 생성되면 PSL(Property Specification Language) 컴파일러를 사용하여 컴파일 오류가 있는지 확인합니다. 컴파일에 실패한 속성은 생성된 코드에 오류 또는 불일치가 있음을 나타냅니다. PropertyGPT는 수정 프롬프트를 사용하여 반복적인 수정 프로세스를 안내하고, 언어 모델에 규칙 코드를 수정하고 구조적 및 구문적 일관성을 유지하면서 오류를 수정하도록 지시합니다. 언어 모델은 오류를 분석하고 필요한 수정을 식별하며 속성의 수정된 버전을 생성합니다. 이 반복적인 프로세스는 속성이 컴파일 가능하거나 최대 수정 시도 횟수에 도달할 때까지 계속됩니다. ^[1]

PropertyGPT는 컴파일을 통해 속성의 구문적 정확성을 보장하는 것 외에도 속성이 의미가 있고 의도된 동작을 캡처하는지 확인하기 위해 추가 검사를 수행합니다. 예를 들어 속성에 대상 제목 함수가 포함되어 있는지, 원하는 동작을 테스트하는 데 기능적으로 의미가 있는지 확인합니다. PropertyGPT는 후보 속성을 반복적으로 생성하고 수정함으로써 구문적으로 정확하고 제목 코드에 대해 기능적으로 의미 있는 속성을 생성하는 것을 목표로 합니다. 이 반복적인 접근 방식을 통해 개선 및 향상이 가능하여 생성된 속성의 정확성과 효율성이 향상됩니다. ^[1]

속성 사양 언어(PSL)

PSL(Property Specification Language)은 PropertyGPT에서 스마트 컨트랙트 속성을 지정하기 위해 제안된 중간 언어입니다. PSL은 Solidity 프로그래밍 언어를 확장하여 속성을 정의하는 구조화되고 표현력이 풍부한 방법을 제공합니다. 이를 통해 컨트랙트 실행 중에 항상 유지되어야 하는 속성인 불변성을 정의할 수 있습니다. 이러한 불변성은 상태 변수에 대해 정의되어 컨트랙트 수명 주기 전반에 걸쳐 필수 특성 및 제약 조건이 유지되도록 보장합니다. ^[1][3]

함수 사전 및 사후 조건은 Hoare 삼중항을 사용하여 지원됩니다. 사전 조건은 함수가 실행되기 전에 충족해야 하는 요구 사항을 지정하고, 사후 조건은 함수 실행 후 예상되는 결과 또는 보장을 정의합니다. 이는 개별 함수의 정확성과 기능을 보장하는 데 도움이 됩니다. ^[1][3]

PSL의 시나리오 기반 속성은 제한된 환경 또는 특정 조건에서 정의되고 가정 및 어설션을 통해 다른 규칙으로 구현됩니다. 가정은 컨트랙트의 상태 또는 충족해야 하는 조건과 관련이 있는 반면, 어설션은 컨트랙트 내의 특정 조건 또는 동작을 확인합니다. PSL은 구문 및 구조의 대부분을 Solidity와 공유하므로 컨트랙트 사양을 쉽게 작성하고 복잡한 논리 바인딩을 피할 수 있습니다. 이 단순성은 사양 작성 및 유지 관리의 용이성을 향상시킵니다. ^[1][3]

PSL 사양은 재사용 및 업그레이드가 가능합니다. PSL은 상속 및 모듈화 관리가 가능한 Solidity의 사용자 정의 변형이기 때문입니다. 이를 통해 다른 컨트랙트 사양을 포함하여 재사용 및 확장이 용이합니다. 또한 PSL 사양은 컨트랙트 코드에서 직접 자동화할 수 있으므로 사양 품질을 보장하고 오류 및 불일치 가능성을 줄일 수 있습니다. ^[1][3]

공식 증명기

PropertyGPT의 공식 증명기는 스마트 컨트랙트에 대해 생성된 속성의 정확성을 검증하도록 설계된 구성 요소입니다. 공식 검증 기술을 사용하여 속성 및 컨트랙트 코드를 엄격하게 분석하여 가능한 모든 실행 시나리오에서 정확성을 보장합니다. 여기에는 시스템이 지정된 속성 또는 사양을 충족하는지 확인하기 위해 논리적 추론 및 수학적 방법을 적용하는 것이 포함됩니다. ^[1]

PropertyGPT에서 공식 증명기는 컨트랙트 코드와 PSL(Property Specification Language)에 지정된 속성을 검사합니다. 제어 흐름, 데이터 흐름 및 상태 전환을 분석하여 속성이 충족되는지 확인합니다. 증명기는 모델 검사, 정리 증명 또는 기호 실행을 사용합니다. 모델 검사는 모든 시스템 상태 및 전환을 탐색하고, 정리 증명은 수학적 논리를 사용하여 속성을 설정하고, 기호 실행은 속성을 확인하기 위해 가능한 모든 입력 및 경로를 고려합니다. ^[1]

검증 중에 증명기는 속성이 위반되는 반례 또는 시나리오를 식별하여 개발자가 이러한 위반으로 이어지는 특정 조건을 이해하고 컨트랙트 코드의 잠재적 취약점을 해결할 수 있도록 지원합니다. 잠재적인 문제 및 불일치를 식별함으로써 공식 증명기는 스마트 컨트랙트의 보안 및 신뢰성을 향상시켜 의도한 대로 작동하고 악용 또는 실패 위험을 줄입니다. 공식 증명기에서 사용되는 특정 기술 및 알고리즘은 컨트랙트 코드의 복잡성, 검증되는 속성 및 원하는 보증 수준에 따라 다릅니다. ^[1]

가중 알고리즘

PropertyGPT의 가중 알고리즘은 관련성 및 중요도에 따라 생성된 속성에 가중치를 할당합니다. 이 프로세스는 반복적인 접근 방식을 사용하여 제목 코드에 대한 후보 속성 집합을 생성하는 것으로 시작됩니다. 그런 다음 각 후보 속성은 제목 코드와의 유사성을 분석하고 코드의 컨텍스트와 목적을 고려하여 관련성을 평가합니다. ^[1][2]

이어서 복잡성, 중요도 및 영향과 같은 요소를 기반으로 각 후보 속성의 중요도를 평가합니다. 이러한 관련성 및 중요도 평가를 기반으로 각 후보 속성에 가중치가 할당됩니다. 후보 속성은 할당된 가중치에 따라 순위가 매겨지며, 가중치가 높을수록 우선 순위가 높음을 나타냅니다. ^[1][2]

이 알고리즘을 통해 사용자 피드백 또는 도메인별 지식을 기반으로 가중치 및 순위를 반복적으로 개선할 수 있습니다. 이 방법을 사용하면 속성 생성에 대한 목표적이고 효율적인 접근 방식을 보장하여 테스트 및 검증에 가장 관련성이 높고 중요한 속성의 우선 순위를 지정합니다. 유사성의 여러 차원을 고려하고 그에 따라 가중치를 할당함으로써 알고리즘은 중요한 동작을 캡처하고 정확성을 보장하며 공식 검증의 효율성을 향상시킵니다. ^[1][2]