Anthropic ระบุว่า Claude พิสูจน์คุณสมบัติด้านความปลอดภัยของไลบรารี 123 รายการได้

เมื่อวันที่ 22 ตุลาคม 2026 Anthropic เผยแพร่งานวิจัย โดยรายงานว่า Claude สร้างบทพิสูจน์เชิงรูปแบบที่ตรวจสอบด้วยเครื่องได้เกี่ยวกับคุณสมบัติด้านความปลอดภัยในระดับโค้ดภาษาแอสเซมบลีของ RISC-V สำหรับจุดเริ่มต้นการทดสอบฟัซซ์ 239 จุดในไลบรารีโอเพนซอร์ส 123 รายการ โดยร่วมมือกับ Theorem

Anthropic ระบุว่า Claude แก้ไขบั๊กที่พบ แล้วพิสูจน์ว่าโปรแกรมจะสิ้นสุดการทำงานตามปกติเสมอ โดยไม่ก่อให้เกิดข้อผิดพลาดด้านความปลอดภัยของหน่วยความจำหรือทำให้การยืนยันเงื่อนไขล้มเหลว สำหรับอินพุตทุกชุดที่มีขนาดต่ำกว่า 64 MB และการตอบสนองของระบบปฏิบัติการ Linux กับผังหน่วยความจำทุกรูปแบบที่อยู่ในแบบจำลอง บทพิสูจน์ตั้งอยู่บนสมมติฐานว่าโปรแกรมทำงานเป็นไบนารีแบบสแตติกเธรดเดียว โดยมีงบประมาณหน่วยความจำคงที่ บน CPU สถาปัตยกรรม RISC-V ที่ใช้ Linux Anthropic กล่าวว่า บทพิสูจน์มีความยาวรวมประมาณ 180 ล้านบรรทัดใน Rocq โดยบทพิสูจน์ทั่วไปมีความยาวประมาณ 600,000 บรรทัด เพื่อครอบคลุมไบนารีที่มีความยาวค่ามัธยฐาน 18,000 คำสั่ง RISC-V บริษัทกล่าวว่า เท่าที่ทราบ นี่เป็นความพยายามขนาดใหญ่ครั้งแรกในการใช้ AI กับการตรวจสอบเชิงรูปแบบสำหรับซอฟต์แวร์ที่ใช้งานจริงในระดับโค้ดภาษาแอสเซมบลี

บทพิสูจน์บางส่วน รวมถึงความหมายเชิงอรรถศาสตร์ของ RISC-V และระบบปฏิบัติการที่อยู่เบื้องหลังบทพิสูจน์เหล่านั้น กำลังเผยแพร่บน GitHub Anthropic กล่าวว่า ยังจะเผยแพร่องค์ประกอบที่เชื่อถือได้ซึ่งพัฒนาขึ้นสำหรับโครงการนี้และยังไม่เปิดเผยต่อสาธารณะ บทพิสูจน์ฉบับสมบูรณ์สำหรับการทดสอบฟัซซ์ที่ไม่ต้องแก้ไขโค้ด และข้อกำหนดสำหรับการทดสอบฟัซซ์ที่ไม่สามารถพิสูจน์ได้ ขณะเดียวกันจะไม่เผยแพร่บทพิสูจน์ที่อาจเปิดเผยบั๊กซึ่งยังไม่ได้แก้ไข

เปลี่ยนการทดสอบฟัซซ์ให้เป็นบทพิสูจน์เชิงรูปแบบ

แนวทางนี้แปลงการทดสอบฟัซซ์เดิมของแต่ละไลบรารีที่สามารถคอมไพล์ได้ให้เป็นข้อกำหนดเชิงรูปแบบ ซึ่งกำหนดกฎข้อเดียวว่า การทดสอบจะไม่ล้มเหลวสำหรับอินพุตใด ๆ ที่มีขนาดต่ำกว่า 64 MB ข้อกำหนดนี้นิยามขึ้นบนคำสั่ง RISC-V ที่คอมไพล์แล้ว โดยใช้ความหมายเชิงรูปแบบของชุดคำสั่ง RISC-V และกระบวนการของ Linux จาก Theorem จากนั้นตัวตรวจสอบบทพิสูจน์ Rocq จะตรวจสอบบทพิสูจน์ที่เสร็จสมบูรณ์แต่ละรายการเทียบกับข้อกำหนด Anthropic ระบุว่า แนวทางนี้ทำให้เหลือองค์ประกอบเพียงสามส่วนที่นักพัฒนาต้องเชื่อถือ ได้แก่ แบบจำลองเชิงรูปแบบของ RISC-V และกระบวนการของ Linux ข้อความทฤษฎีบทที่ถูกต้องตรงตามต้นฉบับ และตัวตรวจสอบ Rocq เอง

