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

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

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

อีกมุมหนึ่ง งานนี้ยังเป็นการโชว์ศักยภาพของ Google DeepMind ในการทำ formal verification ด้วยเฟรมเวิร์ก AI ตัวใหม่ที่ชื่อว่า AlphaProof Code

ต้นฉบับจาก Ars Technica ระบุว่าตอนนี้วงการกำลังให้ความสนใจกับการใช้ AI ช่วยทำ formal verification กันมาก เพราะแนวทางนี้ถูกมองว่าเป็นเหมือนจอกศักดิ์สิทธิ์ของความปลอดภัยซอฟต์แวร์มานาน เนื่องจากใช้หลักคณิตศาสตร์ตรวจสอบและยืนยันว่าซอฟต์แวร์ทำงานตรงตามที่ออกแบบไว้จริง ไม่มีช่องโหว่ร้ายแรงแอบแฝง

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