การทดสอบและการยืนยันอย่างเป็นทางการสำหรับ Web3 Smart Contract Security

อ่านเวลา: 9 นาที

ลองนึกภาพไปดิ่งพสุธา ก่อนกระโดดลงจากเครื่อง เช็คร่มชูชีพเป็นร้อยครั้งเลยดีมั้ย? การตรวจสอบและทดสอบเป็นส่วนสำคัญของการรักษาความปลอดภัย คิดเกี่ยวกับสิ่งที่เกี่ยวข้องกับความปลอดภัย น่าจะมีกลไกการทดสอบตามมาภายหลัง ไม่ว่าจะเป็น การติดตั้งกล้องวงจรปิด หรือ การตรวจหมึกในปากกาก่อนสอบข้อเขียนในโรงเรียน เราทุกคน ปฏิบัติตามมาตรการความปลอดภัย ยิ่งมีความเสี่ยงสูง เราก็ยิ่งทดสอบสิ่งต่างๆ และเมื่อเราพูดถึงสัญญาอัจฉริยะ ความเสี่ยงนั้นสูงมาก คุณไม่สามารถประมาทได้เมื่อพูดถึงการรักษาความปลอดภัยสัญญาอัจฉริยะ

1. จำเป็นต้องมีความปลอดภัยเสมอ

คุณสามารถล็อคประตูสองครั้งหรือสามครั้งได้อย่างแน่นอน คุณแน่ใจหรือว่าบ้านของคุณจะไม่ถูกโจรกรรมในขณะที่คุณไม่อยู่? คุณไม่สามารถทำได้เพราะคุณไม่รู้ว่าโจรจะทำอะไรเพื่อบุกเข้าไปในบ้าน เช่นเดียวกับทุกมาตรการความปลอดภัยที่เราใช้ ไม่มีวิธีใดที่ปลอดภัยอย่างสมบูรณ์ซึ่งจะรับประกันความปลอดภัยได้ ถึงกระนั้น การกระทำที่เราทำอย่างรวดเร็วจะเพิ่มโอกาสในการปลอดภัย ซึ่งเป็นสิ่งที่เกมนี้เป็น เราต้องการเพิ่มโอกาสในการปลอดภัยโดยใช้มาตรการต่างๆ

โลกของ Web3 นั้นไม่แตกต่างกัน ไม่มีวิธีใดที่ปลอดภัยในการช่วยตัวคุณเอง แต่การมีผู้ตรวจสอบที่มีประสบการณ์จาก QuillAudits สามารถเพิ่มโอกาสที่โปรโตคอลของคุณจะปลอดภัยได้อย่างมาก และจะทำให้คุณมั่นใจในการรักษาความปลอดภัยที่ทันสมัย ใน web3 มีกลไกสำคัญสองอย่างที่ช่วยให้คุณเข้าใจว่าคุณปลอดภัยเพียงใดโดยทำการทดสอบโปรโตคอลของคุณ:-

1. การทดสอบสัญญาอัจฉริยะ
2. การตรวจสอบอย่างเป็นทางการของสัญญาอัจฉริยะ

มาทำความเข้าใจรายละเอียดเหล่านี้และเรียนรู้ว่าสิ่งเหล่านี้ช่วยให้เราทราบจุดอ่อนหรือช่องโหว่ของสัญญาของเราได้อย่างไร

2. การทดสอบสัญญาอัจฉริยะ

นักพัฒนาที่มีประสบการณ์สามารถอธิบายการทำงานกับเครื่องด้วยรหัส ถึงกระนั้น บางครั้งเครื่องก็ไม่ได้แสดงกลไกที่แน่นอนตามที่นักพัฒนาคิดไว้ เนื่องจากข้อบกพร่องหรือข้อผิดพลาดเชิงตรรกะในโค้ด การทดสอบเป็นกระบวนการที่ช่วยระบุจุดที่โค้ดของเราล้มเหลว และสิ่งที่สามารถทำได้เพื่อให้สอดคล้องกับการดำเนินการที่เราต้องการให้ดำเนินการ

