Quartz 🪬

Analysis of Blockchain Smart Contracts - Techniques and Insights

10 min read

Introduction

Các tác giả tổng hợp 391 bài báo khác nhau có từ khóa “smart contract” ở trong tên hoặc abstract. Sau đó, họ phân tích từng bài báo một cách chặt chẽ và lọc ra được 67 bài liên quan đến smart contract analysis và phân chúng thành ba chủ đề chính: static analysis cho vulnerability detection, static analysis cho program correctness và dynamic analysis. Đối với từng topic, các tác giả lại tạo các phân loại nhỏ hơn và cung cấp các key insights về các thách thức mở và các hướng nghiên cứu trong tương lai.

Blockchain Smart Contracts

Bitcoin là nền tảng của việc phát triển smart contract nhưng nó không hỗ trợ các general-purpose smart contract và nó chỉ lưu lịch sử của các giao dịch ở trong các block. Ethereum được tạo ra để phát triển các general-purpose smart contract.

Ethereum

Etherum là một nền tảng công khai và phân tán dựa trên công nghệ blockchain.

Blockchain của Ethereum sử dụng đồng tiền điện tử Ether và vận hành một hệ thống máy ảo có tên là Ethereum Virtual Machine (EVM).

  • EVM có các instruction mang tính Turing-complete và tường minh hơn Bitcoin’s scripting language.
  • EVM chứa:
    • Một operand stack1 để thực thi các instruction.
    • Một bộ nhớ byte-addressed (mỗi 1 byte ở trong bộ nhớ sẽ có một địa chỉ độc nhất) linh hoạt.
    • Một không gian lưu trữ vĩnh viễn theo dạng key-value có kích thước 32 bytes.
  • Đồng thời, nó hoạt động dựa trên một cơ chế tài nguyên có tên là “gas”.
    • Để thực thi một instruction thì cần phải sử dụng một lượng gas nhất định.
    • Các sender nodes trong mạng lưới gán cho transaction mà có chứa smart contract một gas price nào đó. Gas price này là số tiền mà sender nodes sẵn sàng trả cho miner để thực hiện việc xác thực.
    • Miner sẽ được nhận reward có giá trị là gas price nhân với gas cost cần sử dụng để thực thi smart contract. Ví dụ, nếu gas price của transaction là và gas cost để thực thi smart contract ở trong transaction là thì tổng reward mà miner nhận được sẽ là .

Ethereum có một nhược điểm là khó mở rộng vì mỗi node phải giữ toàn bộ lịch sử các giao dịch.

Solidity

Là một ngôn ngữ contract-oriented và statically-typed lấy cảm hứng từ C++, Python và JavaScript.

Có thể xem các contract trong Solidity như là một class ở trong OOP. Mỗi contract có thể bao gồm những thành phần sau:

  • State variables: là các biến toàn cục và sẽ được lưu vĩnh viễn ở trong bộ nhớ của contract (cũng như là blockchain).
  • Functions: có thể đọc và chỉnh sửa state variable.
  • Events: giúp contract gửi thông báo đến các ứng dụng bên ngoài về sự thay đổi state xảy ra trong contract.
  • Modifiers: giúp đảm bảo một số điều kiện trước khi thực thi hàm.

Library là một contract đặc biệt và được deploy ở một địa chỉ cụ thể. Contract gọi sử dụng thư viện bằng cách gọi hàm deletegatecall2.

EVM Bytecode

EVM sẽ biên dịch các ngôn ngữ lập trình chẳng hạn như Solidity thành bytecode. Bytecode có 114 opcode và biểu diễn logic thực thi dưới dạng stack-based1.

EVM bytecode bao gồm:

  • Creation code: bao gồm dãy các instruction của các constructor. Các instruction này chỉ được thực thi một lần duy nhất khi client tạo contract.
  • Runtime code: là code sẽ được deploy lên blockchain. Nó sẽ có một địa chỉ và bộ nhớ riêng.

Khi một node gọi thực hiện một function bằng cách gửi một transaction có chứa transaction data3 lên mạng lưới, Ethereum sẽ điều hướng program counter đến hàm tương ứng bằng cách kiểm tra xem 4 byte đầu tiên ở trong transaction data4.

Techniques

Tổng quan về các loại smart contract analyzer:

