Move Prover란 무엇인가?

Move Prover Architecture
Move Prover Architecture

Introduction — Move Prover의 기능과 의의

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

Move and Prover

Move Prover Design

Move Prover Architecture
Fig. 1: Move Prover Architecture
  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

  • 모든 로케이션에 대해 단 하나의 가변 참조자 또는 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에 대한 참조는 함수 전체 또는 일부에서 반환될 수 없습니다.
Fig 3. Reference Elimination of Immutable Reference
Fig 4. Reference Elimination of Mutable Reference
  • Read: l의 데이터의 복사본을 생성하고,
  • Update: 해당 데이터에 대한 일련의 mutation을 시행합니다. 이는 purely functional data updates 로 표현됩니다.
  • Write: l의 데이터에 대한 마지막 참조가 스코프 밖으로 벗어나면, 업데이트된 value가 l에 쓰여집니다. 이는 참조가 있는 명령형 프로그램을 alias-free 명령형 프로그램 (global memory나 스택의 변수에 대한 state updates만 존재하는)로 바꿀 수 있게 합니다.
Fig 5. Exception Case in Dynamic Mutable Reference
Fig 6. Reference Elimination of Dynamic Mutable Reference
  • 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되었는지 확인할 수 있습니다.

Global Invariant Injection

  • Inductive(귀납적) invariant는 global memory에서 항상 유지되도록 move module에서 선언된 속성입니다. Move의 borrow semantics에 따르면, inductive invariants는 메모리가 mutate되기 전까지 유지될 필요가 없습니다.
  • Update invariant는 이전 state와 현재 state를 연관시키는 속성입니다. 일반적으로 글로벌 메모리를 업데이트 한 후 적용됩니다.
Fig 7. Basic Global Invariant Injection
  • 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인 경우, 업데이트 또는 호출 전에 메모리 스냅샷을 저장한 것을 주입합니다.
Fig 8. Global Invariant Injection and Genericity

Monomorphization

Fig 9. Basic Monomorphization
Fig 10. Example Exception Function of Monomorphization
  • 모든 modified(f)의 메모리 M에 대해, modified(f) + accessed(f)의 메모리 M'이 있고, MM'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

--

--

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store