GI-Radar 298: Formale Verifikation arithmetischer Schaltungen

 

Sehr geehrte Leserinnen und Leser,

Unicode hat viele Probleme mit Zeichensätzen gelöst. Die damit einhergehende Komplexität sorgt aber bis heute für Probleme, wie eine unserer Kurzmitteilungen zeigt. Das Thema im Fokus gibt einen Einblick in die Formale Verifikation, mit der sich Daniela Kaufmann, Gewinnerin des GI-Dissertationspreises 2020, beschäftigt. Ein neues Gewissensbit stellen wir Ihnen in den GI-Meldungen vor. Und auch das Fundstück regt dieses Mal zum Nachdenken an.

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

auf gi-radar.de weiterlesen

Gesichtserkennung + Ransomware + Gefahr durch Unicode + digitale Insekten + Digitalisierung in der Schule + Formale Verifikation von arithmetischen Schaltungen + Gewissensbit + Rückblick INFORMATIK 2021 + Junior-Fellows gesucht + Digital Autonomy-Preis + FAS für GI-Mitglieder + Tracking von Gesundheitsdaten

KURZMITTEILUNGEN

Gesichtserkennung: wie funktioniert sie und warum ist sie gefährlich? (NZZ) Derzeit ist die automatische Gesichtserkennung wieder mal in aller Munde. Tatsächlich wurde diese Technologie bereits in den 60er Jahren entwickelt, aber erst viel später erkannte man sie als potenzielle Gefahr. Ein Überblicksartikel erklärt, wie sie funktioniert, wo sie eingesetzt wird und wie die rechtlichen Bestimmungen aussehen.  weiterlesen

Ransomware-Gruppe REvil identifiziert (heise). Erpressung im Internet hat sich längst zu einem erträglichen Geschäft entwickelt. Höchst selten werden jedoch die Erpresser identifiziert, geschweige denn gefasst. Nun ist es gelungen, eine Gruppe ausfindig zu machen. Allerdings ist es bislang nicht möglich, der Verantwortlichen habhaft zu werden.  weiterlesen

Unicode-Befehle korrumpieren Programmiersprachen (golem). Sicherheitsforscher der Universität Cambridge haben herausgefunden, dass sich Programme in vielen Programmiersprachen durch Unicode-Steuerzeichen korrumpieren lassen. Eingefügte Strings können beim Kompilieren zu Schadsoftware mutieren. Perfiderweise lässt sich der so eingeschleuste Code bei einem Code-Review häufig nicht erkennen. Nun müssen Compiler und Entwicklungsumgebungen angepasst werden.  weiterlesen

Museum digitalisiert Millionen Insekten (Forschung und Lehre). Das Naturkundemuseum in Berlin beherbergt rund 14,5 Millionen Insekten, die sich bislang nur vor Ort bestaunen lassen. Mittels einer „Digitalisierungsstraße“ sollen nun pro Tag rund 5000 Tiere fotografiert, gescannt und so besser verfügbar gemacht.  weiterlesen

Studie zur Digitalisierung in der Schule (Tagesspiegel). Die Telekom-Stiftung hat im Sommer eine Studie zum Thema „Stand der Digitalisierung in den Schulen“ gemacht. Befragt wurden rund 1500 Lehrkräfte zum Stand der Lernplattformen, der Ausstattung und dem Breitbandausbau in den verschiedenen Ländern. Eines der Ziele der Studie war es, die Wirkung der Investitionsprogramme von Bund und Ländern zu evaluieren. Das Ergebnis der Studie liegt jetzt vor.  weiterlesen

THEMA IM FOKUS

Das heutige Thema im Fokus gibt einen Einblick in die Dissertation „Formal Verification of Multiplier Circuits using Computer Algebra“ unserer diesjährigen Dissertationspreisträgerin Daniela Kaufmann (Dissertation: danielakaufmann.at).

Formale Verifikation von arithmetischen Schaltungen. Sie lesen dieses GI-Radar gerade an einem Bildschirm, haben vielleicht noch ein Smartphone neben sich liegen und tragen möglicherweise auch noch eine Smartwatch am Handgelenk. Computer werden heutzutage nicht nur im persönlichen Umfeld eingesetzt, sondern etwa auch im Finanzwesen, zur Verkehrsflussregelung oder in Intensivstationen. In diesen sicherheitsrelevanten Bereichen ist die korrekte Funktion eines Computers unabdingbar.

