note: Learn how to fuzz like a pro: Fuzzing Arithmetics

video note

Summary

เป็น video ที่สอนการเทคนิคการ fuzzing smart contract ด้วย ehidna โดยเทคนิคที่จะสอนคือ

• การใช้ config file เพื่อเก็บ setting ของ echidna
• การทำ pre-condition เพื่อ bound กำหนดขอบเขตการ fuzz
• การกำหนด action ที่จะ test การทำงาน
• การกำหนด post condition เพื่อที่จะ debug หรือเปลี่ยนเงื่อนไขการ assert
• การ fuzz rounding error
• การ debug ผลลัพธ์จากการ fuzzing ด้วย event
• การ debug ผลลัพธ์จากการ fuzzing ด้วย try/catch
• การ try/catch เพื่อ test ว่าบรรทัดนั้นๆจะไม่ revert
• การ fuzzing ด้วยการ setup ชุดของ contract ที่จะให้ทำงานด้วยกัน
• การ optimize file test เพื่อให้ echidna ทำงานได้เร็วขึ้น
• differential testing assembly contract
• การดู coverage ของ echidna
• การ guide path การ fuzz ให้ echidna

โดยจะทำการสอนด้วยการ fuzzing

• contract ABDKMath64x64 เป็น library ที่ใช้ในการคำนวณ math operation เช่น log โดยจะทำงานกับ floating point number (จะใช้ 64 bit ในการเก็บทดศนิยม, 63 bit ในการเก็บจำนวนเต็ม และ 1 bit ในการเก็บว่าติดลบมั้ย)

โดยเค้าทำการแก้ตัว lib เพื่อซ่อน bug เอาไว้

• contract staking

เอาละ มาเริ่มกัน

contract ABDKMath64x64

1. การใช้ config file เพื่อเก็บ setting ของ echidna

ในการ fuzz contract โดยกำหนดให้มีการ random function input จะต้องใช้ syntax assert ในการ fuzz ดังรูป

ถ้าเราจะรัน echidna ก็ต้องใส่ arg เป็น assert mode ตลอด

แต่เราสามารถใส่ arg ใน config ไฟล์แทนได้ จะได้ไม่ต้องพิมพ์ยาวๆ

2. การ debug ผลลัพธ์จากการ fuzzing ด้วย event

โดยในการ fuzzing บางครั้งเราก็ไม่รู้ว่าไป bug ที่ function ไหน

เช่น จากรูป เค้า fuzz การทำงานของ add sub ใน ABDKMath64x64 โดย test ว่าตัว lib จะต้อง hold invariant (x+y) — y = x

ซึ่งตัว echidna ทำการระบุ x,y ที่ทำให้เกิด bug มาให้

ประเด็นคือ ใน function test มีทั้งการทำ add และ sub

แล้ว bug เกิดขึ้นในขั้นตอนไหน ?

เราสามารถ debug ได้โดยการ emit event ในแต่ละ step ตามรูปด้านบน

2. การทำ pre-condition เพื่อ bound กำหนดขอบเขตการ fuzz

จากรูป เค้าทำการ test การทำงานของ div โดยการกำหนด invariant

x/y != y/x

แต่ปัญหาคือ invariant นี้เอาไว้ควรเอาไว้ test เมื่อ x != y

ดังนั้นเค้าจึงต้องใส่ require เป็น pre condition เพื่อไม่ให้ echina ให้ผลลัพธ์ที่เป็น false positive ออกมา

3. การกำหนด post condition เพื่อที่จะ debug หรือเปลี่ยนเงื่อนไขการ assert

แต่ปัญหาของการใช้ pre condition โดยการ require ก็คือ เราจะไม่ได้ test case ที่เรา skip ไว้

เช่น จริงๆแล้วเมื่อ abs(x) = abs(y) แล้ว ก็ควรจะได้ x/y = y/x สิ

แทนที่จะทำ pre condition เราสามารถทำ post condition ได้แทน เป็น

4. การ optimize file test เพื่อให้ echidna ทำงานได้เร็วขึ้น

โดยปกติแล้ว echidna จะกำหนดรอบในการ fuzz อยู่ เช่น 50k รอบ

แต่ถ้าเราทำ pre condition ไว้ เข้าใจว่า เราจะเสียรอบบางส่วนไปเมื่อไม่ผ่าน require

โดยเราสามารถ optimize เพื่อให้ไม่เสียรอบไปเปล่าๆ

ด้วยการแก้ให้ค่าที่ fuzz มาไม่มีทางติด require แทน

โดยนอกจากวิธีนี้ จริงๆการกำหนด require ที่มีโอกาส revert น้อยมากๆ หรือการใช้ % เพื่อ bound state แทน require ก็ใช้ได้เหมือนกัน

5. diffenetial testing assembly contract

อันนี้เป็นการพูดถึงการใช้ fuzzing กับ assembly contract แบบคร่าวๆ

โดยการ test assembly contract เราสามารถใช้วิธี differential testing ได้

โดยการเขียน contract ใน version non assembly มา 1 อัน

แล้วทำการ fuzz test ทั้ง assembly และ non assembly version ไปพร้อมๆกัน

ถ้าผลลัพธ์ไม่เหมือนกัน แสดงว่า การเขียนใน assembly มีส่วนที่ไม่ตรงกับ version ที่เราทำใน non assembly ละ

6. การ fuzz rounding error

หัวข้อนี้ อธิบายคร่าวๆ และให้เป็นการบ้านแทน

contract staking

1. การ fuzzing ด้วยการ setup ชุดของ contract ที่จะให้ทำงานด้วยกัน