การทดสอบสัญญาอัจฉริยะ เป็นช่วงหนึ่งในวงจรการพัฒนาที่เราทำการวิเคราะห์สัญญาของเราโดยละเอียด และพยายามค้นหาว่าโค้ดของเราล้มเหลวที่ใดและเพราะเหตุใด สัญญาอัจฉริยะเกือบทั้งหมดผ่านขั้นตอนนี้ การทดสอบสัญญาอัจฉริยะทำได้สองวิธี มาสำรวจกัน

2.1 อัตโนมัติ

ตามชื่อที่แนะนำ วิธีการทดสอบสัญญาอัจฉริยะนี้ใช้เพื่อดำเนินการทดสอบสคริปต์ มันเกี่ยวข้องกับซอฟต์แวร์อัตโนมัติที่ทำการทดสอบซ้ำ ๆ เพื่อค้นหาช่องโหว่และข้อบกพร่องในสัญญาอัจฉริยะ เครื่องมือทดสอบอัตโนมัติเหล่านี้สามารถกำหนดค่าได้ด้วยข้อมูลการทดสอบและผลลัพธ์ที่คาดหวัง จากนั้นจึงนำผลลัพธ์จริงมาเปรียบเทียบกับที่คาดไว้เพื่อตรวจสอบว่าสัญญาทำงานอย่างถูกต้องหรือไม่ การทดสอบอัตโนมัติสามารถแบ่งออกได้อีกสามประเภท

2.1.1. การทดสอบการทำงาน

สมมติว่าคุณเขียนโปรแกรมเพื่อรับตัวเลขสองตัว a และ b แล้วส่งคืนการบวกของตัวเลขทั้งสอง ดังนั้นในการตรวจสอบโปรแกรมนั้น คุณให้ 2 และ 8 และป้อนผลลัพธ์ที่คาดไว้เป็น 10 ตอนนี้เมื่อโปรแกรมทำงาน ควรคืนค่า 10 ด้วยเช่นกัน ถ้าเป็นเช่นนั้น แสดงว่าใช้งานได้ดี และโค้ดของเราถูกต้อง แต่ถ้าเป็นเช่นนั้น ไม่ได้ แสดงว่ามีข้อผิดพลาดบางอย่างกับรหัสของเรา 

การทดสอบการทำงานจำเป็นต้องเข้าใจว่าสัญญาของคุณควรทำงานอย่างไรในเงื่อนไขบางประการ เราสามารถทดสอบได้โดยเรียกใช้การคำนวณด้วยค่าที่เลือกและเปรียบเทียบผลลัพธ์ที่ส่งคืน การทดสอบการทำงานมีสามชั้น:-

1. การทดสอบหน่วย:- สิ่งนี้เกี่ยวข้องกับการทดสอบส่วนประกอบแต่ละส่วนของสัญญาอัจฉริยะเพื่อความถูกต้อง มันกล้าแสดงออกหรือต้องการคำสั่งเกี่ยวกับตัวแปร

2. บูรณาการ ทดสอบง: – ข้อตกลงเหล่านี้เกี่ยวข้องกับการทดสอบส่วนประกอบแต่ละส่วนร่วมกัน การทดสอบการรวมเป็นระดับที่สูงกว่าในลำดับชั้นมากกว่าการทดสอบหน่วย ช่วยให้เราระบุข้อผิดพลาดที่เกิดจากการโต้ตอบของฟังก์ชันต่างๆ ซึ่งอาจเป็นส่วนหนึ่งของสัญญาอัจฉริยะอื่นๆ

3. System ทดสอบง: – นี่คือระดับสูงสุดในลำดับชั้น ในเรื่องนี้ เราทดสอบสัญญาทั้งหมดเป็นระบบเดียวที่ผสานรวมอย่างสมบูรณ์เพื่อดูว่าทำงานตามความต้องการของเราหรือไม่ ทำได้จากมุมมองของผู้ใช้ และวิธีที่ดีที่สุดคือการปรับใช้บน testnet

2.1.2. การวิเคราะห์แบบคงที่

การวิเคราะห์แบบสแตติกสามารถทำได้โดยไม่ต้องรันโปรแกรมด้วยซ้ำ มันเกี่ยวข้องกับการวิเคราะห์ซอร์สโค้ดหรือ bytecode ของสัญญาอัจฉริยะก่อนดำเนินการ ดังนั้นการตั้งชื่อ การวิเคราะห์แบบสแตติกสามารถส่งผลให้เกิดการตรวจจับช่องโหว่ทั่วไปบางรายการ

