2.1 ATL 모델 체킹 문제

그림. 1. ATL formula의 semantics

Fig. 1. The semantics of ATL formula

ATL(Alternating-time Temporal Logic) 모델 체킹은 정형 검증(formal verification) 기법 중에 하나로서, 주어진 모델이 사용자가 검증하고자하는 property를 만족하는지를 자동적으로 검증하는 기술이다. ATL 모델체킹에서는 검증하고자 하는 시스템은 game structure^(8,15)로 나타내고, property는 ATL formula⁽⁸⁾로 나타낸다. 이 절에서는 ATL 모델 체킹 문제에 대해 자세히 설명한다. 이 문제 정의는 ATL과 game structure에 대한 정의를 필요로 하기 때문에 ATL의 정의부터 설명하기로 한다.

ATL의 syntax는 아래와 같다. 여기서, Π는 atomic proposition들의 집합이며, Σ는 player들의 집합이다.

(1) 모든 atomic proposition p∈Π는 ATL formula이다.

(2) φ1과 φ2가 ATL formula이면, ¬φ1, φ1∨φ2, φ1∧φ2도 역시 ATL formula이다.

(3) A⊆Σ가 player들의 집합이고, φ1과 φ2가 ATL formula이면, ≪A≫Xφ1, ≪A≫Gφ1, ≪A≫Fφ1, ≪A≫φ1Uφ2도 ATL formula이다.

ATL 모델 체킹에서 검증 대상 모델을 표현하는 game structure는 다음과 같이 S=(k, Q, Π, π, d, δ)로 나타낼 수 있다.

∙ k는 player의 개수이다. 그리고, 각각의 player들은 해당 숫자로 나타내며, player들의 집합인 Σ는 {1, 2, ..., k}가 된다.

∙ Q는 state들의 집합이며, intial state들의 집합은 Q0로 나타낸다.

∙ Π는 atomic proposition들의 집합이다.

∙ π: Q→2Π는 labeling 함수로서, 각각의 state q∈Q에서 true인 atomic proposition들의 집합 π(q)⊆2Π을 나타낸다.

∙ 각 player a∈{1, 2, ..., k}와 state q∈Q에 대해서, 자연수 da(q)≥1는 해당 player a가 state q에서 가능한 move의 개수를 의미한다.

∙ 각 state q∈Q와 move 벡터 (m1, m2, ..., mk)에 대해서, δ(q, m1, m2, ..., mk)는 각각의 player a들이 state q에서 move ma를 선택했을 때의 다음 state를 나타내며, 이러한 함수 δ를 transition function이라고 한다.

그림 1은 game structure에 기반한 ATL formula의 semantics를 정의한다. Game structure S=(k, Q, Π, π, d, δ)와 state q∈Q, ATL formula φ가 주어졌을 때, 만약 game structure S의 state q에서 ATL formula φ를 만족하는 경우, S, q ⊧φ라고 한다. 그리고, S가 명백한 경우, q ⊧φ로 표시할 수 있다. 그리고, S의 모든 initial state q0∈Q0에 대해서, q0 ⊧φ인 경우, S ⊧φ라고 한다. 최종적으로, Game structure S=(k, Q, Π, π, d, δ)와 ATL formula φ가 주어졌을 때, 주어진 S와 φ에 대해서 S ⊧φ인지를 검사하는 문제가 ATL 모델 체킹 문제이다.

2.2 ATL 모델 체킹 예제

그림 2는 본 논문에서 이용하는 ATL 모델 체킹 기법을 설명하기 위한 예제를 보여주고 있다. 이 예제에서는 두 개의 프로세스 px와 py가 존재한다. 프로세스 px는 Boolean 변수 x를 컨트롤하며, 프로세스 py는 Boolean 변수 y를 컨트롤한다. 즉, x의 값이 false인 경우, px는 (1) x의 값을 그대로 유지하거나 (2) true로 변경할 수 있다. 하지만, x가 true인 경우에는 px가 x의 값을 변경할 수는 없고 true로 유지할 수밖에 없다. 비슷하게, y의 값이 false인 경우, py는 (1) y의 값을 그대로 유지하거나 (2) true로 변경할 수 있다. 하지만, y가 true인 경우에는 py가 y의 값을 변경할 수는 없고 true로 유지할 수밖에 없다.

