타임드 오토마타를 이용한 스마트 컨트랙트 모델링 = Modeling smart contract by timed automata

국문 초록 (Abstract)

본 연구는 블록체인 기반 플랫폼인 이더리움의 스마트 컨트랙트 모델링에 관한 연구이다.
블록체인의 진보된 형태로써 스마트 컨트랙트가 다양한 형태로 도입이 시도되고 있는 것에 반해, 아직까지는 기술의 개념 증명(Proof of concept)의 단계로써 체계적인 모델링 방법이 제시되지는 못하고 있다. 오히려 스마트 컨트랙트의 기반인 블록체인은 분산 원장(Distributed Ledger) 방식으로 기존의 중앙집중식 시스템과는 완전히 다른 모델임에도 불구하고, 기존의 설계 방식으로 설계되고 있어 문제가 발생하고 있다. 실제로 현재 이더리움에 등록되어 있는 2만여 개의 스마트 컨트랙트 중 45%가 설계상의 문제로 오류 가능성과 취약성을 가지고 있으며, 스마트 컨트랙트의 설계 상의 버그를 이용해 악의적으로 이용될 수 있는 가능성도 여러 연구를 통해 언급되고 있다. 특히 스마트 컨트랙트는 수백만 달러에 상응하는 가상 화폐를 다룰 수 있는데, 이러한 설계 상 취약점은 악의적인 목적을 가진 공격자에게 언제든지 공격 당할 수 있는 충분한 위험 요소를 가지고 있는 것과 같다. 2016년 이더리움 TheDAO에 6천만 달러의 손실을 일으킨 원인으로 밝혀진 재진입 취약성은 이러한 스마트 컨트랙트 설계에 대한 중요성을 보여준 단적인 예라고 할 수 있다. 버그가 발견되면 개선될 수 있는 기존의 분산 네트워크와는 달리, 블록체인 기반인 스마트 컨트랙트는 발생된 결과에 대해 되돌릴 수 없다. 따라서 스마트 컨트랙트를 처음 등록하기 전, 안전한 설계를 하는 것은 매우 중요하다라고 할 수 있다.
스마트 컨트랙트에 대한 모델링 방법의 연구에서는 크게 두 가지 단계가 필요한데, 첫 번째는 적합한 모델링 도구를 선택하는 것이고, 두 번째는 모델링 도구에서 표현할 요소를 도출해내는 방법이다. 본 연구에서는 스마트 컨트랙트가 같은 입력값에 따라 같은 출력값이 결정되는 결정론적 특징을 가지고 있다는 점과, 상태와 상태전환을 포함하는 실시간 시스템의 특성을 가지고 있다는 특징에 착안하여 모델링 도구로써 타임드 오토마타를 제안하였다. 또한, 스마트 컨트랙트의 특징 요소를 타임드 오토마타의 정형 언어와 비교하여 주요 모델링 요소인 상태, 트랜잭션, 상태 전이 함수를 도출하는 프로세스와 함께, 인출(withdraw) 단계의 뮤텍스(mutex) 상태를 도입하는 것을 제안하였다.
이에 대한 사례 연구로 은행 상품 중 하나인 적금을 모델링 하는 프로세스를 수행해봄으로써, 본 연구에서 제안하는 타임드 오토마타를 이용한 모델링 방법이 기존의 다른 모델링 방법에 비해 시간적 제약사항을 정확히 반영할 수 있고, 재진입 취약점 보완을 위한 상태를 도출할 수 있는 것을 확인하였다.
본 연구를 통한 스마트 컨트랙트에 타임드 오토마타를 활용하여 모델링 하는 것은, 표준 UML을 확장한 객체지향 방법론을 활용하는 것에 비해 시간의 흐름에 따른 거래 제약을 표현하기에 적합하며, 재진입 취약성을 도출하여 표현함으로써 보안성을 높일 수 있으며, 정형 언어를 활용함으로써 자동화된 모델 체킹이 용이해지는 효과를 기대할 수 있다.

목차 (Table of Contents)

• 제 1장 서론
• 제 1절 연구의 필요성
• 제 2절 연구의 구성 및 전개
• 제 2장 관련연구
• 제 3장 연구 배경
• 제 1절 타임드 오토마타 (Timed Automata)
• 제 2절 스마트 컨트랙트 (Smart Contract)
• 1. 정의
• 2. 재진입 취약성 (Reentrancy Vulnerability)
• 제 4장 제안 모델링 방법론
• 제 1절 상태 (state)
• 제 2절 뮤텍스 (mutex)
• 제 3절 트랜잭션 (transaction)
• 제 4절 상태 전이 (State Transition)
• 제 5장 사례를 통한 모델링 검증
• 제 1절 모델링 요소 도출
• 1. 상태 및 뮤텍스 도출
• 2. 트랜잭션 도출
• 3. 상태 전이 도출
• 제 2절 모델링 결과 및 분석
• 제 3절 모델링 비교 평가
• 제 6장 결론
• 참고문헌