2.1.3. การวิเคราะห์แบบไดนามิก

ซึ่งแตกต่างจากการวิเคราะห์แบบคงที่ การวิเคราะห์แบบไดนามิกจะดำเนินการระหว่างรันไทม์ของสัญญาอัจฉริยะเพื่อระบุปัญหาในโค้ด ตัววิเคราะห์รหัสแบบไดนามิกจะสังเกตสถานะการทำงานของสัญญาและสร้างรายงานโดยละเอียดเกี่ยวกับช่องโหว่และการละเมิดคุณสมบัติ Fuzzing มาจากการวิเคราะห์ DYnamic Fuzzing กำลังป้อนอินพุตที่ไม่ถูกต้องหรือเป็นอันตรายเพื่อทำให้เกิดการเรียกใช้โค้ดที่ไม่ได้ตั้งใจ

2.2 คู่มือ

ตามชื่อที่แนะนำ วิธีการทดสอบสัญญาอัจฉริยะนี้เกี่ยวข้องกับการโต้ตอบกับนักพัฒนาที่เป็นมนุษย์เป็นประจำ การตรวจสอบรหัสที่นักพัฒนาใช้รหัสหลายบรรทัดอยู่ภายใต้โหมดการทดสอบสัญญาอัจฉริยะแบบแมนนวล

โหมดแมนนวลต้องใช้เวลา ทักษะ เงิน และความพยายามอย่างมาก ถึงกระนั้น ผลลัพธ์ก็มักจะคุ้มค่า เพราะด้วยวิธีนี้ เราระบุช่องโหว่ที่อาจไม่มีใครสังเกตเห็นในการทดสอบอัตโนมัติ การทดสอบด้วยตนเองมีสองประเภทที่สำคัญ:-

2.2.1 การตรวจสอบโค้ด:- 

วิธีที่ดีที่สุดในการทดสอบว่ามาตรการความปลอดภัยของคุณทำงานได้อย่างถูกต้องหรือไม่คือการพยายามทำลายมัน ตัวอย่างเช่น หากคุณต้องการตรวจสอบว่าล็อครถของคุณทำงานปกติหรือไม่ ให้ลองหักดู ตอนนี้คุณอาจขอให้ขโมยรถที่เชี่ยวชาญสามารถเจาะรถของฉันได้อย่างง่ายดาย ฉันอาจจะไม่ ดังนั้นทางออกคือจ้างคนที่เชี่ยวชาญในการบุกเข้ามาเพื่อที่เขาจะสามารถแนะนำคุณได้!

 ใช่ ฉันกำลังพูดถึง QuillAudits เราเป็นทีมงานผู้สอบบัญชีที่เชี่ยวชาญซึ่งสามารถแนะนำคุณได้ การตรวจสอบโค้ดต้องใช้ความคิดของผู้โจมตีเพื่อค้นหาช่องโหว่ที่เป็นไปได้ทั้งหมดในซอร์สโค้ด การตรวจสอบโค้ดคือการประเมินโดยละเอียดของโค้ดของสัญญาอัจฉริยะเพื่อเปิดเผยช่องโหว่และข้อบกพร่องที่อาจเกิดขึ้น

2.2.2 ค่าหัวแมลง:-

หากคุณคิดว่าอาจมีจุดบกพร่องด้านความปลอดภัยในซอร์สโค้ดของคุณ (ซึ่งส่วนใหญ่จะเป็นอย่างนั้น) และคุณไม่สามารถหาเจอได้ คุณสามารถจ้างคนทำงานอิสระจากภายนอกงานนี้โดยสร้างระบบการให้รางวัล มันเหมือนกับการประกาศรางวัลสำหรับใครก็ตามที่สามารถแฮ็กสัญญาอัจฉริยะของคุณได้ เมื่อทำเช่นนี้ คุณจะได้เรียนรู้เกี่ยวกับช่องโหว่ที่มีอยู่ในสัญญาอัจฉริยะของคุณ เพื่อให้คุณสามารถปกป้องได้ดีขึ้นและช่วยผู้ใช้ของคุณจากการสูญเสีย