Anthropic กล่าวว่า ได้นำกระบวนการนี้ไปใช้กับโครงการหลายร้อยโครงการในโครงการ OSS-Fuzz ของ Google ซึ่งให้บริการทดสอบฟัซซ์อย่างต่อเนื่องแก่โครงการโอเพนซอร์สที่มีคุณสมบัติตรงตามเกณฑ์ และติดตั้งเครื่องมือวัดผลให้โปรแกรม C และ C++ โดยอัตโนมัติด้วย AddressSanitizer ซึ่งเป็นเครื่องมือที่ทำให้โปรแกรมหยุดทำงานทุกครั้งที่มีการเข้าถึงหน่วยความจำอย่างไม่ถูกต้อง ภาคผนวกลงวันที่ 22 ตุลาคม 2026 ระบุทฤษฎีบทฉบับเต็มที่พิสูจน์ไว้ว่า สำหรับอินพุตทั้งหมดที่มีขนาดต่ำกว่า 64 MiB และผังหน่วยความจำทุกรูปแบบ ทั้งไบนารีที่ติดตั้ง ASan และไบนารีปกติจะไม่เกิดข้อผิดพลาด ไม่ยุติการทำงานอย่างผิดปกติ หรือแสดงพฤติกรรมที่ไม่ได้อยู่ในแบบจำลอง และทั้งคู่จะมีร่องรอยการอ่านและเขียน พฤติกรรมเมื่อสิ้นสุดการทำงาน และสถานะระบบไฟล์สุดท้ายเหมือนกัน

ภาคผนวกระบุว่า Claude เขียนโค้ด Rocq ประมาณหนึ่งพันล้านบรรทัดระหว่างดำเนินงาน โดยประมาณ 180 ล้านบรรทัดผ่านการตรวจสอบบทพิสูจน์ จุดเริ่มต้นของตัวแยกวิเคราะห์ใน cJSON ซึ่งมีความยาว 391 บรรทัด ได้รับบทพิสูจน์ยาว 630,000 บรรทัด ขณะที่ fftw3 ซึ่งมีโค้ดที่ลิงก์เข้ามา 51,000 บรรทัด ได้รับบทพิสูจน์ยาว 480,000 บรรทัด เนื่องจาก Claude ได้รับอนุญาตให้แก้ไขโค้ดก่อนพิสูจน์เสร็จ Anthropic กล่าวว่า บริษัทหักคะแนนสำหรับการแก้ไขโค้ด ให้คะแนนพิเศษสำหรับการพิสูจน์ว่าแพตช์เปลี่ยนแปลงอินพุตใดบ้าง และบันทึกพร้อมตรวจสอบแพตช์เพื่อยับยั้งการแฮ็กรางวัล

บั๊กที่พบระหว่างการพยายามพิสูจน์

Anthropic รายงานว่า ความพยายามในการพิสูจน์เผยให้เห็นบั๊กหลายร้อยรายการ ซึ่งหลายรายการเป็นบั๊กที่เครื่องมือฟัซซ์ไม่น่าจะพบได้ ระหว่างพิสูจน์จุดเริ่มต้นของไลบรารีแห่งหนึ่ง Claude พบตัวนับในโปรแกรมคลายการบีบอัดมีค่าอันเดอร์โฟลว์ จนทำให้เกิดการเขียนข้อมูลนอกขอบเขต แต่จะเกิดขึ้นเฉพาะกับอินพุตขนาดประมาณ 20 MB ที่มีผังหน่วยความจำเฉพาะแบบซึ่งพบได้ยากเท่านั้น สิ่งที่พบอื่น ๆ ได้แก่ การอ่านข้อมูลนอกขอบเขตในตัวถอดรหัสภาพ ซึ่งต้องใช้อินพุตขนาด 64 MB และหน่วยความจำมากกว่า 2 GB การอ่านข้อมูลนอกขอบเขตที่ต้องอาศัยลำดับการเรียกใช้เฉพาะระหว่างแฮนเดิลสองรายการที่อ้างถึงไฟล์เดียวกัน และการค้นพบ CVE-2026-56132 ใน libexpat อีกครั้ง ซึ่งต้องใช้อินพุตที่ซ้อนกันลึกหลายชั้น

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