그림. 2. ATL 모델 체킹 예제

Fig. 2. ATL model checking example

이 예제에서 ≪px≫F (x=true)라는 ATL formula를 생각해 보자. 이 ATL formula는 “px는 다른 player들이 어떤 수를 쓰더라도, 변수의 x의 값을 미래 어느 순간에는 true로 만들 수 있다”라는 property를 의미한다. 이 ATL formula는 intial state인 q0에서 만족한다. 왜냐하면, state q0에서 프로세스 px가 변수 x의 값을 true로 변경하는 move를 선택하기만 하면, 프로세스 py가 어떤 move를 선택하건 간에 x의 값은 true가 되기 때문이다. 반면에 ≪py≫X (x=y)라는 ATL formula는 initial state q0에서 만족하지 않는다. (참고로 이 formula는 “py는 다른 player들이 어떤 수를 선택하더라도, 모든 next state에서 x와 y의 값을 같게 만들 수 있다”라는 property를 의미한다.) 왜냐하면, state q0에서 (1) py가 y의 값을 유지하는 경우는 px가 x의 값을 true로 만들어서 x≠y를 만들 수 있고, (2) py가 y의 값을 변경하는 경우에는 px가 x의 값을 false로 유지할 수 있어서 x≠y를 만들 수 있기 때문이다. 즉, 위의 예제를 나타내는 game structure를 S라고 할 때, S⊨≪px≫F (x=true)이지만, S⊭≪py≫X (x=y)이다.

3.1 Solidity 언어

Solidity⁽⁹⁾는 이더리움 블록체인 시스템에서 사용할 수 있는 스마트 컨트랙트를 개발하기 위한 객체 지향 언어이다. 그림 4는 userWallet이라는 간단한 스마트 컨트랙트의 일부를 예제로서 보여주고 있다. userWallet 스마트 컨트랙트는 2개의 변수 (owner, myBalance)와 3개의 함수(constructor 함수, 이름을 갖지 않는 fallback 함수, withdrawTotalBalance 함수)를 포함하고 있다. 이번 장에서는 본 연구에서 제안하는 변환 방법을 3가지 기준(프로그램 구조, control flow, 메모리 연산)에 따라서 설명한다.

그림. 4. userWallet 스마트 컨트랙트

Fig. 4. The userWallet smart contract

3.2 프로그램 구조에 대한 변환

Solidity 프로그램은 한 개 이상의 이더리움 스마트 컨트랙트를 구현할 수 있으며, 각각의 컨트랙트는 변수 선언, 매핑 선언, 이벤트 정의, 함수들로 구성된다. 반면에 MCMAS 언어는 game structure의 player들을 나타내는 agent들의 집합으로 구성된다. 따라서, 하나의 Solidity 컨트랙트를 하나의 MCMAS agent로 변환한다.

Solidity 컨트랙트의 각 부분들(변수 선언, 매핑 선언, 이벤트 정의, 함수)은 아래와 같은 방식으로 변환한다. 본 연구에서 허용하는 Solidity 변수 타입들은 Boolean, integer, address, array, enum, structure이다. 이것들은 Solidity 변수 타입의 전체는 아니지만, 거의 대부분을 포함하며 대부분의 스마트 컨트랙트를 검증할 수 있는 정도로 충분한 정도이다. MCMAS의 검증 수행 시간은 상태 공간(state space)의 크기에 영향을 받기 때문에, 본 연구에서는 integer와 address의 경우 적절한 abstraction을 통해서, MCMAS의 bounded integer로 변환한다. 또한, array와 structure의 경우는 MCMAS 언어에서 해당 타입을 제공하지 않기 때문에, 이러한 타입의 변수는 flatten하여 여러 개의 변수를 이용하여 변환한다.