3. การตรวจสอบ Smart Contract อย่างเป็นทางการ

การตรวจสอบอย่างเป็นทางการคือกระบวนการประเมินความถูกต้องของสัญญาตามข้อกำหนดที่เป็นทางการ ซึ่งหมายความว่าการตรวจสอบอย่างเป็นทางการจะประเมินว่ารหัสทำตามที่ตั้งใจไว้หรือไม่ การตรวจสอบอย่างเป็นทางการใช้วิธีการที่เป็นทางการในการระบุ ออกแบบ และตรวจสอบโปรแกรม

3.1 ข้อกำหนดอย่างเป็นทางการคืออะไร?

ในบริบทของสัญญาอัจฉริยะ ข้อกำหนดที่เป็นทางการหมายถึงคุณสมบัติซึ่งจะต้องเหมือนเดิมในทุกสถานการณ์ที่เป็นไปได้ สิ่งเหล่านี้เป็นคุณสมบัติ ” ไม่แปรเปลี่ยน ” เนื่องจากไม่สามารถเปลี่ยนแปลงและแสดงการยืนยันเชิงตรรกะเกี่ยวกับการดำเนินการตามสัญญา

ข้อกำหนดอย่างเป็นทางการคือชุดของข้อความที่เขียนด้วยภาษาที่เป็นทางการ ข้อมูลจำเพาะครอบคลุมคุณสมบัติต่างๆ และอธิบายว่าคุณสมบัติของสัญญาควรทำงานอย่างไรในสถานการณ์อื่นๆ ข้อกำหนดที่เป็นทางการมีความสำคัญอย่างยิ่ง เนื่องจากหากสัญญาไม่สามารถเปลี่ยนแปลงตัวแปรที่ไม่แปรเปลี่ยนหรือคุณสมบัติระหว่างการดำเนินการได้ อาจนำไปสู่การแสวงหาประโยชน์จากทรัพย์สินได้ ซึ่งอาจนำไปสู่การสูญเสียครั้งใหญ่

สามารถช่วยให้เราระบุได้ว่าสัญญาอัจฉริยะเป็นไปตามข้อกำหนดหรือมีลักษณะการทำงานที่ไม่คาดคิดหรือไม่ การตรวจสอบอย่างเป็นทางการมีสามองค์ประกอบ: ข้อมูลจำเพาะ รุ่น และกลไกการตรวจสอบ

3.1.1 คุณสมบัติ

ข้อมูลจำเพาะคือคำอธิบายที่ชัดเจน ไม่กำกวม และครบถ้วนของข้อกำหนดสำหรับสัญญาอัจฉริยะ ควรอธิบายว่าสัญญาควรทำอะไรและไม่ควรทำอะไร ต่อไปนี้คือตัวอย่างข้อมูลจำเพาะสำหรับ Smart Contract แบบง่ายที่บวกตัวเลขสองตัว:

// Specification: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function add(uint a, uint b) public view returns (uint) {
// Implementation details are not relevant to the specification
// …
}

รุ่น 3.1.2

แบบจำลองแสดงถึงสัญญาที่ชาญฉลาดอย่างเป็นทางการซึ่งสามารถใช้ให้เหตุผลเกี่ยวกับพฤติกรรมของมันได้ รูปแบบหนึ่งที่ได้รับความนิยมสำหรับสัญญาอัจฉริยะคือภาษาโปรแกรม Solidity นี่คือรูปแบบตัวอย่างสำหรับฟังก์ชันเพิ่มที่อธิบายไว้ข้างต้น:

// Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function add(uint a, uint b) public view returns (uint) {
return a + b;
}

3.1.3 เครื่องมือตรวจสอบ

เครื่องมือตรวจสอบเป็นเครื่องมือที่สามารถวิเคราะห์แบบจำลองและตรวจสอบความถูกต้องเกี่ยวกับข้อกำหนดที่กำหนด มีเครื่องมือตรวจสอบหลายอย่างสำหรับสัญญาอัจฉริยะ ได้แก่ :

มิธริล: เครื่องมือดำเนินการเชิงสัญลักษณ์แบบโอเพ่นซอร์สที่สามารถตรวจจับช่องโหว่ด้านความปลอดภัยที่หลากหลายใน Solidity smart contracts

