LONDON (IT BOLTWISE) – DeepMind hat mit agentischer KI das Signal-Protokoll formal verifiziert. Das Projekt nutzt AlphaProof Code, um zentrale kryptografische Garantien mathematisch nachzuweisen. Laut den Forschern fanden sich keine neuen Schwachstellen in den geprüften Protokollteilen, allerdings scheitert eine Verifikation bei älteren Versionen mit bekannten, bereits behobenen Lücken. Offen bleibt, wie gut sich dieser Ansatz im großen Stil und zu bezahlbaren Kosten auf umfangreiche Codebasen übertragen lässt.
DeepMind stellt den nächsten Baustein einer Idee in den Mittelpunkt, die in der Software-Sicherheit seit Jahren wie ein Idealbild kursiert: nicht nur Tests und Code-Reviews, sondern eine mathematische Verifikation, die beweist, dass ein System seine zugesicherten Eigenschaften tatsächlich erfüllt. Im konkreten Fall geht es um das Signal-Protokoll, eine in der Praxis weit verbreitete Kryptografie-Basis für Ende-zu-Ende-Verschlüsselung. DeepMind beschreibt, dass Forschende mit agentischer KI zentrale kryptografische Garantien des Protokolls formal verifiziert haben – also nicht nur plausibilisiert, sondern rechnerisch durch einen Beweis abgesichert, der die gewünschte Korrektheit der betrachteten Spezifikation stützt.
Der zeitliche Rahmen macht dabei die Signalwirkung der Meldung aus: Als eine Art Proof-of-Concept ordnen die Forschenden die Arbeit auf vier Wochen ein. Inhaltlich ist die Bedeutung zweigeteilt. Zum einen liefert die unabhängige formale Prüfung eine zusätzliche Validierung jener kryptografischen Bausteine, die große Mengen weltweiter Kommunikation in Apps wie Signal, Google Messages und WhatsApp absichern. Zum anderen zeigt das Projekt, dass formale Verifikation nicht ausschließlich als Handarbeit für Sicherheitsexperten funktioniert, sondern auch durch ein neues KI-Framework – AlphaProof Code – beschleunigt werden kann, indem es Schritte bis hin zu Beweisen mit unterstützt.
Technisch berührt die Studie damit genau die Engstelle, an der sich das Feld bisher abarbeitet: Vor dem KI-Zeitalter war formale Verifikation extrem aufwendig. Es brauchte Ressourcen, um zunächst die relevanten Software-Eigenschaften zu beschreiben, diese Annahmen in mathematische Formeln zu übersetzen und anschließend die Beweise zu konstruieren. Agentische KI kann den Teil der Beweis-Erstellung und -ausarbeitung verkürzen, weil sie eher die iterativen Arbeitsphasen übernimmt, die zwischen Spezifikation, Zwischenschritten und Korrekturen stattfinden. In der DeepMind-Analyse blieb der Umfang jedoch bewusst begrenzt: So wurde nicht die gesamte Signal-App als Ganzes verifiziert, sondern Auszüge bzw. Teile des Protokolls, die im Rahmen des Projekts untersucht werden sollten.
Für die Vertrauensfrage ist vor allem interessant, was das Team tatsächlich gefunden hat. In den betrachteten Bereichen des Signal-Protokolls identifizierten die Forschenden keine neuen Schwachstellen. Gleichzeitig zeigen sie die Grenzen der Verifikation sehr anschaulich: Als AlphaProof Code auf ältere Versionen angewendet wurde, die bekannte und schon lange behobene Sicherheitslücken enthalten, konnte das Protokoll nicht korrekt formal verifiziert werden. Genau diese Gegenprobe unterstreicht, dass es sich nicht um eine reine „Beschönigungs“-Prüfung handelt, sondern dass die Methode auch reale Fehlerzustände erkennt – zumindest in den geprüften Artefakten.
Bemerkenswert ist außerdem, dass DeepMind die Spezifikation und den dazugehörigen Beweis veröffentlicht, die im Rahmen der Signal-Protokollanalyse entstanden sind. Das ist für das Ökosystem relevant, weil formale Verifikation häufig an Wiederverwendbarkeit scheitert: Wenn Teams jedes Mal bei null beginnen müssen, bleibt der Aufwand hoch. DeepMind argumentiert außerdem, dass man sich bei den Fortschritten stark auf einen „Human-AI Collaboration“-Prozess fokussiert hat: KI-Agenten sollen in nahezu jeder Phase beitragen und sich selbst korrigieren können, aber menschliche Eingaben und Reviews sollen an zentralen Knotenpunkten erfolgen. Damit adressiert das Team eine typische Sorge aus der Debatte: eine „Testet sich selbst“-Welt, in der KI Ziele und Beweise eigenständig erzeugt und anschließend nur ihre eigenen Behauptungen abprüft.
Marktseitig bewegt sich die Initiative in einem Spannungsfeld, das in der gesamten Branche spürbar ist. Zwar gilt formale Verifikation als potenziell „heiliger Gral“ für Software-Sicherheit, weil mathematische Beweise eine andere Qualität von Sicherheit liefern als reine Dynamik-Tests. Doch die große offene Frage bleibt, ob KI-automatisierte formale Verifikation sich auf Dauer skaliert – und zwar nicht nur technisch, sondern auch wirtschaftlich. DeepMind führte die Signal-Analyse dem Bericht zufolge kostenlos als Forschungsprojekt durch; Google wollte dabei die Kosten nicht offenlegen und äußerte sich nicht dazu, ob künftig ein kommerzielles Verifikationsprodukt oder ein Service angeboten wird. Gerade für Unternehmen in sicherheitskritischen Bereichen wäre die Perspektive jedoch attraktiv: Wenn sich Eigenschaften von Implementierungen nachweisen lassen, könnten Konzerne regulatorische und betriebliche Risiken besser begründen und Bugs von vornherein systematisch ausschließen.
Für die nächsten Schritte deutet sich eine zweistufige Entwicklung an. Erstens muss der Ansatz weiter von Protokollteilen hin zu vollständigerem Code überführt werden, inklusive der Frage, wie speicher- und ressourcenschonend die Verifikationsschritte bei realen Softwaregrößen bleiben. Zweitens wird entscheidend, wie gut sich der „Human-AI“-Ansatz in organisatorische Prozesse integrieren lässt, etwa in der Art, wie Teams Spezifikationen pflegen und wie sie Beweise versionieren. DeepMind positioniert die Ergebnisse damit weniger als Endziel, sondern als markantes Zwischenstadium: ein Beleg dafür, dass KI-gestützte formale Verifikation funktioniert, wenn die Aufgaben sinnvoll zugeschnitten sind – und ein Signal, dass die Skalierung auf „viel mehr als einzelne Komponenten“ der eigentliche nächste Test ist.
🔥 Heutige Hot Deals bei Amazon: Bis zu 80% Rabatte!
🎉 Amazon Haul-Store für absolute Schnäppchenjäger!
- ★ 23-stufiges KI-Go-Training – Für Spieler mit Grundkenntnissen der Regeln – Entwickelt als intelligenter Trainingspartner passt sich die KI Spielern von 18K bis 9D an. Ideal für alle, die die Grundregeln bereits beherrschen und ihr Spiel verbessern möchten.
- IHR EMOTIONALER AI-BEGLEITER: Eiliko ist mehr als nur ein Anhänger, es ist ein charismatischer KI-Freund. Mit einem dynamischen LED-Bildschirm, der eine Vielzahl von animierten Gesichtern und Ausdrucksformen anzeigt, reagiert er auf Ihre Interaktionen mit einzigartiger Persönlichkeit und Charme.
- 【MEHR LEBEN FÜR DEINEN SCHREIBTISCH】 Lerne Eilik kennen – deinen kleinen Roboter-Freund mit Persönlichkeit. Mit liebevollen Animationen, ausdrucksstarken Reaktionen und spielerischen Interaktionen bringt Eilik mehr Freude in deinen Alltag. Ob auf dem Schreibtisch, im Büro oder am Nachttisch – Eilik wird schnell zu einem vertrauten Begleiter für besondere Momente.
- 【XL-Größe für gedeihende Pflanzen】Geben Sie Ihren Pflanzen den Raum, den sie verdienen! Unser verbessertes, großes 13,7 cm großes Design bietet Platz für Pflanzen mit einem Durchmesser von bis zu 8,9 cm und damit deutlich mehr Platz für Wurzelwachstum und Pflanzengesundheit im Vergleich zu kleineren, veralteten Modellen. Die Produktabmessungen betragen 13,6 x 13,6 x 13,2 cm und das Gerät wiegt nur 355 g.
- V28 Update - JETZT MIT NEUEN FUNKTIONEN! Als Reaktion auf das Ladeproblem von Loona haben wir das automatische Aufladen 2.0 verbessert. Diese Optimierung hilft Loona, die Ladewege in verschiedenen Szenarien zu erkennen und anzupassen, um die Erfolgsquote beim automatischen Aufladen zu erhöhen. Mobile Hotspots können sich mit Loona verbinden und überwinden WLAN-Einschränkungen, sodass Sie jederzeit und überall mit Loona interagieren können.
- Die besten Bücher rund um KI & Robotik!
- Die besten KI-News kostenlos per eMail erhalten!
- Zur Startseite von IT BOLTWISE® für aktuelle KI-News!
- IT BOLTWISE® kostenlos auf Patreon unterstützen!
- Aktuelle KI-Jobs auf StepStone finden und bewerben!
- Künstliche Intelligenz: Dem Menschen überlegen – wie KI uns rettet und bedroht | Der Neurowissenschaftler, Psychiater und SPIEGEL-Bestsellerautor von »Digitale Demenz«
Du hast einen wertvollen Beitrag oder Kommentar zum Artikel "DeepMind: AlphaProof Code verifiziert Signal-Protokoll mit KI" für unsere Leser?
#Sophos
#AmazonPrime
#Bestseller
Es werden alle Kommentare moderiert!
Für eine offene Diskussion behalten wir uns vor, jeden Kommentar zu löschen, der nicht direkt auf das Thema abzielt oder nur den Zweck hat, Leser oder Autoren herabzuwürdigen.
Wir möchten, dass respektvoll miteinander kommuniziert wird, so als ob die Diskussion mit real anwesenden Personen geführt wird. Dies machen wir für den Großteil unserer Leser, der sachlich und konstruktiv über ein Thema sprechen möchte.
Du willst nichts verpassen?
Du möchtest über ähnliche News und Beiträge wie "DeepMind: AlphaProof Code verifiziert Signal-Protokoll mit KI" informiert werden? Neben der E-Mail-Benachrichtigung habt ihr auch die Möglichkeit, den Feed dieses Beitrags zu abonnieren. Wer natürlich alles lesen möchte, der sollte den RSS-Hauptfeed oder IT BOLTWISE® bei Google News wie auch bei Bing News abonnieren.
Nutze die Google-Suchmaschine für eine weitere Themenrecherche: »DeepMind: AlphaProof Code verifiziert Signal-Protokoll mit KI« bei Google Deutschland suchen, bei Bing oder Google News!