Digitale Schaltungen sind ein wesentlicher Bestandteil von Computern und digitalen Systemen. Diese Schaltungen implementieren logische Funktionen und können zahlreiche digitale Komponenten und arithmetische Operationen modellieren. Die Hauptkomponenten digitaler Schaltungen sind Logikgatter, welche einfache Boolesche Funktionen repräsentieren. Beispiele für diese Gatter sind Negation (NOT), Konjunktion (UND) und Disjunktion (ODER). Diese logischen Gatter können kombiniert werden, um komplexere Funktionen darzustellen. Eine Unterkategorie von digitalen Schaltungen sind Schaltnetze. Schaltnetze werden in Computern eingesetzt, um Boolesche Algebra zu implementieren. Zum Beispiel ist die arithmetisch-logische Einheit (ALU) in einem Prozessor, die zur Berechnung von mathematischen Operationen eingesetzt wird, aus Schaltnetzen konstruiert. Arithmetische Schaltungen sind spezielle Schaltnetze, die Rechenoperationen wie zum Beispiel Multiplikation durchführen.

Aufgrund des weitreichenden, mitunter sicherheitskritischen Einsatzes von digitalen Schaltungen ist es äußerst wichtig, ihre Korrektheit sicherzustellen. Fehler in den Schaltungen können fatale Folgen in der Anwendung haben. Ein berühmtes Beispiel für eine fehlerhafte Schaltung ist der FDIV-Bug in frühen Intel Pentium Prozessoren (heise). Die Gleitkommaeinheit (FPU) dieser Prozessoren enthält einen Hardwarefehler, der bei Division von bestimmten Zahlen zu falschen Ergebnissen führt. Im schlimmsten Fall ist bereits die vierte Nachkommastelle falsch. Der Fehler wurde erst 1994, rund eineinhalb Jahre nach Markteinführung des Prozessors bekannt und kostete Intel damals ca. 500 Millionen US-Dollar (uni-jena.de). Eine gleichartige Panne würde heutzutage wohl ernsthafte finanzielle Schwierigkeiten, auch für große Prozessorhersteller, bedeuten. Daher wollen diese Firmen die Korrektheit ihrer Hardware zu hundert Prozent garantieren können.

Eine Möglichkeit die Korrektheit sicherzustellen wäre es, alle möglichen Zustände der Eingangssignale einer Schaltung zu überprüfen. Dies skaliert jedoch nicht, denn jedes Eingangssignal kann die binären Werte 0 und 1 annehmen. Das heißt, mit jedem zusätzlichen Eingangssignal verdoppelt sich die Menge der Testfälle. Bei Schaltungen mit 8 Eingängen sind dies 256 Testfälle, bei 9 Eingängen sind es bereits 512 Testfälle. Bei Schaltungen mit mehr als 300 Eingängen übersteigt die Anzahl der Testfälle bereits die Anzahl der Atome im beobachtbaren Universum (youtube.com). Man kann sich also leicht vor Augen führen, dass das Testen von großen Schaltungen nicht zielführend ist, um deren Korrektheit zu bestimmen.

Mittels formaler Verifikation lässt sich die Korrektheit von Software oder Hardware in Bezug auf eine zuvor definierte Spezifikation formal beweisen. Dazu wird das gegebene System in ein mathematisches Modell übersetzt und automatisierte Beweistechniken werden eingesetzt, um die gewünschten Korrektheitsbeweise zu erzielen. Die verschiedenen Verifikationstechniken unterscheiden sich durch die zugrundeliegenden mathematischen Modellierungen des Systems.

Mehr als 25 Jahre nach Bekanntwerden des FDIV-Bugs ist die automatisierte Verifikation von Schaltungen jedoch noch immer nicht vollautomatisiert lösbar. Besonders Integer-Multiplizierer, das sind arithmetische Schaltungen, die Multiplikationen von ganzen Zahlen ausführen, stellen aufgrund ihres internen Aufbaus der Logikgatter eine Herausforderung für bestehende Verifikationsmethoden dar. In der Praxis bedeutet dies, dass industrielle Entwickler von arithmetischen Schaltungen momentan entweder aufwändige manuelle Verifikation mittels Theorembeweisern betreiben, oder sich komplett auf Simulationen verlassen. Immer bessere Optimierungen in der Entwicklung erhöhen einerseits die Effizienz einer Schaltung, steigern andererseits aber deren Komplexität. Daher gelten Simulationen in der Praxis nicht mehr als vertrauenswürdig. Das Fehlen von vollautomatisierten Verifikationsmethoden für arithmetische Schaltungen ist aktuell immer noch ein großer Makel.

