การทดสอบสัญลักษณ์ด้วย Halmos: ใช้ประโยชน์จากการทดสอบที่มีอยู่สำหรับการตรวจสอบอย่างเป็นทางการ

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

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

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

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

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

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

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

ข้อกำหนดเหนือศีรษะ

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

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

เชื่อมช่องว่างระหว่างการทดสอบและการตรวจสอบอย่างเป็นทางการด้วยการทดสอบเชิงสัญลักษณ์และ Halmos

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

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

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

ตัวอย่าง: การทดสอบ isPowerOfTwo() ฟังก์ชัน

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

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

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

อย่างไรก็ตาม Halmos ช่วยให้นักพัฒนานำการทดสอบที่มีอยู่แล้วเหล่านี้กลับมาใช้ซ้ำได้สำหรับการตรวจสอบอย่างเป็นทางการโดยใช้ความพยายามเพียงเล็กน้อย เครื่องมือตรวจสอบว่าการทดสอบผ่านสำหรับอินพุตที่เป็นไปได้ทั้งหมดโดยดำเนินการทดสอบโดยใช้สัญลักษณ์ จากนั้นจึงตรวจสอบว่าไม่มีการละเมิดการยืนยัน (หรือหากการยืนยัน is ละเมิด, โดยการให้ตัวอย่างเปรียบเทียบ). ซึ่งหมายความว่าหากการทดสอบผ่าน Halmos ความถูกต้องของฟังก์ชันจะได้รับการตรวจสอบอย่างเป็นทางการ ซึ่งหมายความว่าอัลกอริทึมจะถูกนำไปใช้อย่างถูกต้อง และได้รับการแปลอย่างถูกต้องโดยคอมไพเลอร์เป็น bytecode

ข้อจำกัด: การดำเนินการเชิงสัญลักษณ์ที่มีขอบเขต

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

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

ตัวอย่างเช่น พิจารณาเวอร์ชันซ้ำต่อไปนี้ของ isPowerOfTwo() ฟังก์ชันซึ่งมีฟีเจอร์การวนซ้ำแบบไม่มีขอบเขต โดยที่จำนวนการวนซ้ำถูกกำหนดโดยจำนวนบิตขั้นต่ำที่ต้องใช้ในการแสดงหมายเลขอินพุต

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

การสาธิต: การตรวจสอบอย่างเป็นทางการของ ERC721A ด้วย Halmos

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

คุณสมบัติการทดสอบสัญลักษณ์

เนื่องจากการทดสอบที่มีอยู่สำหรับ ERC721A ถูกเขียนด้วย JavaScript ด้วย Hardhat (ซึ่ง Halmos ยังไม่รองรับในขณะนี้) เราจึงเขียนการทดสอบใหม่ใน Solidity สำหรับฟังก์ชันจุดเข้าใช้งานหลัก: mint(), burn()และ transfer(). การทดสอบเหล่านี้ตรวจสอบว่าแต่ละฟังก์ชันอัปเดตความเป็นเจ้าของโทเค็นและยอดคงเหลืออย่างถูกต้อง และมีผลกับผู้ใช้ที่เกี่ยวข้องเท่านั้นโดยไม่เปลี่ยนแปลงยอดคงเหลือหรือความเป็นเจ้าของของผู้ใช้รายอื่น สิ่งหลังนี้ไม่ใช่เรื่องเล็กน้อยที่ต้องพิสูจน์เนื่องจากการใช้อัลกอริธึมโครงสร้างข้อมูลสันหลังยาวใน ERC721A ตัวอย่างเช่น การทดสอบต่อไปนี้ตรวจสอบว่า transfer() ฟังก์ชันปรับปรุงความเป็นเจ้าของโทเค็นที่ระบุอย่างถูกต้อง:

