Google DeepMind ใช้เอเจนต์ AI ตรวจสอบโค้ดเครื่องหลักของ Signal

Google DeepMind เปิดตัว AlphaProof Code เมื่อวันที่ 10 พฤศจิกายน 2026 โดยใช้ทีมเอเจนต์ AI สร้างบทพิสูจน์ Lean ที่ตรวจสอบด้วยเครื่องได้ สำหรับคุณสมบัติด้านความปลอดภัยที่ระบุไว้ของโค้ด libsignal ที่คอมไพล์แล้วของ Signal ทีมนักวิจัย 5 คนทำงานพิสูจน์เสร็จภายใน 4 สัปดาห์ และเผยแพร่ข้อกำหนดกับชุดข้อมูลประกอบการตรวจสอบเพื่อให้บุคคลภายนอกทบทวน

งานนี้ก้าวพ้นจากแบบจำลองนามธรรมของการออกแบบโปรโตคอลของ Signal ไปสู่การนำไปใช้งานในรูปแบบที่คอมไพล์แล้ว นักวิจัยห่อหุ้ม crates ของ libsignal v0.105.4 และ SPQR v1.6.0 ที่ไม่ได้ดัดแปลงไว้ในโปรแกรมบรรทัดคำสั่งขนาดเล็ก จากนั้นใช้ rustc รุ่นมาตรฐานสร้างไฟล์ปฏิบัติการ Linux สำหรับ AArch64 ที่ลิงก์แบบสแตติก บทความวิชาการระบุว่า ผลงานนี้เป็นบทพิสูจน์ความปลอดภัยระดับโปรโตคอลชุดแรกสำหรับโค้ดที่ไม่ได้ดัดแปลงของการนำโปรโตคอลเข้ารหัสไปใช้งาน ซึ่งมีการใช้งานอย่างแพร่หลาย

AlphaProof Code แบ่งงานกันอย่างไร

นักวิจัย 5 คนใช้เวลา 4 สัปดาห์ทำงานพิสูจน์ โดยให้เอเจนต์ทำงานอย่างต่อเนื่องบนเวิร์กสเตชันของตน พร้อมดำเนินการพิสูจน์ทั้งแบบเชิงสัญลักษณ์และเชิงคำนวณควบคู่กัน บทความรายงานว่าเอเจนต์สร้างโค้ดบทพิสูจน์ Lean ที่ตรวจสอบด้วยเครื่องได้ประมาณ 6.5 ล้านบรรทัด โดยอาศัยข้อกำหนดที่ผ่านการรับรองความน่าเชื่อถือและความหมายของ AArch64 รวมกันราว 26,000 บรรทัด

มนุษย์เป็นผู้เลือกคุณสมบัติ จัดการความกำกวมและการแลกเปลี่ยนระหว่างความปลอดภัยกับปัจจัยอื่น ทบทวนข้อกำหนด และคงอำนาจอนุมัติขั้นสุดท้ายไว้ เอเจนต์ที่ขับเคลื่อนด้วย Gemini 4 Carbon และ Claude Opus 5.5 ร่างและทบทวนข้อกำหนดเหล่านั้น โดยมีการทบทวนจากโมเดลคนละตระกูลด้วย จากนั้นทีมเอเจนต์ Gemini 4 Carbon ก็สร้างโค้ดบทพิสูจน์ทั้งหมด โดยไม่มีผู้เขียนคนใดเขียนโค้ดบทพิสูจน์เอง การทำงานแต่ละรอบโดยทั่วไปใช้เอเจนต์ 40 ถึง 80 ตัวบนเครื่องเดียวเป็นเวลา 24 ถึง 72 ชั่วโมง โดยมีตัวประสานงานและหัวหน้าทีมคอยประสานงานผู้ปฏิบัติงานด้านการพิสูจน์ ขณะที่ผู้รับบทสถาปนิกและผู้รวมงานดูแลฐานบทพิสูจน์ร่วมกัน

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

ขอบเขตการตรวจสอบความปลอดภัยและการทดสอบบั๊กในอดีต

เป้าหมายที่ผ่านการตรวจสอบคือโค้ดเซสชันแบบหนึ่งต่อหนึ่ง ซึ่งครอบคลุมการจับมือ PQXDH และการรับส่งข้อความด้วย Triple Ratchet นักวิจัยรายงานว่ามีข้อพิสูจน์อิสระต่อกัน 2 แนวทาง ได้แก่ ทฤษฎีบทเชิงสัญลักษณ์ 10 ข้อภายใต้สมมติฐานการเข้ารหัสแบบอุดมคติ และบทพิสูจน์เชิงคำนวณที่กำหนดขอบเขตความได้เปรียบของผู้โจมตีด้วยสมมติฐานทางการเข้ารหัสและพจน์ทางสถิติ คุณสมบัติที่พิสูจน์ครอบคลุมการรักษาความลับของข้อความก่อนหน้าแม้สถานะปัจจุบันถูกขโมย การยืนยันตัวตน ความปลอดภัยหลังถูกเจาะระบบซึ่งเกี่ยวข้องกับการฟื้นคืนความปลอดภัยหลังเกิดการเจาะระบบ และการรักษาความลับของการจับมือ นอกจากนี้ ข้อพิสูจน์เชิงสัญลักษณ์ยังครอบคลุมการรักษาความลับของการจับมือหลังจากเกิดการโจมตี Diffie–Hellman ในภายหลัง

เพื่อทดสอบว่าข้อกำหนดเหล่านั้นตรวจจับข้อผิดพลาดที่เกิดขึ้นจริงได้หรือไม่ ทีมได้ย้อนกลับการแก้ไขสำหรับบั๊ก libsignal ที่เคยได้รับการแก้ไขแล้ว 2 รายการ ซึ่งเรียกว่า weak state และ small subgroup จากนั้นคอมไพล์ไบนารีที่ดัดแปลงใหม่ ในทั้งสองกรณี ทีมสร้างบทพิสูจน์ Lean ที่แสดงให้เห็นว่าทฤษฎีบทความปลอดภัยเชิงสัญลักษณ์ไม่เป็นจริง คลังข้อมูลสำหรับตรวจสอบสาธารณะแยกเนื้อหาเชิงคำนวณ เชิงสัญลักษณ์ ไบนารีที่ใช้ร่วมกัน และความหมายของ AArch64 ออกจากกัน พร้อมอธิบายวิธีสร้างบทพิสูจน์ขึ้นใหม่และตรวจสอบบทพิสูจน์อย่างเป็นอิสระ

Ehren Kret ประธานเจ้าหน้าที่ฝ่ายเทคโนโลยีของ Signal กล่าวว่า งานนี้ “ทำให้เรามั่นใจยิ่งขึ้นในหลักประกันด้านความเป็นส่วนตัวของโค้ดของเรา”

ข้อจำกัดและขั้นตอนถัดไป

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

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

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

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