Google DeepMind ใช้ AI พิสูจน์ทางคณิตศาสตร์ว่า Signal Protocol ปลอดภัยจริง

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

เรื่องนี้น่าสนใจเพราะ Signal protocol คือเทคโนโลยีเข้ารหัสที่อยู่เบื้องหลังการสื่อสารของคนทั่วโลก ไม่ใช่แค่แอป Signal แต่ยังรวมถึง Google Messages และ WhatsApp ด้วย การพิสูจน์ครั้งนี้จึงเป็นการยืนยันความปลอดภัยจากฝ่ายอิสระอีกชั้นหนึ่ง

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

Swarat Chaudhuri นักวิจัยของ DeepMind บอกกับ Wired ว่าทีมตื่นเต้นกับผลลัพธ์นี้มาก แต่ยังมีทางต้องไปอีกยาวก่อนจะขยายวิธีนี้ไปใช้กับซอฟต์แวร์ทั้งโลกได้

เราตื่นเต้นมากกับผลลัพธ์นี้ แต่ยังมีทางยาวไกลก่อนที่เราจะสามารถขยายมันไปใช้กับซอฟต์แวร์ทั้งโลกได้ และเราต้องการทำแบบนั้น

ฝั่ง Signal เองก็ออกมาพูดถึงเรื่องนี้ Ehren Kret ซึ่งเป็น CTO ของ Signal ระบุว่าวิธีของ Google DeepMind ช่วยขยายขอบเขตการตรวจสอบได้มากกว่าการพิสูจน์แบบเดิมที่เคยทำแค่บางส่วนของโค้ด และยิ่งทำให้มั่นใจเรื่องการปกป้องความเป็นส่วนตัวมากขึ้น

อย่างไรก็ตาม DeepMind ทำโปรเจกต์นี้แบบไม่คิดค่าใช้จ่ายในฐานะงานวิจัย และ Google ก็ไม่เปิดเผยต้นทุนที่ใช้ รวมถึงไม่ตอบว่ามีแผนจะทำเป็นผลิตภัณฑ์หรือบริการเชิงพาณิชย์หรือไม่ คำถามใหญ่ในวงการตอนนี้คือ formal verification ที่ใช้ AI ช่วยนี้จะขยายสเกลไปใช้ได้จริงในวงกว้างและคุ้มค่าหรือไม่