스마트 컨트랙트 (7) | 보안성을 갖춘 컨트랙트 작성법

 

1. 이더리움 내 모든 데이터는 공개되어 있음을 명심하자 

- private variable로 선언되었더라도, getStorageAt 함수를 통해 해당 컨트랙트의 변수를 읽어낼 수 있다. 

- 구체적으로는 상기 함수를 통해 컨트랙트 내 변수가 인코딩된 값을 받게 되는데, 데이터타입에 따라 복잡도는 다를 수 있어도 충분히 해석할 수 있다. 

 

 

 

2. 이더리움 송금은 transfer method를 사용하자

* 송금 방법 1 : address.send(value)

- 송금 실패 시 false만 반환하고 exception을 발생시키지 않음. 

 

* 송금 방법 2 : address.transfer(value)

- 송금 실패 시 exception을 발생시키고 중단됨

- 2300 가스만 보내서 실행되므로 컨트랙트의 무한 호출을 방지 가능

 

* 송금 방법 3 : address.call.value(value)()

- call method는 외부 컨트랙트 메소드 호출 시 사용

- value, gas modifier를 파라미터로 받음. 가스 미지정 시 전체 가스가 남겨져 위험성 있음. 

- call이 송금 대상 계정의 fallback을 부르고, 그 송금 대상 계정이 악의적으로 fallback을 통해 다시 withdraw를 재귀적으로 호출할 경우 무한 루프에 빠져 송금 발신 계 전체 잔고를 모두 가져올 때까지 송금을 반복시킬 우려가 있음. 

- 무한 루프의 경우 require 문등을 활용해 call.value의 리턴 값을 받아줘서 트랜잭션 취소를 진행하는 임시 방편 해결안이 있음.

 

 

 

3. 이더리움 송금은 하나의 메소드 당 하나의 transfer를 사용하자 (withdraw pattern)

- 하나의 송금 메소드 안에 여러 대상으로의 transfer를 넣을 경우, 공격자가 의도적으로 transfer를 실패하는 컨트랙트 주소를 transfer 대상에 추가해서, 해당 메소드 자체가 오류가 발생하도록 공격할 수 있음. 즉, 하나의 계정 실패로 전체 컨트랙트의 송금 메소드가 마비될 우려가 있음. 

- 공격자가 transfer를 실패하도록 하는 수법으로는, transfer 송금 대상 컨트랙트의 fallback 함수를 만들지 않거나, fallback 함수에 payable 조건을 추가해주지 않는 경우 등이 있음. 

- Withdraw Pattern : Contract 내부의 balance를 관리하다가 withdraw 요청이 올 경우 해당 address 하나로만 송금/출금시켜주는 방식

 

 

 

4. Check-Effects-Interactions 패턴을 사용하자

(1) Check : 확인 작업. 누가 메소드를 호출했고, arg에는 문제가 없고, 잔액은 충분한 지 등. 

(2) Effects : 확인에 문제가 없을 경우 컨트랙트 내부 변수 값을 우선 업데이트. 

(3) Interactions : 다른 컨트랙트와의 인터랙션, 외부 컨트랙트 메소드 호출은 함수 가장 마지막에 위치. 

 

 

 

5. Remix IDE Analysis 기능을 이용하자

https://remix.ethereum.org/

 

 

 

6. Overflow, Underflow에 유의하자 (SafeMath)

- integer 사용시 overflow가 발생하면 최소값, underflow가 발생하면 최대값으로 변경되는 솔리디티 특성에 유의하자. 

- assert 문을 활용해 연산 이전에 연산의 조건을 미리 확인해 이를 방지하는 임시 해결책이 있다. 

- 안전하게 사용하기 위해서는 OpenZeppelin의 safemath와 같은 외부 라이브러리를 임포트 해 메소드를 통해 연산하자.

import "github.com/OpenZepplin/OpenZepplin-contracts/contracts/math/SafeMath.sol"

GitHub - OpenZepplin/OpenZepplin-contracts

 

 

 

7. 컨트랙트의 balance에 절대적으로 의존하지 말자

- payable method 외에도 다양한 방법으로 컨트랙트 내 잔고는 변경 가능하다

- 예를 들어 외부 컨트랙트가 selfdestruct하는 과정에서 우리의 컨트랙트로 송금을 보내올 수도 있다

- 따라서 contract의 잔고 값은 우리 내부적인 payable 함수가 만들어내는 supply 양과 같을 것을 기대하더라고, 항상 그보다 클 수 있다는 사실을 명심하자

assert(address(this).balance >= totalSupply);

 

 

 

8. 코드 오류 검증 절차를 준수하자

