note: certora_tutorials
/02.Lesson_InvestigateViolations (Part 1)

Nattawat Songsom

3 min readOct 31, 2023

มาลองเรียน Certora กัน

โอเค ผมจะจด note ระหว่างเรียนการเขียน Certora ไปเรื่อยๆ

เริ่มจากบทเรียนนี้เป็นบทเรียนที่จะสอนการ trace error ที่ certora แสดงผล

note: อยู่ดีๆก็รัน certora ที่เป็น vscode extension ไม่ได้แหะ เลยต้องกลับมารัน cli

note2: พอต้องสลับมาเป็น cvl1 ตอนเรียก tutorial เนี่ย จะมี error python นิดหน่อย แต่พอลง package setuptools ก็โอเคละ

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

เราจะ verify contract อะไร ?

เป็น contract สำหรับการ vote โดยจะแบ่ง actor เป็น 2 role คือ

voter คือคนที่ vote ได้
contender คือคนที่ voter ลงคะแนนให้ได้

โอเค มาลองดู spec certora ที่เค้าให้มากัน

เริ่มจาก

// Checks that a voter's "registered" mark is changed correctly -
// if it's false after a function call, it was false before
// if it's true after a function call it either started as true or changed from false to true via registerVoter()
rule registeredCannotChangeOnceSet(method f, address voter) {
 env e;
 calldataarg args;
 uint256 age;
 bool voterRegBefore;
 bool voted;
 uint256 vote_attempts;
 bool black_listed;
 age, voterRegBefore, voted, vote_attempts, black_listed = getFullVoterDetails(e, voter);
 f(e, args);
 bool voterRegAfter;
 age, voterRegAfter, voted, vote_attempts, black_listed = getFullVoterDetails(e, voter);
 
 assert(voterRegAfter != voterRegBefore =>
  (!voterRegBefore && voterRegAfter && f.selector == registerVoter(uint8).selector),
  "voter was registered from an unregistered state, by other function than registerVoter()");
}

โอเค มาดูทีละส่วนกัน

(voterRegAfter != voterRegBefore) => (!voterRegBefore && voterRegAfter)

ตรงนี้ใช้ logic ถ้าแล้ว นั่นคือ ถ้า user เคย registered แล้ว จะไม่สามารถกลับไปเป็น not registered ได้อีก โดยใน code จะไม่อนุญาติให้ voterRegBefore = true และ voterRegAfter = false นั่นเอง

f.selector == registerVoter(uint8).selector

โดยมีอีกเงื่อนไขคือ การเปลี่ยนสถานะจาก not registered เป็น registered จะต้องทำได้ผ่าน function ชื่อ registerVoter เท่านั้น

note: จะสังเกตุได้ว่าพวกค่าที่ใช้เป็น input เช่นค่า voter ที่นำไปเป็น input ให้ getFullVoterDetails เค้าจะใส่เป็น parameter ของ rule แทนการประกาศข้างใน rule เหมือนว่าทำแบบนี้แล้วเวลาค่า input โชว์ในเว็บจะหาง่ายดีแหะ

โอเค จริงๆยังมีอีกหลาย rule แต่มา focus rule ที่เราจะต้องมา debug เป็นอันแรกกัน

// Checks that a each voted contender's points received the correct amount of points
rule correctPointsIncreaseToContenders(address first, address second, address third) {
 env e;
 mathint firstPointsBefore = getPointsOfContender(e, first);
 mathint secondPointsBefore = getPointsOfContender(e, second);
 mathint thirdPointsBefore = getPointsOfContender(e, third);
 
 vote(e, first, second, third);
 
 assert(getPointsOfContender(e, first) - firstPointsBefore == 3, "first choice received other amount than 3 points");
 assert(getPointsOfContender(e, second) - secondPointsBefore == 2, "second choice received other amount than 2 points");
 assert(getPointsOfContender(e, third) - thirdPointsBefore == 1, "third choice received other amount than 1 points");
 
}

จาก rule ด้านบน จะเป็นการเช็คว่า คะแนนที่ vote ไป เป็นไปตามลำดับ 1 2 3 ในการ vote รึเปล่า

note: จะเห็นได้ว่า rule นี้จะเรียก vote ตรงๆเลย ไม่ได้ให้เรียกทุก function โดยใช้ f() เหมือน rule ที่แล้ว

โอเค มาลองรันกัน

certoraRun BordaBug3.sol:Borda --verify Borda:Borda.spec

จะได้ผลลัพธ์คือ

โอเค โดย rule ที่เขียนไว้คือ

 mathint firstPointsBefore = getPointsOfContender(e, first);
 mathint secondPointsBefore = getPointsOfContender(e, second);
 mathint thirdPointsBefore = getPointsOfContender(e, third);
 
 vote(e, first, second, third);
 
 assert(getPointsOfContender(e, first) - firstPointsBefore == 3, "first choice received other amount than 3 points");
 assert(getPointsOfContender(e, second) - secondPointsBefore == 2, "second choice received other amount than 2 points");

นั่นคือ เมื่อมีการ vote แล้ว contender second ได้รับคะแนนไปผิดนั่นเอง

โอเค มาดู error trace กัน