Move Prover란 무엇인가?

Move Prover Architecture

Boom Labs는 Web 3 개발자들을 온보딩시키고, 생태계를 활성화시키기 위해 교육을 비롯한 여러 활동들을 하고 있습니다. 저희 비전에 공감하여 동참하고자 하는 분들은 Boom Labs의 문을 두드려주세요!

Disclaimer: 이 글은 정보 전달을 위한 목적으로 작성되었으며, 특정 프로젝트에 대한 투자 권고, 법률적 자문 등 목적으로 하지 않습니다. 모든 투자의 책임은 개인에게 있으며, 이로 발생된 결과에 대해 어떤 부분에서도 Boom Labs는 책임을 지지 않습니다. 본문이 포괄하는 내용들은 특정 자산에 대한 투자를 추천하는 것이 아니며, 언제나 본문의 내용만을 통한 의사결정은 지양하시길 바랍니다.

이 글을 쓰게 된 계기는 최근 회사(Baekdu Technologies)에서 Move Prover 및 Sui와 관련된 일을 맡아 하게되었고, Move lang 및 Move prover에 언어적 매력을 느끼게 되어 이를 알리고자 작성하게 되었습니다.

이 글은 Move Prover 논문을 읽고, 일부 개인적인 견해를 덧붙여 번역 정리한 글입니다. 이 글을 읽고 흥미를 갖게된 분이 있다면, 최하단 참고 문헌의 논문들을 읽으시길 바랍니다. 이 글의 이해를 위해 컴퓨터 언어의 구조나, 컴퓨터 언어가 기계어로 번역되는 과정에 대한 기본적인 이해가 있으면 좋습니다. 또한 Move가 Rust에게 영향을 받아 만들어진 언어이다 보니, Rust 언어에 대한 기본 지식이 있으면 좋습니다.

Introduction — Move Prover의 기능과 의의

Move Prover(MVP)는 compiler, linter, type checker 등과 같은 개발 툴과 (속도 차원에서) 비슷한 개발자 경험을 주면서도 빠르게 로직을 검증할 수 있는 도구입니다. 이는 편의성 차원에서 중요한데요.
기존에 테스트넷에 배포하여 로직을 검사하거나, 로컬에 네트워크를 구성하여 검사하던 많은 오류를 정적 테스트를 통해 잡아낼 수 있습니다. 이러한 행위를 가능하게 한 건 본 논문에서 서술할 아키텍처와 더불어서 일반 소프트웨어 대비 스마트 컨트랙트의 차별적 특징 (코드 사이즈가 작고, 잘 알려진 고립된 환경에서 실행되며, 연산은 보통 sequential & deterministic & 환경과의 상호작용은 최소화하여 진행) 때문입니다.

MVP의 속도와 신뢰성에 개선을 가져온 아이디어는 다음과 같습니다:

1. move의 borrow 시맨틱(rust와 유사)에 기반한 alias-free 메모리 모델
2. fine-grained invariant (불변값) 검사. 이는 개발자가 불변값을 명시적으로 일시 중단하는 경우를 제외하고 불변값이 모든 상태를 유지하도록 보장한다.
3. Move의 제네릭 struct, 함수, properties 등의 타입 파라미터를 인스턴스화하는 monomorphization (Rust의 monomorphization과 유사)

Move and Prover

Move와 Prover에 대한 practical한 설명은 Move 튜토리얼, Move prover 예제, Move prover 가이드 및 Move Specification Language 문서로 갈음합니다.

관련해서 기회가 된다면, 추가 글을 통해 서술하도록 하겠습니다.

Move Prover Design

Fig. 1: Move Prover Architecture

Move Prover의 아키텍처는 위 도표에 잘 표현되어 있습니다. 이에 대해 서술하자면 아래와 같습니다.

1. 유저가 Move Code 작성하면,
2. Move Parser가 Specification을 위한 AST를 생성합니다.
   또한 move 실행코드로 구성된 AST도 만들어 compiler에게 넘겨줍니다.