Static Analysis for Vulnerability Detection

🤔 Các kỹ thuật static analysis được dùng để phát hiện lỗ hổng:

  • Symbolic execution
  • Abstract interpretation
  • Machine learning:
    • Long-short term memory
    • Convolution neural network
    • N-gram language model

Các kỹ thuật/công cụ khác:

  • SmartCheck sử dụng kỹ thuật XPath Query 🤔.
  • Servois giúp phát hiện các lỗ hổng liên quan đến concurrency-related vulnerability.
  • SIF là một framework bao gồm một số công cụ analysis chẳng hạn như assertion checker, có mục đích là để phát hiện các arithmetic vulnerability.
  • Slither là một framework giúp phát hiện lỗ hổng cũng như là để visualize code.
  • SmartEmbed: sử dụng kỹ thuật structural code embedding 🤔 giúp chuyển đổi smart contract thành một dạng biểu diễn có cấu trúc bao gồm các cú pháp cũng như là ngữ nghĩa của contract. Cách biểu diễn này cho phép ứng dụng kỹ thuật formal verification 🤔 và automated reasoning 🤔 để tìm lỗ hổng cũng như là đảm bảo tính đúng đắn của smart contract.

Ngoài ra còn có một số kỹ thuật phát hiện lỗ hổng dựa trên EVM bytecode hoặc WebAssembly:

  • Mythril: là một model checking5 tool gồm nhiều module giúp phát hiện các loại lỗ hổng sau 🤔: unprotected suicide instructions (deprecated, use selfdestruct instead), unprotected Ether send, reentrancy, và delegatecall.
  • EasyFlow là một arithmetic overflow detector hoạt động dựa trên taint analysis 🤔.

Static Analysis for Program Correctness

Kỹ thuật phổ biến nhất là model checking: sử dụng một formal model của nhiều trạng thái hữu hạn và tự động chứng minh xem đặc tả của input có tuân thủ theo model hay không. Các contract viết bằng ngôn ngữ Solidity là đối tượng chính của kỹ thuật này.

Formal verification là kỹ thuật phổ biến thứ hai được dùng cho program correctness. Nó chứng minh correctness của một formal model so với một formal specification. Kỹ thuật này không chỉ được áp dụng cho Solidity và EVM bytecode mà nó còn có thể được áp dụng cho các ngôn ngữ Oak và Michelson.

Những kỹ thuật khác dùng cho program correctness là: program synthesis, inductive synthesis và resource analysis 🤔.

Dynamic Analysis

Các kỹ thuật dynamic analysis có điểm mạnh so với static analysis là nó không yêu cầu source code và có tỷ lệ dương tính giả (false positive)6 thấp. Các kỹ thuật phổ dynamic analysis phổ biến:

  • Fuzzing: thực thi các chương trình với random input.
  • Runtime verification 🤔: nó theo dõi việc thực thi của các contract ở runtime nhằm phát hiện hoặc bảo vệ các hành vi độc hại.
  • Concolic testing 🤔: kỹ thuật này kết hợp symbolic evaluation với concrete execution.

🤔 Các kỹ thuật khác:

  • Mutation testing
  • Specification mining

Insights

Open Challenges

Ambiguity in Contract Behaviors

Bởi vì smart contract thực thi trên các hệ thống phân tán và tương tác với các bên khác, một số hành vi của nó có thể không rõ ràng hoặc không dự đoán được.

Một trong những trường hợp ví dụ là vấn đề về trạng thái không mong đợi (unexpected state) có thể xảy ra do việc sắp xếp các transaction phụ thuộc vào việc khai thác (miner-dependent transaction ordering) trong mạng blockchain.

Cụ thể, khi một smart contract được triển khai trên mạng blockchain, các transaction liên quan đến việc triển khai (deploying transaction) của smart contract đó có thể được gửi từ nhiều nguồn khác nhau tới các nodes. Miner có thể tự do chọn thứ tự xử lý các giao dịch này trước khi đưa vào một block.

Việc các deploying transaction có thể được sắp xếp theo thứ tự khác nhau có thể dẫn đến trạng thái của smart contract trở nên phức tạp và không dễ dàng dự đoán.

Đồng thời, nhiều contract có chứa các logic mà tương tác với các nguồn off-chain (bên ngoài blockchain) để lấy các dữ liệu cần thiết.

