Google hat den Zugang zu Gemini 4 Carbon erweitert und gibt an, dass auf diesem Modell basierende Agenten dazu beigetragen haben, zentrale Sicherheitsgarantien des Codes des Signal-Protokolls formal zu überprüfen.
- Google erweitert den Zugang zu Gemini 4 Carbon für zahlende Entwickler, Unternehmen und Ultra-Abonnenten.
- Carbon-basierte Agenten beweisen zentrale Sicherheitsgarantien des Signal-Protokolls formal.
- Fünf Forscher erzeugen in vier Wochen rund 6,5 Millionen Zeilen Beweise in Lean.
- Die Ergebnisse gelten nur für die kompilierte Codeversion, nicht für die Signal-Apps selbst.
Entwickler und Unternehmen, die bezahlen, können Carbon nun über die Gemini-API und Gemini for Business nutzen, und Google AI Ultra-Abonnenten haben ebenfalls Zugang. Einführungspreise von 2 $ und 10 $ pro Million Eingabe- bzw. Ausgabe-Tokens gelten bis zum 30. November, bevor sie verdoppelt werden. Ein Token ist eine Texteinheit, die das Modell verarbeitet, um Inhalte zu lesen oder zu erzeugen.
Bisher konnten nur bestimmte Cybersicherheits-Experten, die Mitglieder von Googles Fairwind-Programm sind, Carbon nutzen. Sie müssen weiterhin diesem Programm angehören, um Zugang zu Carbon for Cyber zu erhalten, einer Version, die Google als führend in wichtigen Benchmarks für die Erkennung, Ausnutzung und Behebung von Schwachstellen bezeichnet.
Anwendungen in der Cybersicherheit
Laut Google hat das Unternehmen Wiz Carbon for Cyber genutzt, um in zwei Stunden Zero-Day-Schwachstellen bei zwei großen SaaS-Anbietern zu finden. Googles Cloud Vulnerability Research (CVR)-Team seinerseits nutzte das Modell, um zu bestätigen, dass zwei Fehler in einem beliebten Open-Source-Projekt ausnutzbar waren, mit einer Schwere vergleichbar mit PHP2Shell, einem bereits von Angreifern ausgenutzten Paar von PHP-Schwachstellen.
„Durch die Nutzung von Carbon zum Erstellen eines Proof of Concept hat CVR den Maintainern geholfen, den Fehler als kritisch neu einzustufen und schnell einen Patch zu veröffentlichen », erklärt Google.
Überprüfung des Signal-Codes
Zudem hat Google DeepMind AlphaProof Code vorgestellt, das menschliche Experten mit KI-Agenten kombiniert, um Software formal zu verifizieren, also mathematisch nachzuweisen, dass sie definierte Anforderungen erfüllt. Das Team wandte es auf libsignal an, die Referenzimplementierung des Signal-Protokolls. Versionen dieses Protokolls funktionieren auch in WhatsApp und Google Messages.
Menschen arbeiteten mit Agenten, die auf Carbon und Claude Opus 5.5 liefen, um die Spezifikationen zu formulieren, die beschreiben, was bewiesen werden sollte. Auf Carbon basierende Agenten erzeugten dann die gesamten etwa 6,5 Millionen Zeilen von Beweisen, geschrieben in Lean, einem Beweisassistenten, der ungültige Beweise zurückweist. Laut Google gelten die bewiesenen Garantien, darunter Forward Secrecy, Sicherheit nach Kompromittierung und Authentifizierung, für den kompilierten Maschinencode, während die meisten Protokollüberprüfungen nur das Design betreffen.
Fünf Forscher führten die Beweisarbeit in vier Wochen durch, eine Arbeit, die Google traditionell auf Jahre für Spezialisten schätzt. Um zu überprüfen, ob die Methode echte Schwachstellen erkennt, führte das Team zwei bereits behobene alte Fehler von libsignal wieder ein und bewies, dass diese Versionen die Sicherheitsgarantien nicht mehr erfüllen.
Die Ergebnisse beziehen sich auf die von Google kompilierte Codeversion, die über ein kleines Kommandozeilen-Tool ausgeführt wird, und nicht auf „die Signal-Anwendungen selbst ». Einige Seitenkanäle wurden ebenfalls von Teilen der Analyse ausgeschlossen. „Die Ergebnisse deuten darauf hin, dass KI die formale Verifikation, die historisch für die meisten Software zu teuer war, für reale Systeme praktikabel machen kann », schreiben die Forscher. Ehren Kret, Technischer Leiter von Signal, erklärte seinerseits: „Während die mit KI verbundenen Sicherheitsbedrohungen zunehmen, gibt uns die rigorose Überprüfung der Implementierung des Signal-Protokolls noch größeres Vertrauen in die Datenschutzgarantien unseres Codes. » Google veröffentlicht zudem die Spezifikationen und Beweise.
