note: มาดูการ formal verify WETH กัน (Part 2)
มาดูการใช้ Z3 ทำ symbolic execution กัน
fyi: เป็นบทความแปลจาก https://www.zellic.io/blog/formal-verification-weth + ใส่เนื้อหาเพิ่มนะครับ
Introduction
ใน part ที่แล้ว เรา formal verify ด้วย CHC based approach ไปแล้วว่า totalSupply() ≤ sum balanceOf(address) เสมอ
ใน part นี้ เราจะมา formal verify กันว่า ผู้ถือ WETH สามารถถอน native ETH ออกมาได้เท่ากับที่ถือตลอดมั้ย
โดยเราจะทำ formal verify ด้วย CHC based approach เหมือน part ที่แล้วก็ได้
แต่ดูจะไม่ค่อยเหมาะเท่าไหร่
เพราะถ้าทำแบบ CHC based เราจะไม่สามารถจำลองการเรียกตาม Control flow ของ contract WETH ซึ่งเป็น ERC20 ได้
เช่น การเรียก approve ก่อน transferFrom
ก่อนหน้านี้เราใช้พวกฟังก์ชันที่ไม่ต้องเรียกต่อกันมาตลอด เลยโอเคที่จะใช้ CHC based approach ในตอนนั้น
แต่ตอนนี้เราต้องเปลี่ยนมาใช้ symbolic execution based approach แล้ว
Background
Symbolic execution ?
คือเทคนิคนึงในการวิเคราะห์โปรแกรม โดยคำนวณค่าที่เป็นไปได้ของแต่ละตัวแปรในแต่ละบรรทัด ซึ่งจะทำให้เราสามารถรู้ได้ว่าโปรแกรมสามารถไปถึงเงื่อนไขที่เราคาดหวังได้รึเปล่า
เช่นจากโปรแกรม
ถ้าแปลงเป็น flow ในการรันโปรแกรมคงได้ประมาณนี้
- ส่ง x,y และ ,msg.value ไปเป็น input
- เนื่องจากไม่มี payable ถ้า msg.value > 0 ก็จะ revert
- ในบรรทัด require ถ้า x+y ≥ x จะ return แต่ถ้าไม่ ก็จะ revert
แต่นอกจาก
- path ทั้งหมดที่เกิดขึ้นในการรันโปรแกรม
- ผลลัพธ์ของ path นั้นๆ
อีกคำถามนึงคือ
แต่ละตัวแปรใน path นั้นๆ มีค่าที่เป็นไปได้ในช่วงไหนบ้าง ?
เช่นใน path 1–1 เราจะได้ว่า
- msg.value == 0
- x + y ≥ x
ซึ่งการรันโปรแกรม โดยคำนวณค่าที่เป็นไปได้ของแต่ละตัวแปรในแต่ละบรรทัดไปเรื่อยๆ เรียกว่า symbolic execution
โอเค ทฤษฎี ประมาณนี้ ไปดูตัวอย่างกัน
Methods
มาดูการเขียน symbolic execution ด้วย Z3 กัน
โดยมี 2 ขั้นตอนคือ
- แปลง code เป็น symbolic execution
เริ่มจาก function approve ของ WETH ซึ่งมี solidity code ดังนี้
ซึ่งสามารถแปลงเป็น code Z3 (Z3Py) ได้เป็น
โอเค มาไล่ทีละบรรทัดกัน
ดึงค่าที่เป็นไปได้ทั้งหมดออกมา
จาก code solidity เราแปลงเป็น Z3Py ใน logic เดียวกันได้ นั่นคือ
x = allowance[msg_sender][guy]
x = wad
y = allowance[msg_sender]
y = x
allowance = y
ที่เข้าใจคือให้คิดว่า คล้ายๆกับการเขียนโปรแกรมแบบ AST ประมาณว่าไม่มี pointer ต้องชี้เองไปทีละนิด
ส่วน event เราจะไม่ได้เอามาคำนวณ
สุดท้าย เราจะ return ค่าที่เป็นไปได้ออกไป
โอเค function approve จบละ ต่อมาก็ deposit
จาก solidity code
พอเขียนเป็น Z3Py จะออกมาเป็น
โอเคมาดูทีละบรรทัดกัน
เนื่องจากเป็น payable function ดังนั้นเราต้องเช็คว่า address(msg.sender) ≤ msg.value เสมอ
และทำการลด/เพิ่ม native ETH balance ของ msg.sender และ WETH contract ตาม msg.value
จากนั้นก็ทำการชี้ balanceOf ไปยัง mapping(address => โดยที่ balanceOf[msg.sender] + msg.value)
เช่นเดียวกับ approve เราจะไม่สนใจ event
โอเค deposit ก็ประมาณนี้ ไปต่อกันที่ transferFrom เลย
transferFrom ของ WETH มี solidity code ดังนี้
โดยเราสามารถแปลงเป็น Z3Py ได้เป็น
โอเค เรามาดูทีละบรรทัดกัน
เช็ค balanceOf ว่าพอมั้ย ตรงนี้เค้าต้องเขียน function สำหรับการ require ใน z3py เองด้วยแหะ
syntax บรรทัดอื่นคล้ายๆกัน แต่จะมีบรรทัดที่แปลกหน่อยคือ
ซึ่งมาจาก solidity code
จริงๆแล้ว If ใน solidity ครอบทั้ง 2 บรรทัดใน {} เลย
แต่เหมือน z3py จะเขียน If ครอบทีละหลายๆบรรทัดไม่ได้
เลยต้องใส่ If แยกไปในแต่ละบรรทัดแทน ตามรูป
ซึ่ง impile ก็คือ ถ้า แล้ว โดยใน case นี้เรานำมาใช้แทน if นั่นเอง
โอเค การประกาศ function จะประมาณนี้
เค้ามีพูดถึง loop ด้วย แต่ไม่มีตัวอย่างแหะ
2. เขียน proof
เค้าใช้ Principle of induction ในการพิสูจน์
เราลองมาดูกันก่อนว่า Principle of induction คืออะไร
ถ้าเรามีสมมติฐานคือ
ซึ่งพอแทนเลขลงไปเรื่อยๆ ก็ดูเหมือนจะเป็นจริงตลอด
แต่เราจะรู้ได้ยังไงว่า สมมติฐานนี้จะเป็นจริงตลอดในทุกๆ n
หนึ่งในวิธีพิสูจน์ทางคณิตศาสตร์คือการใช้ Principle of induction ซึ่งประกอบด้วยขั้นตอนดังนี้
- ยกตัวอย่าง case ที่สมมติฐานนี้เป็นจริง เรียกว่า base case
2. จากนั้น พิสูจน์ว่าเมื่อมี case หนึ่งเป็นจริงแล้ว เราสามารถพิสูจน์ได้ว่าอีก case หนึ่งจะเป็นจริงด้วย เราเรียก case นี้ว่า inductive case
โอเค มาลองดูกัน
เริ่มจาก base case กันก่อน
เหมือนเค้าจะไม่เขียน base case ใน z3py แหะ น่าจะต้องไปเขียน unit test แยกเอง แล้วเอาผลลัพธ์มาดูว่าเป็นจริงทั้ง base case และ inductive case มั้ย
โอเคมาดู inductive case กัน
โดยในการเขียน inductive case จะมีขั้นตอนคือ
- ประกาศ state
เริ่มจากการประกาศ start stateโดยกำหนด state ต่างๆที่ต้องใช้ และ address ของ user
2. ประกาศเงื่อนไขเพิ่มเติมในการ proof
ซึ่งเงื่อนไขพวกนี้ช่วยในการลดเวลา proof ได้
ใน part ที่แล้วเราพิสูจน์แล้วว่า totalSupply ของ WETH ≤ balance native ETH ของ WETH ดังนั้นเราสามารถนำมาเขียนเป็นเงื่อนไขได้เลย
และเราต้องเขียนเงื่อนไขเพิ่ม เพื่อจำลองการทำงานของ evm ด้วย เช่น ไม่มี address ไหนมี native ETH มากกว่าจำนวน native ETH ทั้งหมด
3. ประกาศ assumption
ต่อมาคือการ assumption โดยเราจะตั้งด้วย case ที่ยังไม่มีใครมี WETH และยังไม่มีการ approve เกิดขึ้น
จะเห็นได้ว่าเราต้องกำหนดด้วยว่า address ของ user ไม่เท่ากับ address WETH ซึ่งเป็นเงื่อนไขของ evm ที่เราต้องเขียนมือเอง
โอเค สุดท้ายเราทำการ deposit ไป เพื่อที่จะพิสูจน์การ withdraw ในภายหลัง
โอเค จบการ assumption ละ เหมือนเค้าค่อนข้างย้ำเรื่อง don’t do over assumption แหะ อันนี้เหมือนเป็น bare minimum assumption เลย
4. run symbolic transaction
โดยทำการรัน proof ย่อยๆ ดังนี้
deposit แบบ symbolic โดยให้ user อื่น deposit เข้าไป ถ้าเป็น user ตัวเอง เดาว่า พอมาเช็ค balance ทีหลังน่าจะเช็คยาก เลยให้ deposit รอบเดียว
แล้วลอง withdraw ดูว่า error มั้ย
จากนั้นก็ทดสอบ proof อื่นๆแยกกันไป
- proof คนอื่น withdraw แล้ว เรา withdraw ไม่ error
- proof คนอื่น approve แล้ว เรา withdraw ไม่ error
- proof คนอื่น transfer แล้ว เรา withdraw ไม่ error
- proof คนอื่น transferFrom แล้ว เรา withdraw ไม่ error
จุดที่น่าสนใจคือ เค้าไม่ได้บอกให้ z3 proof ว่า สมมติฐาน satisfiable ในทุกๆเงื่อนไข แต่เค้าบอกให้ proof ว่า unsatisfiable ในการพยายามทำให้สมมติฐานไม่เป็นจริง ตามรูป
Result
z3py พบว่า การพยายามทำให้ สมมติฐาน “ผู้ถือ WETH สามารถถอน native ETH ออกมาได้เท่ากับที่ถือตลอด” ให้เป็นเท็จนั้น ไม่สำเร็จ
ดังนั้น สรุปได้ว่า ผู้ถือ WETH สามารถถอน native ETH ออกมาได้เท่ากับที่ถือตลอด
โดย z3py จะสามารถ list มาได้ด้วยว่าติด assert ตรงไหนบ้าง เลยทำให้การพยายาม hack ไม่สำเร็จ
ซึ่งถ้า assert ที่เราใส่ไปไม่ได้อยู่ในนี้ แสดงว่าการใส่ assert นั้น ไม่ได้จำเป็นต่อการป้องกันการ hack นั่นเอง
Limitation
จริงๆแล้ว เค้าสามารถใส่ reentrancy เข้ามาใน code ได้ แต่เค้า assume ว่า 2300 gas ไม่พอต่อการทำ reentrancy เลยข้ามไป
โอเค ประมาณนี้ก่อนแล้วกัน การเขียน z3 เองน่าจะใช้เวลาเยอะอยู่แหะ เราลองมาดูกันต่อไปว่าถ้าเราจะสร้าง tool based on symbolic execution เนี่ย เราไปท่าไหนได้บ้าง