(1) 테스트 코드를 작성한다

 

(2) truffle 등의 도구를 활용해 테스트를 자동으로 실행한다

 

(3) Code Review, Code Audit을 수행하자

- 오픈제플린 등 스마트컨트랙트 전문 감사 기업도 활용 가능하다

 

(4) Formal Verification을 사용하자

- 수학적 기법을 통한 기능 구현 검증 작업을 의미한다.

- Slither, Echidna, Manticore 등이 사용 가능하다.

 

(5) SMT Checker 모듈을 컴파일러에서 활성화시키자

 

 

 

8-1. Slither

- 슬리더는 솔리디티용 정적 분석 프레임워크이다. 

- 소스 코드를 솔리디티 컴파일러를 통해 syntax 트리를 구한 뒤 분석을 진행한다

- 기본 제공 취약점 분석 외 API를 제공

Slither is a Solidity static analysis framework written in Python 3. It runs a suite of vulnerability detectors, prints visual information about contract details, and provides an API to easily write custom analyses. Slither enables developers to find vulnerabilities, enhance their code comprehension, and quickly prototype custom analyses.

How to install
Slither requires Python 3.6+ and solc, the Solidity compiler.
Using Pip ) pip3 install slither-analyzer

Slither, the Solidity source analyzer
https://github.com/crytic/slither 

GitHub - crytic/slither: Static Analyzer for Solidity

Slither – a Solidity static analysis framework

 

This paper describes Slither, a static analysis framework designed to provide rich information about Ethereum smart contracts. It works by converting Solidity smart contracts into an intermediate representation called SlithIR. SlithIR uses Static Single Assignment (SSA) form and a reduced instruction set to ease implementation of analyses while preserving semantic information that would be lost in transforming Solidity to bytecode. Slither allows for the application of commonly used program analysis techniques like dataflow and taint tracking.
Our framework has four main use cases: (1) automated detection of vulnerabilities, (2) automated detection of code optimization opportunities, (3) improvement of the user’s understanding of the contracts, and (4) assistance with code review.

In this paper, we present an overview of Slither, detail the design of its intermediate representation, and evaluate its capabilities on real-world contracts. We show that Slither’s bug detection is fast, accurate, and outperforms other static analysis tools at finding issues in Ethereum smart contracts in terms of speed, robustness, and balance of detection and false positives. We compared tools using a large dataset of smart contracts and manually reviewed results for 1000 of the most used contracts.

Slither: A Static Analysis Framework For Smart Contracts
Josselin Feist, Gustavo Grieco, Alex Groce, 26 Aug 2019
https://arxiv.org/pdf/1908.09878.pdf 

slither example.sol

slither --print contract-summary example.sol

slither --print data-dependency example.sol

# customAnalyser.py based on Slither API

import sys
from slither import Slither

# create Slither Object with solidity file
slither = Slither('example.sol')

for contract in slither.contracts:
	print(f'Contract: {contract.name}')
    for function in contract.functions:
    	print(f'\t{function.full_name}:')
        print(f'\t\tVisibility: {function.visibility}')
        print(f'\t\tContract: {function.contract}')
        print(f'\t\tModifier: {[m.name for m in function.modifiers]}')
        print(f'\t\tIs constructor?: {function.is_constructor}')
        print(f'\t\tIs payable?: {function.payable}')

 

 

 

8-2. SMT Checker Module

- 컴파일러 내부 모듈로 컴파일 중 assertion을 검사한다

- require와 assert가 기존과 다른 기능을 가지게 된다

- require: 증명에 이용되는 가정 역할이다

- assert: assert statement를 증명하고자 한다

- 컴파일러는 assert statement를 위반하는 상황을 찾고자 노력해서, 찾을 경우 반례를 제시해 코드 오류를 보여준다

Solidity implements a formal verification approach based on SMT (Satisfiability Modulo Theories) and Horn solving. The SMTChecker module automatically tries to prove that the code satisfies the specification given by require and assert statements. That is, it considers require statements as assumptions and tries to prove that the conditions inside assert statements are always true. If an assertion failure is found, a counterexample may be given to the user showing how the assertion can be violated. If no warning is given by the SMTChecker for a property, it means that the property is safe.

The other verification targets that the SMTChecker checks at compile time are:
Arithmetic underflow and overflow.
Division by zero.
Trivial conditions and unreachable code.
Popping an empty array.
Out of bounds index access.
Insufficient funds for a transfer.

https://docs.soliditylang.org/en/v0.8.13/smtchecker.html#smtchecker-options-and-tuning 

To enable the SMTChecker, you must select which engine should run, where the default is no engine. Selecting the engine enables the SMTChecker on all files.