การทดลองเพิ่มเติมและข้อค้นพบด้านประสิทธิภาพ

นอกเหนือจาก OSS-Fuzz แล้ว Anthropic ยังให้ Claude เขียนข้อกำหนดเชิงรูปแบบของ RFC 1950 ซึ่งเป็นเอกสารทางเทคนิคที่กำหนดรูปแบบการบีบอัด zlib แล้วพิสูจน์ว่า zlib ที่นำไปใช้ในเคอร์เนล Linux ทำงานได้ถูกต้องตามข้อกำหนดดังกล่าว Claude พิสูจน์ไบนารีที่คอมไพล์สำหรับ x86 โดยตรง โดยใช้ความหมายเชิงรูปแบบของชุดคำสั่ง x86 ที่ Claude สร้างขึ้น และ Anthropic ระบุว่าได้นำกระบวนการเดียวกันไปใช้กับไลบรารีอื่น ๆ ที่มีผู้ใช้อย่างแพร่หลายอีกครึ่งโหล พร้อมพบบั๊กเล็กน้อยในกรณีขอบที่ไม่สามารถนำไปใช้โจมตีได้ ซึ่งกำลังส่งรายงานไปยังโครงการต้นทาง บริษัทยังรายงานด้วยว่า การสร้างความหมายเชิงรูปแบบของ x86 เผยให้เห็นข้อผิดพลาดหลายร้อยรายการในเอกสารอ้างอิงอย่างเป็นทางการ และบั๊กอีกจำนวนหนึ่งที่น้อยกว่าในตัวฮาร์ดแวร์เอง อีกทั้งการทำงานตามความหมายเชิงรูปแบบทีละคำสั่งยังสามารถบูตสภาพแวดล้อมผู้ใช้ของ Ubuntu บนเคอร์เนล Linux ได้

ในการทดลองอีกครั้ง Claude สร้างตัวแปลภาษา (interpreter) สำหรับภาษา Python ส่วนใหญ่ด้วยภาษา Rust และใช้เครื่องมือตรวจสอบ Verus พิสูจน์ว่าตัวแปลภาษานี้เป็นไปตามความหมายของ CPython ที่ระบุไว้ในบทความวิชาการ ภาคผนวกทางเทคนิค ระบุว่ามีการพิสูจน์ครบทั้ง 17 ระดับของตัวแปลภาษา โดยทฤษฎีบทที่พิสูจน์ได้ระบุว่า “เมื่อใดก็ตามที่ตัวแปลภาษาส่งคืนผลลัพธ์ ผลลัพธ์นั้นจะตรงกับที่ความหมายเชิงรูปแบบกำหนดไว้” Anthropic ระบุว่า การทดสอบเชิงประจักษ์กับโปรแกรม Python ที่สุ่มสร้างขึ้น 1.7 ล้านโปรแกรมพบว่ามีพฤติกรรมเหมือนกับ CPython ในการทดสอบ 99.95% ส่วนข้อผิดพลาด 7 รายการที่จงใจใส่เข้าไปนั้น มี 5 รายการที่ผ่านการทดสอบแบบสุ่ม แต่ทั้ง 7 รายการทำให้การพิสูจน์ไม่ผ่าน

