Escaping the Quicksand: A Call to Arms

Stellen Sie sich eine Welt vor, in der die unsichtbare Maschinerie des modernen Lebens – unsere Banken, Krankenhäuser, Stromnetze und Kommunikationsnetzwerke – auf einem Fundament errichtet ist, das langsam einsinkt. Dies ist die Realität, mit der die Computerindustrie heute konfrontiert ist. Jahrzehntelang war die Standardmethode zum Erstellen von Software, eine grobe Beschreibung dessen zu verfassen, was ein Programm tun soll, dann den Code zu schreiben und ihn schließlich durch das Ausführen mit verschiedenen Eingaben zu testen, um zu sehen, ob er abstürzt. Diese Methode, bekannt als Test-and-Debug-Entwicklung, hat die Technologie zwar aufblühen lassen, hinterlässt jedoch Systeme voller verborgener Mängel. Da die ursprünglichen Beschreibungen oft vage sind und in gewöhnlicher Sprache verfasst wurden, können sie nicht von Maschinen überprüft werden, und da das Testen nur einen winzigen Bruchteil der Milliarden möglichen Arten abdecken kann, wie sich ein Programm verhalten könnte, schlüpfen viele Fehler durch. Da künstliche Intelligenz beginnt, mehr Code zu schreiben, droht dieser Zyklus dies zu beschleunigen und schafft riesige neue Systeme, die noch komplexer und fragiler sind als zuvor – gebaut auf einem „Quicksand“ (Quicksand) aus jahrzehntealten Designentscheidungen, die getroffen wurden, als Cyberangriffe selten und Rechenleistung knapp waren.

Zwei Forscher, Peter Sewell von der University of Cambridge und Jean Pichon-Pharabod von der Aarhus University, argumentieren, dass die Industrie seit fünfundsiebzig Jahren in einer gefährlichen Schleife feststeckt. Sie beobachten, dass wir zwar unglaublich geschickt darin geworden sind, Code zu schreiben, aber die präzisen Definitionen dessen, was dieser Code erreichen soll, vernachlässigt haben. Der aktuelle Ansatz stützt sich auf Prosa-Spezifikationen – Textabsätze, die das Verhalten eines Systems beschreiben. Während diese für Menschen leicht lesbar sind, sind sie von Natur aus mehrdeutig und unvollständig. Ein menschlicher Leser interpretiert einen Satz vielleicht auf eine Weise, während eine Maschine oder ein anderer Mensch ihn anders interpretiert. Da diese Beschreibungen nicht direkt von einem Computer getestet werden können, sind Entwickler gezwungen zu raten, welches das korrekte Verhalten sein sollte, wobei sie sich oft auf einfache Prüfungen wie „stürzt das Programm ab?“ verlassen, anstatt zu verifizieren, ob das Programm tatsächlich das Richtige tut. Diese Lücke zwischen der geschriebenen Absicht und dem tatsächlichen Code erzeugt eine enorme Menge an technischer Schuld – eine versteckte Kostenlast, die sich in Sicherheitslücken und Systemfehlern manifestiert, die von Angreifern ausgenutzt werden können.

Die Autoren schlagen vor, dass die Lösung nicht darin besteht, das Testen aufzugeben, sondern die Art und Weise zu ändern, wie wir Spezifikationen verwenden. Anstatt vage Absätze zu schreiben, schlagen sie vor, Spezifikationen zu erstellen, die ausführbar sind, was bedeutet, dass sie in einer Form geschrieben sind, die ein Computer ausführen kann. Stellen Sie sich eine Spezifikation vor, die als lebender Schiedsrichter während des Entwicklungsprozesses fungiert. Während Code geschrieben oder generiert wird, läuft diese ausführbare Spezifikation parallel dazu und prüft sofort, ob das Verhalten des Codes mit den beabsichtigten Regeln übereinstimmt. Wenn der Code versucht, etwas zu tun, das die Spezifikation verbietet, meldet das System dies sofort. Dies schafft eine viel engere Feedbackschleife und ermöglicht es Entwicklern, Fehler abzufangen, während sie entstehen, anstatt erst Wochen später. Dieser Ansatz kann auf verschiedene Weise angewendet werden: Man kann mit dem Code beginnen und eine Spezifikation passend dazu schreiben, mit einer Spezifikation beginnen und Code generieren, der ihr entspricht, oder beides gemeinsam aufbauen. Der entscheidende Punkt ist, dass die Spezifikation nicht nur ein Dokument zum Lesen ist, sondern ein Werkzeug zur Anwendung.

