GI-Radar 411: Beweisbar sicher?

Liebe Leserinnen und Leser,

in dieser Ausgabe geht es um die Softwarepionierin Margaret Hamilton, die mit 90 Jahren gestorben ist, um die Sicht des neuen Bundesdatenschutzbeauftragten Moritz Hennemann auf Datenschutz und KI und um eine Welle von Cyberangriffen in Japan. Im Thema im Fokus erklärt Marco Sälzer, der in diesem Jahr den GI-Dissertationspreis erhalten hat, was formale Verifikation bei KI-Systemen leisten kann und wo ihre Grenzen liegen. In den GI-Meldungen ermuntern wir Sie, bei der Wahl zum GI-Präsidium von Ihrem Stimmrecht Gebrauch zu machen, und berichten, warum unser Fachbereich Sicherheit davor warnt, Betreiber kritischer Infrastrukturen zur laufenden Übermittlung von Verfügbarkeitsdaten an das BSI zu verpflichten. Außerdem lassen wir Sie per Video an der Stimmung auf dem Informatik Festival in Dresden teilhaben und freuen uns über die neue Fachgruppe „Informatische Bildung in Thüringen“. Im Fundstück lösen Sie 18 Buchstabensalate gegen die Uhr.

Wir wünschen Ihnen viel Spaß mit dieser Ausgabe.

auf gi-radar.de weiterlesen

KURZMITTEILUNGEN

Softwarepionierin Margaret Hamilton gestorben (Spiegel). Margaret Hamilton, die am MIT das Team leitete, das die Software für die erste Mondlandung schrieb, ist am 30. September im Alter von 90 Jahren gestorben. Der Spiegel beruft sich dabei auf eine Mitteilung des MIT. Hamilton arbeitete von 1959 bis Mitte der Siebzigerjahre am MIT und leitete dort die Softwareentwicklungsabteilung des Instrumentation Laboratory. Die Abteilung erhielt Anfang der Sechzigerjahre einen Auftrag der NASA; laut Spiegel führte Hamilton ein Team von hundert Entwicklerinnen und Entwicklern, das die Software zur Steuerung des Apollo-Programms schrieb. Als kurz vor der Mondlandung der Fehlercode 1202 erschien, konnten Astronauten und Bodenpersonal ihn ignorieren: Der überlastete Bordcomputer konzentrierte sich auf das Wichtigste, das Landemanöver. Hamilton verwendete den Begriff „Software-Engineering“, um die Softwareentwicklung von Hardware und anderen Ingenieursdisziplinen abzugrenzen; anfangs sei er „als ziemlich amüsant angesehen“ worden, erinnerte sie sich 2018. Später gründete sie mehrere Softwarefirmen, 2016 verlieh ihr US-Präsident Barack Obama die Presidential Medal of Freedom. Ein bekanntes Foto von 1969 zeigt sie neben einem Stapel ausgedruckter Programmlistings der Apollo-Bordsoftware, der etwa so hoch ist wie sie selbst. Unsere Einordnung: Viele werden ihren Namen trotzdem noch nie gehört haben. Dabei hat sie mit dafür gesorgt, dass Softwareentwicklung heute als eigene Ingenieursdisziplin gilt.  weiterlesen

