Program Analysis for High-Value Smart Contract Vulnerabilities: Techniques and Insights at SBC 2023 (สรุป)
มาดู tool ที่ Dedaub (บริษัท audit smart contract) ใช้กัน
โอเค session แบ่งเป็น 2 ช่วง
- Technique
- Insight
Techniques
Dedaub ใช้ tool 2 ตัวในการหาช่องโหว่มูลค่าสูง (*ช่องโหว่มูลค่าสูงที่ Dedaub หมายถึงนั้น เค้าเข้าร่วม 10 bug bounties และได้รางวัลมากว่า $3M) ใน smart contract
โดยทั้ง 2 tool ประกอบด้วย
- Symvalic Analysis (Symbolic Value-Flow Static Analysis)
- Corpus analysis
โอเค มาดูทีละตัวกัน
Symvalic Analysis ?
Symvalic analysis ย่อมาจาก SYMBOLIC-VALUE-FLOW STATIC ANALYSIS
จากชื่อจะเห็นได้ว่า Symvalic analysis = SYMBOLIC analysis (เป็นหนึ่งใน dynamic analysis) + Static analysis
โอเค Symvalic Analysis = symbolic analysis กับ static analysis ผสมกัน
งั้นก่อนจะเข้าใจ Symvalic Analysis เรามาทำความเข้าใจ symbolic analysis กับ static analysis กันก่อน
Symbolic analysis (Symbolic execution)
คือการที่เราพยายามวิเคราะห์โปรแกรม โดยคำนวณค่าที่เป็นไปได้ของตัวแปรทั้งหมด และกรองค่าที่เป็นไปไม่ได้ออก โดยดูว่าที่บรรทัดนั้น มี logic ยังไง
เช่นจากรูป
เราจะเห็นได้ว่าเมื่อเราใช้ symbolic execution
ในตอนแรกค่าของตัวแปร x และ y จะเป็นไปได้ทุกๆค่า int เลย
แต่พอมีการรัน code ไปเรื่อยๆ
เราจะพบว่า ใน if (x > y) assert false; นั้น เป็นไปไม่ได้ที่ if นั้นจะเป็นจริง
เนื่องจากพอเราลองทดค่าดู จะพบว่าถ้า if (x > y) assert false; เป็นจริง แสดงว่า ในบรรทัด int x,y; นั้น จะต้องมี x > y และ y < x ซึ่งเป็นไปไม่ได้
จะเห็นได้ว่าการใช้ symbolic execution จะเป็นการนำค่าแต่ละตัวแปร มาอ้างอิงถึงกัน (คล้ายๆ โซ่) เพื่อกรองค่าที่เป็นไปได้ของตัวแปรๆหนึ่ง ออกไปเรื่อยๆ ตามรูป
จากเทคนิคนี้ทำให้ symbolic execution มีความแม่นยำ (precision) สูง
แต่การที่ต้องทำการ execute code เพื่อคำนวณค่าที่เป็นไปได้ ก็ทำให้ symbolic execution มีโอกาสที่จะรัน code บางชุดไม่ไหว เช่น code ที่มี loop ใหญ่ๆ แล้วต้องทำการคำนวณค่าที่เป็นไปได้ทั้งหมด
หรือก็คือ symbolic execution มี completeness ที่ต่ำ นั่นเอง
โอเค ต่อมาคือ
Static analysis
static analysis คือการที่เราทำการ analysis โดยไม่ได้ทำการ execute code ตรงๆ แต่ใช้เทคนิคอื่นๆ ที่ทำการจำลองการ execute code แบบคร่าวๆ แทน
โอเค มายกตัวอย่างกัน
เช่น การทำ taint analysis โดยใช้ static analysis
โอเค ก่อนอื่นการทำ taint analysis คืออะไร ?
taint analysis คือการหาว่า มีค่าไหนบ้าง ที่ user ไม่ควรที่จะแก้ไขเองได้ (ถ้า user แก้ไขได้ จะกลายเป็นช่องโหว่ของระบบ)
เช่นจากรูป
เราตั้งว่า owner เป็น untainted value (ค่าที่ user ไม่ควรจะแก้เองได้)
จากนั้นเราจะนำ code ไปเข้า static analysis framework ที่จะทำการจำลองการทำงานของ code ทั้งหมด
เช่น ทำการแปลง code Solidity เป็น code Datalog ตามรูป
โดย code ใน version Datalog จะทำการสรุป logic ของ code Solidity
เพื่อที่สุดท้าย เราจะมาดูกันว่า สรุปแล้ว user สามารถแก้ไขค่า owner เป็นค่าที่ตัวเองต้องการได้มั้ย
ถ้าใช่ แสดงว่า code Solidity นี้ พอทำ taint analysis แล้วพบว่า มีช่องโหว่ที่ user สามารถแก้ค่า owner เป็นค่าที่ตัวเองต้องการได้
ซึ่งจะนำไปสู่การ attacker ด้วยการ withdraw ต่อไป
โอเค พอเราทำการจำลอง (หรือสรุป) การทำงานของ code มาคร่าวๆ แล้ว
เราจะต้องทำการ input ค่าของแต่ละตัวแปรเข้าไป ในแบบจำลอง code นั้น
โดย static analysis มักจะทำการประกาศ set ของค่าที่เป็นไปได้ของตัวแปรแต่ละประเภทไว้เลย ตามรูป
โดยเราจะไม่สามารถ กรอง ค่าที่เป็นไปไม่ได้ออก เหมือนใน symbolic execution
เช่นจากรูป ในบรรทัด token.transfer(sendTo, adjusted) นั้น
ตัว static analysis อาจจะสรุปออกมาว่า
adjusted = 31, amount = 10,000
ซึ่งจริงๆแล้วเป็นไปไม่ได้
เพราะ บรรทัด uint256 adjusted = amount * 103 / 100
แต่ static analysis ไม่สน
เนื่องจาก adjusted
- ไม่ได้ใช้ใน if, require ใดๆ
- ไม่ได้มีการเปลี่ยนค่าหลังจาก initial
- ไม่ได้เอาไปคิดค่าอื่นๆใน contract ต่อ
จะเห็นได้ว่า static analysis จะมี completeness ที่สูง (สามารถวิเคราะห์ code ได้ทุกบรรทัด เพื่อหา pattern ช่องโหว่)
ซึ่ง completeness ที่สูงก็มาจากการที่ไม่ได้ทำการ execute / ทด ค่าจากการรันจริงๆ
จึงทำให้มี precision ที่ต่ำ เนื่องจากผลลัพธ์ที่ออกมา อาจจะผิด นั่นเอง
Symvalic Analysis ?
symvalic analysis คือ ผสมกันของ static analysis และ symbolic execution
โดยตัว static analysis จะใช้ symbolic execution (แต่เค้าเรียกว่า symbolic solver แหะ) ในการกรองค่าที่เป็นไปไม่ได้ออก
เช่นจากรูป
เมื่อเรามาถึงบรรทัด token.transfer(sendTo,adjusted)
เราจะได้ว่าจาก set ค่าตัวแปรที่เป็นไปได้
เมื่อทำการใช้ตัว symbolic solver มาช่วย จะเหลือค่าที่เป็นไปได้แค่
adjusted = 1030
เนื่องจาก amount ที่ผ่านเงื่อนไข if(amount ≥ 1,000 && amount < 100,000) มีแค่ amount = 1,000 นั่นเอง
*เราจะสมมติว่า code เขียนว่า if(amount ≥ 1,000 && amount < 100,000) ไม่ใช่ if(amount ≥ 10,000 && amount < 100,000) ละกัน
จะเห็นได้ว่า symvalic analysis ที่ใช้ static analysis เป็น core หลักนั้น
ได้รับ completeness ที่สูงมาจาก static analysis
และยังเพิ่ม precision ด้วยการให้ symbolic solver ช่วย
ดังนั้น
Symvalic analysis มี precision สูงกว่า static analysis แบบปกติ
และมี completeness สูงกว่า symbolic execution แบบปกติ นั่นเอง
โอเค นั่นคือ อาวุธแรกของ Dedaub
มาต่อที่อาวุธที่สองกัน
Corpus analysis
โอเค ก่อนจะพูดถึง Corpus analysis มาลองกลับไปดู code เดิมกัน
จากรูป เราอาจจะใช้ symvalic analysis ในการทำ tool เพื่อหาว่า sendTo เป็น untainted หรือ tainted value (ถ้า user ปกติ สามารถส่ง token ให้ sentTo ใดๆได้ แสดงว่ามีช่องโหว่)
แต่ประเด็นคือ
ถ้าเราจะทำ tool ที่รันอัตโนมัติได้
ตัว tool จะรู้ได้ยังไงว่าตัวแปร sendTo เป็นตัวแปรสำคัญ ที่ห้ามเป็น untainted value
ถ้า sendTo ไม่ได้ชื่อ sendTo ละ ?
ถ้า sendTo ไม่ได้เป็น parameter ตัวที่สามของ withdrawToken ละ ?
ถ้า function ไม่ได้ชื่อว่า withdrawToken ?
ถ้า token.transfer เป็น logic ที่ซับซ้อนขึ้นเช่น pool.swap ?
…
คำตอบคือ
การใช้ Corpus analysis ซึ่งสามารถ
- สรุป pattern ของ code ได้ เพื่อทำการหาว่าจะ analysis ยังไงต่อ
- สรุป pattern การทำงานหลักๆที่ function ใน code นั้นๆ ทำงานได้ เช่น ถึงแม้จะเปลี่ยนชื่อ function จาก swap เป็น trade … ตัว analysis ก็ยังเข้าใจนั่นเอง
Insights
จาก technique ที่ว่ามา
พอลองมารันกับ smart contract (ที่ถูก deploy ไปใช้งานจริงๆ) พบว่า
- warning rate อยู่ที่ 0.5% ( tool ทำการ flag 1 / 200 contract)
ซึ่งถ้าในเชิง academic ตัวจำนวนถือว่าน้อยไป
พูดอีกอย่างก็คือ ถ้า มี 99.5% ที่ไม่มีช่องโหว่
ถึงเราหา 0.5% ที่มีช่องโหว่ได้
ก็อาจจะไม่ได้มี impact เยอะขนาดนั้นรึเปล่า
แต่ทาง Dedaub ก็แสดงให้เห็นว่า จำนวน 0.5% นั้น เมื่อถูก attack แล้ว เสียหายเป็นระดับล้าน usd เลย
2. false positive rate อยู่ที่ 98% (จาก 100 warning มีที่เป็นช่องโหว่จริงๆ 2 อัน)
ซึ่ง false positive 98% ในเชิง academic นั้น ถือว่าสูงเกินไป (ปกติแล้วต้อง < 60%)
แต่ทาง Dedaub ก็แสดงให้เห็นว่าถึง false positive สูงขนาดนี้ ก็เพียงพอต่อการที่ Dedaub นำ tool ไปใช้ เพื่อป้องกันความเสียหายในระดับล้าน usd ได้ นั่นเอง
พูดอีกอย่างก็คือ tool ที่มี false positive ต่ำ อาจจะไม่ได้หาช่องโหว่ที่มีมูลค่าสูงเจอ เท่ากับ tool ที่มี false positive สูง
โดย จาก paper นี้ ระบุว่า ในปี 2021 จากการลองรัน tool เพื่อหา ช่องโหว่ของ smart contract ดู มีเพียง 0.27% ของ smart contract ที่ถูกระบุว่ามีช่องโหว่เท่านั้น ที่ถูก hack เพื่อเอาเงินจริงๆ (เพราะ ช่องโหว่มีมูลค่าน้อยเกินไป, ต้องใช้ effort มากเกินไปในการ hack etc. )
โอเค สรุป Program Analysis for High-Value Smart Contract Vulnerabilities: Techniques and Insights ประมาณนี้ครับ
