DeepMind อ้างว่าได้พิสูจน์ความปลอดภัยของ Signal protocol ที่ใช้ใน WhatsApp

Google DeepMind เผยผลวิเคราะห์ที่ระบุว่าได้ “formally verified” ความปลอดภัยของ Signal protocol ซึ่งเป็นโปรโตคอลเข้ารหัสแบบ end-to-end ที่ใช้กับ Signal รวมถึง WhatsApp และ Google Messages ด้วย งานนี้ถูกมองว่าเป็นความก้าวหน้าสำคัญทั้งในฝั่งคริปโตกราฟีและ AI เพราะเป็นการใช้ agentic AI มาช่วยทำ formal verification ซึ่งเป็นวิธีพิสูจน์เชิงคณิตศาสตร์ว่าโปรโตคอลทำงานตามคุณสมบัติความปลอดภัยที่อ้างไว้ภายใต้ทุกเงื่อนไข

Formal verification ต่างจากการทดสอบซอฟต์แวร์ทั่วไปตรงที่ไม่ได้พยายามแค่หาช่องโหว่ แต่พยายามพิสูจน์ว่าระบบไม่มีสถานการณ์ใดที่ทำให้ข้อกำหนดความปลอดภัยล้มเหลวตามที่กำหนดไว้ ในกรณีนี้ DeepMind ชี้ว่าผลลัพธ์ดังกล่าวช่วยยืนยันความแข็งแรงของโปรโตคอลที่ถูกใช้กว้างขวางในบริการส่งข้อความยอดนิยมหลายตัว และยังสอดคล้องกับภาพลักษณ์ของ Signal ที่ถูกมองเป็นมาตรฐานทองคำของระบบเข้ารหัสแบบ end-to-end มานาน โดย Edward Snowden เคยออกมาสนับสนุนแพลตฟอร์มนี้ด้วย

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

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

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