Google DeepMind ใช้ AI สร้างโค้ดพิสูจน์ 6.5 ล้านบรรทัด ตรวจสอบโปรโตคอล Signal แบบตัวต่อตัว

กูเกิล ดีปมายด์ (Google DeepMind) ใช้ AI agent ตรวจพิสูจน์คุณสมบัติด้านความปลอดภัยหลักของโค้ดสำหรับการสนทนาแบบตัวต่อตัวในโปรโตคอลเข้ารหัสของ Signal ด้วยคณิตศาสตร์ การวิเคราะห์ใช้เวลา 4 สัปดาห์ และไม่ได้ครอบคลุมการสนทนาแบบกลุ่มหรือแอป Signal ทั้งระบบ

กูเกิล ดีปมายด์เผยผลการศึกษาผ่านบล็อกทางการและเอกสารทางเทคนิคพร้อมหลักฐานพิสูจน์เมื่อวันที่ 10 งานนี้ใช้ AlphaProof Code ซึ่งเป็นเฟรมเวิร์กการตรวจสอบเชิงรูปแบบที่ให้ AI agent เขียนบทพิสูจน์จากเงื่อนไขด้านความปลอดภัยที่มนุษย์กำหนด

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

นักวิจัยเป็นผู้กำหนดคุณสมบัติด้านความปลอดภัยที่จะพิสูจน์ รวมถึงเขียนและตรวจทานข้อกำหนด บทพิสูจน์ที่ AI agent สร้างต้องผ่านตัวตรวจสอบของ Lean จึงจะได้รับการยอมรับ ผลสรุปจึงไม่ได้อาศัยการตัดสินใจของ agent เพียงอย่างเดียว

สิ่งที่นำมาตรวจสอบคือไฟล์โปรแกรมสำหรับการสนทนาแบบตัวต่อตัวที่สร้างด้วย libsignal 0.105.4 และ SPQR 1.6.0 นักวิจัยนำไลบรารีที่ไม่ได้แก้ไขไปครอบด้วยเครื่องมือบรรทัดคำสั่ง แล้วคอมไพล์เป็นโค้ดเครื่อง AArch64 เพื่อวิเคราะห์

ฟังก์ชันที่ตรวจสอบประกอบด้วย PQXDH ซึ่งใช้ตกลงคีย์เข้ารหัสเมื่อเริ่มการสนทนา และ Triple Ratchet ซึ่งปรับคีย์ใหม่ในทุกข้อความ โปรโตคอลในตระกูล Signal ยังถูกใช้ใน Google Messages, WhatsApp และ Meta Messenger ด้วย

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

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

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

งานวิจัยนี้ไม่ได้จำกัดอยู่แค่เอกสารออกแบบโปรโตคอล แต่เปรียบเทียบการทำงานของไฟล์โปรแกรมที่คอมไพล์แล้วกับข้อกำหนด อย่างไรก็ตาม สิ่งที่พิสูจน์คือไฟล์โปรแกรมบรรทัดคำสั่งที่นักวิจัยสร้างขึ้น ไม่ใช่ไฟล์โปรแกรมของแอป Signal

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

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

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

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

เอห์เรน เครต (Ehren Kret) ประธานเจ้าหน้าที่ฝ่ายเทคโนโลยีของ Signal กล่าวว่า “การตรวจสอบเชิงรูปแบบที่ผ่านมาเน้นโค้ดเพียงส่วนเล็ก ๆ แต่วิธีการของกูเกิล ดีปมายด์ขยายขอบเขตได้มากขึ้น” เครตชื่นชมที่มีการตรวจสอบการนำโปรโตคอลไปใช้ในวงกว้างขึ้น

ไวร์ด (WIRED) ระบุว่ายังไม่ชัดเจนว่างานนี้แก้ปัญหาการขยายการใช้งานจริงและต้นทุนของการตรวจสอบเชิงรูปแบบที่มี AI ช่วยได้แล้วหรือไม่ กูเกิลไม่ได้เปิดเผยค่าใช้จ่ายในการวิเคราะห์หรือแผนเปิดตัวผลิตภัณฑ์และบริการตรวจสอบเชิงพาณิชย์

เอกสารวิจัยเสนอให้การตรวจสอบในอนาคตครอบคลุมการส่งข้อความแบบกลุ่ม ฟังก์ชันซ่อนตัวตนผู้ส่ง และโปรโตคอลฝั่งเซิร์ฟเวอร์ กูเกิล ดีปมายด์เผยแพร่ข้อกำหนดและเอกสารประกอบการพิสูจน์แล้ว