เพื่อวัดประสิทธิภาพ Anthropic สร้างงานตรวจสอบขนาดเล็ก 36 งาน โดยย่อจุดเริ่มต้นการทำงานจริงของ OSS-Fuzz ให้เป็นโปรแกรมที่มีคำสั่ง 283–2,491 คำสั่ง จำกัดอินพุตไว้ที่ 64 ไบต์ และแทนที่ AddressSanitizer ด้วยรันไทม์ “mini-ASan” ที่มีคำสั่งประมาณ 100 คำสั่ง Anthropic รายงานว่า Opus 5.5 พิสูจน์งานได้ครึ่งหนึ่งโดยใช้โทเค็นน้อยกว่า Opus 5 ประมาณ 40% Anthropic ยังรายงานด้วยว่าเอเจนต์ที่ได้รับอนุญาตให้คัดลอกข้อพิสูจน์ของกันและกันในพื้นที่ทำงานร่วมกันใช้โทเค็นน้อยกว่าเอเจนต์ที่ทำงานลำพัง 17% โดยบางเอเจนต์ทำงานสำเร็จหลังจากก่อนหน้านี้ล้มเหลวเมื่อทำงานคนเดียว และเอเจนต์ที่ทำงานลำพังไม่สามารถทำข้อพิสูจน์ให้เสร็จได้ 2 รายการ บริษัทระบุว่าผลจากการนำงานของกันและกันกลับมาใช้ซ้ำแบบเดียวกันนี้เกิดขึ้นในวงกว้างระหว่างโครงการ OSS-Fuzz โดยทีมเอเจนต์คัดลอกข้อพิสูจน์ที่ทำเสร็จแล้วมาปรับใช้ เพราะเนื้อหาส่วนใหญ่ของแต่ละข้อพิสูจน์ครอบคลุมโค้ดเริ่มต้นของรันไทม์ C และ AddressSanitizer ที่ใช้ร่วมกัน

ข้อจำกัดที่ระบุไว้และโครงการ OSS Verify

Anthropic ระบุว่าข้อพิสูจน์เหล่านี้ไม่ได้หมายความว่าคลังซอฟต์แวร์ปลอดจากข้อผิดพลาด เพราะข้อผิดพลาดที่ยังเหลืออยู่อาจอยู่ในองค์ประกอบที่เชื่อถือได้ หรืออยู่นอกขอบเขตของการพิสูจน์ ข้อพิสูจน์ครอบคลุมไบนารี RISC-V แบบเธรดเดียวและแบบสแตติกที่ลิงก์กับ musl libc ขณะที่ผู้ใช้ส่วนใหญ่ใช้งานคลังซอฟต์แวร์เหล่านี้บน x86 หรือ ARM และลิงก์แบบไดนามิกกับ glibc อีกทั้ง AddressSanitizer ก็ตรวจจับข้อผิดพลาดด้านความปลอดภัยของหน่วยความจำได้ไม่ทั้งหมด บริษัทกล่าวว่าคาดว่าข้อจำกัดเหล่านี้จะจัดการได้เมื่อโมเดลพัฒนาขึ้น

Theorem เปิดให้โครงการโอเพนซอร์สที่มีคุณสมบัติตามเกณฑ์ใช้กระบวนการเดียวกันได้ฟรีผ่านโครงการ OSS Verify การสมัครเข้าร่วมทำได้โดยส่งคำขอรวมโค้ด (pull request) เพื่อเพิ่มไฟล์ project.yaml, Dockerfile และ build.sh ลงในคลังของโครงการ โดย Theorem ระบุว่าจะพิจารณาโครงการในแนวทางคล้ายกับ OSS-Fuzz และให้ความสำคัญกับโครงสร้างพื้นฐานสำคัญที่มีผู้ใช้งานอย่างแพร่หลาย ตามข้อมูลของ Theorem ผู้ดูแลโครงการจะได้รับข้อพิสูจน์ Rocq ซึ่งตรวจสอบโดยเคอร์เนล Rocq ว่าเป้าหมายการฟัซซิงแต่ละรายการจะไม่ทำให้โปรแกรมหยุดทำงานเมื่อได้รับอินพุตใดๆ ที่มีขนาดไม่เกิน 64 MiB ข้อผิดพลาดที่พบระหว่างกระบวนการพิสูจน์จะได้รับการเปิดเผยเป็นการส่วนตัวแก่ผู้ดูแลโครงการทางอีเมล โดยไม่มีกำหนดเวลาสำหรับการเปิดเผยต่อสาธารณะ และการจัดทำข้อพิสูจน์อาจใช้เวลาหลายวัน แผนงานของ Theorem มุ่งตรวจสอบระบบนิเวศ Nix ทั้งหมด รวมถึงโครงสร้างพื้นฐานสำคัญอย่าง glibc, OpenSSL และ cURL