การทดสอบอื่นตรวจสอบว่า transfer() ฟังก์ชันไม่เปลี่ยนความสมดุลของที่อยู่อื่น ซึ่งพิสูจน์ได้ยากตามที่กล่าวไว้ก่อนหน้านี้:

ผลการตรวจสอบ

เราทำการทดสอบการตรวจสอบโดยใช้ Halmos บนสัญญาอัจฉริยะ ERC721A โดยเขียนผลรวมของ การทดสอบ 19. การทดสอบดำเนินการผ่าน Halmos โดยมีการวนซ้ำ 3 ขอบเขต ซึ่งใช้เวลา 16 นาทีจึงจะเสร็จสมบูรณ์ รายละเอียดของเวลาการตรวจสอบสามารถเห็นได้ในตารางด้านล่าง การทดลองดำเนินการบน MacBook Pro ที่มีชิป M1 Pro และหน่วยความจำ 16 GB

ทดสอบ	เวลา
ทดสอบ BurnBalanceUpdate	6.67
testBurnNextTokenId ไม่เปลี่ยนแปลง	1.40
ทดสอบ BurnOtherBalancePreservation	5.69
ทดสอบ BurnOtherOwnershipPreservation	189.70
ทดสอบ BurnOwnershipUpdate	3.81
ทดสอบ BurnRequirements	71.95
ทดสอบ MintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
ทดสอบ MintOtherBalancePreservation	0.26
ทดสอบ MintOtherOwnershipPreservation	5.74
ทดสอบ MintOwnershipUpdate	1.38
ทดสอบ MintRequirements	0.09
ทดสอบ TransferBalance ไม่เปลี่ยนแปลง	9.03
ทดสอบ TransferBalanceUpdate	53.53
testTransferNextTokenId ไม่เปลี่ยนแปลง	4.47
ทดสอบ TransferOtherBalancePreservation	19.57
ทดสอบการโอนสิทธิ์การเป็นเจ้าของอื่นๆ การเก็บรักษา	430.61
ทดสอบ TransferOwnershipUpdate	18.71
ทดสอบข้อกำหนดการโอน	149.18

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

โดยรวมแล้ว ผลการทดลองนี้บ่งชี้ว่า Halmos สามารถตรวจสอบความถูกต้องของรหัสสัญญาอัจฉริยะได้อย่างมีประสิทธิภาพ ช่วยเพิ่มความมั่นใจในความสมบูรณ์ของโค้ด แม้ว่า Smart Contract จะมีความซับซ้อนและอาจมี Edge Case ก็ตาม

ทดลองกับบั๊กที่ถูกฉีด

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

งานที่เกี่ยวข้อง

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

แม้ว่า Halmos จะเป็นส่วนเสริมที่มีค่าสำหรับชุดเครื่องมือสำหรับการตรวจสอบสัญญาอัจฉริยะ แต่ก็มีไว้เพื่อเสริม (ไม่ใช่แทนที่) เครื่องมือที่มีอยู่ นักพัฒนาสามารถรวม Halmos เข้ากับเครื่องมืออื่นๆ เพื่อให้ได้ระดับการรับประกันที่สูงขึ้นในสัญญาของพวกเขา ด้านล่าง เราจะเปรียบเทียบ Halmos กับเครื่องมือที่เป็นทางการบางประเภทที่รองรับ EVM bytecode

