MIT: Neues Dateisystem mathematisch beweisbar ohne Datenverluste

Ein neues Dateisystem soll zukünftig dafür sorgen, dass Abstürze nicht mehr mit Datenverlusten verbunden sind. Die Entwickler setzen dafür allerdings nicht darauf, alle denkbaren Fehlerquellen zu bedenken und entsprechende Notfall-Maßnahmen einzubauen. Weiterhelfen soll schlicht ordentliche Mathematik. Entwickelt wurde das neue Dateisystem von Informatikern an der renommierten Technologie-Universität MIT. Diese wollen die Ergebnisse ihrer Forschung nun im Oktober auf der Fachkonferenz "ACM Symposium on Operating Systems Principles" der Öffentlichkeit vorstellen. Vorab haben sie bereits einen kleinen Einblick gegeben - wohl auch, um etwas Interesse an der ansonsten für Nichtakademiker wohl recht trockenen Veranstaltung zu wecken.

Es kommt bei den meisten Nutzern im Alltag nur selten vor, aber die Gefahr besteht immerhin und wenn es einmal passiert, dann natürlich im ungünstigsten Augenblick: Während das Betriebssystem gerade die verarbeiteten Daten einer Anwendung auf das Speichermedium schreibt, gibt es einen Absturz und es kommt zu Informations-Verlusten. Das kann im schlimmsten Fall dazu führen, dass die Arbeit von Stunden verloren ist oder eine Anwendung überhaupt nicht mehr korrekt funktioniert.

Um das zu verhindern, sind in den letzten Jahren immer mehr Schutzmechanismen in die Betriebssysteme eingebaut worden. Doch stellen diese letztlich auch keine allumfassende Lösung dar. Im Gegensatz dazu soll es bei dem neuen Dateisystem, das am MIT entwickelt wurde, mathematisch bewiesen sein, dass es nicht zu Datenverlusten kommen kann.

Man bewegt sich auf Neuland

Im Grunde sind auch verschiedene existierende Dateisysteme so konzipiert, dass die Datensicherheit in den zugrundeliegenden Algorithmen sichergestellt ist. "Diese Beweise mögen auf dem Papier auch völlig korrekt sein", erklärte Daniel Ziegler von dem Entwicklerteam. Es gibt aber derzeit kein Dateisystem, bei dem dies letztlich auch bei der vorliegenden Implementation zu beweisen wäre. Das muss noch nicht mal an der Umsetzung des Codes an sich liegen - denn benötigt würde beispielsweise auch eine Programmiersprache und ein Compiler, die mathematisch beweisbar richtig arbeiten.

Bei der Entwicklung des neuen Dateisystems musste man daher von ganz unten anfangen. Wie die Informatiker ausführten, flossen dabei fast 90 Prozent der Zeit in die Aufgabe, mathematisch korrekte Definitionen für die zahlreichen System-Komponenten und ihre Beziehungen zueinander zu finden und zu beweisen.

Die aktuelle Umsetzung der umfangreichen theoretischen Arbeit in die Praxis arbeitet noch wesentlich langsamer als die bestehenden Dateisysteme. Allerdings besteht hier letztlich noch viel Raum für Optimierungen. Außerdem, so merken die Forscher an, habe man sich hier quasi in weiten Teilen auf Neuland bewegt und die nun vorliegenden Ergebnisse können auch als Grundlage für andere Entwickler dienen, formal korrekt arbeitende Dateisysteme zu bauen.