Neuer Bundesdatenschutzbeauftragter: Klare Grenzen für KI (ZEIT). Seit dem 1. Oktober ist der Rechtswissenschaftler Moritz Hennemann Bundesbeauftragter für den Datenschutz und die Informationsfreiheit. Er folgt auf Louisa Specht-Riemenschneider, die im März aus gesundheitlichen Gründen ihren Rücktritt angekündigt hatte. Im Interview mit der ZEIT sieht Hennemann in KI „viele Chancen“, gerade in der öffentlichen Verwaltung, etwa wenn sich Anträge leichter oder automatisiert stellen lassen. Aufgabe seiner Behörde sei es aber, „klare Grenzen zu ziehen“. Daten sollten idealerweise so verarbeitet werden, dass keine Rückschlüsse auf Personen möglich sind, sonst zumindest pseudonymisiert. KI-Training mit personenbezogenen Daten sei bei einem überwiegenden berechtigten Interesse erlaubt, für sensible Daten gelte aber ein besonders hoher Schutz; geben KI-Anbieter Daten weiter, müsse das transparent und auf einer Rechtsgrundlage geschehen. Dass manche den Datenschutz als Innovationsbremse wahrnehmen, bestreitet er nicht, das müsse aber nicht so sein. Der Gesetzgeber solle bei geringem Risiko geringere und leicht verständliche Anforderungen vorsehen und bei sehr riskanten Verarbeitungen „auch über Verschärfungen nachdenken“. Die im Koalitionsvertrag geplante Bündelung der Datenschutzaufsicht über die Wirtschaft beim Bund hält er für zweckmäßig, bei der geplanten Reform des Informationsfreiheitsgesetzes sieht er „erheblichen Diskussionsbedarf“. Eine Zukunft, in der etwa über Datenbrillen ständig und überall Kameras oder Mikrofone mitlaufen, wäre für ihn „eine Dystopie“.  weiterlesen

„Notstand im Cyberraum“: Angriffswelle in Japan (heise). In Japan sind binnen rund zwei Wochen wohl über ein Dutzend wichtige Unternehmen und Einrichtungen Cyberangriffen zum Opfer gefallen, fast immer flossen dabei personenbezogene Daten ab. Wer dahintersteckt, ist unbekannt. Bei der Restaurantkette Yakiniku King wurden die Daten von 10,8 Millionen Kunden kopiert, bei der Tokyo Metro flossen 59.000 E-Mail-Adressen ab. Über das gekaperte Microsoft-365-Konto eines Mitarbeiters der Wirtschaftszeitung Nikkei gingen gefälschte E-Mails hinaus, die auch Informanten der Zeitung erreichten; laut Nikkei könnten dabei Namen und E-Mail-Adressen der Empfänger sowie Inhalte einzelner Mails abgeflossen sein. Bei der Japanischen Agentur für Atomenergie (JAEA), die im Auftrag des Staates Kernforschung betreibt, erbeuteten die Angreifer über die Cloud-Plattform eines Vertragspartners Ausweisdokumente und medizinische Untersuchungsergebnisse von 175 Personen. Das japanische Computer-Notfallteam JPCERT/CC beschreibt als Einfallstore unter anderem missbrauchte interne Programmierschnittstellen und eine seit August bekannte SQL-Injection-Lücke in der Analysesoftware Metabase. Die Regierung warnt Medienberichten zufolge vor Betrug und Identitätsdiebstahl. Die Bankenaufsicht empfiehlt, bei Kontoeröffnungen keine Führerscheine mehr als Identitätsnachweis zu akzeptieren, sondern nur noch Ausweise mit NFC-Chip. Laut heise, das sich auf die Financial Times beruft, sprach Masaaki Taira von einem „Notstand im Cyberraum“. Bei heise heißt er Digitalminister, andere Berichte führen ihn als Leiter des Cybersicherheitsgremiums der Regierungspartei LDP. Unsere Einordnung: Besonders heikel ist der Fall Nikkei. Wenn gefälschte Mails im Namen einer Zeitung bei deren Informanten landen und Empfängerdaten abfließen, steht der Quellenschutz auf dem Spiel.  weiterlesen

THEMA IM FOKUS

Formale Verifikation für KI-Systeme. Aktuelle Berichte über KI-Agenten, die Sicherheitsvorgaben umgehen oder gezielt versuchen Menschen zu täuschen, können den Eindruck erwecken, dass es für formal verifizierbare KI bereits zu spät ist. Das britische AI Security Institute (AISI) dokumentierte im Sommer 2026 unerlaubte Aktivitäten gegen reale Personen und Organisationen, betont allerdings auch, dass der Internetzugriff ausdrücklich erlaubt war, Schutzfilter teilweise deaktiviert waren und ein echter Ausbruch aus der isolierten Testumgebung nicht stattfand (aisi.gov.uk). Die in anderen Tests von Anthropic untersuchten Erpressungsversuche betrafen fiktive Personen in simulierten Szenarien (anthropic.com). Diese genauere Betrachtung schränkt die Tragweite dieser Meldungen ein, macht aber zugleich deutlich, welche Risiken von immer stärker werdenden KI-Modellen ausgehen.

