Echidna는 버그를 먹어치우며 전기 감도가 매우 높은 이상한 생명체입니다 (Jacob Stanley에게 사과의 뜻을 전하며)
더 진지하게 말하자면, Echidna는 이더리움 스마트 컨트랙트의 퍼징/속성 기반 테스트를 위해 설계된 Haskell 프로그램입니다. 이는 컨트랙트 ABI를 기반으로 한 정교한 문법 기반 퍼징 캠페인을 사용하여 사용자 정의 술어나 Solidity 단언문을 반증합니다. Echidna는 모듈성을 염두에 두고 설계되었기 때문에, 새로운 변이를 포함하거나 특정 사례에서 특정 컨트랙트를 테스트하도록 쉽게 확장할 수 있습니다.
.. 그리고 아름다운 고해상도 수제 로고.
Echidna의 핵심 기능은 echidna라는 실행 파일로, 컨트랙트와 불변성 목록(항상 참으로 유지되어야 하는 속성)을 입력으로 받습니다. 각 불변성에 대해 컨트랙트에 대한 무작위 호출 시퀀스를 생성하고 불변성이 유지되는지 확인합니다. 불변성을 반증할 방법을 찾으면, 그렇게 하는 호출 시퀀스를 출력합니다. 찾지 못하면, 컨트랙트가 안전하다는 어느 정도의 보증을 얻을 수 있습니다.
불변성은 echidna_로 시작하는 이름을 가지며, 인자가 없고, 불리언을 반환하는 Solidity 함수로 표현됩니다. 예를 들어, 20 아래로 절대 내려가서는 안 되는 balance 변수가 있다면, 다음과 같이 컨트랙트에 추가 함수를 작성할 수 있습니다:```solidity
function echidna_check_balance() public returns (bool) {
return(balance >= 20);
}
To check these invariants, run:```sh
$ echidna myContract.sol
테스트가 포함된 예제 컨트랙트는 tests/solidity/basic/flags.sol에서 확인할 수 있습니다. 실행하려면 다음을 수행해야 합니다:```sh $ echidna tests/solidity/basic/flags.sol
Echidna는 `echidna_sometimesfalse`를 반증하는 호출 시퀀스를 찾아야 하며, `echidna_alwaystrue`에 대한 반증 입력을 찾을 수 없어야 합니다.
### 테스트 모드
위 예제는 기본 **property** 모드를 사용하지만, Echidna는 구성 파일의 `testMode` 또는 CLI의 `--test-mode`를 통해 구성되는 여러 테스트 모드를 지원합니다:
* **`property`** (기본값): `bool`을 반환하는 `echidna_` 접두사 함수를 테스트합니다.
* **`assertion`**: `assert()` 및 Foundry의 `assertX` 헬퍼(`assertTrue`, `assertEq` 등)로부터의 어서션 실패를 감지합니다.
* **`foundry`**: Foundry 스타일 테스트를 실행하며, 명명 규칙을 따릅니다: `test` 접두사 단위 및 퍼즈 테스트(`testFail` 접두사 테스트는 revert가 예상됨)와 `invariant` 또는 `statefulFuzz` 접두사 상태 기반 불변성. `check` 및 `prove` 접두사 함수는 심볼릭 진입점이지만, 이 모드는 퍼징 캠페인이므로 다른 테스트 함수와 마찬가지로 퍼징됩니다.
* **`verification`**: 단일 트랜잭션을 사용하여 컨트랙트의 각 함수를 심볼릭하게 검증합니다. `check` 및 `prove` 접두사 함수는 항상 진입점으로 사용됩니다.
* **`overflow`**: 정수 오버/언더플로를 감지합니다 (Solidity >= 0.8.0).
* **`optimization`**: `int256`을 반환하는 `echidna_` 접두사 함수의 반환 값을 최대화합니다 (property 모드와 동일한 구성 가능한 접두사 사용).
* **`exploration`**: 속성을 확인하지 않고 커버리지를 수집합니다.
### 커버리지 수집 및 시각화
캠페인을 완료한 후, Echidna는 `corpusDir` 구성 옵션으로 지정된 특수 디렉터리에 커버리지를 최대화하는 **코퍼스**를 저장할 수 있습니다. 이 디렉터리에는 두 개의 항목이 포함됩니다: (1) Echidna가 재생할 수 있는 JSON 파일이 있는 `coverage`라는 디렉터리와 (2) 커버리지 주석이 포함된 소스 코드의 복사본인 `covered.txt`라는 일반 텍스트 파일.
`tests/solidity/basic/flags.sol` 예제를 실행하면, Echidna는 `coverage` 디렉터리에 몇 개의 직렬화된 트랜잭션 파일과 다음 줄이 포함된 `covered.$(date +%s).txt` 파일을 저장합니다:```text
*r | function set0(int val) public returns (bool){
* | if (val % 100 == 0)
* | flag0 = false;
}
*r | function set1(int val) public returns (bool){
* | if (val % 10 == 0 && !flag0)
* | flag1 = false;
}
우리 도구는 코퍼스의 각 실행 트레이스를 다음과 같은 "라인 마커"로 표시합니다:
*roeEchidna는 crytic-compile을 사용하여 Foundry, Hardhat, Truffle을 비롯한 다양한 스마트 컨트랙트 빌드 시스템으로 컴파일된 컨트랙트를 테스트할 수 있습니다. 현재 컴파일 프레임워크로 Echidna를 호출하려면 echidna .를 사용하세요.
그뿐만 아니라, Echidna는 복잡한 컨트랙트를 테스트하는 두 가지 모드를 지원합니다. 첫째, 기존 네트워크 상태를 활용하여 이를 Echidna의 기반 상태로 사용할 수 있습니다. 둘째, Echidna는 CLI에서 해당 Solidity 소스를 전달하여 알려진 ABI를 가진 모든 컨트랙트를 호출할 수 있습니다. 이 기능을 켜려면 설정에서 allContracts: true를 사용하세요.
우리의 Building Secure Smart Contracts 저장소에는 예제, 레슨, 연습 문제를 포함한 Echidna 단기 집중 과정이 있습니다.
GitHub Actions 워크플로의 일부로 echidna를 실행하는 데 사용할 수 있는 Echidna 액션이 있습니다. 사용 방법과 예제는 crytic/echidna-action 저장소를 참조하세요.
Echidna의 CLI를 사용하여 테스트할 컨트랙트를 선택하고 설정 파일을 로드할 수 있습니다.```sh $ echidna contract.sol --contract TEST --config config.yaml
구성 파일을 통해 사용자는 EVM 및 테스트 생성 매개변수를 선택할 수 있습니다. 기본 옵션이 포함된 완전하고 주석이 달린 구성 파일의 예시는
[tests/solidity/basic/default.yaml](https://github.com/crytic/echidna/blob/master/tests/solidity/basic/default.yaml)에서 확인할 수 있습니다.
사용 가능한 구성 옵션에 대한 더 자세한 정보는 [문서](https://secure-contracts.com/program-analysis/echidna/configuration.html)를 참조하십시오.
Echidna는 세 가지 다른 출력 드라이버를 지원합니다. 기본 `text`
드라이버, `json` 드라이버, 그리고 모든 `stdout` 출력을 억제해야 하는 `none` 드라이버가 있습니다. JSON 드라이버는 전체 캠페인을 다음과 같이 보고합니다.```
Campaign = {
"success" : bool,
"error" : string?,
"tests" : [Test],
"seed" : number,
"coverage" : Coverage
}
Test = {
"contract" : string,
"name" : string,
"status" : string,
"error" : string?,
"testType" : string,
"transactions" : [Transaction]?
}
Transaction = {
"contract" : string,
"function" : string,
"arguments" : [string]?,
"gas" : number,
"gasprice" : number
}
Coverage는 특정 커버리지 증가 호출을 설명하는 dict입니다. 이러한 인터페이스는 추후에 좀 더 사용자 친화적으로 변경될 수 있습니다. testType은 property, assertion, optimization, exploration, call 중 하나이며, status는 항상 fuzzing, shrinking, solved, passed, error 중 하나를 가집니다.
Echidna의 성능 문제를 진단하는 한 가지 방법은 프로파일링을 활성화하여 echidna를 실행하는 것입니다.
기본 프로파일링으로 Echidna를 실행하려면 원래의 echidna 명령에 +RTS -p -s를 추가하세요:```sh
$ nix develop # alternatively nix-shell
$ cabal --enable-profiling run echidna -- ... +RTS -p -s
$ less echidna.prof
이것은 가장 많은 CPU와 메모리 사용량을 차지하는 함수를 보여주는 보고서 파일(`echidna.prof`)을 생성합니다.
기본 프로파일링이 도움이 되지 않는다면, 더 [고급 프로파일링 기법](https://haskell.foundation/hs-opt-handbook.github.io/src/Measurement_Observation/Haskell_Profiling/eventlog.html)을 사용할 수 있습니다.
우리가 관찰한 성능 문제의 일반적인 원인:
- 핫 패스에서 호출되는 비용이 큰 함수
- 썽크를 축적하는 지연 데이터 생성자
- 핫 패스에서 사용되는 비효율적인 데이터 구조
이러한 사항을 확인하는 것이 좋은 시작점입니다. 특정 계산이 너무 지연되어 메모리를 누수한다고 의심된다면, `Control.DeepSeq`의 `force`를 사용하여 평가되도록 할 수 있습니다.
## 제한 사항 및 알려진 문제
EVM 에뮬레이션과 테스트는 어렵습니다. Echidna는 최신 릴리스에서 몇 가지 제한 사항이 있습니다. 일부는 [hevm](https://github.com/argotorg/hevm)에서 상속된 것이고, 일부는 설계/성능 결정의 결과이거나 단순히 우리 코드의 버그입니다. 해당 이슈와 상태("수정 안 함", "보류", "검토 중", "수정됨")를 포함하여 여기에 나열합니다. "수정됨"인 이슈는 다음 Echidna 릴리스에 포함될 것으로 예상됩니다.
| 설명 | 이슈 | 상태 |
| :--- | :---: | :---: |
| Vyper 지원이 제한적임 | [#652](https://github.com/crytic/echidna/issues/652) | *수정 안 함* |
| 테스트를 위한 라이브러리 지원이 제한적임 | [#651](https://github.com/crytic/echidna/issues/651) | *수정 안 함* |
## 설치
### 사전 컴파일된 바이너리
시작하기 전에 Slither가 [설치](https://github.com/crytic/slither)되어 있는지 확인하세요 (`pip3 install slither-analyzer --user`).
Linux 또는 MacOS에서 Echidna를 빠르게 테스트하려면, Ubuntu에서 빌드된 정적으로 링크된 Linux 바이너리와 대부분 정적인 MacOS 바이너리를 [릴리스 페이지](https://github.com/crytic/echidna/releases)에서 제공합니다. [CI 파이프라인](https://github.com/crytic/echidna/actions?query=workflow%3ACI+branch%3Amaster+event%3Apush)에서도 동일한 유형의 바이너리를 얻을 수 있으며, Linux 또는 MacOS용 바이너리를 찾으려면 커밋을 클릭하기만 하면 됩니다.
### Homebrew (macOS / Linux)