Seit dem Bekanntwerden des FDIV-Bugs werden formale Verifikationstechniken entwickelt, welche die Korrektheit von arithmetischen Schaltungen und insbesondere von Multiplizierern beweisen sollen. Eine gängige Verifikationsmethode ist, das Verifikationsproblem als ein Erfüllbarkeitsproblem der Aussagenlogik (SAT) zu kodieren. SAT wird unter anderem als „key technology for the 21st century“ (Edmund Clark, 2007 ACM Turing Award Recipient) bzw. als „killer app“ (Donald Knuth, 1974 ACM Turing Award Recipient) gesehen (iospress.com). Bei dieser Methode wird die Schaltung zu einer Formel in konjunktiver Normalform übersetzt und ein SAT-Solver eingesetzt, um die Erfüllbarkeit dieser Formel zu überprüfen. Im Jahr 2016 wurde eine größere Menge von solchen Kodierungen für arithmetische Schaltungen als Benchmarks zur jährlichen SAT-Competition eingereicht (satcompetition.org). Bei diesem Wettbewerb werden die aktuell besten SAT-Solver anhand einer Menge von Benchmarks ermittelt. Die Ergebnisse dieser Evaluierung zeigen allerdings, dass Kodierungen von Multiplizierern zu exponentiell großen Beweisen führen; dies deutet auf eine exponentielle Laufzeit von SAT-Solvern hin.

Seit rund 5 Jahren werden Verifikationstechniken basierend auf Computeralgebra als ein vielversprechender Zugang zur automatisierten Verifikation von arithmetischen Schaltungen und insbesondere Multiplizierern gesehen. Computeralgebra beschäftigt sich mit der Entwicklung von Algorithmen für exakte Lösungen für komplexe mathematische Probleme. In dieser Methode werden alle Logikgatter des Multiplizierers sowie die Spezifikation als ein Polynom kodiert. Mittels algebraischer Reduktion basierend auf multivariater Polynomdivision kann nun das Problem, ob eine gegebene Schaltung einen korrekten Multiplizierer implementiert, gelöst werden, indem die Normalform des Spezifikationspolynoms bezüglich der Gatterpolynome berechnet wird. Der Multiplizierer ist fehlerfrei genau dann, wenn diese Normalform null ist.

Das klingt auf den ersten Blick offensichtlich, doch wie so oft, ist es in der Praxis dann doch nicht so leicht wie es klingt. Experimente zeigen, dass bereits für einfache 8-Bit-Multiplizierer mit 16 Eingängen die Normalform der Spezifikation nicht mehr in gängigen Computeralgebra-Systemen ermittelt werden kann. Der Grund dafür ist, dass die Zwischenresultate der einzelnen Polynomdivisionen exponentiell anwachsen, bevor sie zu null reduzieren. Daher sind in der Praxis dedizierte Vorbearbeitungsschritte notwendig, um die mathematische Modellierung des Multiplizierers zu vereinfachen. Mit diesen Techniken ist es heutzutage möglich, 2048-Bit-Multiplizierer mit 4096 Eingangssignalen innerhalb einer Stunde erfolgreich in eigens entwickelten Verifikationstools zu verifizieren.

An dieser Stelle kann man sich die Frage stellen: Wer verifiziert eigentlich den Verifizierer? Denn auch in der Verifikation können Fehler passieren und zu falschen Ergebnissen führen. Eine Möglichkeit ist es, das Verifikationstool mit Hilfe eines Theorembeweisers zu verifizieren. Dies gilt aber aufgrund der Komplexität der Software als nicht praktikabel. Eine einfachere Methode ist es daher, ein simples Beweiszertifikat zu erstellen, welches es ermöglicht, die Verifikationsschritte nachzuvollziehen und unabhängig zu überprüfen. Man kann sich das ähnlich zu einer Rechenprobe wie bei Division von Zahlen vorstellen. Für SAT ist dieses Prozedere bereits gang und gäbe und wird seit 2013 auch in der jährlichen SAT-Competition vorgeschrieben. Für algebraische Beweistechniken werden seit rund 3 Jahren praktische Beweisformate entwickelt, welche es erlauben, während der Verifikation ein simples Beweiszertifikat zu generieren. Diese Zertifikate können dann mit einem eigenständigen Beweis-Checker auf Korrektheit überprüft werden (danielakaufmann.at).

Und wer beweist nun den Beweis-Checker? Es kann immer noch der Fall eintreten, dass während der Verifikation ein Fehler gemacht worden ist, der auch im Beweiszertifikat enthalten ist, aber vom Beweis-Checker nicht erkannt wird. An dieser Stelle kann man sich zu Nutze machen, dass Beweis-Checker üblicherweise sehr einfache Tools sind. Für Verifikation mittels Computeralgebra sind im Beweis-Checker nur die Operationen Polynomaddition und -multiplikation notwendig. Diese Operationen lassen sich in einem Theorembeweiser, wie etwa Isabelle/HOL, zertifiziert implementieren (tum.de). Vereinfacht gesagt basieren Theorembeweiser auf einem minimalen Kernel, der so simpel ist, dass man ihm vertraut. Jegliche zusätzliche benötigte Operation muss im Theorembeweiser formal bewiesen werden, um die Korrektheit garantieren zu können. Können wir also die Korrektheit von einem Multiplizierer mit einem Verifikationstool beweisen, und das zugehörige Beweiszertifikat wird von einem zertifizierten Beweis-Checker validiert, können wir uns der Korrektheit der Schaltung sicher sein.

