ทีมนักวิจัย Google DeepMind ได้ทำการตรวจสอบอย่างเป็นทางการด้านความปลอดภัยของ Signal และเชื่อว่าเป็นครั้งแรกที่ AI ช่วยสร้างหลักฐานที่เชื่อมโยงการรับประกันความปลอดภัยระดับโปรโตคอลเข้ากับการใช้งานการเข้ารหัสที่แพร่หลาย
เครื่องมือ AlphaProof Code อาศัยเอเจนต์ที่ถูกควบคุมโดยมนุษย์ในการเขียนข้อกำหนดใน Lean, ประเมินความหมายของโค้ดเครื่อง และสร้างหลักฐานที่เอเจนต์เขียนขึ้นเพื่อตรวจสอบโดยเคอร์เนลของ Lean
ในการนี้ AlphaProof Code ได้ตรวจสอบการจับมือแบบ post-quantum PQXDH และ Triple Ratchet ของ Signal ซึ่งเป็นการยืนยันการออกแบบด้าน forward secrecy, authentication, post-compromise security และ handshake secrecy ของ libsignal
การทำงานนี้เป็นก้าวสำคัญในการตอบสนองต่อความท้าทายของ Beneficial AI Foundation ที่ให้ตรวจสอบโปรโตคอลและแอป Signal ด้วย Lean
แม้เอเจนต์จะสร้างโค้ด Lean ถึง 6.5 ล้านบรรทัด แต่ก็ได้มีการตรวจสอบและติดธงบางส่วนที่ต้องให้มนุษย์ทบทวน โดย Swarat Chaudhuri กล่าวว่านี่คือระบบที่สร้างขึ้นเพื่อการทำงานร่วมกันระหว่างมนุษย์และ AI โดยพื้นฐาน
ทีมนักวิจัยเชื่อว่า AlphaProof Code สามารถลดต้นทุนการตรวจสอบอย่างเป็นทางการได้อย่างมาก แม้ว่างาน Signal นี้จะใช้เวลาสี่สัปดาห์สำหรับทีมห้าคนและ ‘โทเค็นจำนวนมาก’ แต่พวกเขาก็ตั้งเป้าว่าจะขยายขนาดเทคโนโลยีนี้ต่อไปในการออกแบบซอฟต์แวร์โดยทั่วไป ไม่ใช่แค่โปรโตคอลการเข้ารหัสเท่านั้น
ศัพท์ที่ควรรู้
- Signal – แอปพลิเคชันส่งข้อความเข้ารหัสที่ใช้เทคนิคการรักษาความปลอดภัยสูง
- AlphaProof Code – เครื่องมือที่ใช้ AI ในการช่วยตรวจสอบความถูกต้องของระบบรักษาความปลอดภัย
- Lean – ภาษาสำหรับการพิสูจน์ทางคณิตศาสตร์ที่ใช้ในการตรวจสอบความถูกต้องของโปรโตคอล
- post-quantum PQXDH – หนึ่งในโปรโตคอลการจับมือที่ทนทานต่อการโจมตีจากคอมพิวเตอร์ควอนตัม
- Triple Ratchet – กลไกการรักษาความลับที่ใช้ในโปรโตคอลการส่งข้อความเพื่อป้องกันการถูกเจาะข้อมูลย้อนหลัง
ที่มา: The Register