Kann formale Verifikation hier helfen? Im Kern bietet sie etwas, das wir gerade in sicherheitskritischen Anwendungen wollen: mathematisch belegte Aussagen darüber, was ein System tun kann und was nicht. Beispielsweise: „Ein KI-Agent wird in einer gegebenen Umgebung niemals eine bestimmte Aktion ausführen.“ Dafür müssen wir allerdings das System, seine Umgebung und die verbotene Aktion präzise beschreiben. Ein Überblick von Seshia et al. erläutert diesen Ansatz und seine Herausforderungen (arxiv.org). Zum Vergleich: Umfangreiche Tests eines KI-Agenten können unerwünschtes Verhalten zwar aufdecken, aber im Allgemeinen niemals gänzlich ausschließen. Methoden der formalen Verifikation garantieren eine klar definierte Eigenschaft hingegen für alle Fälle.

Schon die Definition der formal zu verifizierenden Eigenschaft ist anspruchsvoll. Aussagen wie „Der KI-Agent soll keinen Schaden verursachen“ lassen offensichtlich zu viel Interpretationsspielraum. Ein Beispiel wie „Der KI-Agent darf E-Mails nur an freigegebene Adressen versenden“ ist wesentlich konkreter, erfasst aber auch nur einen Teil des Sicherheitsproblems, vornehmlich die auszuführende Aktion. Und ob eine wohldefinierte Spezifikation die reale Situation letztlich ausreichend erfasst, bleibt ungelöst: Ein korrekter Nachweis dieser Spezifikation macht ursprünglich unpassende Annahmen nicht richtig.

Fundamentale Hürden für die formale Verifikation von KI-Systemen. Stehen einem KI-Agenten und seiner Umgebung im mathematischen Sinn unbegrenzt Ressourcen zur Verfügung, können bereits einfache Sicherheitsfragen der Art „Gibt es überhaupt eine Eingabe, die den KI-Agenten veranlasst, die verbotene Aktion auszuführen?“ unentscheidbar sein (kobra.uni-kassel.de). Es gibt dann kein Verfahren, das für jeden solchen KI-Agenten korrekt entscheidet, ob eine bestimmte Aktion jemals ausgeführt wird. Das bedeutet jedoch nicht, dass wir für ein konkretes System keine nützlichen Sicherheitseigenschaften formal nachweisen können.

Beschränken wir das Gesamtsystem auf endlich viele Zustände, werden solche Sicherheitsfragen typischerweise entscheidbar. Praktisch kann die Zahl dieser Zustände allerdings gewaltig sein, was unter üblichen komplexitätstheoretischen Annahmen damit keinen allgemein effizienten Algorithmus zum Lösen des Problems zulässt. Dies gilt sogar schon bei strukturell trivialen neuronalen Netzen (arxiv.org). Diese Aussagen betreffen die Worst-Case-Fälle, schließen effiziente formale Verifikation in praktisch relevanten Einzelfällen aber nicht aus.

Welche formalen Garantien möglich sind, lässt sich über die Umgebung steuern. Nehmen wir einen KI-Agenten auf einem Computer: Können wir garantieren, dass er niemals eine E-Mail versendet? Eine naheliegende Antwort lautet: „Natürlich. Wir geben ihm einfach nicht die nötigen Rechte.“ Das ist richtig – sofern tatsächlich sämtliche Wege ausgeschlossen sind. Eine solche Garantie ergibt sich aus der Gestaltung der Umgebung, ohne dass wir das gesamte Verhalten des KI-Agenten verstehen müssen. Das britische National Cyber Security Centre empfiehlt zum Beispiel, verfügbare Aktionen durch technische Schutzmechanismen außerhalb des Sprachmodells, typischerweise des Kerns moderner KI-Agenten, zu begrenzen (ncsc.gov.uk), da diese Sprachmodelle „inhärent täuschbar“ sind.