Solidity 언어의 경우, state 변수, local 변수, global 변수를 제공하는데, MCMAS의 경우는 이러한 종류의 구분을 제공하지 않는다. 그래서, 같은 이름을 갖는 state 변수와 local 변수가 overwrite되는 것을 방지하기 위해서, local 변수에 함수 이름을 접두사로 붙여 준다. 또한, Solidity 소스 파일에 나오는 global 변수에 대해서는 같은 이름의 MCMAS 변수를 생성한다. 예를 들어, userWallet 컨트랙트의 경우, 현재 트랜잭션 호출 체인의 최초 호출자(caller)를 나타내는 tx.origin이라는 global 변수를 사용하고 있는데, 이에 대응하는 MCMAS 변수 tx_origin을 생성한다.

Array 변수와 비슷하게, 매핑의 경우도 MCMAS에서 제공하지 않기 때문에 여러 개의 변수를 이용하여 flatten하여 나타낸다.

Solidity 언어와 MCMAS 언어의 가장 중요한 차이점 중 하나가 실행 방식이다. Solidity 언어의 경우는 일반 프로그래밍 언어와 같이, 각 statement들이 순차적으로 실행되는 반면에, MCMAS 언어는 game structure의 evolution 함수를 나타내기 때문에 agent의 실행을 나타내는 evolution 함수의 각 라인들이 조건에 맞기만 하면 동시에 실행될 수 있다. 이러한 evolution 함수는 guided condition과 assignment들로 이루어지는 라인들의 집합으로 구성되며, 각 라인의 guided condition이 만족하는 경우, 그 라인에 있는 assignment들이 수행된다. 결국, Solidity의 순차적 실행을 MCMAS의 evolution 함수로 모사하기 위해서, Solidity 컨트랙트가 현재 어느 라인을 수행 중인지를 나타내는 보조적 변수로서 pc(program counter)를 추가한다.

Solidity의 constructor 함수는 Solidity 컨트랙트가 생성될 때 자동적으로 실행되는 함수이므로, 이 함수의 statement들은 MCMAS의 initial states 섹션의 수식으로 인코딩된다. 또한, MCMAS에서는 함수 호출이 지원되지 않기 때문에, Solidity의 함수 호출을 MCMAS에서 모사하기 위해서 call stack을 나타내는 보조 변수들을 추가한다.

3.3 Control Flow에 대한 변환

Solidity 프로그램의 실행은 일반적인 프로그래밍 언어와 동일하게 순차적으로 실행되기 때문에, MCMAS 언어에서는 pc(program counter)의 값을 1씩 증가시키는 방법으로 모사할 수 있다.

하지만, 순차적 실행의 몇 가지 예외로써, 함수 호출, 조건 분기, 반복문, require, assert등이 있다. 그 중에 함수 호출의 경우는, 현재 pc의 값을 call stack 변수들에 저장하고, 호출된 함수의 시작 line을 pc 값으로 설정해 줌으로서 모사하게 된다. 또한, 호출된 함수가 return해서 caller로 돌아오는 경우에는 call stack 변수들에 저장되어 있는 주소 값을 pc로 복원함으로서 함수 리턴을 정확하게 모사할 수 있다.

If와 같은 조건 분기문의 경우는, MCMAS의 implication 연산을 통해서 변환한다. 즉, if의 guided condition이 true로 계산될 때는 then 블록의 시작 주소를 pc에 할당하고, false로 계산될 때는 else 블록의 시작 주소를 pc에 할당한다. 또한, then 블록이 끝났을 때는 if 전체 블록이 완전히 끝나는 주소를 pc에 할당한다. 반복문(for, while, do..while)의 경우도 비슷한 방식으로 변환한다. 즉, 주어진 Solidity 반복 statement와 동일하게 초기화, 종료 조건, 증감식을 MCMAS의 문법에 맞도록 번역하여 변환한다.