3. Move compiler는 이로부터 실행 바이트코드를 생성합니다.
4. 바이트코드와 Spec AST를 합쳐서 Move Model을 생성합니다.
5. Prover Compiler가 바이트코드 transformation (Reference Elimination, Specification Injection, Mono-morphization)을 수행하여 Boogie intermediate verification Language로 컴파일합니다.
6. Boogie는 SMT(satisfiability modulo theories) solver Z3 통해 verification을 진행합니다.

Reference Elimination

Reference Elimination을 통해 alias-free memory model을 가능케 하고, 이를 통해 시스템의 속도와 reliability를 좋게 만듭니다.

Move의 reference 시스템은 borrow semantics을 베이스로 하는데, 이는 Rust의 그것과 동일합니다. Initial borrow는 global memory (블록체인 네트워크의 전역 메모리) 또는 stack의 지역 변수로 부터 빌려야 합니다.
지역 변수에 대해서는, 불변 참조자 (&x) 또는 가변 참조자 (&mut x)로 참조를 생성할 수 있습니다. Global memories에 대해서는, 참조는 borrow_global 또는 borrow_global_mut 빌트인을 통해 생성될 수 있습니다.
전체 struct에 대해 참조가 주어지면, field는 &mut x.f &x.f를 통해 빌릴 수 있습니다. 벡터에서의 참조도 유사하게, native function인 Vector::borrow(v, i), Vector::borrow_mut(v, i)를 통해 element를 빌릴 수 있습니다.

Borrow checker을 통해 move는 아래 특성을 보장합니다.

• 모든 로케이션에 대해 단 하나의 가변 참조자 또는 n개의 불변 참조가자 있을 수 있습니다. 이는 Rust의 borrow semantics와 유사한데, global memories(Rust에는 없는 개념이기 때문)에 대한 것만 예외입니다. Global memories의 경우엔 acquires annotation을 통해 이 규칙이 강제됩니다.

Fig 2. Account Example Program

• 위의 예시에서, withdraw 함수는 Account global location을 acquires 하므로, withdraw 함수는 Account 을 빌리거나 변경할 수 있는 다른 함수(ex: deposit)를 호출하는 것이 금지됩니다.
• 스택 데이터에 대한 참조의 라이프타임은 스택 로케이션의 라이프타임을 초과할 수 없습니다. 여기에는 함수 내부에서 빌린 global memories도 포함됩니다. global memories에 대한 참조는 함수 전체 또는 일부에서 반환될 수 없습니다.

Immutable Reference

Fig 3. Reference Elimination of Immutable Reference

위와 같이 불변 참조자의 경우, 참조자 타입 및 참조자를 사용하는 연산을 모두 삭제하고, 값으로 대체합니다. Move 실행 프로그램에서는 불변 참조자가 성능 및 소유권의 강제를 위해 copy를 피하는 용도로 중요하지만, specification 에서는 중요치 않습니다.

Mutable Reference

Fig 4. Reference Elimination of Mutable Reference