รีมิกซ์ IDE: สภาพแวดล้อมการพัฒนาแบบบูรณาการที่มีเครื่องมือตรวจสอบอย่างเป็นทางการที่สามารถตรวจสอบความถูกต้องของสัญญาอัจฉริยะ

ผู้พิสูจน์ Certora: เครื่องมือเชิงพาณิชย์ที่สามารถตรวจสอบความถูกต้องของสัญญาอัจฉริยะโดยใช้เหตุผลทางคณิตศาสตร์อัตโนมัติ ต่อไปนี้คือตัวอย่างวิธีการใช้การตรวจสอบอย่างเป็นทางการเพื่อตรวจสอบความถูกต้องของสัญญาอัจฉริยะโดยใช้ Certora Prover:

pragma solidity 0.7.6; // Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function add(uint a, uint b) public pure returns (uint) {
return a + b;
} // Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function add(uint a, uint b) public pure returns (uint) {
return a + b;
} // Specification: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function test_add(uint a, uint b) public pure returns (bool) {
uint expected = a + b;
uint actual = add(a, b);
return expected == actual;
} // Verification: Verify the correctness of the add function contract TestAdd {
function test_add(uint a, uint b) public view returns (bool) {
return CertoraProver.verify(test_add, a, b);
}
}

ในตัวอย่างข้างต้น เรากำหนด Solidity smart contract ที่มีโมเดลของฟังก์ชันเพิ่ม ข้อมูลจำเพาะสำหรับฟังก์ชัน และเครื่องมือตรวจสอบความถูกต้อง (Certora Prover) ที่สามารถตรวจสอบความถูกต้องของฟังก์ชันได้ เรายังกำหนดฟังก์ชันทดสอบ (test_add) ที่สามารถใช้ตรวจสอบความถูกต้องของฟังก์ชันได้

3.2 การทดสอบ VS การตรวจสอบอย่างเป็นทางการ

ดังที่เราได้กล่าวไปแล้ว การทดสอบจะส่งกลับผลลัพธ์ที่คาดไว้สำหรับข้อมูลอินพุตบางตัวที่บอทขาดไป เนื่องจากเราไม่สามารถพูดถึงข้อมูลที่ยังไม่ได้ทดสอบได้ เป็นไปไม่ได้เลยที่จะตรวจสอบในทุกอินพุตที่เป็นไปได้ ดังนั้นเราจึงไม่แน่ใจเกี่ยวกับ "ความถูกต้องของการทำงาน" นั่นคือที่มาของการยืนยันอย่างเป็นทางการ วิธีการตรวจสอบอย่างเป็นทางการใช้เทคนิคทางคณิตศาสตร์ที่เข้มงวดในการระบุและตรวจสอบซอฟต์แวร์หรือสัญญาอัจฉริยะ

3.3 เทคนิคการตรวจสอบอย่างเป็นทางการ

การตรวจสอบอย่างเป็นทางการมีขอบเขตกว้างของเทคนิคในการเพิ่มประสิทธิภาพ การรักษาความปลอดภัยสัญญาอัจฉริยะ. ในส่วนนี้ของบล็อก เราจะสำรวจทีละส่วน

3.3.1 การตรวจสอบแบบจำลอง

เมื่อเราพูดถึงข้อกำหนดที่เป็นทางการแล้ว เราจะตรวจสอบสัญญาอัจฉริยะกับข้อกำหนดในเทคนิคการตรวจสอบที่เป็นทางการนี้ สัญญาอัจฉริยะเหล่านี้แสดงเป็นระบบการเปลี่ยนสถานะ และคุณสมบัติถูกกำหนดโดยใช้ตรรกะชั่วคราว 

เทคนิคนี้ใช้เป็นหลักในการประเมินคุณสมบัติชั่วคราวที่แสดงถึงพฤติกรรมของสัญญาอัจฉริยะเมื่อเวลาผ่านไป คุณสมบัติการควบคุมการเข้าถึง (การโทรของผู้ดูแลระบบ ทำลายตัวเอง) สามารถเขียนเป็นตรรกะทางการได้ จากนั้นอัลกอริธึมการตรวจสอบแบบจำลองจะสามารถตรวจสอบได้ว่าสัญญาเป็นไปตามการตรวจสอบอย่างเป็นทางการนี้หรือไม่

