formal verification smart contract part 1
มาลองดูการทำ formal verification บน smart contract โดยใช้ why3 กัน
fyi: บทความนี้เป็นการศึกษาตาม clip นี้ ซึ่งเป็น clip เก่าแล้ว (ปี 2016) และ demo ใน clip ไม่สามารถทำงานได้แล้ว เนื่องจาก remix ได้เอา feature แปลง solidity to why3 ออกตั้งแต่ปี 2017 แล้ว ส่วนตัวยังไม่เคยทำ formal verification เหมือนกัน ถือว่าเป็นการลองดู demo เพื่อทำความเข้าใจ concept formal verification แล้วกันนะ
formal verification in my own word
คือการทดสอบว่า โปรแกรม ตรงตามเงื่อนไข รึเปล่า โดยไม่จำเป็นต้องระบุ input หรือ state ใดๆ ของโปรแกรมนั้น เช่น
จากโปรแกรม
เราจะ test การทำงานของ function transfer โดยเราคาดหวังให้ จำนวนเงิน จาก from ไปยัง to ได้อย่างถูกต้อง
จะเห็นได้ว่าปัญหามี 2 ส่วนคือ
- if(balances[from] > amount) เขียนผิดอยู่ต้องเป็น ≥ amount
2. balances[from] -= amount สามารถถูกโจมตีด้วย underflow/overflow ได้รึเปล่า … อันนี้ไม่มั่นใจว่า เงื่อนไข if(balances[from] > amount) กันได้มั้ยแหะ แต่นั่นแหละคือสิ่งที่ทำให้เราต้อง test แล้วจะ test แบบไหนดี ?
ถ้าเขียน unit test ?
จะต้องระบุ parameter ที่เป็น input เอง โดย เราต้องจูนค่าต่างๆเอง ให้ตรงกับ test ที่เราต้องการเช่น
case 1:
set state ให้ balances[from] = 20
set input ให้ amount = 21
case 2:
set state ให้ balances[from] = 20
set input ให้ amount = 20
case 3:
case 1:
set state ให้ balances[from] = 20
set input ให้ amount = 19
case xxx: …
จะเห็นได้ว่าปัญหาของการเขียน unit test คือ เราจะ test ได้แค่ตามจำนวน test case ที่เราป้อนเข้าไป
แต่ถ้าเราใช้ formal verification ละ ?
เราสามารถระบุเงื่อนไขที่เราอยากทดสอบโปรแกรมได้เลย โดยไม่ต้องระบุ input และ state เช่น sum balance ของทุกๆ account เท่ากัน ก่อนและหลัง การเรียก transfer รึเปล่า ?
โอเค งั้นเรามาลองดูตัวอย่างการทำ formal verfication โดยใช้ why3 กัน
จากโปรแกรม
เราจะทดสอบกันว่าโปรแกรมนี้ทนทานต่อ reentrancy attack รึเปล่า
โดยวิธีการที่ใช้คือเราจะเขียน comment เงื่อนไขที่เราอยากทดสอบโปรแกรมลงไป
เช่นการทำงานของ transfer คือ
ก่อนเรียก transfer shares = 30, balance contract = 30
เรียก transfer ด้วย amount = 20
หลังเรียก transfer ถ้าทำ reentrancy attack ไม่ได้ … shares = 10, balance contract = 10
หลังเรียก transfer ถ้าทำ reentrancy attack ได้ … shares = 10, balance contract = 0
ดังนั้น ถ้า transfer ทนทานต่อ reentrancy attack แสดงว่าจะได้เงื่อนไข
ค่าตัวแปร shares ก่อนการเรียก function ใดๆ — balance contract ก่อนการเรียก function ใดๆ = ค่าตัวแปร shares หลังการเรียก function ใดๆ — balance contract หลังการเรียก function ใดๆ
ตาม comment ในรูป
อันนี้ไม่นับรวมกรณีที่มีการส่ง ether มาตรงๆเวลาเรียก transfer ละนะ
โดยเราจะแปลงไปเป็นภาษา why3
โดยเมื่อเป็นภาษา why3 แล้ว จะสามารถบอกได้แล้วว่า โปรแกรม ผ่านเงื่อนไขที่ตั้งไว้รึเปล่า
จากภาพเราจะเห็นได้ว่า โปรแกรมตรงตามเงื่อนไขที่ตั้งไว้ แม้ว่าจะอยู่ใน state หรือมี input เป็นแบบไหน
เช่น ใน case integer overflow ตามภาพ จะพบว่าโปรแกรมเราผ่าน นั่นคือไม่เกิด integer overflow
และจะเห็นได้อีกว่าตัวโปรแกรมได้รันถึง 3 ความเป็นไปได้ ในการทดสอบเงื่อนไขที่ตั้งไว้ (3 post condition)
อันนี้น่าจะมาจาก 2 if ในโปรแกรม โดยน่าจะเอา case TT, TF, FF ส่วน FT น่าจะไม่เอา เพราะเป็น if ซ้อน if เลยไม่มี case นี้เกิดขึ้น
โอเค สรุปแล้ว formal verification จะทำให้เราสามารถทดสอบทั้ง desired/undesired behavior ได้ โดยไม่ต้องระบุ input หรือ mock state เอง
reference