로케이션 l의 값 변경은 해당 로케이션에 저장된 전체 데이터를 initial borrow하는 것부터 시작합니다. 이 빌림은 참조자 r 을 생성하고, r이 살아있는 동안은, move 코드는 해당 값을 업데이트할 수 있거나 (*r = v), 하위 참조자를 만들 수 있습니다 (r’ = &mut r.f). 그리고 r(과 derived r')이 scope 밖으로 나가면서 mutation은 끝납니다.

borrow checker는 로케이션 l의 데이터에서 mutation이 일어나는 동안에는, 같은 데이터에 대해 다른 참조자가 존재하지 않음을 보장합니다.

이 semantics는 read-update-write 사이클을 통해 가변 참조자를 핸들링할 수 있게 합니다.

• Read: l의 데이터의 복사본을 생성하고,
• Update: 해당 데이터에 대한 일련의 mutation을 시행합니다. 이는 purely functional data updates 로 표현됩니다.
• Write: l의 데이터에 대한 마지막 참조가 스코프 밖으로 벗어나면, 업데이트된 value가 l에 쓰여집니다. 이는 참조가 있는 명령형 프로그램을 alias-free 명령형 프로그램 (global memory나 스택의 변수에 대한 state updates만 존재하는)로 바꿀 수 있게 합니다.

Dynamic Mutable Reference

Fig 5. Exception Case in Dynamic Mutable Reference

위 사례와 같이, 참조 로케이션이 정적으로 확인하기 어려울 수도 있습니다. 이러한 경우를 처리하기 위해서는 논리 인코딩의 추가 정보가 필요합니다.

Fig 6. Reference Elimination of Dynamic Mutable Reference

참조가 스코프를 벗어나면 업데이트된 값을 다시 쓰기 위해 참조가 어느 위치에서 파생되었는지 알아야 합니다. 위 Fig 6.의 코드는 이를 위한 접근 방식을 보여줍니다. 본질적으로, T가 파생된 위치와 T의 값을 모두 추적하기 위해 MVP 내부엔 새로운 유형 Mut가 도입됩니다. Mut는 다음 작업을 지원합니다.

• Mvp::mklocal(value, LOCAL_ID) 는 주어진 local id에 대한 새로운 mutation value를 생성합니다. Local id는 함수의 지역 변수에 대한 고유 식별자입니다.
• Mvp::mkglobal(value, TYPE_ID, addr) 역시 비슷하게 type id와 address를 식별자로 사용하여 global에 대한 새 mutation value를 생성합니다.
• r’ = Mvp::field(r, FIELD_ID) 는 해당 field id를 식별자로 하여 생성된 하위 참조자에 대한 mutation value입니다.
• mutation할 값은 r’ = Mvp::set(r, v)을 통해 치환되며, v = Mvp::get(r) 을 통해 값을 조회할 수 있습니다.
• Mvp::is_local(r, LOCAL_ID) 는 r이 주어진 local id로 derived되었는지 확인할 수 있습니다. Mvp::is_global(r, TYPE_ID, addr) 역시 비슷하게 글로벌 로케이션에 대한 것을 확인할 수 있습니다. Mvp::is_field(r, FIELD_ID) 는 r이 주어진 field id로 derived되었는지 확인할 수 있습니다.

MVP는 data flow analysis를 통해 프로그램으로 부터 borrow graph를 구성하여 transformation을 구현합니다.

Global Invariant Injection

스마트 컨트랙트에서의 정합성은 대부분 블록체인 state의 정합성에 대한 것이므로, move spec에서 global invariant가 중요합니다.

예를 들면, global invariant는 같은 주소에 저장되는 여러 다른 타입이 계정과 동반해야 한다던지, 특정 state의 변경은 특정 account에만 권한이 있다던지 등의 필수 조건을 캡처할 수 있습니다.

대부분의 소프트웨어 검증 도구는 함수의 input에서 invariant를 가정하고, exit에서 증명함으로써 함수가 invariant를 보존한다는 것을 증명합니다. 모듈이나 클래스에서의 invariant 역시 public function에서 invariant가 보존된다는 것을 증명하면 됩니다. 이전 버전의 move prover는 이 방식을 취했습니다.

현재의 prover 버전은 반대의 접근방식을 취하는데, 사용자가 일부 invariants를 일시 중단하도록 명시적으로 지시하지 않는 한, 모든 instruction 뒤에 invariants가 유지되도록 보장합니다. 이 방식에는 성능적 이점이 있는데, 중지되지 않는 한 invaraints들은 그것들을 무효화할 수 있는 instruction이 수행될 때에만 증명하기만 하면 되며, single instruction으로 야기되는 변화는 일반적으로 작기 때문에 증명이 간단하기 때문입니다.

또 다른 장점은, 코드의 거의 모든 곳에 invariant가 존재하기 때문에, abort condition과 같은 다른 속성을 정의할 수 있습니다.

Invariant Types and Proof Methodology

• Inductive(귀납적) invariant는 global memory에서 항상 유지되도록 move module에서 선언된 속성입니다. Move의 borrow semantics에 따르면, inductive invariants는 메모리가 mutate되기 전까지 유지될 필요가 없습니다.
• Update invariant는 이전 state와 현재 state를 연관시키는 속성입니다. 일반적으로 글로벌 메모리를 업데이트 한 후 적용됩니다.

위 두 가지 invariant 모두 메모리 업데이트가 발생되는 시점이 아닌, 메모리를 업데이트하는 함수의 호출 사이트에서 검증됩니다.

invariant가 때때로 모듈의 내부 계산 중에 유지되지 않기 때문에 이 기능은 fine-grained invariant 검사를 필요로 합니다. 예를 들어, 변수가 순차적으로 업데이트될 때 상태 변수 간의 관계가 유지되지 않을 수 있습니다. 외부 호출자가 있는 함수(공용 또는 스크립트 함수)는 invariant가 각 함수의 시작과 끝에 유지되는 것으로 가정되기 때문에 invariant 검증을 중단할 수 없습니다.

Modular Verification

새로운 (untrusted) 모듈이 추가되어도, 이미 입증된 invariant를 해치지 않는 시스템을 추구합니다. 각 invariant에는 move module의 하위 집합 (cluster)가 있습니다. 만약 cluster의 모듈에 의해 invariant가 증명된다면, 그것은 다른 모든 모듈들(증명 당시 정의되지 않은 모듈들에서도)에서도 invariant가 증명될 것을 보장합니다. 클러스터에는 invariant를 무효화할 수 있는 모든 함수가 포함되어야 하며, invariant의 suspension의 경우 해당 함수의 모든 호출자가 포함되어야 합니다. 즉, 클러스터 외부의 함수는 invariant를 무효화할 수 없습니다.

Basic Translation

Fig 7. Basic Global Invariant Injection

위 코드는 inductive invariant (귀납적 불변성) I1의 주입의 예시입니다. function entry 이전에서 assume (가정)하고, state update 이후에 assertion을 합니다. I2는 update invariant로서, 이전 상태와 이후 상태를 연관시킵니다. 이를 위해 상태 스냅샷은 I2_BEFORE에 저장되고, 이는 assertion에 사용됩니다.

접근 및 수정된 메모리에 대해 정적 분석을 통해 Prover가 얻은 정보들을 토대로 global invariant injection은 최적화됩니다.

accessed(f)를 함수가 접근한 메모리라 하고, modified(f)를 변경된 메모리라 하겠습니다. 그리고 accessed(I)를 (이를 호출하는 모든 함수에 전이적으로 포함하는) invariant(불변값)이라 하겠습니다.

• accessed(f)가 accessed(I)와 overlap되면 함수 f의 entry에 assume I를 주입합니다.
• 만약 아래 중 하나가 참이면, assert I를 모든 프로그램 step 뒤에 주입합니다.
  (a) 해당 step이 accessed(I) 안의 메모리 로케이션 M을 변경했을 경우
  (b) 해당 step이 다른 함수 f'을 호출하고, 그로 인해 I가 중지되고, modified(f')가 accessed(I)와 겹치는 경우
