EthIR
1.0.0
กรอบสำหรับการวิเคราะห์ระดับสูงของ Ethereum bytecode Ethir สร้าง CFG ที่สมบูรณ์และมีเสียงของ Ethereum bytecode และสร้าง การเป็นตัวแทนตามกฎ (RBR) ของโปรแกรม การเป็นตัวแทนระดับสูงนี้ช่วยให้สามารถใช้การวิเคราะห์ระดับสูงที่มีอยู่เพื่ออนุมานคุณสมบัติของรหัส EVM
ดาวน์โหลดแหล่งโฟลเดอร์ที่มีการทำงานแบบคงที่ของคอมไพเลอร์ความแข็งแกร่ง
เพิ่มลงในเส้นทางและทดสอบว่ามีการติดตั้ง
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 เพื่อติดตั้งหกขอไลบรารี Python
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
ไฟล์ทั้งหมดที่สร้างโดย ETHIR ในระหว่างการดำเนินการจะถูกเก็บไว้ใน direcrtory/tmp/costabs/
เมื่อ ติด ตั้ง ETHIR สมมติว่าเราต้องการสร้าง RBR ของการแยกการ บล็อกการบล็อกการบล็อก ก่อนอื่นเราต้องไปที่ไดเรกทอรี Ethir และดำเนินการตามคำสั่ง ./oyente-ethir -s ../examples/blockking.evm.disasm -disasm ที่นั่น
ในระหว่างการดำเนินการ ETHIR ได้สร้างไดเรกทอรี /TMP/costAbs/ ที่เก็บ RBR ที่เกี่ยวข้องกับไฟล์ blockking.evm.disasm หากเราตรวจสอบไดเรกทอรีนี้เราจะพบไฟล์ชื่อ RBR.RBR ที่มี RBR หากเราเปิดไฟล์ด้วยตัวแก้ไขทั่วไป (GEDIT, EMACS) เราจะเห็น RBR ที่สร้างขึ้น ด้านล่างนี้เป็น skecth ของ rbr ที่สร้างขึ้นสำหรับ blockking.evm.disasm ไฟล์:
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 แทนที่จะเป็นหนึ่งข้างต้น RBR ที่ Ethir ผลิตมีคำอธิบายประกอบ NOP ด้านล่างเป็นภาพร่างของ RBR ที่มีคำอธิบายประกอบ NOPS ที่สร้างขึ้นสำหรับ blockking.evm.disasm :
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 เก็บ CFG ในไฟล์ที่มีส่วนขยาย . CFG ในไดเรกทอรี /TMP/costAbs/
โปรดทราบว่าไฟล์อาจมีสัญญาอัจฉริยะมากกว่าหนึ่งไฟล์ ในกรณีนั้น Ethir จะสร้างไฟล์หนึ่งไฟล์ต่อแต่ละสัญญา rbr0.rbr, rbr1.rbr, ... rbrn.rbr
ตัวอย่าง โฟลเดอร์ประกอบด้วยตัวอย่างการทำงานเพื่อทดสอบเครื่องมือ มีทั้งไฟล์ความแข็งแกร่ง EVM และไฟล์แยกชิ้นส่วน
ตัวอย่างส่วนใหญ่เช่น bloccking.evm.disasm, โฆษณา. sol, validtoken.sol หรือ cryptophoenix.sol เป็นสัญญาโลกแห่งความจริงที่ได้รับจาก blockchain ในขณะที่คนอื่น ๆ เช่น loop1.sol และ sum.sol เป็นตัวอย่างที่ง่ายกว่า
SACO เป็นเครื่องวิเคราะห์แบบคงที่สำหรับวัตถุที่เกิดขึ้นพร้อมกันซึ่งสามารถอนุมานได้ในบรรดาคุณสมบัติอื่น ๆ ขอบเขตบน ของจำนวนการวนซ้ำของลูป โปรดทราบว่านี่เป็นขั้นตอนแรกที่สำคัญในการอนุมานการใช้ก๊าซของสัญญาอัจฉริยะ
การเป็นตัวแทนภายในของ SACO ตรงกับไวยากรณ์ของ RBR ที่สร้างขึ้นโดย ETHIR หลังจากการแปลวากยสัมพันธ์เล็กน้อย ต้องขอบคุณสิ่งนี้ทำให้สามารถพิสูจน์การสิ้นสุดของลูปได้ว่าตัวอย่างบางตัวอย่างมีและสร้างขอบเขตเชิงเส้นสำหรับลูปเหล่านั้น นี่คือบางส่วนของขอบเขตลูปที่อนุมานโดย SACO สำหรับสัญญาอัจฉริยะบางส่วนที่มีอยู่ใน ตัวอย่าง โฟลเดอร์:
| สัญญาอัจฉริยะ | ผูกพัน | สัญญาอัจฉริยะ | ผูกพัน |
|---|---|---|---|
| การปิดกั้น | NAT (G8/10)*36+8934493 | Cryptophoenix | NAT (G3)*228409344+4113285485 |
| ลูป 1 | NAT (A)*25+234 | เอลิกมา | NAT (_numberofreturns)*2628+134 |
| ลอตเตอรี | 159 | blocksquareseriea | 286 |
| โอบล้อม | 268 | เครื่องกำเนิดไฟฟ้า | 264 |
| โฆษณา | การติดเชื้อ | validtoken | การติดเชื้อ |
SACO จะทำให้เส้นตรงเชิงเส้นสำหรับสัญญาอัจฉริยะสี่ตัวแรกที่แสดงในตารางด้านบน ขอบเขตของสัญญาอัจฉริยะการบล็อกและ cryptophoenix ขึ้นอยู่กับมูลค่าของหนึ่งในฟิลด์ของพวกเขา (แปดและสามตามลำดับ) สำหรับสัญญาอัจฉริยะ Loop1 และ Eligma ขอบเขตที่ได้รับขึ้นอยู่กับข้อโต้แย้งของฟังก์ชั่นบางอย่าง (a และ _numberofreturns) ในกรณีที่สัญญาอัจฉริยะไม่มีลูปใด ๆ เช่นลอตเตอรี, blocksquareseriea, enclaves หรือ auctusether, saco infers ค่าคงที่
โปรดทราบว่าเนื่องจากข้อ จำกัด ที่แม่นยำของ SACO (ไม่มีการดำเนินการบิตและแบบจำลองสำหรับฟังก์ชั่น sha3) ตัววิเคราะห์ลืมข้อมูลเกี่ยวกับตัวแปรบิต เนื่องจากปัจจัยนี้ SACO จึงไม่สามารถอนุมานได้ว่ามีการทำสัญญาอัจฉริยะบางอย่างเช่น ValidToken หรือโฆษณาและส่งคืน Inf
เครื่องวิเคราะห์ระดับสูงอื่น ๆ ที่ทำงานในรูปแบบระดับกลางเช่นระบบการเปลี่ยนจำนวนเต็มหรือส่วนของฮอร์น (เช่น Aprove, T2, มาก, Cofloco) สามารถปรับเปลี่ยนได้ง่ายเช่นกันเพื่อทำงานในโปรแกรมแปล RBR ที่ผลิตโดย Ethir
หากคุณน่าสนใจในการใช้ Ethir ร่วมกับ Saco Contact Saco Developers ผ่านการขอร้องหรือปัญหาใหม่
คุณสามารถลองต้นแบบแรกได้ที่นี่ GASTAP ติดอยู่ในระดับบนของก๊าซที่เกี่ยวข้องในการทำธุรกรรมแต่ละครั้ง
