LLM 기반 스마트 계약 속성 생성을 통한 형식적 검증

Core Concepts

PropertyGPT는 기존 인간이 작성한 속성을 활용하여 새로운 스마트 계약 코드에 대한 포괄적이고 고품질의 속성을 자동으로 생성할 수 있다.

Abstract

PropertyGPT는 LLM(Large Language Model)의 in-context learning 기능을 활용하여 기존 인간이 작성한 속성을 참조하여 새로운 스마트 계약 코드에 대한 속성을 자동으로 생성한다. 이를 위해 PropertyGPT는 다음과 같은 주요 단계를 거친다:

기존 인간 작성 속성을 벡터 데이터베이스에 임베딩하여 저장한다.
새로운 스마트 계약 코드를 입력받아 벡터 데이터베이스에서 유사한 코드와 속성을 검색한다.
검색된 속성을 참조하여 LLM을 통해 새로운 속성을 생성한다.
생성된 속성이 컴파일 가능하도록 컴파일러 피드백을 활용하여 반복적으로 수정한다.
생성된 속성들을 유사도 기반 가중치 알고리즘으로 순위화하여 상위 K개를 선별한다.
선별된 속성들을 전용 프루버를 통해 형식적으로 검증한다.

PropertyGPT의 실험 결과, 기존 인간 작성 속성 대비 80%의 recall과 64%의 precision을 달성하였다. 또한 PropertyGPT는 37개의 CVE 및 공격 사례 중 26개를 탐지하였고, 4개의 실제 프로젝트에서 12개의 제로데이 취약점을 발견하여 $8,256의 버그 바운티를 받았다.

Stats

기존 인간 작성 속성 623개를 23개 Certora 프로젝트에서 수집하였다.
90개의 속성을 테스트 데이터로 사용하였고, 나머지를 참조 데이터로 활용하였다.
PropertyGPT는 테스트 데이터 90개 중 72개의 속성을 생성하였다.

Quotes

"PropertyGPT는 기존 인간 작성 속성을 활용하여 새로운 스마트 계약 코드에 대한 포괄적이고 고품질의 속성을 자동으로 생성할 수 있다."
"PropertyGPT는 37개의 CVE 및 공격 사례 중 26개를 탐지하였고, 4개의 실제 프로젝트에서 12개의 제로데이 취약점을 발견하였다."

Key Insights Distilled From

PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation

by Ye Liu,Yue X... at arxiv.org 05-07-2024

https://arxiv.org/pdf/2405.02580.pdf

Deeper Inquiries

스마트 계약 속성 생성 및 검증 이외에 PropertyGPT가 활용될 수 있는 다른 영역은 무엇이 있을까?

PropertyGPT는 스마트 계약 속성 생성 및 검증 외에도 다양한 영역에서 활용될 수 있습니다. 예를 들어, 보안 취약점 탐지, 코드 품질 평가, 자동화된 코드 리뷰, 소프트웨어 테스트 자동화 등의 소프트웨어 개발 및 보안 관련 작업에 적용할 수 있습니다. 또한, PropertyGPT의 속성 생성 및 검증 기능을 활용하여 블록체인 기반의 다른 응용 프로그램이나 분산 시스템에서도 활용할 수 있습니다.

스마트 계약 속성 생성 및 검증 이외에 PropertyGPT가 활용될 수 있는 다른 영역은 무엇이 있을까?

PropertyGPT가 생성한 속성과 인간이 작성한 속성의 주요 차이점은 주로 다음과 같습니다. PropertyGPT가 생성한 속성은 자동화된 과정을 통해 생성되며, 인간이 작성한 속성에 비해 일관성과 효율성 측면에서 우수할 수 있습니다. 그러나 PropertyGPT가 생성한 속성은 도메인 전문 지식이나 상황적인 이해를 반영하기 어려울 수 있으며, 특정한 케이스나 예외 상황을 고려하지 못할 수도 있습니다.

PropertyGPT의 성능을 더욱 향상시키기 위해서는 어떤 방향으로 연구를 진행해야 할까?

PropertyGPT의 성능을 더욱 향상시키기 위해서는 다음과 같은 방향으로 연구를 진행할 수 있습니다.

더 다양한 속성 생성: PropertyGPT가 생성하는 속성의 다양성을 높이고, 더 많은 유형의 속성을 자동으로 생성할 수 있도록 개선하는 연구를 진행해야 합니다.
더 정확한 검증: 생성된 속성의 검증 과정을 더욱 정교하게 개선하여 보다 정확한 결과를 도출할 수 있도록 연구를 진행해야 합니다.
실제 환경 적용: PropertyGPT의 성능을 실제 환경에서 검증하고, 실제 시나리오에 적용하여 효과적인 결과를 얻을 수 있도록 연구를 진행해야 합니다.