Solidity 프로그램에서는 주어진 조건이 만족하지 않는 경우 프로그램의 실행을 강제로 종료하는 require와 assert 문장이 있다. 하지만, MCMAS 언어에서는 이와 같은 명령문이 없기 때문에, 주어진 조건이 만족하지 않는 경우, pc의 값을 해당 함수의 가장 마지막 라인으로 할당하는 방법으로 모사한다.

3.4 메모리 연산에 대한 변환

메모리 연산에는 assignment와 산술 연산이 포함된다. 이러한 Solidity 메모리 연산의 경우는 몇 가지 syntactic sugar들을 제외하고는 MCMAS 언어에 동일한 의미의 연산이 있어서 그대로 이용할 수 있다. 하지만, MCMAS 언어에서 제공하지 않는 syntactic sugar들의 경우는 같은 의미의 기본 연산으로 변환 후에 MCMAS 언어로 변환한다. 예를 들어, x += y의 경우는, MCMAS 언어에서 += 연산을 제공하지 않기 때문에, 일단 x = x + y로 변환하고 그 문장을 MCMAS 언어로 옮긴다.

3.5 변환 예제

그림 5는 3.1절과 그림 4에서 설명한 userWallet 스마트 컨트랙트를 본 논문에서 제안하는 방법을 통해서 MCMAS 언어로 변환한 것이다. 즉, Solidity userWallet contract는 MCMAS 언어에서 같은 이름의 agent로 변환되었다. 참고로 MCMAS 언어에서는 --로 시작되는 줄은 프로그래머를 위한 주석(comment)이다.

변환된 userWallet agent는 변수 선언 섹션으로부터 시작된다. 처음 나오는 변수 pc와 returnAddr (line 3~4)는 Solidity 언어의 순차 실행과 함수 호출을 모사하기 위한 것이며, 이 변수들의 범위인 0..18은 Solidity 소스 파일의 라인 수에서 비롯된다. 그 이후에는 Solidity 소스 파일에 나오는 state, local, global 변수들과 대응하는 MCMAS 변수의 선언들(line 5~13)이 나온다.

Actions 선언과 Protocol 섹션(line 15~21)은 함수의 호출과 리턴을 MCMAS 언어로 모사하기 위한 것들이다. 즉, Actions 선언의 경우는 현재 컨트랙트가 어떤 함수들을 호출할 수 있고, 현재 컨트랙트의 어떤 함수들이 리턴을 할 수 있는지를 선언한다. 또한, Protocols 섹션은 Solidity 컨트랙트의 몇 번째 라인에서 해당 액션(함수 호출과 리턴)들이 발행할 수 있는지를 명시한다.

그림. 5. 변환된 MCMAS 입력

Fig. 5. MCMAS input translated

Solidity 소스 파일에 나오는 함수들(constructor 함수 제외)은 MCMAS 파일의 Evolution 섹션으로 변환된다. constructor 함수의 경우는 InitStates 섹션의 assignment들로 변환한다. 이 예제의 fallback 함수(그림 4의 line 10~11)는 아무런 statement를 포함하고 있지 않기 때문에, MCMAS 파일에서도 단순히 pc 값을 1씩 증가시키는 라인으로만 변환된다(그림 5의 line 24~25). Solidity 파일의 if 문의 조건식은 MCMAS 파일의 2개 라인으로 변환되었다(line 29~30). 즉, (tx_origin = owner)가 true로 계산될 때는 pc의 값을 1만큼 증가시키고, false로 계산될 때는 pc의 값을 17로 이동하였다. 그림 4의 userWallet 컨트랙트의 15번째 라인의 함수 호출의 경우는 MCMAS 변수 returnAddr에 현재 pc 값을 저장하고(line 31), call_transfer 액션을 발생시킴으로서(line 18) 모사하였다. 또한, 해당 함수에서 다시 userWallet 컨트랙트로 돌아오는 것은 저장된 returnAddr보다 1만큼 큰 값을 다시 pc 값으로 회복함으로서 모사하였다(line 32).

