บริษัท Anthropic ได้นำเสนอผลการทดลองโดยใช้แบบจำลอง AI เพื่อตรวจสอบความน่าเชื่อถือและความปลอดภัยของโครงการที่มีอยู่แล้วอย่างเป็นทางการ ในระหว่างการทดลอง แบบจำลอง AI ถูกนำมาใช้เพื่อสร้างหลักฐานทางคณิตศาสตร์ว่าไม่มีข้อผิดพลาดเกี่ยวกับหน่วยความจำสำหรับไลบรารีโอเพนซอร์ส 123 ไลบรารีที่ทดสอบในโครงสร้างพื้นฐาน OSS Fuzz
การตรวจสอบดำเนินการในระดับโค้ดแอสเซมบลีที่คอมไพล์แล้วสำหรับสถาปัตยกรรม RISC-V ปริมาณรวมของหลักฐานที่สร้างขึ้นมีจำนวนประมาณ 180 ล้านบรรทัดของโค้ดสำหรับระบบตรวจสอบ Rocq Prover (ประมาณ 600 บรรทัดต่อไฟล์ไบนารีที่มีคำสั่ง RISC-V จำนวน 18 คำสั่ง) หลักฐานเหล่านี้สร้างขึ้นโดยการแปลงการทดสอบฟัซซิ่งที่มีอยู่ให้เป็นข้อกำหนดอย่างเป็นทางการโดยอัตโนมัติ หลังจากนั้นแบบจำลอง AI ของ Claude พิสูจน์ได้ว่าโปรแกรมไม่มีข้อผิดพลาดสำหรับข้อมูลอินพุตใด ๆ ที่มีขนาดสูงสุดถึง 64 MB
ในระหว่างกระบวนการสร้างหลักฐาน ระบบ AI สามารถระบุและเตรียมแก้ไขข้อบกพร่องหลายร้อยรายการที่ก่อนหน้านี้ตรวจไม่พบโดยการทดสอบแบบฟัซซิ่ง ซึ่งรวมถึงช่องโหว่บัฟเฟอร์โอเวอร์โฟลว์เมื่อประมวลผลข้อมูลอินพุตบางอย่าง (เช่น CVE-2026-56132 ใน libexpat) รวมถึงข้อผิดพลาดเชิงตรรกะ นอกจากนี้ ระบบ AI ยังถูกใช้เพื่อพิสูจน์ความสอดคล้องของการใช้งานอัลกอริทึม zlib ในเคอร์เนลอีกด้วย Linux ข้อกำหนด RFC 1950
นอกจากนี้ ยังมีการสร้างตัวแปลภาษาสำหรับภาษา Python บางส่วนในภาษา Rust โดยมีการเตรียมหลักฐานยืนยันความสอดคล้องกับหลักการทำงานของ CPython อย่างเป็นทางการโดยใช้ชุดเครื่องมือ Verus เพื่อเปรียบเทียบพฤติกรรมกับ CPython ได้มีการรันโปรแกรม Python ที่สร้างขึ้นแบบสุ่มมากกว่า 1.7 ล้านโปรแกรม ใน 99.95% ของกรณี ผลลัพธ์ของการรันโปรแกรมเหล่านี้ในระบบใหม่และใน CPython ตรงกัน และความคลาดเคลื่อนใด ๆ ที่พบเป็นกรณีพิเศษที่ทราบกันดีอยู่แล้ว
การตรวจสอบอย่างเป็นทางการช่วยรับประกันการปฏิบัติตามข้อกำหนด แต่ไม่ได้ขจัดปัญหาด้านความปลอดภัยอย่างสมบูรณ์ เนื่องจากความเสี่ยงที่เกิดจากปัญหาการทำงานแบบมัลติเธรด การเชื่อมโยงแบบไดนามิก และพฤติกรรมที่ผิดปกติบนฮาร์ดแวร์จริงยังคงไม่ได้รับการตรวจสอบอย่างเป็นทางการ ข้อได้เปรียบที่สำคัญของแนวทางที่เสนอคือ สามารถทำงานได้โดยตรงกับไฟล์ไบนารี ทำให้ไม่จำเป็นต้องเขียนโค้ดที่มีอยู่ใหม่ในภาษาที่สามารถตรวจสอบอย่างเป็นทางการได้
ที่มา: opennet.ru
