Neuroforger: LLM을 통한 스마트 컨트랙트 검증용 인증된 위반 증거 생성

최근의 대규모 언어 모델 (LLMs)은 스마트 컨트랙트가 특정 속성을 준수하는지 예측하는 데 뛰어난 성능을 발휘하는 추론 능력을 통합하고 있으며, 이는 스마트 컨트랙트 검증 (smart contract verification)을 위한 전통적인 형식 방법론 (formal-methods) 기반 기술에 대한 상호 보완적인 접근 방식을 시사합니다. 그러나 이러한 맥락에서 LLM의 적용에는 두 가지 주요한 문제가 있습니다: 1) 자연어로 표현된 속성은 본질적으로 모호하며, 2) LLM이 반환하는 답변은 정확성이 보장되지 않습니다. 본 논문에서는 다음을 통해 두 문제를 동시에 해결합니다: 1) 추상 타입 (abstract types)을 통해 Solidity를 확장하는 새로운 형식 명세 언어 (formal specification language)를 도입하고, 2) LLM을 타입 체크 (type checking) 및 구체적 실행 (concrete execution)과 결합하여 위반 증거 (violation witnesses, 즉 반례)를 생성하고 검증하는 워크플로우를 설계합니다. 핵심 아이디어는 명세를 추상 타입의 (존재 양화된) 변수를 가진 Solidity 테스트로 표현하는 것입니다. 이러한 변수들을 (올바른 타입의) 구체적인 값으로 인스턴스화하는 것은 해당 테스트를 대상 속성에 대한 실행 가능한 반례 (PoC)로 구체화합니다. 우리는 이 절차를 Neuroforger라는 도구로 구현하였으며, 문헌에서 추출한 스마트 컨트랙트 검증 데이터셋을 통해 실험적으로 평가하여 실제 환경에서의 잠재적 적용 가능성을 보여주는 유망한 결과를 얻었습니다.