Tuy nhiên, các nguồn dữ liệu này có thể cung cấp các dữ liệu không mong đợi (unexpected data) và kể cả nếu không xảy ra vấn đề này, tính chất của môi trường phân tán vẫn có thể gây ra sự sai khác dữ liệu nhận được giữa các node. Bởi vì smart contract hành xử khác nhau dựa trên dữ liệu khác nhau, dẫn đến, hành vi của chúng cũng sẽ mang tính bất định.

Nguyên do cuối cùng cho vấn đề này là về code opacity.

Cụ thể hơn, các smart contract không có mã nguồn mở sẽ được xem là không rõ ràng. Việc một smart contract không có mã nguồn mở không chỉ làm mất tính minh bạch mà còn gây khó khăn trong việc kiểm tra và phát hiện lỗi, cũng như khả năng sửa chữa và nâng cấp.

Unstable Language Semantics

Các ngôn ngữ lập trình smart contract hiện tại thiếu đặc tả hoặc có nhưng trải qua những thay đổi ngữ nghĩa liên tục do các vấn đề bảo mật.

Lack of Clear Property Definition

Mặc dù có nhiều nỗ lực tập trung vào việc phát hiện các lỗ hổng của contract, nhưng chúng ta vẫn gặp khó khăn trong việc xác định chính xác cái gì cấu thành một lỗ hổng.

Để giải quyết vấn đề này, ta cần định nghĩa những đặc tính mà một vulnerability của smart contract có thể có. Một vài ví dụ:

  • Tính reentrancy: một external contract gọi thực hiện một hàm nhiều lần trong khi lời gọi hàm ban đầu chưa hoàn tất việc thực thi.
  • Tính access control: những người dùng hoặc smart contract dù được không được ủy quyền nhưng vẫn có thể gọi thực hiện những hàm bên trong smart contract.
  • Tính arithmetic safety: các phép tính toán trong smart contract xảy ra overflow hoặc undeflow.

Directions in Future Research

Các hướng nghiên cứu trong tương lai:

  • Language design: thiết kế các ngôn ngữ mới phục vụ cho việc analysis, chẳng hạn như ngôn ngữ Scillia.
  • Type-based approaches: enrich ngôn ngữ bằng một kiểu dữ liệu tường minh là một cách khác để phân tích các smart contract. Lý do là vì hiện tại các ngôn ngữ lập trình chưa hỗ trợ type checking, mặc dù chúng đều là các ngôn ngữ statically-typed.
  • Machine learning: áp dụng các phương pháp học máy chẳng hạn như mô hình LSTM 🤔 nhằm tìm ra các trace vulnerability 🤔 hay mô hình CNN 🤔 giúp chuyển một tập nhiều EVM bytecode thành các mã màu RGB nhằm report các lỗi biên dịch tiềm ẩn.
  • Rising platforms and languages: đa số các nghiên cứu trước đây đều tập trung vào một nền tảng là Ethereum và một ngôn ngữ là Solidity/EVM bytecode. Tuy nhiên, cộng đồng blockchain phát triển rất nhanh và các nền tảng hay ngôn ngữ này có thể trở nên out-dated một lúc nào đó.

Footnotes

  1. Xem thêm Bitcoin’s Scripting Language. ↩ ↩2

  2. Xem thêm Delegatecall | Solidity by Example | 0.8.17 (solidity-by-example.org) ↩

  3. Transaction data của transaction gọi hàm thường có những thông tin sau: địa chỉ của smart contract, function signature, giá trị của các đối số, gas limit và gas price. ↩

  4. Giải thích: khi một hàm được khai báo ở trong smart contract, Solidity sẽ tự động tạo một mã hash duy nhất từ tên hàm và kiểu dữ liệu của các tham số. Function selector được tính bằng cách lấy 4 byte đầu tiên của mã hash. Khi một transaction gọi hàm được gửi lên mạng lưới, 4 byte đầu tiên ở trong transaction data sẽ chứa function selector của hàm được gọi. Dựa vào function selector, Ethereum sẽ điều hướng program counter đến vị trí của hàm ở trong bytecode để thực thi. ↩

  5. Xem thêm Knowledge. ↩

  6. Xem thêm Static Analysis và bài báo Static Analysis for Security. ↩

Backlinks