본 논문에서 제안하는 변환 방법은 보조적 agent로 Environment를 추가한다. 이러한 Environment agent는 userWallet agent와 또 다른 사용자 agent들 간의 turn을 조정하는 역할을 한다. 따라서, userWallet agent의 Evolution 섹션에 있는 각각의 라인들은 Environment.turn이 T_userWallet일 때만 활성화되어 실행된다. Abdellatif의 연구⁽¹⁴⁾는 본 연구와 비슷하게 스마트 컨트랙트들과 그들 간의 실행 environment들을 모델링하여 검증하는 방법을 제안하였다. 하지만, 그 연구에서는 이러한 모델에 통계적 모델 체킹 기법을 적용하였기 때문에, 본 논문에서 제안하는 게임 기반 ATL property들에 대한 모델 체킹은 적용할 수가 없다는 단점이 있다.

4.1 DAO 공격

DAO(Digital decentralized Autonomous Organization)는 탈중앙화된 디지털 자율 조직 관점의 투자자 중심의 벤처 캐피탈이다⁽³⁾. 이러한 DAO 컨트랙트는 2016년 이더리움에 공개되었고,

그림. 6. DAO attack 소스 코드

Fig. 6. DAO attack source code

20여 일 동안 투자자들로부터 약 1억 달러 가치의 이더를 모집하였다. 하지만, DAO 컨트랙트 소스 코드에 포함된 재진입 오류로 인해 360만개의 이더(약 5000만 달러)의 손실을 입었고, 이 사건으로 인해 이더리움은 이더리움과 이더리움 클래식으로 나뉘게 되었다. 그림 6은 DAO 컨트랙트의 재진입 오류를 보여주는 소스 코드이다. 그 중 그림 6(a)는 이러한 재진입 오류를 가지고 있는 요약된 DAO 컨트랙트이고, 그림 6(b)는 이러한 오류를 공격할 수 있는 attacker 컨트랙트이다.

이 오류에 대한 공격은 공격자가 DAOattack 컨트랙트의 startAttack 함수를 호출하면서 시작된다. 공격자는 일단 10 wei를 DAO 펀드에 있는 자신의 account에 입금하고, 바로 전액 인출을 시도한다(line 27~29). 이 공격자가 DAOfund의 withdrawTotalBalance 함수를 호출하면, DAOfund 컨트랙트는 caller의 잔액을 확인하고, 그 잔액만큼을 돌려주기 위해서 msg.sender.call.value(total Balance)라는 명령문을 실행시킨다(line 11). Solidity 언어에서의 위 명령문은 caller인 DAOattack의 fallback 함수를 호출하게 된다. 이 때, DAOattack 컨트랙트의 fallback 함수는 해당 금액에 대한 인출 처리를 수행하지 않고, 악의적으로 전액 인출을 요구하는 withdrawTotalBalance 함수를 또다시 호출하게 된다(line 34). DAOfund 컨트랙트는 아직 공격자의 잔액을 0으로 수정하지 않았기 때문에, 또 다시 10 wei를 인출해 주는 fallback 함수를 호출하게 되고(line 11), 이러한 인출은 DAOfund가 보유하고 있는 이더가 모두 소진될 때까지 계속적으로 반복된다.

