การใช้ halmos ในการทำ symbolic execution

a note from an excellent presentation by 0xKarmacoma

โอเค มาเริ่มกัน

โดยเค้าจะ test properties เหล่านี้ ของ function transferFrom ของ WETH

โอเค เริ่มจาก

address ที่ไม่ได้เกี่ยวข้องกับการ transferFrom ควรมี balance WETH เท่าเดิม

ตัว syntax เค้า เหมือนกับการใช้ Foundry test ปกติเลยนั่นแหละ

โดยอันนี้จะนับเป็นการทำ functional testing เพราะเราระบุเลยว่า จะให้ file test ทำการ transferFrom

โดยในการทำ symbolic execution ตัว Halmos จะทำการแทนค่าตัวแปรให้เป็นค่า symbolic แทน

โดยจะทำการลองรัน code ในทุกๆ path เพื่อหาว่า ถ้าไปจนสุดทางใน path นั้นๆ จะทำให้ assert เป็น false ได้ไหม

ตัวอย่างก็จะคล้ายๆรูปนี้

https://dl.acm.org/doi/pdf/10.1145/2389836.2389853

โอเค มายกตัวอย่างกัน

เช่น path แรกที่ไปให้สุดคือ balance ของ from ไม่พอกับ amount ที่จะโอน

ก็จะได้ว่า assert ยังเป็น true

path ที่ 2 คือ balance พอให้โอน และ msg.sender เป็นคนโอนเอง จะได้ว่าไม่ต้องเช็ค allowance

พอไปจนสุด path เราจะได้ symbolic ของแต่ละตัวแปร

เช่น

src = src (ไม่ได้เปลี่ยนค่า)

dst = dst (ไม่ได้เปลี่ยนค่า)

wad = wad (ไม่ได้เปลี่ยนค่า)

balanceOf[src] (after) = balanceOf[src] (before) — wad

balanceOf[dst] (after) = balanceOf[src] (before) + wad

PC =

call value == 0 && balanceOf[src] ≥ wad && src == msg.sender

จะเห็นได้ว่าตัว symbolic value สุดท้ายที่ได้ จะประมาณว่า

call value == 0

&& balanceOf[src] ≥ wad

&& src == msg.sender

&& balanceOf[src] (after) = balanceOf[src] (before) — wad

&& balanceOf[dst] (after) = balanceOf[src] (before) + wad

ซึ่งก็ยังทำให้ assertion balanceOf[gal] (after) == balanceOf[gal] (before) && gal != srt && gal != dst เป็น true อยู่

แสดงว่าใน path นี้ เมื่อไปจนสุด ก็ยัง test ผ่านนั่นเอง

จากนั้น Halmos ก็จะทำแบบนี้เรื่อยๆจนครบทุก path

ถ้าผ่านการเช็ค assertion ครบทุก path ก็จะแสดงว่าตัวโปรแกรมผ่านการทำ formal verification ด้วยเทคนิค symbolic execution นั่นเอง

โดย symbolic execution จะเหนือกว่า fuzzing ตรงที่ จะเป็นการบอกได้ 100% เลยว่า bug นี้จะไม่เกิดขึ้น (เพราะใช้ math มาเทียบค่าที่เป็นไปได้เลย) แต่ fuzzing ที่ใช้การสุ่มค่า เพื่อให้เข้าถึง path ต่างๆได้ อาจจะสุ่มโดนเลขที่ทำให้เกิด bug หรือไม่ก็ได้

แต่การทำ symbolic execution เพียวก็จะมีข้อเสียเหมือนกัน เช่นการไปรันกับโปรแกรมที่มี loop ทำให้ต้องทำการหา symbolic value ของการรันใน loop ไปเรื่อยๆ ไม่รู้จบ … ก็ต้องอาศัยการ optimize ของ Halmos ละนะ

โอเค มา part ต่อไปกัน

ตัว test ที่เพิ่งทำไป จริงๆแล้วจะไม่ได้ไปทุก path ซะทีเดียว

เช่น path allowance < wad

นั่นเป็นเพราะว่า เราไม่ได้บอกให้ Halmos ทำการทำ symbolic value ของตัวแปร allowance ตาม code

ซึ่งแก้ได้โดยการให้ทำการ approve ด้วย symbolic value ตาม code

note: รู้สึกว่าถ้าใช้ certora น่าจะทำการ symbol ค่าตัวแปรได้เลย โดยไม่ต้องบอกว่าจะใช้ function ไหนในการเปลี่ยนค่านั้นรึเปล่า ? ไว้ค่อยว่ากันละกัน

เราจะได้ว่า path allowance < wad ถูก visit ได้แล้ว

note: ภาพนี้เค้าน่าจะต้องคิดเองมั้ง ถ้าเป็น echidna จะมีไฟล์ map บอกว่า line ไหนถูกรันบ้าง ไม่รู้ว่า Halmos จะมีกับเค้าไหม

เอาละ ตอนนี้รัน Halmos ผ่านตลอดเลย

ถ้า Halmos ใช้ได้จริง แสดงว่า ถ้าเราเปลี่ยนไป test contract อื่นๆ ที่ไม่ใช่ WETH … Halmos ควรจะต้อง error บ้าง

เช่นถ้าไปรันกับ contract ERC20 fee on transfer

ก็จะได้ว่า error เนื่องจาก gal หรือก็คือคนรับ fee มี balance ที่เปลี่ยนไปด้วยนั่นเอง

จากตัวทฤษฎีเอง ไม่ว่าจะเป็น fuzzing หรือ symbolic execution ก็ยังคงเจอปัญหากับการ test โปรแกรมที่มี path เยอะมากๆ อย่างที่เคยบอกไปอยู่ดีละนะ … ดังนั้นการ implement ก็จะต้องพยายาม optimize จุดนี้

โดยเค้าแนะนำให้ใช้คู่กันไปเลยละนะ

Reference