길현영 교수의 연구실에서 발표한 논문 "Formal Verification of Blockchain Smart Contracts via ATL Model Checking"이 "IEEE Access" 2022년 호에 게재되었다.  

논문 사이트로 이동

이더리움과 같은 최신 블록체인 기술은 스마트 컨트랙트 구현에서 Turing-complete한 프로그래밍 언어를 제공함으로써, 특히 신뢰성이 중요한 금융 분야에 적용되게 하였다. 그러나 스마트 컨트랙트의 사소한 에러들은 금전적으로 막대한 손실을 야기하곤 하는데, DAO 오류, Parity multi-signature 오류, integer underflow/ overflow 오류 등이 그 사례이다. DAO 오류의 경우 5000만 달러 상당의 이더를 도난당하게 하여 이더리움이 이더리움과 이더리움 클래식으로 나뉘게 되는 계기를 만들었다. 이러한 스마트 컨트랙트 상의 오류들을 검출하기 위해 정적 프로그램 분석과 정리 증명기법 기반의 연구들이 진행되어왔으나, 정적 프로그램 분석은 사전에 정의된 패턴의 에러만을 검출할 수 있고, 정리 증명기법 기반 연구는 완전 자동화가 불가능하여 전문가의 참여가 필수적이라는 단점을 갖고 있다. 본 연구는 스마트 트랜잭션의 정확성을 검증하기 위해서, ATL (Alternating-time Temporal Logic) 모델체킹 기법을 이용한다. ATL 모델 체킹이란, 검증 대상인 시스템의 모델과 검증하고자 하는 ATL property가 주어지면, 해당 시스템의 모델이 모든 경우에 주어진 ATL property를 만족하는지를 자동적으로 검증하는 기법이다. ATL 모델체커는 주어진 모델이 property를 만족하는 경우에는 true를 리턴하지만 만족하지 않는 경우에는 counter-example을 알려줌으로써, 개발자가 스마트 컨트랙트의 어느 부분에서 오류가 발생하였는지를 알 수 있게 한다. 

본 연구에서는 주어진 스마트 컨트랙트를 ATL 모델체커로 검증하기 위해서, 이더리움 스마트 컨트랙트에서 주로 사용되는 Solidity 언어를 ATL 모델체커 MCMAS]의 언어로 정확하게 번역할 수 있는 방법론을 제안하고, DAO Attack, TX.ORIGIN Attack, Safe Remote Purchase Contract 등 3가지 사례에 대한 적용을 통해, 본 연구의 방법론이 실제 스마트 컨트랙트 검증에 성공적으로 사용될 수 있음을 보였다. 또한 본 연구실은 블록체인뿐만 아니라 Service composition, Aircraft systems 등 다양한 Software System의 정확성과 안정성에 대한 검증 연구를 해왔고, 최근에는 인공지능 신경망에 대한 검증 연구를 진행 중이다.