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

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