การตรวจสอบโมเดลใช้เทคนิคที่เรียกว่า State Space exploration ซึ่งโดยพื้นฐานแล้วเป็นการลองสถานะที่เป็นไปได้ทั้งหมดที่เป็นไปได้ของสัญญาอัจฉริยะของเรา จากนั้นตรวจสอบว่ามีสิ่งใดที่ส่งผลให้เกิดการละเมิดทรัพย์สินหรือไม่ อย่างไรก็ตามสิ่งนี้อาจนำไปสู่หลายรัฐอย่างไม่มีที่สิ้นสุด ดังนั้นตัวตรวจสอบแบบจำลองจึงอาศัยเทคนิคนามธรรมเพื่อทำให้การวิเคราะห์สัญญาอัจฉริยะเป็นไปได้อย่างมีประสิทธิภาพ

3.3.2 การพิสูจน์ทฤษฎีบท

การพิสูจน์ทฤษฎีบทนั้นเกี่ยวกับการให้เหตุผลทางคณิตศาสตร์เกี่ยวกับความถูกต้องของโปรแกรม มันเกี่ยวข้องกับการสร้างความประทับใจเชิงตรรกะของระบบและข้อกำหนดของสัญญาและการตรวจสอบ "ความเท่าเทียมกันทางตรรกะ" ระหว่างข้อความ การสมมูลเชิงตรรกะเป็นความสัมพันธ์ทางคณิตศาสตร์ที่บอกว่าข้อความ A เป็นจริงก็ต่อเมื่อข้อความ B เป็นจริงเท่านั้น

ดังที่เราได้เรียนรู้ในเทคนิคการตรวจสอบแบบจำลอง เราจำลองสัญญาเป็นระบบการเปลี่ยนแปลงที่มีสถานะจำกัด การพิสูจน์ทฤษฎีบทสามารถจัดการการวิเคราะห์ระบบอนันต์สถานะได้ อย่างไรก็ตาม เครื่องพิสูจน์ทฤษฎีบทแบบอัตโนมัติไม่สามารถทราบได้เสมอไปว่าปัญหาเชิงตรรกะสามารถตัดสินใจได้หรือไม่ จึงมักต้องการความช่วยเหลือจากมนุษย์เพื่อเป็นแนวทางในการพิสูจน์ทฤษฎีบทในการพิสูจน์ความถูกต้อง

4 ข้อสรุป

การทดสอบและการตรวจสอบอย่างเป็นทางการเป็นส่วนสำคัญของการพัฒนาสัญญาอัจฉริยะ วิธีการเหล่านี้ใช้เพื่อทำให้สัญญาอัจฉริยะมีความปลอดภัยและช่วยให้สัญญาพร้อมสำหรับการปรับใช้ แต่อย่างที่คุณทราบ การรักษาความปลอดภัยไม่เคยเพียงพอ สัญญาอัจฉริยะจำนวนมากถูกแฮ็กเพียงเพราะไม่มีการทดสอบที่เหมาะสม ตอนนี้ชุมชน web3 ต้องการโปรโตคอลที่ปลอดภัยมากขึ้นกว่าเดิม 

พวกเราที่ QuillAudits มีพันธกิจที่จะช่วยปกป้องโปรโตคอลของคุณ ด้วยทีมงานที่มีทักษะและประสบการณ์ของเรา เรามั่นใจว่าจะไม่มีใครสังเกตเห็นแม้แต่ช่องโหว่เดียว เยี่ยมชมเว็บไซต์ของเราและรับโครงการ Web3 ของคุณอย่างปลอดภัย!

28 เข้าชม

• เนื้อหาที่ขับเคลื่อนด้วย SEO และการเผยแพร่ประชาสัมพันธ์ รับการขยายวันนี้
• เพลโตบล็อคเชน Web3 Metaverse ข่าวกรอง ขยายความรู้. เข้าถึงได้ที่นี่.
• ที่มา: https://blog.quillhash.com/2023/02/16/testing-and-formal-verification/