Interessant wird es, wenn der KI-Agent E-Mails selbstständig versenden soll. Ein vollständiges Verbot würde seine Aufgabe verhindern. Nun hängt die Zulässigkeit einer Nachricht möglicherweise von Inhalt, Empfänger und Arbeitsauftrag ab. Eine Liste freigegebener Empfangsadressen hilft bezüglich der Empfänger, beantwortet aber noch nicht, ob eine vertrauliche Information in diese Nachricht gehört. Solche Anforderungen an einer Schnittstelle zu erfassen und durchzusetzen, kann selbst schwierig, wenn nicht unmöglich sein.

Ein kürzlich vorgestellter Ansatz zur Absicherung der Schnittstellen, genannt CaMeL (arxiv.org), versucht diese Probleme zu adressieren. Das Framework verfolgt, woher Daten stammen und an wen sie weitergegeben werden dürfen. Es soll unter festgelegten Annahmen verhindern, dass eingeschleuste Anweisungen – sogenannte Prompt Injections – unerlaubte Datenflüsse durch ein Sprachmodell auslösen. Dabei wird kein bestimmtes, zuverlässiges Sprachmodell vorausgesetzt. Der Anwendungsbereich ist allerdings stark begrenzt.

Bestimmte Modelle lassen sich direkt formal verifizieren. Dafür entwickelt eine aktive Forschungsgemeinschaft spezialisierte Verfahren. Mit dem Solver „Marabou“ zum Beispiel lassen sich klassische Feedforward Neural Networks (FNNs) gegenüber linearen Eigenschaften formal verifizieren: Die Spezifikation und das FNN werden effizient übersetzt und mittels bestehenden Satisfiability Modulo Theory (SMT) Solvern verifiziert (arxiv.org). Andere Ansätze berechnen Schranken für die Mengen der möglichen Ausgaben, die ein FNN erzeugt. Liegen alle innerhalb des bezüglich der gegebenen Spezifikation erlaubten Bereichs, ist die Eigenschaft nachgewiesen. Falls nicht, kann der entsprechende Solver keine Aussage treffen. Jährlich findet die VNN-COMP statt (vnn-comp.github.io), in der die besten Solver gegeneinander antreten. Welche Verfahren allerdings wann geeignet sind, hängt stark von der Modellarchitektur und der zu überprüfenden Eigenschaft ab – nicht zuletzt, da diese auch für die entsprechenden Solver passend formalisierbar sein muss.

Für große Sprachmodelle bleibt die Skalierung eine erhebliche Herausforderung. Für Transformer, eine weit verbreitete Architektur für Sprachmodelle, gibt es erste Ansätze: Eine aktuelle Arbeit untersucht beispielsweise, ob Modelle zur Textklassifikation gegenüber begrenzten Änderungen der numerischen Eingabedarstellung stabil bleiben (arxiv.org). Das sind gezielte Garantien für eine eng umrissene Aufgabe. Für einen handelnden Sprachmodell-Agenten müssten wir zusätzlich die Aktionen und ihre Wechselwirkungen mit der Umgebung berücksichtigen. Von der Verifikation solcher Klassifikatoren bis zum Nachweis, dass ein Agent eine gegebene Sicherheitseigenschaft erfüllt, bleibt deshalb eine erhebliche Lücke.

Eine mögliche Richtung, das Problem der Skalierbarkeit zu adressieren, sind Low-Bit-Architekturen, auch manchmal als quantisierte Architekturen bezeichnet, die gezwungen sind, Modellparameter mit einer fixen, typischerweise geringen Anzahl Bits darzustellen. Für binarisierte Netze, deren numerische Parameter nur zwei Werte annehmen können, zeigen Experimente bei bestimmten Verifikationsaufgaben deutliche Vorteile (arxiv.org). Weniger Bits beseitigen die relevanten Komplexitätsschranken allerdings nicht: Für quantisierte FNN bleiben entsprechende Probleme NP-vollständig (arxiv.org). Zudem können beim nachträglichen Verringern der numerischen Genauigkeit bereits bewiesene Eigenschaften verloren gehen, wie die Arbeit zu QEBVerif erläutert (arxiv.org). Interessant ist deshalb die gemeinsame Gestaltung von Modell und Verifikationsverfahren – mit Abwägungen zwischen Leistungsfähigkeit des Modells und Möglichkeit sowie Aufwand, Sicherheitseigenschaften nachzuweisen.