ก่อนหน้านี้ เวลาเรา fuzz เราก็มักจะ inherit target มา แล้วเขียนไฟล์ fuzz

ปัญหาคือถ้า target ที่ต้อง fuzz มีหลายตัว และทำงานร่วมกัน วิธีนี้จะงานเยอะมากๆ

เพื่อแก้ปัญหา เราจะเปลี่ยนวิธีเป็นการ deploy target ที่ต้อง fuzz แล้วทำการ test การทำงานร่วมกันในที่เดียวแทน

ข้อเสียของวิธีนี้คือเราจะไม่สามารถเปลี่ยน msg.sender ที่เห็นบน target ได้ (เพราะเราใช้ middle man ติดต่อแทน ตามรูป)

โดยวิธีนี้จะเขียนคล้ายกับการ test ใน foundry … ทำการ deploy ทุก contract แล้วค่อย test

โดยถ้าเรามีการ import contract ต่างๆเข้ามาเพื่อ test ให้เรากำหนด destination ในการ test เป็น folder แทน เช่น . คือ ทุกๆไฟล์ใน folder นี้

เพื่อให้ echidna รู้ว่าต้องหาไฟล์ที่ import มาจากไหน

2. การดู coverage ของ echidna

จากรูปเค้าทำการ test การทำงานของ stake

โดย invariant คือ หลัง stake แล้ว เงินของคน stake จะต้องลดไป เท่ากับ ยอด stake ที่ update ใน contract

จะเห็นได้ว่ามีการใช้เทคนิค bounding เพื่อ optimize ด้วยการ 1 + และ % ด้วย

แต่ประเด็นคือหลัง fuzz เสร็จ echidna ให้ผลการ coverage มาเป็น

จากรูปเราจะเห็นได้ว่ามีเครื่องหมาย r มาถึงบรรทัด require

หลังจากนั้นไม่มีเครื่องหมายอะไร

ผลการ coverage นี้แปลว่าอะไร ?

r แปลว่า การรัน test file ที่บรรทัดนั้น revert

และไม่มีเครื่องหมายการ test case ที่ fuzz มา ยังรันไปไม่ถึง test file บรรทัดนั้น

กลับมาดูรูปกันอีกรอบ

นี่แปลว่าการ fuzz ยังไม่มี case ไหนผ่าน require เข้ามาเลย

เหตุผลเป็นเพราะว่า ตัว ERC20 ที่ใช้ test ไม่สามารถทำการ mint ผ่านตัว fuzzer ได้

จึงไม่มีเหรียญไปเรียก stake

เค้าเลยแก้ให้ทำการ mint ได้ตรงๆ

แต่เข้าใจว่าจริงๆแล้วไม่ต้องเรียก mint ใน constructor เองก็ได้ echidna มีโอกาสที่จะ fuzz ไปเรียก mint ได้เอง

3. การ guide path การ fuzz ให้ echina

แต่ถ้าเราไม่อยากให้ echidna ข้ามการเรียก mint

โดยที่เราก็ไม่อยากมาเรียก mint ก่อนการ test เองด้วย

เราสามารถ guide echidna โดยเพิ่มการ function test การ mint ไปใน file test เพื่อให้ echidna ลองทำการเรียน function mint ดู จะได้เอาไปใช้ในการ fuzz ต่อไปถูก นั่นเอง

โอเค กลับมาที่การดู coverage report กันหน่อย

โดยนอกจากการดูว่า test file บรรทัดไหนถูกรันยังไงบ้าง

เรายังสามารถดูได้ว่า contract บรรทัดแต่ละบรรทัด รันแล้วเป็นยังไง ได้ด้วย

เช่น พอเราเพิ่มให้ mint ได้ไปละ แล้วมา test อีกรอบ

เราจะเจอว่าเมื่อ stake แล้ว ก็ติด revert ตลอด ไปไม่ถึง assert สักที

โดยเมื่อมาดู coverage ของตัว contract จะพบว่าติดที่บรรทัด transferFrom เพราะมี allowance ไม่พอนั่นเอง

โดยเค้าแก้โดยการยกเลิกการเช็ค allowance ไปเลย เพื่อให้ test ต่อได้

โอเค สุดท้ายเค้าก็สามารถทำให้ echidna ทำการ coverage test ทุกบรรทัดบน file test ได้

โดยตัว contract function stake เอง ก็ coverage ทุกบรรทัดเช่นกัน

โดยในบางบรรทัดจะมีหลายเครื่องหมายผสมกัน

เช่น *r แปลว่า มีทั้ง case ที่ไม่ผ่าน require และ case ที่ผ่าน require นั่นเอง

4. การ try/catch เพื่อ test ว่าบรรทัดนั้นๆจะไม่ revert

ปกติแล้วถ้าบรรทัดอันไหน revert echidna จะไม่สนใจ แล้วไป test case ต่อไปต่อ

แต่เราสามารถ test เพื่อเข็คว่าจะไม่มีการ revert เกิดขึ้นได้

โดยทำการ try catch แล้วใส่ assert(false) ใน catch

5. การ debug ผลลัพธ์จากการ fuzzing ด้วย try/catch

ประเด็นคือ พอใส่ try/catch ไปแล้ว

1. ถ้าไม่ error … ทำไมถึงไม่ error
2. ถ้า error … ทำไมถึง error

เราสามารถ emit ค่าทั้งใน try และ catch เพื่อ debug ได้

โดยนอกจากการ try catch เรายังสามารถทำการ debug ด้วยกันไม่ให้ error bubble ออกมา โดยใช้ syntax call ได้เช่นกัน

Reference