Newsletter Subscribe
Enter your email address below and subscribe to our newsletter
[forminator_form id="25163"]
Google DeepMind-ის ხელოვნურმა ინტელექტმა Signal-ის დაშიფვრის უსაფრთხოება დაამტკიცა
- WIRED-ის ცნობით, Google DeepMind-ის ახალმა AI ჩარჩომ, AlphaProof Code-მა, ოთხკვირიანი პროექტის ფარგლებში Signal-ის პროტოკოლის რამდენიმე ძირითადი უსაფრთხოების გარანტია მათემატიკურად დაამტკიცა
wired.com. - ინსტრუმენტმა სწორად აღმოაჩინა Signal-ის ძველ ვერსიებში არსებული, დიდი ხნის წინ გამოსწორებული ხარვეზები; კვლევა არ მოიცავდა მთლიან აპლიკაციას, DeepMind კი მტკიცებულებების გასაჯაროებას გეგმავს
wired.com. - Signal-ის ტექნიკურმა დირექტორმა ერენ კრეტმა განაცხადა, რომ ეს ნამუშევარი "კიდევ უფრო მეტ ნდობას" იძლევა, ხოლო Google-მა არ დააკონკრეტა პროექტის ღირებულება ან კომერციული ვერსიის შექმნის გეგმები
wired.com.
Google DeepMind-ის მკვლევრებმა ახალი AI ჩარჩო, სახელწოდებით AlphaProof Code, გამოიყენეს Signal-ის პროტოკოლის რამდენიმე ძირითადი კრიპტოგრაფიული გარანტიის მათემატიკურად დასამტკიცებლად. WIRED-ის 10 ნოემბრის ცნობით, ოთხკვირიანმა საპილოტე პროექტმა პროტოკოლის შესწავლილ ნაწილებში ახალი დაუცველობები არ გამოავლინაwired.com.
შედეგი მნიშვნელოვანია არა მხოლოდ Signal-ის აპლიკაციისთვის. ეს პროტოკოლი ასევე უზრუნველყოფს Google Messages-ისა და WhatsApp-ის (Meta Platforms, Inc. ) შეტყობინებების დაცვას, ამიტომ ანალიზი დაშიფვრის დამოუკიდებელ შემოწმებას წარმოადგენს, რომელიც მსოფლიო კომუნიკაციების დიდ ნაწილს იცავს. ეს ასევე აჩვენებს, რომ AI აგენტებს შეუძლიათ დააჩქარონ ფორმალური ვერიფიკაცია, რაც პროგრამული უზრუნველყოფის გამართულობის მათემატიკური დასაბუთების ნელი, მაგრამ მოთხოვნადი მეთოდიაwired.com.
რა გამოავლინა ანალიზმა
მკვლევრებმა AlphaProof Code გამოსცადეს Signal-ის ძველ ვერსიებზე, რომლებიც შეიცავდა ცნობილ, დიდი ხნის წინ გამოსწორებულ ხარვეზებს. WIRED-ის ცნობით, ინსტრუმენტმა სწორად იპოვა ეს ხარვეზები და აჩვენა, რომ აღნიშნული ვერსიების ფორმალური ვერიფიკაცია შეუძლებელი იყო. DeepMind აქვეყნებს სპეციფიკაციებსა და მტკიცებულებებს, რათა სხვა ვერიფიკაციის პროექტებმაც შეძლონ მათი გამოყენებაwired.com.
კვლევის მასშტაბი შეზღუდული იყო. ნამუშევარი არ მოიცავდა Signal-ის სრულ მობილურ აპლიკაციას და მკვლევრებმა მას მხოლოდ ერთი ეტაპი უწოდეს უფრო ხანგრძლივ პროცესში. "ჩვენ ძალიან მოხარულები ვართ ამ შედეგით, თუმცა ჯერ კიდევ დიდი გზაა გასავლელი, სანამ ამას მსოფლიოს ყველა პროგრამულ უზრუნველყოფაზე გავავრცელებთ, მაგრამ ჩვენ სწორედ ამის გაკეთება გვსურს," განუცხადა DeepMind-ის მკვლევარმა სვარატ ჩაუდჰურიმ WIRED-სwired.com.
გუნდის თქმით, Signal-ის მიერ ადრე ჩატარებულმა ფორმალურმა ვერიფიკაციამ მათ საწყის ეტაპზე დახმარება გაუწია. "მიუხედავად იმისა, რომ წინა ფორმალური ვერიფიკაცია კოდის მცირე ნაწილებზე იყო ფოკუსირებული, Google DeepMind-ის მიდგომა მნიშვნელოვანი გაფართოების საშუალებას იძლევა," განაცხადა Signal-ის ტექნიკურმა დირექტორმა ერენ კრეტმა და დასძინა, რომ ვერიფიკაცია კომპანიას "კიდევ უფრო მეტ ნდობას" ანიჭებს AI-ზე დაფუძნებული უსაფრთხოების საფრთხეების ზრდის ფონზეwired.com.
გადატვირთული სფერო
DeepMind-ის ნამუშევარი მაშინ გამოჩნდა, როდესაც სხვა ჯგუფებიც მსგავს მიზნებს ისახავენ. 2026 წლის აპრილში Signal-მა, Beneficial AI Foundation-მა და Lean FRO-მ წამოიწყეს Signal Shot, საჯარო ინიციატივა Signal-ის პროტოკოლისა და მისი Rust იმპლემენტაციის შესამოწმებლად Lean-ის დამხმარე საშუალებების გამოყენებით. ფონდის ცნობით, პროექტი მიზნად ისახავს Signal-ის რეალური კოდის Lean-ში გადატანას და იმის დამტკიცებას, რომ ის შეესაბამება პროტოკოლის ვერიფიცირებულ მოდელს. Startup Fortune-ის აღნიშვნით, DeepMind-ის შედეგი ამ პროექტისგან დამოუკიდებელიაbeneficialaifoundation.org+2.
ღია კითხვები ხარჯების შესახებ
ჯერჯერობით გაურკვეველია, შესაძლებელია თუ არა AI-ით ავტომატიზებული ვერიფიკაციის მასშტაბირება მისაღებ ფასად. DeepMind-მა Signal-ის ანალიზი უფასოდ, კვლევითი პროექტის ფარგლებში ჩაატარა. WIRED-ის ცნობით, Google-მა არ დააკონკრეტა ხარჯები და არც ის, გეგმავს თუ არა კომერციული ვერიფიკაციის პროდუქტის შექმნასwired.com.
ჩაუდჰურის თქმით, მთავარი მიღწევა იყო პროცესი, რომელშიც AI აგენტები თავადვე უწყობენ ხელს და ასწორებენ საკუთარ ნამუშევარს, ხოლო ადამიანები მას საკვანძო მომენტებში აკონტროლებენ. "ჩვენ არ გვსურს ისეთი სამყარო, სადაც AI ადგენს მიზნებს, AI ქმნის მტკიცებულებებს და ფაქტობრივად აბარებს თვითშემოწმებად ტესტებს," თქვა მან. "არსებობს ოქროს შუალედი."wired.com
წყაროები (26)
- 1 A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure www.wired.com
- 2 Signal Shot: One Giant Lean for Protocol Security www.beneficialaifoundation.org
- 3 Signal Shot - Beneficial AI Foundation www.beneficialaifoundation.org
- 4 Google DeepMind's AI proves key Signal protocol guarantees in four weeks - Startup Fortune startupfortune.com
- 5 Google DeepMind usó IA para verificar matemáticamente la seguridad del cifrado de Signal www.infobae.com
- 6 DeepMind AI Verifies Signal Protocol in 4 Weeks, Finding No ... www.zetik.com
- 7 DeepMind’s AI tool formally verifies parts of the Signal protocol aiunderstanding.org
- 8 DeepMind proves Signal protocol cryptographic guarantees… | TLDR tldr.tech
- 9 Google DeepMind Proves Signal Protocol Security Using AI in ... www.contentbuffer.com
- 10 Google DeepMind’s new AI mathematically proved key parts… | TLDR tldr.tech
- 11 Google DeepMind’s new AI mathematically proved key parts of Signal’s encryption are secure madrobot.blog
- 12 Google AI News aiunderstanding.org
- 13 DeepMind Uses AI Tools to Formally Verify the Security of the Signal Protocol www.techflowpost.com
- 14 Lean: Extensible, Scalable, Trusted. leodemoura.github.io
- 15 BAIF Launches 'Signal Shot' to Verify Signal Protocol Using AI www.verity.news
- 16 The Lean Theorem Prover: Design, Evolution, and Impact leodemoura.github.io
- 17 Signal Shot: The Platform Is Ready - Leonardo de Moura leodemoura.github.io
- 18 SVIL 2026 · Fall beneficial-ai-foundation.github.io
- 19 Cryspen | Software Verification in Lean cryspen.com
- 20 Blog — Beneficial AI Foundation www.beneficialaifoundation.org
- 21 Leonardo de Moura leodemoura.github.io
- 22 Theorem Proving in Industry with Lean lean-lang.org
- 23 Signal — Blog — Beneficial AI Foundation www.beneficialaifoundation.org
- 24 Frontier models are failing one in three production attempts - LinkedIn www.linkedin.com
- 25 Software Verification in Lean leodemoura.github.io
- 26 Google DeepMind Used AlphaProof Code to Analyze the Signal Protocol mezha.net
