Google DeepMind-ის ხელსაწყომ Signal-ის პროტოკოლის უსაფრთხოება დაამტკიცა

Google DeepMind-ის მკვლევრებმა აგენტური ხელოვნური ინტელექტი გამოიყენეს, რათა მათემატიკურად დაემტკიცებინათ, ანუ „ფორმალურად შეემოწმებინათ“, Signal-ის პროტოკოლის რამდენიმე ძირითადი კრიპტოგრაფიული გარანტია. ეს მნიშვნელოვანი მიღწევაა როგორც ფართოდ გამოყენებული კრიპტოგრაფიისთვის, ისე თავად ხელოვნური ინტელექტისთვის.

სამუშაო, რომელიც ერთგვარი კონცეფციის დამადასტურებელი პროექტის სახით მხოლოდ ოთხ კვირაში ჩატარდა, ორი მიზეზითაა მნიშვნელოვანი. ის კიდევ ერთხელ, დამოუკიდებლად ადასტურებს იმ კრიპტოგრაფიის სანდოობას, რომელიც მსოფლიოს საკომუნიკაციო მიმოწერის უზარმაზარ მოცულობას იცავს ისეთ პლატფორმებზე, როგორიცაა Signal-ის აპი, Google Messages და WhatsApp. ამასთან, ნაჩვენებია Google DeepMind-ის ფორმალური შემოწმების შესაძლებლობები ახალი ხელოვნური ინტელექტის ჩარჩოს, AlphaProof Code-ის გამოყენებით.

უფრო ფართოდ, ხელოვნური ინტელექტით დახმარებული ფორმალური შემოწმება ახლა აქტუალური თემაა, თუმცა გაურკვეველია, რამდენად პრაქტიკული იქნება მისი ფართოდ გამოყენება და რამდენად ეფექტურად დაიცავს ის დიდი მოცულობის კოდს. პროგრამული უზრუნველყოფის უსაფრთხოების სფეროში ფორმალური შემოწმების მომხრეები მას დიდი ხანია ერთგვარ საოცნებო მიზნად მიიჩნევენ, რადგან ამ მეთოდით მათემატიკის გამოყენებით მოწმდება და დასტურდება, რომ პროგრამა დანიშნულებისამებრ მუშაობს, ანუ მას კრიტიკული მოწყვლადობები არ აქვს.

ხელოვნური ინტელექტის ეპოქამდე ადამიანებს ძალიან დიდი დრო სჭირდებოდათ პროგრამული უზრუნველყოფის იმ მახასიათებლების აღსაწერად, რომელთა დამტკიცებაც სურდათ, ამ აღწერების ფორმულებად გარდასაქმნელად და შემდეგ მტკიცებულების შესამუშავებლად. აგენტურ ხელოვნურ ინტელექტს შეუძლია ამ უკანასკნელ სამუშაოზე დახარჯული დრო საგრძნობლად შეამციროს და ისეთი ანალიზი შესაძლებელი გახადოს, როგორიც DeepMind-მა Signal-ზე ჩაატარა. თუმცა ეს ანალიზიც შეზღუდული მასშტაბის იყო: მაგალითად, ფორმალურად არ შეუმოწმებიათ Signal-ის მთელი მობილური აპი. DeepMind-ის მკვლევრები ხაზს უსვამენ, რომ მათი მიგნებები უფრო ფართო პროცესის მხოლოდ ერთი ეტაპია.

DeepMind-ის მკვლევარმა სვარატ ჩაუდჰურიმ უაირდს (Wired) უთხრა: „ეს შედეგი ძალიან გვახარებს, მაგრამ წინ გრძელი გზაა, ვიდრე მსოფლიოს ყველა პროგრამულ უზრუნველყოფაზე ამის გავრცელებას შევძლებთ, და ჩვენ ამის გაკეთება გვინდა“.

DeepMind-ის ანალიზმა Signal-ის პროტოკოლის შესწავლილ ნაწილებში ახალი მოწყვლადობები ვერ აღმოაჩინა. თუმცა, როცა მკვლევრებმა AlphaProof Code Signal-ის ძველ ვერსიებზე გამოიყენეს, რომლებშიც ცნობილი და დიდი ხნის წინ გამოსწორებული მოწყვლადობები იყო, სისტემამ ისინი სწორად ამოიცნო და აჩვენა, რომ პროტოკოლის ფორმალური შემოწმება შეუძლებელი იყო. მკვლევრები Signal-ის პროტოკოლის ანალიზისთვის შექმნილ სპეციფიკაციასა და მტკიცებულებას აქვეყნებენ, რათა ფორმალური შემოწმების სხვა სამუშაოებსაც დაეხმარონ.