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

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

რა დაადგინა ანალიზმა

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

რატომ არის ფორმალური ვერიფიკაცია მნიშვნელოვანი

ფორმალური ვერიფიკაცია მათემატიკას იყენებს იმის შესამოწმებლად, რომ პროგრამული უზრუნველყოფა განზრახვისამებრ მუშაობს, ამიტომ მისი მომხრეები მას დიდი ხანია პროგრამული უსაფრთხოების ერთგვარ „წმინდა გრაალად“ მოიხსენიებენ. AI-ის ეპოქამდე ძალიან დიდ დროს მოითხოვდა სასურველი მახასიათებლების აღწერა, მათი ფორმულებად გადაქცევა და მტკიცებულების შემუშავება. აგენტურ ხელოვნურ ინტელექტს შეუძლია მნიშვნელოვნად შეამციროს ბოლო ამოცანის დრო, რაც შესაძლებელს ხდის ისეთ ანალიზებს, როგორიც DeepMind-ის Signal-ის შეფასებაა. DeepMind-ის მთავარ მიღწევებს შორისაა ადამიანისა და AI-ის თანამშრომლობის პროცესი: აგენტებს შეუძლიათ წვლილი შეიტანონ და თითქმის ყველა ეტაპზე თავად გამოასწორონ შეცდომები, გადამწყვეტ მომენტებში კი ადამიანის ჩართულობასა და გადახედვას ითხოვენ. „ჩვენ არ გვინდა ისეთი ‚ვაიბის‘ სამყარო, სადაც AI აყალიბებს მიზნებს, AI ქმნის მტკიცებულებებს და ფაქტობრივად თავადვე დაწერილ გამოცდებს აბარებს“, ამბობს Swarat Chaudhuri, DeepMind-ის მეცნიერ-მკვლევარი, WIRED-თან საუბარში. „არსებობს შუალედური გზაც“.

ღია კითხვები მასშტაბსა და ხარჯებზე

ჯერ გაურკვეველია, რამდენად პრაქტიკული იქნება AI-ის დახმარებით ფორმალური ვერიფიკაცია ფართო გამოყენებისთვის და რამდენად ეფექტურად დაიცავს კოდის დიდ მოცულობას. DeepMind-მა Signal-ის ანალიზი უფასოდ, კვლევითი პროექტის სახით ჩაატარა, ხოლო Google-მა უარი თქვა ანალიზის ღირებულების გამჟღავნებაზე და კომენტარი არ გააკეთა იმაზე, გეგმავს თუ არა კომერციული ფორმალური ვერიფიკაციის პროდუქტის ან სერვისის გამოშვებას. Signal-ის ტექნიკური დირექტორი Ehren Kret განცხადებაში ამბობს, რომ ადრინდელი ფორმალური ვერიფიკაცია კოდის უფრო მცირე ნაწილებზე იყო ორიენტირებული, Google DeepMind-ის მიდგომა კი მნიშვნელოვან გაფართოებას იძლევა. „როცა AI-ით გამოწვეული უსაფრთხოების საფრთხეები იზრდება, Signal-ის პროტოკოლის იმპლემენტაციის მკაცრი ვერიფიკაცია ჩვენი კოდის კონფიდენციალურობის გარანტიებში კიდევ უფრო მეტ თავდაჯერებას გვაძლევს“, ამბობს Kret. Google Cloud-ის მთავარი მეცნიერი და DeepMind-ის კვლევის ვიცე-პრეზიდენტი Pushmeet Kohli ამბობს, რომ თუ იმპლემენტაციების სისწორის გადამოწმება ახლა შესაძლებელი ხდება, კომპანიებს, რომლებიც გარანტიებს ეყრდნობიან და ბაგებზე ღელავენ, შეეძლებათ თქვან, რომ ამ თვისებების დამტკიცება შეუძლიათ. Chaudhuri ამბობს, რომ DeepMind შედეგით აღფრთოვანებულია, თუმცა ჯერ დიდი მანძილია მსოფლიოს ყველა პროგრამულ უზრუნველყოფამდე.

წყაროები: Wired