• K เป็นกรอบการตรวจสอบอย่างเป็นทางการที่มีประสิทธิภาพที่ช่วยให้การตรวจสอบแบบนิรนัยและการพิสูจน์ทฤษฎีบทเชิงโต้ตอบ ทฤษฎีพื้นฐานและการนำไปปฏิบัติให้ความหมายในระดับสูง ทำให้เหมาะสำหรับการตรวจสอบโปรแกรมและอัลกอริทึมที่ซับซ้อน อย่างไรก็ตาม ควรสังเกตว่า K ไม่ได้ออกแบบมาโดยเน้นหนักไปที่การตรวจสอบอัตโนมัติ และขาดคุณสมบัติการทำงานอัตโนมัติบางอย่างซึ่งอาจต้องใช้ความพยายามด้วยตนเองมากขึ้นในระหว่างกระบวนการตรวจสอบ ในการใช้กรอบงาน K ข้อกำหนดที่เป็นทางการจะเขียนเป็นภาษา K ซึ่งต้องเรียนรู้ก่อนใช้งาน จุดแข็งของมันมีประโยชน์อย่างยิ่งในการตรวจสอบระบบที่ซับซ้อน ซึ่งอาจเป็นเรื่องยากในการวิเคราะห์โดยใช้เหตุผลอัตโนมัติ
• เซอร์โตร่า เป็นเครื่องมือการตรวจสอบอย่างเป็นทางการสำหรับสัญญาอัจฉริยะที่เน้นการตรวจสอบอัตโนมัติและสนับสนุนการตรวจสอบแบบจำลองที่มีขอบเขต คล้ายกับ Halmos หากต้องการใช้ Certora นักพัฒนาจะต้องเรียนรู้ภาษาใหม่ ซีวีแอลเพื่อเขียนข้อมูลจำเพาะ ภาษานี้อนุญาตให้มีคำอธิบายสั้น ๆ ของคุณสมบัติที่สำคัญมากมายผ่านค่าคงที่ของสัญญา ซึ่งเป็นคุณสมบัติที่ Halmos ไม่รองรับในขณะนี้ แม้ว่า Certora จะเป็นเครื่องมือแบบปิดซอร์สที่เป็นกรรมสิทธิ์ แต่ Certora ก็มีเครื่องมือตรวจสอบอย่างเป็นทางการที่มีประสิทธิภาพ พร้อมการพัฒนาอย่างต่อเนื่องและการสนับสนุนผู้ใช้ที่ดี
  
  ในทางกลับกัน Halmos เป็นเครื่องมือโอเพ่นซอร์สที่มีขนาดเล็กกว่าและปัจจุบันยังขาดคุณสมบัติบางอย่างที่ Certora จัดหาให้ แต่มีไว้เพื่อใช้เป็นสินค้าสาธารณะและมีไว้เป็นโซลูชันเฉพาะสำหรับการตรวจสอบสัญญาอัจฉริยะอย่างรวดเร็วโดยไม่ต้องใช้ ความจำเป็นในการติดตั้งและบำรุงรักษาที่กว้างขวาง
• สจล เป็นอีกเครื่องมือตรวจสอบอย่างเป็นทางการที่คล้ายกับ Halmos ก่อนหน้านี้เคยเป็นส่วนหนึ่งของ DappTools ซึ่งเป็นผู้นำของ Foundry ทั้ง HEVM และ Halmos มีคุณสมบัติที่ไม่ต้องการข้อกำหนดแยกต่างหากและสามารถดำเนินการทดสอบที่มีอยู่ในเชิงสัญลักษณ์เพื่อระบุการละเมิดการยืนยัน ซึ่งช่วยให้ผู้ใช้สามารถใช้ทั้งสองเครื่องมือแทนกันได้หรือรันแบบขนานสำหรับการทดสอบเดียวกัน โดยมีตัวเลือกมากมายสำหรับการทดสอบเชิงสัญลักษณ์
  
  เป็นที่น่าสังเกตว่า แม้จะมีความคล้ายคลึงกัน แต่ HEVM และ Halmos ก็ได้รับการพัฒนาโดยอิสระและแตกต่างกันในรายละเอียดการใช้งาน โดยเฉพาะอย่างยิ่งในแง่ของการเพิ่มประสิทธิภาพและกลยุทธ์การให้เหตุผลเชิงสัญลักษณ์ นอกจากนี้ HEVM ยังเขียนด้วยภาษา Haskell ในขณะที่ Halmos เขียนด้วยภาษา Python ทำให้ได้สัมผัสกับระบบนิเวศของ Python ที่สมบูรณ์ ความสามารถในการใช้เครื่องมือทั้งสองช่วยให้ผู้ใช้มีความยืดหยุ่นและมีตัวเลือกมากขึ้นในการรับประกันความปลอดภัยและความถูกต้องของสัญญาอัจฉริยะ

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