Wir danken Frau Kaufmann, die diesen in ihr Forschungsgebiet einführenden Text geschrieben hat.

GI-MELDUNGEN

Gewissensbit: Sicherheit, Bequemlichkeit, Expertise: was ist Ihnen am wichtigsten? Wir alle nutzen Apps, die uns das Leben erleichtern – häufig auch, ohne die Sicherheitsvorkehrungen zu duchschauen. Solange es nicht um personenbezogenen Daten geht, mag das angehen, aber was, wenn persönliche Daten in falsche Hände gelangen und/oder gefälscht werden? Wer ist für die Sicherheit von Apps verantwortlich? Wer soll wie und an wen Sicherheitslücken melden? Kniffelige Fragen, die im aktuellen Gewissensbit skizziert werden. Wie würden Sie entscheiden? Die Autorinnen freuen sich auf eine rege Diskussion.  weiterlesen

INFORMATIK 2021: der Rückblick im Film. Vor vier Wochen haben sich rund 1000 Informatikerinnen und Informatiker zur GI-Jahrestagung getroffen und rund um das Thema Nachhaltigkeit zahlreiche Facetten der Informatik diskutiert. Einen bewegten Rückblick gibt es jetzt.  weiterlesen

GI-Junior-Fellows gesucht. Die GI-Junior-Fellows besetzen innerhalb der GI mittlerweile viele herausragende Positionen und wirken so an der Arbeit an und mit der GI mit. Sie finden sich im Vorstand und leiten die GI-Radar-Redaktion, geben LNI-Reihen heraus, initiieren eigene Projekte und mischen das Präsidium auf. Wir sind auf der Suche nach jungen Informatik-Talenten, die sich bereits profiliert haben und daran interessiert sind, in der GI aktiv mitzumachen. Bewerbungs- bzw. Nominierungsschluss ist der 25. Mai.  weiterlesen

Preis des GI-Verbundprojektes Digital Autonomy Hub ausgeschrieben. Gemeinsam mit anderen Organisationen betreibt die GI das Netzwerk „Digitale Autononomy Hub“, das sich die Stärkung der digitalen Souveränität zum Ziel gesetzt hat. Das Netzwerk schreibt nun einen Preis für innovative und wirksame digitale Lösungen aus, die Menschen einen reflektierten und selbstbestimmten Umgang mit ihren Daten, Geräten und Anwendungen ermöglichen. Die Bewerbungs- und Nominierungsfrist endet am 7. Dezember. Mehr zum Award hinter dem Link.  weiterlesen

FAS: spezielles Angebot für GI-Mitglieder. Wir haben für GI-Mitglieder mit der Frankfurter Allgemeinen Sonntagszeitung ein besonderes Angebot ausgehandelt. Über die GI können Sie ein vergünstiges Abo abschließen und so auf alle Artikel zugreifen.  weiterlesen

 

Kennen Sie eigentlich den GI-Pressespiegel? Dort sammeln wir die Berichterstattung über unsere Fachgesellschaft in Zeitungs-, Radio- und Fernsehbeiträgen. In dieser Woche berichtet unter anderem heise über einen offenen Brief gegen autonome Waffensysteme, der von vielen GI-Mitgliedern unterzeichnet wurde. Schauen Sie rein, es gibt da immer wieder Neues.

FUNDSTÜCK

Tracking meiner Gesundheitsdaten: Verantwortung oder Auslieferung? (engl., The Guardian). Eigentlich ist es ja durchaus sinnvoll, sich Gedanken um seine Gesundheit zu machen, dafür zu sorgen, dass man sich ausreichend bewegt, gesund isst und gut schläft. Sehr einfach lässt sich das mittels verschiedener Geräte tracken. Leider kann es aber vorkommen, dass die Versicherung einen plötzlich für faul hält und hochstuft – nur weil der Tracker kaputtgegangen ist und durch eine profane Armbanduhr ersetzt wurde. Oder man hält sich plötzlich für schwer krank, weil der Blutzucker einmal hochschießt oder das EKG kurzzeitig merkwürdig aussieht. Will man das wirklich?  Zum Fundstück (theguardian.com, engl.)

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

 

Dies war Ausgabe 298 des GI-Radars. Zusammengestellt hat sie Dominik Herrmann, der sich nun fragt, welche Einsichten er aus seiner automatisch aufgezeichneten Bildschirmzeit gewinnen könnte. GI-Geschäftsführerin Cornelia Winter hat die Mitteilungen und Meldungen zusammengetragen. Das nächste GI-Radar erscheint am 19. November 2021.

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. Links und Texte können Sie uns auch über Twitter (@informatikradar) zukommen lassen.