• 만약 I가 update invariant인 경우, 업데이트 또는 호출 전에 메모리 스냅샷을 저장한 것을 주입합니다.

Genericity

Fig 8. Global Invariant Injection and Genericity

제네릭 타입은 함수가 Invariant를 수정할 수 있는지 여부를 결정하는 문제를 더 어렵게 만듭니다. 위 코드에서, I1은 특정 타입 S<u64>의 인스턴스에 대해 유지되는 반면, I2는 모든 타입 S<T>의 인스턴스에 대해 유지됩니다.

non-제네릭 함수 f는 S<u8> 인스턴스를 다루기 때문에, specialized 인스턴스인 I2[T = u8] 을 주입해야 합니다. invariant I1은 S<u64>와 overlap되지 않기 때문에, 해당 함수에 적용되지 않습니다.
제네릭 타입을 input으로 받는 g는 u64 타입의 인스턴스를 다룰 수 있기 때문에, I1이 I2 [ T = R]과 주입되어야 합니다.

Monomorphization

Monomorphization은 관련 타입 인스턴스들을 specialize하여 제네릭 타입을 제거하는 변환입니다.

Monomorphization의 목표는 타입을 일급 값으로 지원하는 인코딩에서 제네릭 프로그램이 증명되는 것과, specialized 프로그램이 증명되는 것에서 필요충분조건이 만족함입니다.
SMT 로직에서 다중 정렬 representation을 지원하여 값의 generic representatin의 문제를 방지하기 때문에, specialized 프로그램 (monomorphized)이 더 빨리 검증될 것으로 기대됩니다.