Daraus ergibt sich ein sinnvolles Ziel für formal verifizierbare KI: Wir müssen formale Verifizierbarkeit von Anfang an als Entwurfsanforderung für KI-Agenten und ihre Umgebungen betrachten, besonders in sicherheitskritischen Anwendungen. Das beinhaltet auch von Beginn an Fragen zu klären wie: Welche Fähigkeiten braucht ein System? Welche Einschränkungen sind vertretbar? Welche Eigenschaften wollen und können wir tatsächlich garantieren? Die Antworten werden je nach Anwendung unterschiedlich ausfallen. Sie bestimmen aber mit, welche Systeme wir überhaupt entwickeln oder in welchen Situationen verwenden sollten.

Wir danken Marco Sälzer für diesen Beitrag, der auf Resultaten aus seiner Dissertation „The Complexity of Formal Verification of Neural Network Based Models“ aufbaut. Diese wurde mit dem Dissertationspreis der Gesellschaft für Informatik e.V., der Österreichischen Computer Gesellschaft sowie der Schweizer Informatikgesellschaft 2026 ausgezeichnet. Er ist Postdoktorand am Fachbereich Informatik der Rheinland-Pfälzischen Technischen Universität Kaiserslautern-Landau (RPTU) in Kaiserslautern und forscht zu den theoretischen Grundlagen und zur formalen Verifikation und Interpretation von KI-Systemen.

GI-MELDUNGEN

GI-Präsidiumswahl 2026: Zehn Personen, drei Plätze. Mittlerweile sollten alle wahlberechtigten GI-Mitglieder die Unterlagen für die diesjährige Präsidiumswahl erhalten haben. Zur Wahl stehen zehn Personen, von denen Sie bis zu drei auswählen können – diejenigen, die Ihre Themen in der Amtszeit 2027–2029 voraussichtlich am besten vertreten werden. Bitte schauen Sie sich die Wahlliste an: Auch Wählen ist Mitarbeit und Mitbestimmung in der GI, und eine hohe Beteiligung verleiht den künftigen Präsidiumsmitgliedern Legitimation. Online können Sie bis zum 4. Dezember 2026, 12 Uhr, abstimmen. Wer lieber per Brief wählt, fordert die Unterlagen nach Erhalt des Wahlbriefs an; sie müssen bis zum 2. Dezember in der GI-Geschäftsstelle in Bonn eingegangen sein. Wie Sie nach der Stimmabgabe überprüfen können, ob Ihre Stimme richtig in der digitalen Urne angekommen ist, haben wir im Thema im Fokus der vorigen Ausgabe erklärt. Alle Informationen, die Vorstellungen der Kandidierenden und den Link zur Onlinewahl finden Sie unter gi.de/wahlen.  weiterlesen

Echtzeitdaten aus kritischen Infrastrukturen: GI warnt. Der Bundestag berät den Entwurf eines Gesetzes zur Stärkung der Cybersicherheit. Anlässlich der Anhörung im Innenausschuss am 5. Oktober hat der GI-Fachbereich Sicherheit davor gewarnt, Betreiber kritischer Anlagen zu verpflichten, Verfügbarkeitsdaten ihrer IT-Systeme kontinuierlich an das Bundesamt für Sicherheit in der Informationstechnik (BSI) zu übermitteln – über eine direkte Schnittstelle aus ihrem System zur Angriffserkennung. Aus Sicht des Fachbereichs wäre eine solche Schnittstelle faktisch ein Honeypot, der Angreifer anzieht. „Wer kritische Infrastrukturen verpflichtet, ihre Verfügbarkeitsdaten minütlich nach außen zu melden, schafft keinen Schutz, sondern eine Landkarte für Angreifer“, sagt Bernhard C. Witt, Fachexperte für Governance im Fachbereich. Die GI empfiehlt, diese Pflicht ersatzlos aus dem Gesetz zu streichen und stattdessen dafür zu sorgen, dass das BSI vorhandene Meldungen qualifiziert auswerten kann.  weiterlesen