이 예제의 검증을 위해, 위 두 개의 컨트랙트를 3장에서 설명한 방법을 이용하여 MCMAS 언어로 변환하였다. 또한, DAOfund 컨트랙트와 DAOattack 컨트랙트의 turn을 조절하는 Environment agent도 추가하였다. 그 후, 위에서 설명한 공격 시나리오가 실제로 가능한지를 검증하기 위해서, 아래의 ATL formula를 검증에 이용하였다.

≪DAOattack≫ F (DAOattack.totalAmount > DAOattack.currentBalance)

이 ATL formula는 “DAOattack agent가 다른 agent들이 어떤 방법을 쓰더라도, 자신이 소유한 잔액보다 더 많은 금액을 인출할 수 있는지”를 의미한다. MCMAS를 이용한 ATL 모델 체킹 결과, 위의 property는 true임을 확인하였고, 위에서 설명한 것과 같은 witness도 확인하였다.

이러한 재진입 오류를 막는 방법은 여러 가지가 있는데, 그 중 하나는 DAOfund의 withdrawTotalBalance 함수에서 caller에게 잔액을 인출해주는 fallback 함수를 호출하기 전에 caller의 잔액을 0으로 수정하는 것이다. 이렇게 되면, 설령 공격자가 fallback 함수에서 withdrawTotalBalance 함수를 재호출하더라도, 이미 잔액이 0으로 되어 있기 때문에 DAOfund 컨트랙트가 또다시 잔액을 인출해주지 않는다.

이러한 오류 수정이 위에서 설명한 DAO attack을 실제로 방어할 수 있는지를 확인하기 위해서, line 14에 있는 대입문과 line 11~13에 있는 if문의 순서를 바꾼 후, 첫 번째 실험의 과정을 다시 수행하였다. 두 번째 실험의 결과는 MCMAS 툴이 false를 리턴하였고, 그 의미는 “DAOattack agent가 다른 agent들이 어떤 방법을 쓰더라도 자신이 소유한 잔액보다 더 많은 금액을 인출할 수 있지는 않다”라는 것으로, DAOfund의 재진입 오류를 수정한 버전의 컨트랙트는 해당 오류가 없음을 증명한 것이라고 할 수 있다.

4.2 tx.origin 공격

Solidity 언어에서는 전체 블록체인이나 현재 트랜잭션의 정보를 컨트랙트에게 제공해 주기 위해서 특별한 의미를 갖는 global 변수들을 제공한다. 참고로, 일반적인 프로그래밍 언어에서의 global 변수의 역할은 Solidity 언어의 state 변수가 대신한다. 이러한 Solidity global 변수 중에는 비슷하지만 매우 다른 의미를 갖기 변수들이 종종 있기 때문에, 사용에 매우 주의해야만 한다. 예를 들어, 연속적인 함수 호출 체인에 대해서, msg.sender는 이 함수 호출 체인의 가장 최근 호출자 컨트랙트의 address를 의미하는 반면에 tx.origin은 가장 처음에 이 호출 체인을 시작한 컨트랙트의 address를 의미한다.

그림. 7. userWallet에 대한 공격자 컨트랙트

Fig. 7. An attacker contract for userWallet contract

tx.origin 공격⁽¹¹⁾은 이러한 Solidity global 변수 tx.origin을 잘못 사용한 점에서 기인한다. 3장의 그림 4는 tx.origin 오류를 포함하고 있는 간단한 예제이다. 이 예제에 있는 userWallet 컨트랙트의 withdrawTotalBalance 함수의 원래 의도는 이 함수가 불렸을 때, 함수 호출자가 지갑의 소유주라면 잔고 전액을 호출자에게 송금하려고 하는 함수이다. 하지만, 원래 의도와는 다르게 msg.sender를 사용해야 하는 곳에 tx.orgin을 사용함으로서 공격자에게 취약점이 노출되었다. 그림 7은 userWallet 컨트랙트의 이러한 취약점을 공격할 수 있는 간단한 attacker 컨트랙트이다. 일단, 이 공격자는 속기 쉬운 유인책(예: 높은 이자율 보장) 등을 이용해서 userWallet 컨트랙트의 소유자가 소액이라도 attacker에게로의 송금하도록 하여 attacker의 fallback 함수를 호출하게끔 한다. 그 후에 attacker는 자신의 fallback 함수에서 바로 userWallet 컨트랙트의 withdrawTotalBalance 함수를 호출하게 된다(line 11). 이 경우, userWallet 컨트랙트 withdrawTotalBalance 함수에서는 tx.origin이 owner인지를 확인하게 된다(그림 4의 line 14). tx.origin은 함수 호출 체인에서 가장 먼저 시작한 객체의 주소를 의미함으로 지갑의 원래 주인인 owner의 주소와 동일하게 되고, userWallet 컨트랙트는 잔고 전체를 attacker에게 송금하게 된다.