Note Prior to Solidity 0.8.4, the default way to enable the SMTChecker was via pragma experimental SMTChecker; and only the contracts containing the pragma would be analyzed. That pragma has been deprecated, and although it still enables the SMTChecker for backwards compatibility, it will be removed in Solidity 0.9.0. Note also that now using the pragma even in a single file enables the SMTChecker for all files.

https://docs.soliditylang.org/en/v0.8.13/smtchecker.html#smtchecker-options-and-tuning 

SMTChecker and Formal Verification — Solidity 0.8.13 documentation

 

 

 

 

 

9. 설계 수준의 검증을 시도하자

- contract를 formal method로 표현 가능한 transition system으로 모델링하기

- state와 action, transition으로 컨트랙트 내용을 표현해 모델링

- transition의 조건을 guard라 부름 - 상태 변경 조건에 대한 명세

- 설계 수준에서의 명확한 표현을 통해 트랜지션 시스템 기반 검증 기법 활용 가능

(트랜지션 시스템 검증 기법의 예시 : 반드시 지켜야 하는 속성, property를 정의 후 모델 체킹 기법으로 검증)

( Property = AG('close' -> AG(not 'bid')), AG는 모든 path에서 만족함을 의미 )

검증된 패턴은 잘 알려진 문제에만 적용할 수 있고 코딩 단계의 기법이기 때문에 서로 다른 언어에 적용되기 어렵다.
위험 요소를 찾아주는 툴은 자동화가 가능하고 버그가 있다는 것을 알려주지만 버그가 없음을 증명하지 못하는 한계점이 있다.
정형 검증을 통해 버그가 없음을 증명할 수 있다.
정형 검증은 알려지지 않은 형태의 버그를 찾아줄 수 있지만 자동화가 어렵다는 단점이 있다.

 

https://github.com/anmavrid/smart-contracts

Correct-by-Design Smart Contracts: FSolidM / VeriSolid Framework

What is FSolidM?
The adoption of blockchain-based distributed computation platforms is growing fast. Some of these platforms, such as Ethereum, provide support for implementing smart contracts, which are envisioned to have novel applications in a broad range of areas, including finance and Internet-of-Things. However, a significant number of smart contracts deployed in practice suffer from security vulnerabilities, which enable malicious users to steal assets from a contract or to cause damage. Vulnerabilities present a serious issue since contracts may handle financial assets of considerable value, and contract bugs are non-fixable by design. To help developers create more secure smart contracts, we introduce FSolidM, a framework rooted in rigorous semantics for designing contracts as Finite State Machines (FSM). We present a design studio for creating FSMs on an easy-to-use graphical interface and for automatically generating Ethereum contracts. We have integrated in FSolidM a set of design patterns, which we implement as plugins that developers can easily add to their contracts to enhance security and functionality.

@anmavrid anmavrid Anastasia Mavridou
@aronlaszka aronlaszka
@pmeijer pmeijer Patrik Meijer
https://github.com/anmavrid/smart-contracts 

Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach

VeriSolid: Correct-by-Design Smart Contracts for Ethereum

FSolidM Design Studio for Ethereum Smart Contracts | CPS-VO

 

Statecharts: a visual formalism for complex systems

We present a broad extension of the conventional formalism of state machines and state diagrams, that is relevant to the specification and design of complex discrete-event systems, such as multi-computer real-time systems, communication protocols and digital control units. Our diagrams, which we call statecharts, extend conventional state-transition diagrams with essentially three elements, dealing, respectively, with the notions of hierarchy, concurrency and communication. These transform the language of state diagrams into a highly structured and economical description language. Statecharts are thus compact and expressive—small diagrams can express complex behavior—as well as compositional and modular. When coupled with the capabilities of computerized graphics, statecharts enable viewing the description at different levels of detail, and make even very large specifications manageable and comprehensible. In fact, we intend to demonstrate here that statecharts counter many of the objections raised against conventional state diagrams, and thus appear to render specification by diagrams an attractive and plausible approach. Statecharts can be used either as a stand-alone behavioral description or as part of a more general design methodology that deals also with the system's other aspects, such as functional decomposition and data-flow specification. We also discuss some practical experience that was gained over the last three years in applying the statechart formalism to the specification of a particularly complex system.

David Harel, Statecharts: a visual formalism for complex systems,
Science of Computer Programming, Volume 8, Issue 3, 1987,
Pages 231-274, ISSN 0167-6423,
https://doi.org/10.1016/0167-6423(87)90035-9. https://www.sciencedirect.com/science/article/pii/0167642387900359 

Statecharts: a visual formalism for complex systems