Die Forscher räumen jedoch ein, dass dies kein einfacher Schalter ist, den man umlegen kann. Um dies in großem Maßstab umzusetzen, muss die Computer-Community eine neue Ebene der Infrastruktur aufbauen. Derzeit gibt es keine universell akzeptierten, maschinenlesbaren Definitionen für das Verhalten vieler grundlegender Technologien, wie etwa der Programmiersprache C, der Sprache Rust oder der Befehle, die auf Computerchips laufen. Während einige Forscher erfolgreich diese Definitionen für spezifische Teile des Systems erstellt haben, gibt es keinen einheitlichen Rahmen, der sie alle verbindet. Die Autoren weisen darauf hin, dass der Aufbau dieser Infrastruktur eine Herausforderung der Skalierung und Kooperation ist. Es erfordert eine massive, koordinierte Anstrengung von Universitäten, Regierungen und Technologieunternehmen, um diese präzisen Definitionen für den gesamten Stack der Computertechnologie zu erstellen, zu validieren und zu pflegen – vom Hardware-Bereich bis hin zu den Cloud-Diensten.

Das Paper befasst sich auch mit der Rolle der künstlichen Intelligenz. Die Autoren warnen davor, dass die bloße Verwendung von KI, um mehr Code zu schreiben, ohne diese besseren Feedbackschleifen zu nutzen, das Problem nur verschlimmern wird. KI kann Code schneller als Menschen generieren, aber wenn dieser Code auf wackeligen Fundamenten aufgebaut und nur mit den alten, ineffektiven Methoden getestet wird, wird er einfach nur größere Systeme mit mehr verborgenen Fehlern schaffen. Umgekehrt, wenn KI dazu verwendet wird, diese ausführbaren Spezifikationen zu helfen zu generieren und zu prüfen, könnte sie zu einem mächtigen Werkzeug zur Verbesserung der Softwarequalität werden. Die Autoren sehen eine Zukunft voraus, in der KI hilft, rigorose Spezifikationen zu erstellen, und in der diese Spezifikationen dazu verwendet werden, sowohl menschengeschriebenen als der KI-geschriebenen Code zu verifizieren. Dies würde einen graduellen Anstieg des Vertrauens ermöglichen, beginnend mit einfachen Tests und übergehend zu komplexeren mathematischen Beweisen der Korrektheit, ohne dass jeder Entwickler ein Mathematiker werden muss.

Trotz des klaren Weges nach vorne argumentieren die Autoren, dass die Industrie durch eine Diskrepanz der Anreize zurückgehalten wurde. Technologieunternehmen sind motiviert, Produkte schnell zu veröffentlichen, um Marktanteile zu gewinnen, während die Risiken des Scheiterns weitgehend die Gesellschaft und die Endnutzer treffen. Den robusten Aufbau der Infrastruktur, der nötig ist, um diese Ausfälle zu verhindern, zu leisten, ist teuer und zeitaufwendig, und kein einzelnes Unternehmen möchte die vollen Kosten für die Behebung von Problemen tragen, die alle betreffen. Die Forscher rufen zu einer kollektiven Anstrengung auf, ähnlich den groß angelegten Projekten in der Physik oder Biologie, um die Schaffung dieser semantischen Infrastruktur zu finanzieren und zu koordinieren. Sie legen nahe, dass die Kosten zwar erheblich sind, aber nur einen winzigen Bruchteil der derzeitigen Ausgaben für künstliche Intelligenz ausmachen und essenziell für die Sicherung der Zukunft der Computertechnik sind. Ohne diesen Wandel bleibt die Industrie in einem Zyklus gefangen, immer komplexere Systeme auf Fundamenten zu bauen, die zu schwach sind, um sie zu tragen, was die Gesellschaft einem ständigen Risiko aussetzt.

Die Autoren kommen zu dem Schluss, dass die Werkzeuge und Methoden zur Lösung dieses Problems bereits existieren. Forscher haben erfolgreich demonstriert, wie man das Verhalten komplexer Systeme definiert und mit hoher Zuverlässigkeit verifiziert. Was fehlt, ist der Wille, diese Methoden in die alltägliche Praxis zu bringen und die gemeinsame Infrastruktur aufzubauen, die sie für alle zugänglich macht. Das Paper dient als Aufruf zum Handeln an die Forschungsgemeinschaft, die Branchenführer und die Förderstellen, bei dieser Aufgabe zusammenzuarbeiten. Indem wir uns von vagen Beschreibungen weg und hin zu präzisen, ausführbaren Spezifikationen bewegen, kann die Computerwelt dem Quicksand der technischen Schuld entkommen und eine Zukunft gestalten, die nicht nur innovativer, sondern auch grundlegend sicherer und zuverlässiger ist.