이 예제에 대한 ATL 모델 체킹 수행하기 위해서, 일단 userWallet 컨트랙트와 attacker 컨트랙트를 3장에서 제안한 변환법을 이용하여 MCMAS 언어로 변환하였다. 특히, userWallet 컨트랙트에 대한 변환은 그림 5에 나와 있다. 또한, 이 두 개의 컨트랙트들의 turn을 조절하는 Environment agent도 추가하였다. 그리고, 위에서 설명한 오류의 가능성을 검사하기 위하여 아래의 ATL formula를 검증 property로 이용하였다. 이 formula의 의미는 “userWallet 컨트랙트가 attacker의 fallback 함수를 호출하기만 하면, 다른 agent들이 무슨 수를 쓰더라도 attacker는 userWallet으로부터 balance를 획득할 수 있다”라는 의미이다.

AG ((userWallet.Action = call_fallback) →

≪attacker≫F (attacker.balance > 0))

검증 결과는 예상대도 attacker가 악의적으로 userWallet의 이더를 획득 할 수 있다는 것으로 나왔다. 반면에, 이러한 오류를 막기 위해서는, userWallet 컨트랙트의 원래 의도대로, tx.origin 변수 자리에 함수 호출 체인에서 가장 최근 호출자를 의미하는 msg.sender를 사용하게 되면 해결할 수 있다. 즉, 위에서 설명한 시나리오에서 지갑의 소유자가 속아서 attacker의 fallback 함수를 호출하였더라도, 그리고 그 후에 attacker가 userWallet 컨트랙트의 withdrawTotalBalance 함수를 호출하더라도, msg.sender와 owner가 같은지 확인하는 if문(그림 4의 line 14)에서 두 변수의 값이 다르기 때문에 userWallet 컨트랙트는 잔고를 attacker에게 송금하지 않게 된다. 왜냐하면, msg.sender는 attacker이고, owner는 지갑의 원래 소유자이기 때문이다. 그래서, tx.origin을 msg.sender로 수정한 버전을 가지고 두 번째 실험을 수행하였다. 즉, 수정된 버전의 userWallet 컨트랙트와 attacker 컨트랙트를 MCMAS 언어로 변환하고, Environment agent를 동일하게 추가하여 같은 property를 검사하였다. 그 결과, 수정된 버전의 userWallet 컨트랙트에서는 attacker가 위와 같은 공격을 할 수 없다는 결과를 얻었기 때문에, 수정된 버전은 해당 오류가 없다는 사실이 증명되었다. 단, 이러한 검증 결과가 대상 스마트 컨트랙트에 어떠한 오류도 없음을 뜻하는 것은 아니다. 즉, ATL 모델 체킹을 포함한 모든 정형 검증은 검증 대상의 모든 안전성에 대해서 보장해 주는 것은 아니라, 검증을 수행한 특성(property)가 모든 경우에 만족한다는 것을 보장하는 것이다. 본 논문에서 제안하는 ATL 모델 체킹도 검증 절차를 통과한 경우, 검사한 property에 대한 위험이 없다는 것만을 보장하는 것이다.