note: มาดูการ Formal verify WETH กัน (Part 1)
มาดูกันว่า WETH จะมีช่องโหว่มั้ย
เป็นบทความแปลจาก https://www.zellic.io/blog/formal-verification-weth + ใส่เนื้อหาเพิ่มนะครับ ไม่มี hands on guide โอเค มาดูการใช้ Z3 ในการทำ formal verification กัน
Background
Formal verification ?
คือการพิสูจน์ว่าโปรแกรมสามารถทำงานได้ถูกต้อง ตามเงื่อนไขที่เราตั้งไว้มั้ย อธิบายประมาณนี้ก่อน เดี๋ยวเราไปดูตัวอย่างกัน
Z3 (Z3 Theorem prover) ?
Z3 คือ โปรแกรมที่ใช้ในการทำ SMT solver โปรแกรมนึง
SMT solver ?
SMT solver ย่อมาจาก (satisfiability modulo theories solver) หรือ SAT solver
เรามาลองยกตัวอย่างจาก logic กัน
ถ้าเรามี program นึง ซึ่งทำงานตามรูป
ต่อมาเราต้องการเปลี่ยนแปลงโครงสร้างภายในของ program โดยคาดหวังว่าจะมีการทำงานเหมือนเดิมดังรูป
ถ้าเราพิสูจน์ว่าทั้ง 2 โปรแกรมสามารถทำงานได้เหมือนกัน 100% มั้ย ? จะทำยังไงได้บ้าง
วิธีนึงที่ทำได้คือการแปลงทั้ง program เป็น boolean expression ดังรูป
โดยเราจะนำ boolean expression ให้กับ solver เพื่อหาว่า boolean expression สามารถทำงานตามที่เราคาดหวังได้มั้ย
ผลการทำงานของ solver จะแบ่งได้ 2 แบบคือ
- สามารถทำงานตามที่คาดหวังได้ โดย solver จะให้ตัวอย่าง input มาด้วย ตามรูป
2. ไม่สามารถทำงานตามที่คาดหวังได้ โดย solver จะให้ proof มาด้วย
โอเค บทความนี้ เราจะไม่ลงเรื่อง SMT solver ลึกไปกว่านี้ ไปดูการใช้ SMT solver (Z3) ทำ formal verification กัน
Methods
เค้าทำอะไร ?
ทำ formal verification ของ contract WETH โดยทดสอบ 2 อย่างคือ
- totalSupply ต้องเท่ากับ sum ของทุกๆ balanceOf (ทุกๆ account) เสมอ
- account ที่ deposit เข้าไป สามารถถอน native ETH ออกมาได้เสมอ
เค้าใช้ tool อะไรบ้าง ?
- Z3Py
เค้าทำยังไง ?
- พิสูจน์ว่า totalSupply ต้องเท่ากับ sum ของทุกๆ balanceOf (ทุกๆ account) เสมอ
โอเค มาลองดู function totalSupply กันก่อน
จะ return balance native ETH ของ contract WETH ออกมา
โดยปกติแล้วเวลา deposit user ก็จะส่ง native ETH ไป แล้วได้ WETH ออกมาในอัตรา 1:1
และการ withdraw จะเป็นตรงกันข้ามกัน
ดังนั้น ถ้าดูเผินๆ การที่ totalSupply จะเท่ากับ native ETH ของ contract ก็ถูก make sense ดี
แต่ balance native ETH สามารถเพิ่มขึ้นได้ด้วยวิธีอื่นนอกจาก การ deposit ตามภาพ
โอเค มาเริ่มจากการกำหนด invariant หรือค่าคงที่ที่เราจะใช้ในการพิสูจน์กันก่อน
โดยประกอบด้วย
- balanceOf เป็น mapping(address => uint256) โดยจะเป็นตัวแปรที่ใช้เก็บ balance WETH ของทุกๆ account
- weth_balance เป็น uint256 โดยใช้แทนค่าที่ได้จาก totalSupply
- eth_supply เป็น uint256 โดยใช้แทนจำนวน native ETH ทั้งหมดที่อยู่นอก contract WETH
โอเคเราได้ค่าคงที่ที่จะใช้พิสูจน์ หรือ state tuple มาละ คือ
(balanceOf, weth_balance, eth_supply)
แต่มีวิธีการไหนบ้างที่จะใช้เปลี่ยนค่าเหล่านี้ได้
deposit สามารถใช้ update balanceOf และ weth_balance ได้
โดยสามารถเขียนเป็น rule ได้ดังนี้
โอเค มาดู code ของ rule นี้กัน
ซึ่งอันนี้เค้าเขียนตามหลักการ CHC โดยอยู่ในรูปแบบ
นั่นคือ
ถ้า State เป็น state ที่เรารู้จัก และเงื่อนไข p เป็นจริง แล้ว ให้อัพเดท State ด้วยค่าที่ได้จาก rule นี้
ดูเข้าใจยากอยู่ มาลองดู code ทีละส่วนกัน
ทุกๆ balanceOf, weth_balance, eth_supply, msg_sender, msg_value ให้ใช้ rule ดังนี้
Implies = (ถ้า,แล้ว)
โดย
ถ้า คือเงื่อนไขที่เกิดขึ้นในการ deposit
แล้ว คือ ผลลัพธ์จากการ deposit
ดังนั้นข้างล่างนี้คือ
ถ้า
state ของ balanceOf, weth_balance, eth_supply, sum_balanceOf น่าจะเหมือนเป็นการป้อนตัวแปรให้ rule นี้
และ ULE(msg_value, eth_supply) คือ msg.value ≤ eth_supply เสมอ
และ balanceOf(msg_sender) ≤ sum_balanceOf อันนี้ใส่ไว้เพราะ z3 ไม่มี sum ของ array มาให้ใช้
แล้ว
- balanceOf ซึ่งก็คือ mapping(address => uint256) จะเปลี่ยนแปลงไป โดย ค่าจะเปลี่ยนไปดังนี้ balanceOf[msg.sender] = balanceOf[msg.sender] + msg.value
- weth_balance ซึ่งก็คือ balance native ETH ของ contract WETH จะเปลี่ยนไปเป็น address(this).balance = address(this).balance + msg.value
- eth_supply ซึ่งก็คือจำนวน native ETH นอก contract WETH จะเปลี่ยนไปเป็น eth_supply = eth_supply — msg.sender
- sum_balanceOf อันนี้จริงๆถ้า Z3 มี function sum array ให้ใช้ เราก็มีแค่ตัวแปร balanceOf mapping(address => uint256 )ด้านบน อย่างเดียวก็พอ แต่เนื่องจากไม่มี sum array ดังนั้นเราก็คำนวณ sum ของทุกๆ account เอง โดย sum_balanceOf = sum_balanceOf + msg.value
โอเค จบ rule deposit ละ
มีวิธีไหนอีกบ้างที่เปลี่ยนค่า (balanceOf, weth_balance, eth_supply) ได้ ?
ตามภาพเลย
โอเค พอกำหนด rule เสร็จแล้ว
ต่อมาคือการกำหนดค่าเริ่มต้นให้ state (balanceOf, weth_balance, eth_supply) โดยกำหนดตามภาพ
โดยเค้าไม่สามารถให้ Z3 prove ตรงๆได้ว่า satisfied หรือ unsatisfied ได้ เค้าเลยใช้ Z3 เขียนตัว prove เองโดยใช้หลักการของ CHC (ไว้ถ้ามีโอกาสจะมาลงลึกกันว่า CHC คืออะไร สัมพันธ์กับ SMT solver ยังไง)
โอเค เค้าเขียน CHC ด้วย Z3 ด้วยวิธีการดังนี้
ประกาศ State() ไว้เก็บค่าทั้งหมดที่เป็นไปได้ของตัวแปรแต่ละตัว เมื่อมีการใช้ rule ต่างๆ
โดย State() นี้จะเอาไว้เช็ค ความเป็นไปได้ ของตัวแปรต่างๆทีหลังได้
เช่น
State(K(0),0,0) เมื่อเรามาเช็ค ควรจะเป็น false เสมอ
หรือก็คือ
- ทุกๆ mapping(address => uint256) = 0 และ
- balance native ETH ของ contract WETH = 0 และ
- จำนวน native ETH นอก contract WET = 0
ไม่ควรเป็นไปได้
โอเค กลับมายังสิ่งที่เราต้องการพิสูจน์คือ
totalSupply() เท่ากับ balanceOf ของทุกๆ account หรือไม่
สามารถเขียนเป็น assert ได้ดังนี้
ซึ่งเขียน code ได้ดังนี้
โดยเมื่อเราให้ assert กับ SMT solver ไป ตัว SMT จะทำการเช็คว่าจาก
- rule ทั้งหมด และ
- assert ที่เราต้องการพิสูจน์
สามารถพิสูจน์ได้มั้ยว่า assert นั้นเป็นจริงเสมอหรือไม่ โดยถ้าไม่ก็จะให้ proof มาด้วย
โดยจากการใช้ Z3 เพื่อ implement เค้าเจอปัญหาคือ
- Z3 ไม่สามารถหา sum array ที่จะใช้ในการ prove ค่าผลรวมของ balanceOf = weth_balance ได้ เค้าจึงต้องประกาศตัวแปร sum_balanceOf ซึ่งอัพเดทค่าตาม balanceOf
- โดยปกติแล้ว เมื่อกำหนด rule ใดๆเปลี่ยน Z3 จะต้องวนค่าทุกๆ pre state (state ที่เป็นไปได้ก่อนใช้ rule ) ซึ่งเค้าลดเวลาในการวนค่าทุกๆ balanceOf[address] ด้วยการกำหนด pre condition เพิ่มนั่นคือ
- และลดเวลาในการรัน ด้วยการกำหนดช่วงตัวเลขที่เป็นไปได้เพิ่ม
Result
เมื่อรันแล้วพบว่า unsatisfied หรือก็คือ สมมติฐาน ที่ว่า toltalSupply() เท่ากับ sum ของทุกๆ balanceOf ไม่เป็นจริง
โดย Z3 ให้ step to reproduce มาด้วย
ซึ่งแปลได้สั้นว่าเมื่อมีการทำ self destruct มาจะทำให้สมมติฐานไม่เป็นจริง
โดยจริงๆแล้ว ในการใช้งานจริง ถ้า balance native ETH ≥ totalSupply() ก็โอเคแล้ว เพราะแปลว่ามี native ETH เหลือมากพอ
ดังนั้นเราจะเปลี่ยนสมมติฐานจาก totalSupply() == sum ของ balanceOf เป็น totalSupply() ≥ sum ของ balanceOf
โดยเมื่อรันแล้วจะพบว่าสมมติฐานเราเป็นจริง
โอเค part นี้ไว้แค่นี้ก่อนดีกว่า ไว้มาต่อข้อ 2 (account ที่ deposit เข้าไป สามารถถอน native ETH ออกมาได้เสมอ) กันบทความหน้าครับ
