«Programme sind Mathematik, die zur Physik wird»
ETH-Professor Ralf Jung hat sich zum Ziel gesetzt, eine Welt zu schaffen, in der fehlerhafte Software der Vergangenheit angehört. Seine Werkzeuge, um dieses Ziel zu erreichen, sind auch seine grössten intellektuellen Leidenschaften: Mathematik und Logik.
Eine Welt ohne Softwarefehler: Das ist das einfache, wenn auch äusserst schwer zu erreichende Ziel der Forschung von Ralf Jung. Wie die jüngsten Ereignisse einmal mehr gezeigt haben, können fehlerhafte Programme grosse Teile der Weltwirtschaft zum Erliegen bringen. Im schlimmsten Fall kann ein fehlerhafter Code Menschenleben kosten (z. B. Therac-25). Zudem ist es schwer vorhersehbar, wann der nächste katastrophale Fehler auftritt, da die Abhängigkeit von potenziell fehlerhafter Technologie weiter zunimmt.
«Es ist wahnsinnig frustrierend, weil Computerprogramme der Vollkommenheit platonischer Ideen wohl am nächsten kommen. Programme sind im Grunde genommen Mathematik, die in Physik umgewandelt wurde. Und Mathematik sollte streng, reproduzierbar und deterministisch sein», führt Jung aus. Er beklagt, dass die Realität, im Gegensatz zur Idealvorstellung, ganz anders aussieht. Programme stürzen immer wieder ab; und die Menschen haben sich daran gewöhnt. «Je genauer man sich mit den Programmen beschäftigt, desto mehr fragt man sich, warum überhaupt etwas funktioniert. Es ist ein reines Wunder», sagt er.
Eine verblüffende Einsicht
Jungs Forschungsgebiet sind formale Methoden zur Software-Verifikation. Im Gegensatz zu Techniken wie Software-Tests, die die Leistung, die Zuverlässigkeit und die Korrektheit von Programmen in einer begrenzten Anzahl von Situationen überprüfen, zielen formale Methoden darauf ab, mit den strengen Werkzeugen der Mathematik und Logik bestimmte Eigenschaften von Software oder sogar ganzen Programmiersprachen zu beweisen. Das Ziel besteht darin, zu beweisen, ob Computerprogramme abstürzen, sie die erwarteten Ergebnisse produzieren oder es überhaupt ein Ergebnis gibt, nachdem das Programm ausgeführt wurde – und diese Behauptungen müssen immer wahr sein. Es ist eine Arbeit, welche die intellektuellen Aktivitäten miteinander in Verbindung bringt, die Jung am meisten am Herzen liegen.
«Die Entdeckung, dass es eine so tiefe Verbindung zwischen Logik und Programmierung gibt, war einer der grössten Momente in meinem Leben», sagt Jung. Diese Entdeckung verdankt er seinem langjährigen Mentor Gert Smolka, Professor für Informatik an der Universität des Saarlandes in Deutschland. Jung bezeichnet Smolkas Kurs «Einführung in die Computerlogik», den er während seines Studiums belegte, als die einflussreichste Erfahrung, die er in seinen entscheidenden Lebensjahren machte. «Ich hatte mich schon immer für Logik und Programmierung interessiert, und Smolka, der ein sehr enthusiastischer Dozent war, brachte mir bei, dass beides auf einer tiefen Ebene dasselbe ist. Das war absolut verblüffend», erinnert sich Jung.
Mathematik beim Rennen
Seine Vorliebe für Mathematik rührt aus seiner frühen Kindheit. Bei Gesprächen am Esstisch wurde regelmässig über Mathematik gesprochen. Seine Eltern, beide promovierte Wissenschaftler:innen, stellten ihm und seinem jüngeren Bruder mathematische Rätsel, um die Jungen beim Laufen im Wald oder auf langen Autofahrten zu unterhalten. Im Alter von elf Jahren erhielt Jung von seinem Vater ein ganz besonderes Weihnachtsgeschenk: ein Buch, um Kindern die Programmiersprache C beizubringen. Damals war Jung bereits ein begeisterter Gamer, aber er durfte nur sechs Stunden pro Woche am PC sitzen. Schon bald hatte er das Programmierbuch und einige weitere Bücher verschlungen; und seine Eltern verdoppelten seine Bildschirmzeit, damit er genauso viel Zeit mit Programmieren wie mit Videospielen verbringen konnte. Schon vor dem Abschluss des Gymnasiums wusste Jung, dass er Informatiker werden wollte. So kam es, dass er an der Universität des Saarlandes immatrikuliert wurde, die im Bereich Informatik eine Spitzenposition innehat.
«Die Entdeckung, dass es eine so tiefe Verbindung zwischen Logik und Programmierung gibt, war einer der grössten Momente in meinem Leben»Professor Ralf Jung
In dieser schicksalhaften Vorlesung bei Professor Smolka lernte Jung zum ersten Mal den Beweisassistenten Coq kennen, ein Werkzeug zur Durchführung maschinell überprüfter Beweise, das seither eine wichtige Rolle in seiner Forschung spielt. Jung beschreibt seine erste Begegnung mit Coq in Smolkas Kurs als «unglaublich spassig». «Das Abschliessen eines Beweises in Coq verschaffte mir immer einen Endorphinschub, als ob man bei einem Videospiel das nächste Level erreichen würde», erinnert er sich.
Ein Glücksfall führt zum Jobangebot
Als es an der Zeit war, ein Thema für seine Bachelorarbeit zu wählen, gab es für Jung nur eine einzige Vorgabe: Es musste sich um Beweise in Coq drehen. Das war auch die einzige Vorgabe, die ihn bei der Wahl des Themas seiner Doktorarbeit leitete. Die Suche nach einem Doktorvater verlief jedoch nicht völlig linear und wurde auch nicht rein von der Vernunft bestimmt. Auch der Zufall spielte eine Rolle. Eines Tages, im Jahr 2013, stiess Jung nämlich auf ein Plakat, das für Forschungsarbeiten zu maschinell geprüften Beweisen warb. Er schrieb eine E-Mail an Professor Derek Dreyer, der auf dem Plakat genannt wurde, und erhielt innerhalb weniger Tage eine Antwort von ihm – das war ein wahrer Glücksfall. Das Büro von Professor Dreyer befand sich auf dem Campus, aber Jung wusste nichts über ihn, da er mit dem Max-Planck-Institut für Softwaresysteme – und nicht direkt mit der Universität – verbunden war und (noch) keine Kurse unterrichtete.
«Zunächst zögerte ich, mich auf mein Dissertationsthema festzulegen, aber Derek fesselte mich, indem er mich mit einem ständigen Strom interessanter kleiner Probleme versorgte, bis er mir eines Tages den Schlüssel zu einem Büro gab und mich fragte: ‹Soll ich dir ein Gehalt zahlen?›», erinnert sich Jung. «Dreyer hat mich auch während der restlichen Zeit der Promotion und bis heute hervorragend betreut. Er ist wirklich mein ‹Doktorvater›, im besten Sinne des Wortes, und dafür bin ich sehr dankbar», sagt er.
Jung schloss schliesslich im Sommer 2020 seine Promotion unter der Betreuung von Professor Dreyer ab. Auf den fast 300 Seiten seiner Dissertation wird der Coq-Beweisassistent – vielleicht wenig überraschend – 65-mal erwähnt.
Jungs Dissertation wurde mit mehreren renommierten Preisen ausgezeichnet und trug dazu bei, sein Profil als führender Forschender auf dem Gebiet der Programmiersprachen zu schärfen. Gleichzeitig wurde er durch seine Dissertation als einer der grössten Expert:innen für die Programmiersprache Rust bekannt.
Eine Programmiersprache für sichere Software
Graydon Hoare begann um 2009 mit der Entwicklung von Rust, als er noch Softwareentwickler bei Mozilla war. Jung begann sich Anfang 2015 für die neue Sprache zu interessieren, nur wenige Monate, bevor die erste stabile Version von Rust veröffentlicht wurde. Inzwischen programmieren weltweit fast drei Millionen Programmierer:innen in Rust – und viele davon sind von der Sprache sehr angetan. Auch Tech-Giganten vom Kaliber Amazon, Google und Microsoft entwickeln zunehmend Software damit. Sogar das Weisse Haus hat Organisationen empfohlen, in ihren Projekten verstärkt auf Rust zu setzen, um Software ausfallsicherer und weniger anfällig für Cyberattacken zu machen.
Die wachsende Gemeinschaft, die mit Rust baut, bringt Tausende von Enthusiastinnen und Enthusiasten zusammen; und Jung ist stolz darauf, einer von ihnen zu sein. Er ist aber davon überzeugt, dass viele andere Menschen mehr dazu beigetragen haben, Rust zu einem Erfolg zu machen, als er selbst. Er hat aber unbestreitbar eine entscheidende Rolle bei der Schaffung der theoretischen Grundlagen für die Zuverlässigkeit und die Sicherheit gespielt, die Rust so populär gemacht haben und von der Industrie in grossem Umfang angenommen wurden.
Ein Grossteil der Attraktivität von Rust beruht auf den Versprechungen der Entwickler:innen in Bezug auf die Leistung und die Zuverlässigkeit von Programmen, die in dieser Sprache geschrieben werden. Sie behaupten, dass in Rust geschriiebener Code nicht nur sehr schnell läuft und den Entwickler:innen eine feinkörnige Kontrolle darüber gibt, was zur Laufzeit mit kritischen Ressourcen wie dem Speicher geschieht, sondern, dass auf diese Art und Weise geschriebener Code aufgrund seines Designs auch frei von einigen der häufigsten Fehler ist, die in Programmen auftreten, die in älteren Systemprogrammiersprachen wie C und C++ geschrieben wurden. Rust erreicht diesen Effekt, indem es sicherstellt, dass eine Vielzahl von Fehlern, die bei der Handhabung von Speicher in einem Programm auftreten können, vor der Laufzeit durch den Compiler erkannt werden – die Software, die den von der Entwicklerin oder dem Entwickler geschriebenen Quellcode in den für Computer verständlichen Binärcode übersetzt. Auf diese Weise müssen sich die Entwickler:innen nicht selbst um die Suche nach solchen Fehlern kümmern. Wenn ihr Code fehlerhaft ist, gibt der Compiler eine Fehlermeldung mit genauen Anweisungen zur Behebung des Problems aus. Die Sprache ermöglicht es Programmierer:innen aber auch, Code ausserhalb dieses «sicheren Modus» zu schreiben. Der Schlüssel dazu, dass «unsicheres Rust» dem Versprechen gerecht wird, dass die Sprache insgesamt sicher ist, liegt darin, die widerspenstigen Codestücke in Bibliotheken zu verpacken, die sich nach aussen hin so verhalten, als ob alles in «sicherem» Rust geschrieben wäre.
Mit «Legosteinen» zu mathematischen Beweisen
In seiner Dissertation bewies Jung, dass diese Bibliotheken tatsächlich die von den Entwickler:innen von Rust versprochene Sicherheit garantieren. Zu diesem Zweck hat er ein Tool namens RustBelt entwickelt, mit dem Forschende formale Beweise erbringen können. «Mit RustBelt können wir Eigenschaften der Rust-Sprache nachweisen, die durch Softwaretests nicht mit demselben Mass an Sicherheit verifiziert werden könnten», sagt Jung. RustBelt wiederum baut auf Iris auf, einem Framework, das Jung im Rahmen seiner Doktorarbeit entwickelt hat. Iris bietet eine Reihe von Bausteinen, die es Forschenden erleichtern, mathematische Modelle zu erstellen und formale Beweise für jede beliebige Programmiersprache, nicht nur für Rust, durchzuführen.
Mit Iris haben diese Forschenden eine Reihe wiederverwendbarer Teile, die sie für die Beweise, die sie konstruieren, zusammensetzen können. «Es ist, als hätte man Legosteine, um mathematische Beweise auf dem Computer zu erstellen, und die Leute bauen manchmal beeindruckende Türme zusammen», sagt Jung. Iris ist das, was Fachleute als «nebenläufig Trennungslogik» bezeichnen: eine Theorie, mit der Forschende analysieren können, was in einem Programm passiert, wenn mehr als ein Prozess gleichzeitig auf dieselben Daten zugreift. Diese Nebenläufigkeit ist in der modernen Programmierung von entscheidender Bedeutung, da sie es ermöglicht, den Code auf modernen Mehrkernprozessoren schneller auszuführen. Die Nebenläufigkeit ist aber auch die Quelle häufiger Fehler, die dazu führen, dass Programme unkontrolliert abstürzen oder von Cyberkriminellen gehackt werden. Mit Iris können Forschende nachweisen, dass ein nebenläufiges Programm zuverlässig und sicher ist – diese Eigenschaften sind solche, die sich durch Testen nur schwer sicherstellen lassen.
Während RustBelt dabei helfen soll, Rust als Sprache besser zu verstehen, zielt Stacked Borrows, der dritte Beitrag von Jungs Doktorarbeit, darauf ab, Rust weiterzuentwickeln, indem es den Compiler in die Lage versetzt, den von den Entwickler:innen geschriebenen Code zu optimieren und ihn dadurch effizienter zu machen. In den letzten Jahren hat Jung weitere Tools entwickelt, die alle das Ziel verfolgen, ein möglichst genaues Modell des Verhaltens der wichtigsten Komponenten von Rust zu erstellen und mathematische Beweise zu liefern, um das Vertrauen der Entwickler:innen in die Sprache zu stärken.
Jung sieht eine vielversprechende Zukunft für Rust voraus, da die Unternehmen es zunehmend für neue Projekte einsetzen werden, bei denen es auf Leistung, Effizienz und Sicherheit ankommt. «Rust ist eine der besten Möglichkeiten, um die momentan schwierige Situation, was das Thema Software angeht, zu verbessern», sagt er. Es wird hoffentlich nicht mehr lange dauern, bis Jungs Traum von einer Welt ohne Softwarefehler Wirklichkeit wird.
Ralf Jung ist Assistenzprofessor an der ETH Zürich und leitet das Programming Language Foundations Lab, das Teil des Instituts für Programmiersprachen und -systeme ist. Seine Forschungsschwerpunkte sind die Programmiersprache Rust und das Concurrent Separation Logic Framework Iris. Zuvor promovierte er am Max-Planck-Institut für Softwaresysteme und an der Universität des Saarlandes in Saarbrücken, Deutschland. Ausserdem war er als Post-Doc in der PDOS-Gruppe am MIT CSAIL tätig.