**

ความคิดเห็นที่แสดงในที่นี้เป็นความคิดเห็นของบุคลากร AH Capital Management, LLC (“a16z”) ที่ยกมาและไม่ใช่ความคิดเห็นของ a16z หรือบริษัทในเครือ ข้อมูลบางอย่างในที่นี้ได้รับมาจากแหล่งบุคคลที่สาม รวมถึงจากบริษัทพอร์ตโฟลิโอของกองทุนที่จัดการโดย a16z ในขณะที่นำมาจากแหล่งที่เชื่อว่าเชื่อถือได้ a16z ไม่ได้ตรวจสอบข้อมูลดังกล่าวอย่างอิสระและไม่รับรองความถูกต้องของข้อมูลในปัจจุบันหรือที่ยั่งยืนหรือความเหมาะสมสำหรับสถานการณ์ที่กำหนด นอกจากนี้ เนื้อหานี้อาจรวมถึงโฆษณาของบุคคลที่สาม a16z ไม่ได้ตรวจทานโฆษณาดังกล่าวและไม่ได้รับรองเนื้อหาโฆษณาใด ๆ ที่อยู่ในนั้น

เนื้อหานี้จัดทำขึ้นเพื่อวัตถุประสงค์ในการให้ข้อมูลเท่านั้น และไม่ควรใช้เป็นคำแนะนำทางกฎหมาย ธุรกิจ การลงทุน หรือภาษี คุณควรปรึกษาที่ปรึกษาของคุณเองในเรื่องเหล่านั้น การอ้างอิงถึงหลักทรัพย์หรือสินทรัพย์ดิจิทัลใดๆ มีวัตถุประสงค์เพื่อเป็นตัวอย่างเท่านั้น และไม่ถือเป็นการแนะนำการลงทุนหรือข้อเสนอเพื่อให้บริการที่ปรึกษาการลงทุน นอกจากนี้ เนื้อหานี้ไม่ได้มุ่งไปที่หรือมีไว้สำหรับการใช้งานโดยนักลงทุนหรือนักลงทุนที่คาดหวัง และไม่อาจเชื่อถือได้ไม่ว่าในกรณีใดๆ เมื่อตัดสินใจลงทุนในกองทุนใดๆ ที่จัดการโดย a16z (การเสนอให้ลงทุนในกองทุน a16z จะกระทำโดยบันทึกเฉพาะบุคคล ข้อตกลงจองซื้อ และเอกสารที่เกี่ยวข้องอื่นๆ ของกองทุนดังกล่าว และควรอ่านให้ครบถ้วน) การลงทุนหรือบริษัทพอร์ตการลงทุนใดๆ ที่กล่าวถึง อ้างถึง หรือ ที่อธิบายไว้ไม่ได้เป็นตัวแทนของการลงทุนทั้งหมดในยานพาหนะที่จัดการโดย a16z และไม่สามารถรับประกันได้ว่าการลงทุนนั้นจะให้ผลกำไรหรือการลงทุนอื่น ๆ ในอนาคตจะมีลักษณะหรือผลลัพธ์ที่คล้ายคลึงกัน รายการการลงทุนที่ทำโดยกองทุนที่จัดการโดย Andreessen Horowitz (ไม่รวมการลงทุนที่ผู้ออกไม่อนุญาตให้ a16z เปิดเผยต่อสาธารณะและการลงทุนที่ไม่ได้ประกาศในสินทรัพย์ดิจิทัลที่ซื้อขายในตลาดหลักทรัพย์) มีอยู่ที่ https://a16z.com/investments /.

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