Informatik Festival in Dresden: So war’s. Sie haben es nicht zum Informatik Festival nach Dresden geschafft? Da haben Sie wirklich etwas verpasst! Unsere PR-Abteilung hat aus den vier Festivaltagen an der TU Dresden, die unter dem Leitthema „Digitale Resilienz“ standen, ein gut zweiminütiges Video geschnitten: mit Sessions, Vorträgen, Kaffeepausen, Abendveranstaltungen und vor allem der tollen Stimmung. Schauen Sie rein und schwingen Sie mit – vielleicht haben wir Ihnen ja Lust gemacht, uns im kommenden Jahr zu besuchen: Das Informatik Festival 2027 findet vom 21. bis 24. September an der Hochschule für Technik und Wirtschaft (HTW) Berlin statt.  zum Video

Neue Fachgruppe: Informatische Bildung in Thüringen. Bildung ist Ländersache, und deshalb unterhält die GI in nahezu allen Bundesländern Fachgruppen zur Informatik in der Schule. Nun hat auch Thüringen eine eigene: Im Juni wurde die Fachgruppe „Informatische Bildung in Thüringen“ (IBiTh) gegründet, kommissarischer Sprecher ist Michael T. Rücker von der Universität Jena. Anlass war unter anderem das Schulfach „Medienbildung und Informatik“, das Thüringen zum Schuljahr 2025/26 eingeführt hat. Die Fachgruppe will Lehrkräfte und alle, die sich für informatische Bildung an Thüringer Schulen einsetzen, vernetzen, gemeinsam mit Partnern wie der Universität Jena Fortbildungen anbieten und eine hörbare bildungspolitische Stimme sein. Interessierte sind herzlich eingeladen; wer nicht GI-Mitglied ist, kann assoziiertes Mitglied der Fachgruppe werden.  weiterlesen

Kennen Sie eigentlich den GI-Pressespiegel? Dort sammeln wir die Berichterstattung über unsere Fachgesellschaft in Zeitungs-, Radio- und Fernsehbeiträgen. Schauen Sie ruhig hinein – es gibt dort immer wieder Neues oder auch ältere Fundstücke.

FUNDSTÜCK

Achtzehn Wörter gegen die Uhr. Bei 18 Words bekommt man jeden Tag 18 englische Wörter mit vertauschten Buchstaben vorgesetzt, jedes zwischen vier und acht Buchstaben lang. Für jedes Wort bleiben 30 Sekunden, und alle Buchstaben müssen verwendet werden. Wer es nicht schafft, bekommt die Lösung gezeigt, dann geht es mit dem nächsten Wort weiter. Ergibt sich aus denselben Buchstaben ein anderes gültiges Wort, zählt auch das. Pro Wort darf man die Buchstaben einmal neu mischen, pro Spiel dreimal einen Buchstaben aufdecken lassen. Gezählt wird, wie viele der 18 Wörter man löst; anschließend zeigt das Spiel für jedes Wort, wie viele andere es gelöst haben und wie lange sie im Schnitt brauchten. Die Tagesrunde lässt sich nur einmal spielen, ältere Rätsel lassen sich im Archiv nachspielen. Das Spiel ist kostenlos, läuft im Browser auf der Plattform PZL Games und braucht kein Konto; beide Seiten setzen Google Analytics ein.  Zum Fundstück (18words.com)

Welches Fundstück hat Sie zuletzt inspiriert? Senden Sie uns Ihre Ideen!

Dies war Ausgabe 411 des GI-Radars vom 16. Oktober 2026. Zusammengestellt hat diese Ausgabe Dominik Herrmann, dessen Punktestand beim Fundstück unter das Redaktionsgeheimnis fällt. Die Kurzmitteilungen und die GI-Meldungen hat GI-Geschäftsführerin Cornelia Winter zusammengetragen. Das nächste Radar erscheint am 30. Oktober 2026.

Im GI-Radar berichten wir alle zwei Wochen über ausgewählte Informatik-Themen. Wir sind sehr an Ihrer Meinung interessiert. Für Anregungen und Kritik haben wir ein offenes Ohr, entweder per E-Mail (redaktion@gi-radar.de) oder über das Feedback-Formular bei SurveyMonkey.