มาลองแกะ code Oyente กันเถอะ (Part 3 construct CFG dynamic edges)
โอเค ก่อนอื่นมา recap กันก่อนว่าเราแกะส่วนไหนไปแล้วบ้าง และเหลืออะไรบ้าง
ก่อนอื่นมาเริ่มกันจาก
ภาพรวม Oyente
Oyente ทำงานดังนี้
- นำ bytecode และ state ของ contract ไปสร้าง CFG
- นำ CFG นั้นไปทำ symbolic execution เพื่อหา unreachable path และ symbolic values ของ path นั้นๆ
- นำ CFG และ symbolic values ไป detect ช่องโหว่
- กรอง false positive
โดยตอนนี้เราอยู่ที่ part นำ bytecode และ state ของ contract ไปสร้าง CFG
เราแกะส่วนไหนไปแล้วบ้าง ?
เริ่มจาก code ส่วนที่แปลง solidity เป็น bytecode ด้วย solc
จากนั้นแปลง bytecode เป็น opcode
ซึ่ง opcode ที่ได้มาจะเป็น list เรียงลงไปเรื่อยๆ
แต่ flow ในการรันโปรแกรมจริงๆจะมีการกระโดดบรรทัด ไปมา ในลักษณะต้นไม้แบบ CFG
ดังนั้นเราต้องแปลง opcode เป็น CFG
โดยประกอบด้วย 2 ขั้นตอนคือ
- แบ่ง opcode เป็น nodeๆ
- ลากเส้นเชื่อมแต่ละ node
โดยในการแบ่ง opcode เป็น nodeๆ จะใช้การแบ่งที่บรรทัดที่มีการกระโดดในแบบต่างๆ
เราจะได้ node และคำสั่งใน node นั้นๆมา
ต่อมาในการลากเส้นเชื่อมในแต่ละ node เราใช้เทคนิค construct static edges ในการลากเส้นของ case ที่ไม่มีการกระโดดบรรทัดที่ต้องคำนวณค่าจาก stack
เราจะแกะส่วนไหนต่อ ?
เราจะแกะ code ในส่วน
- การลากเส้น CFG ที่ต้องคำนวณค่าจาก stack
- เอา path ที่ unreachable ออกด้วย z3
โอเค มาเริ่มกัน
เริ่มจากการประกาศตัวแปรไว้
- ทดค่าใน stack
- เป็น input เงื่อนไขการทำงานของยอด balance ของ evm
- จำ node ที่เคยไปแล้ว
- ทดค่าใน memory
จากนั้นป้อน input เงื่อนไขการทำงานของยอด balance ของ evm ให้ z3
เริ่มรันจาก node แรก
โดยในแต่ละ node จะจำลองการทำงานของ evm เมื่อรันแต่ละ opcode โดยทดค่าใน stack memory และ storage
ซึ่งผลลัพธ์จากการทดค่าของ stack ทำให้เราสามารถลากเส้น CFG ได้ถูก เช่น JUMP ก็จะ pop ค่าจาก stack แล้วไปยังตำแหน่งนั้น
หรือ JUMPI ก็จะ pop position ที่จะ jump และ condition ในการ jump ออกมา ซึ่งเราจะจำ condition นั้นไว้ก่อน เพื่อใช้ตอน symbolic execution
เมื่อเรากระโดดไปยัง node ต่อไปเรื่อยๆ ก็จะลาก CFG ครบในที่สุด
นอกจากวาด CFG แล้วเราจะกรอง unreachable path ออกจาก CFG โดยใช้ z3 ด้วย
โดยจะเช็คเงื่อนไขว่าการ JUMP สามารถทำได้มั้ย เช่น if(2 > 3) เนี่ย JUMP ไม่ได้
โอเค ประมาณนี้ก่อน ใน part หน้าเราจะมาเริ่มการหา pattern ของช่องโหว่จาก CFG กัน
Referrences:
https://eprint.iacr.org/2016/633.pdf
Useful resource:
เจอ cfg builder https://github.com/crytic/evm_cfg_builder ที่ทีม trail of bits ใช้กันด้วยแหะ น่าลองใช้เหมือนกันนะ