Fig 9. Basic Monomorphization

Monomorphization은 가능한 모든 인스턴스에 대한 제네릭 함수를 검증하기 위해, 타입 매개변수를 삭제하고, 특별한 속성이 없는 새로운 타입에 대해 검증됩니다.

그러나 이 접근 방식은 한 가지 문제가 있는데, 타입이 글로벌 메모리를 인덱싱하는 데에 사용하기 때문에, Move는 전체 타입의 삭제를 허용하지 않는다는 것입니다.

Fig 10. Example Exception Function of Monomorphization

예를 들면 위 함수는 T가 인스턴스화되는 방식에 따라 다르게 동작되는데, T가 u64로 인스턴스화된다면, 함수는 두 번째 move_to에서 항상 중단될 것입니다. 이러한 타입 종속 코드가 존재하는 상황에서 Monomorphization을 가능하게 하는 중요한 속성은 코드에 의해 접근된 메모리 및 주입된 spec을 보고 상황을 식별할 수 있다는 것 입니다. 이로 부터 검증이 필요한 함수의 추가 인스턴스화를 도출할 수도 있습니다.

이러한 검증이 필요한 인스턴스를 계산하는 알고리즘은 다음과 같이 동작합니다.

• 모든 modified(f)의 메모리 M에 대해, modified(f) + accessed(f)의 메모리 M'이 있고, M과 M'이 T1, …, Tn 을 통일할 수 있다면, 결과 치환으로 부터 타입 파라미터 Ti의 인스턴스들을 수집합니다. 이 인스턴스들은 일부 타입 파라미터에 값을 할당하지 않을 수 있으며, 할당되지 않은 변수는 그대로 유지됩니다. 예를 들면, f<T1, T2>는 f<T1, u8>과 같이 부분 인스턴스를 가질 수 있습니다.
• 모든 부분 인스턴스가 계산되면, 인스턴스들을 서로 통합하여 집합을 확장시킵니다. 만약 집합 안에 <T>와 <T'>이 있고, 치환 s에 의해 통일된다면, s<T>도 집합의 일부가 될 것 입니다. 예를 들면, M<T1>과 R<T2>를 수정하고 M<u64>와 R<u8>에 접근하는 f<T1, T2> 에 대해 생각해보면, 이로 부터 <u64, T2>와 <T1, u8>인스턴스가 계산되고, 추가 <u64, u8> 인스턴스가 집합에 추가됩니다.

참고 문헌

• Dill, D., Grieskamp, W., Park, J., Qadeer, S., Xu, M., & Zhong, E. (2022). Fast and reliable formal verification of smart contracts with the Move prover. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (pp. 183–200). Springer, Cham. https://doi.org/10.1007/978-3-030-99524-9_10
• Zhong, J. E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., … & Dill, D. L. (2020, July). The move prover. In International Conference on Computer Aided Verification (pp. 137–150). Springer, Cham. https://doi.org/10.1007/978-3-030-53288-8_7
• Leino, K. R. M. (2008). This is Boogie 2. manuscript KRML, 178(131), 9. http://audentia-gestion.fr/MICROSOFT/krml178.pdf
• Blackshear, S., Dill, D. L., Qadeer, S., Barrett, C. W., Mitchell, J. C., Padon, O., & Zohar, Y. (2020). Resources: A safe language abstraction for money. arXiv preprint arXiv:2004.05106. https://doi.org/10.48550/arXiv.2004.05106