EthIR
1.0.0
이더 리움 바이트 코드의 고급 분석을위한 프레임 워크. Ethir는 Ethereum Bytecode의 완전하고 건전한 CFG를 구축하고 프로그램의 RBR ( Rule Based Presentation )을 생성합니다. 이 높은 수준의 표현은 기존의 고급 분석을 적용하여 EVM 코드의 속성을 추론 할 수 있도록합니다.
Solidity 컴파일러의 정적 실행 파일이 포함 된 폴더 소스를 다운로드하십시오.
경로에 추가하고 설치된 것을 테스트하십시오.
sudo cp source/solc* /usr/bin/
sudo chmod 755 /usr/bin/solc*
solc --version
solcv5 --version
solcv6 --version
최신 버전을 설치하려는 경우 :
sudo add-apt-repository ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install solc
정적 실행 파일은 폴더 소스에 제공됩니다.
경로에 OT를 추가하고 설치되었음을 테스트하십시오.
sudo cp source/evm* /usr/bin/
sudo chmod 755 /usr/bin/evm*
evm --version
최신 버전을 설치하려는 경우 :
sudo apt-get install software-properties-common
sudo add-apt-repository -y ppa:ethereum/ethereum
sudo apt-get update
sudo apt-get install ethereum
소스 코드 폴더를 다운로드하십시오.
폴더를 압축하고 설치하십시오.
unzip z3-z3-4.5.0.zip
cd z3-z3-4.5.0
python scripts/mk_make.py --python
cd build
make
sudo make install
pip install 명령을 사용하여 6 개의 설치를 요청합니다.
pip install six
pip install requests
위의 명령은 PIP 버전에 따라 실패 할 수 있습니다. 그렇다면 이전 명령 대신 다음 명령을 실행하십시오.
python -m pip install six
python -m pip install requests
버전을 확인하려면 명령 pip -V 실행합니다.
Ethir를 실행하려면 Ethir 폴더 내에서 다음 명령 중 하나를 실행하십시오.
./oyente-ethir -s file_name.sol
./oyente-ethir -s file_name.evm -b
./oyente-ethir -s file_name.disasm -disasm
./oyente-ethir -h 명령에는 Ethir의 모든 사용 가능한 옵션이 포함 된 목록이 표시됩니다. 가장 관련성이 높은 것 중 일부는 다음과 같습니다.
./oyente-ethir -s filename -cfg
./oyente-ethir -s filename -saco
./oyente-ethir -s filename -d
ETHITURE가 실행하는 동안 Ethir가 생성 한 모든 파일은 DIRECRTORY/TMP/COSTABS/에 저장됩니다.
Ethir가 설치되면 폴더 예제 에서 사용 가능한 분해 파일 Blockking.evm.Disasm 의 RBR을 생성한다고 가정하십시오. 먼저, 우리는 ethir directory로 가서 명령을 실행해야합니다 ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm .
실행 중에 Ethir는 Directory /TMP/Costabs/ 를 만들었습니다. 여기서 Blockking.evm.Disasm 파일과 관련된 RBR을 저장했습니다. 이 디렉토리를 검사하면 rbr이 포함 된 rbr.rbr 이라는 파일이 있습니다. 공통 편집기 (GEDIT, EMACS)와 함께 파일을 열면 RBR이 생성 된 것을 볼 수 있습니다. 아래는 Blockking.evm.Disasm 파일을 위해 생성 된 RBR의 스키 스크린입니다.
block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
s(0) = 96
s(1) = 64
l(0) = s(0)
s(0) = calldatasize
call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
eq(s(0), 0)
call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
neq(s(0), 0)
call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
s(0) = 224
s(1) = 2
s(0) = s(1)^s(0)
s(1) = 0
s(1) = calldataload
s(0) = s(1)/s(0)
s(1) = 607252836
s(2) = s(0)
call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
우리가 명령을 실행하면 ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -eop 위의 것 대신에 Ethir가 생성하는 rbr은 텍스트에 evm 바이트 코드가 인터리 된 EVM 바이트 코드가있는 nops 주석이 있습니다. 아래는 blockking.evm.disasm 에 생성 된 NOPS 주석이있는 RBR의 스케치입니다.
block0(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance)=>
s(0) = 96
nop(PUSH1)
s(1) = 64
nop(PUSH1)
l(0) = s(0)
nop(MSTORE)
s(0) = calldatasize
nop(CALLDATASIZE)
call(jump0(s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(8), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), calldatasize, calldataload, gas, caller, callvalue, number, gasprice, balance))
nop(ISZERO)
nop(PUSH2)
nop(JUMPI)
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
eq(s(0), 0)
call(block174(g(11), g(8), g(4), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), caller, callvalue, gas, gasprice, number))
jump0(s(0), g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, calldatasize, caller, callvalue, gas, gasprice, number)=>
neq(s(0), 0)
call(block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
block11(g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number)=>
s(0) = 224
nop(PUSH1)
s(1) = 2
nop(PUSH1)
s(0) = s(1)^s(0)
nop(EXP)
s(1) = 0
nop(PUSH1)
s(1) = calldataload
nop(CALLDATALOAD)
s(0) = s(1)/s(0)
nop(DIV)
s(1) = 607252836
nop(PUSH4)
s(2) = s(0)
nop(DUP2)
call(jump11(s(2),s(1),s(0),g(11), g(10), g(9), g(8), g(7), g(6), g(5), g(4), g(3), g(2), g(1), g(0), l(7), l(6), l(5), l(4), l(3), l(2), l(1), l(0), balance, calldataload, caller, callvalue, gas, gasprice, number))
nop(EQ)
nop(PUSH2)
nop(JUMPI)
Ethir는 또한 분석 된 파일의 CFG를 저장할 수 있습니다. 이 경우, 우리는 명령 ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm -cfg 실행해야합니다. Ethir는 디렉토리 /tmp/costabs/ 에 .cfg 확장자가있는 파일에 CFG를 저장합니다.
파일에는 둘 이상의 스마트 계약이 포함될 수 있습니다. 이 경우 Ethir는 각 계약 rbr0.rbr, rbr1.rbr, ... rbrn.rbr에마다 하나의 파일을 생성합니다.
폴더 예제 에는 도구를 테스트하기 위해 실행중인 예제가 포함되어 있습니다. 견고성, EVM 및 분해 파일이 모두 있습니다.
Bloccking.evm.disasm, enderment.sol, sol, validtoken.sol 또는 cryptophoenix.sol과 같은 대부분의 예는 블록 체인에서 얻은 실제 계약이며 Loop1.sol 및 sum.sol과 같은 다른 계약은 탈취 과정을 이해하기가 더 쉬운 임시 예입니다.
SACO는 동시 물체를위한 정적 분석기로, 다른 속성 중에서도 루프 반복 횟수에 대한 상한을 추론 할 수 있습니다. 이것은 스마트 계약의 가스 소비를 추론하는 첫 번째 중요한 단계입니다.
SACO의 내부 표현은 사소한 구문 번역 후 Ethir에 의해 생성 된 RBR의 문법과 일치합니다. 이 덕분에 일부 예제에 해당 루프에 선형 바운드가 포함되어 있고 생성 된 루프의 종료를 증명할 수 있습니다. 다음은 SACO가 폴더 예제 에 포함 된 일부 스마트 계약에 대해 추론 한 루프 경계 중 일부입니다.
| 스마트 계약 | 경계 | 스마트 계약 | 경계 |
|---|---|---|---|
| 블록 킹 | NAT (G8/10)*36+8934493 | cryptophoenix | NAT (G3)*228409344+4113285485 |
| 루프 1 | Nat (a)*25+234 | 엘리그마 | nat (_numberofreturns)*2628+134 |
| 운 | 159 | Blocksquareseriea | 286 |
| 영토 | 268 | auctusether | 264 |
| 광고 | inf | 유효합니다 | inf |
Saco는 위의 표에 표시된 처음 4 개의 스마트 계약에 대한 선형 경계를 유추합니다. 스마트 계약의 경계는 블록킹 및 cryptophoenix의 범위는 해당 분야 중 하나의 가치 (각각 8 및 세 번째)의 가치에 따라 다릅니다. Smart Contracts Loop1 및 Eligma의 경우, 얻은 범위는 일부 기능 (a 및 _numberofreturns)의 주장에 의존합니다. 스마트 계약에 복권, Blocksquareseriea, Enclaves 또는 auctusether와 같은 루프가 포함되어 있지 않은 경우 Saco는 일정한 경계를 유발합니다.
SACO의 정밀한 제한으로 인해 (비트 운영이없고 함수 SHA3 모델) 분석기는 비트 변수에 대한 정보를 잊어 버립니다. 이 요소로 인해 Saco는 ValidToken 또는 광고와 같은 일부 스마트 계약에 대한 경계를 추론 할 수 없으며 INF를 반환 할 수 없습니다.
정수 전이 시스템 또는 혼 클로스 (예 : Aprove, T2, Bethymax, Cofloco)와 같은 중간 형태에서 작동하는 다른 고급 분석기는 Ethir가 생산 한 RBR 번역 프로그램에 대해 쉽게 작업 할 수 있습니다.
Saco와 공동으로 Ethir를 사용하는 것이 흥미로워지면 풀 수복 또는 새로운 문제를 통해 Saco 개발자에게 연락하십시오.
여기서 첫 번째 프로토 타입을 시도해 볼 수 있습니다. Gastap은 각 거래와 관련된 가스의 상한을 유추합니다.
