Crash-Toleranz: MIT arbeitet an mathematisch bewiesenem Dateisystem

Die Forscher des MIT haben ein Dateisystem entwickelt, das besonders robust sein soll. Ein Absturz soll, mathematisch bewiesen, in keinem Fall zu einem Datenverlust führen können. Für den Einsatz in performanten Systemen eignet es sich allerdings noch nicht.

Artikel veröffentlicht am ,
Das MIT arbeitet an einem mathematisch verifizierten Dateisystem für Speichermedien.
Das MIT arbeitet an einem mathematisch verifizierten Dateisystem für Speichermedien. (Bild: Andreas Sebayang/Golem.de)

Das Massachusetts Institute of Technology (MIT) will in Kürze ein Crash-tolerantes Dateisystem vorstellen, das einen besonderen Fokus auf die Datensicherheit hat. Die Forscher gehen sogar so weit, dass der Nutzer niemals Daten verlieren wird. Das bezieht sich aber auf normale Operationen und nicht etwa auf Festplattencrashes.

Stellenmarkt
  1. Product Information Management Specialist (m/w/d)
    SICK AG, Waldkirch
  2. Betreuungsingenieur (w/m/d) OT-Sicherheit
    Wacker Chemie AG, Burghausen
Detailsuche

Damit ein Datenträger keine Daten verliert, mussten die Entwickler unterschiedliche Zeitpunkte eines Absturzes absichern. Laut den MIT-Entwicklern ist die Aufgabe so schwierig, dass selbst jahrelang getestete Dateisysteme immer noch in bestimmten, seltenen Situationen Fehler zeigen, die einen Datenverlust zur Folge haben. Es ist eine Frage des Timings, ob just in dem Moment ein Bit verloren geht.

Beweisführung und Implementierung in Coq

Das MIT will mit einem anderen Ansatz die Entwicklung eines Dateisystems vereinfachen. Die Mathematik soll helfen. Laut dem MIT ist das neue Dateisystem und dessen Crash-Toleranz mathematisch bewiesen. Das würde die aufwendige Fehlersuche und das Erzeugen etlicher Crash-Situationen ersparen. Das MIT spricht von vorher definierten akzeptablen Betriebsgrenzen, in denen der normale Betrieb stattfindet und in dem die Operationen formal verifiziert werden. Helfen soll zudem, dass das Dateisystem in derselben Sprache implementiert wird, in der auch die Beweisführung stattfindet: Coq.

Die Forschungsarbeit soll im Oktober 2015 im Detail vorgestellt werden. Für den Einsatz ist das System nicht geeignet, da es nach heutigen Standards langsam arbeitet, wie die Forscher zugeben. Der Beschreibung nach bietet es aber die Ansätze, um in Zukunft die formale Korrektheit eines Dateisystems schneller zu beweisen und gleichzeitig die Grenzen des Systems zu definieren. Das MIT hofft also, die Grundlagenarbeit für zukünftige Dateisysteme geschaffen zu haben.

Golem Karrierewelt
  1. AZ-104 Microsoft Azure Administrator: virtueller Vier-Tage-Workshop
    19.-22.09.2022, virtuell
  2. Elastic Stack Fundamentals – Elasticsearch, Logstash, Kibana, Beats: virtueller Drei-Tage-Workshop
    26.-28.09.2022, Virtuell
Weitere IT-Trainings

Dateisysteme gehören zu den sehr kritischen Teilen der Softwareinfrastruktur eines Computersystems. Hierin liegt auch der Grund, warum viele Jahre für die Entwicklung gebraucht werden, bis ein Dateisystem als stabil eingestuft wird. Wegen der Komplexität entscheiden sich viele Betriebssystemhersteller oder auch Hersteller von Speicherlösungen gegen den Wechsel eines Dateisystems.

Bitte aktivieren Sie Javascript.
Oder nutzen Sie das Golem-pur-Angebot
und lesen Golem.de
  • ohne Werbung
  • mit ausgeschaltetem Javascript
  • mit RSS-Volltext-Feed


Bitschnipser 27. Aug 2015

Oder du machst es dir einfach und verlässt dich darauf, dass die Leute sagen, dass Coq...

Bitschnipser 27. Aug 2015

Sowas wie Coq ist viel leichter zu validieren als ein Dateisystem. Validieren bedeutet ja...

teenriot* 25. Aug 2015

Relaiv zu "Ich bin Patriot, ich will Schland-Nachrichten, alles Scheiße hier" ist fast...

476f6c656d 25. Aug 2015

Es muss hardwareunabhängig sein. Ich schätze sie haben es formal bewiesen.



Aktuell auf der Startseite von Golem.de
Eichrechtsverstoß
Tesla betreibt gut 1.800 Supercharger in Deutschland illegal

Teslas Supercharger in Deutschland sind wie viele andere Ladesäulen nicht gesetzeskonform. Der Staat lässt die Anbieter gewähren.

Eichrechtsverstoß: Tesla betreibt gut 1.800 Supercharger in Deutschland illegal
Artikel
  1. Bitblaze Titan samt Baikal-M: Russischer Laptop mit russischem Chip ist fast fertig
    Bitblaze Titan samt Baikal-M
    Russischer Laptop mit russischem Chip ist fast fertig

    Ein 15-Zöller mit ARM-Prozessor: Der Bitblaze Titan soll sich für Office und Youtube eignen, die Akkulaufzeit aber ist fast schon miserabel.

  2. Quartalsbericht: Huawei steigert den Umsatz trotz US-Sanktionen wieder
    Quartalsbericht
    Huawei steigert den Umsatz trotz US-Sanktionen wieder

    Besonders im Bereich Cloud erzielt Huawei wieder Zuwächse.

  3. Maschinelles Lernen und Autounfälle: Es muss nicht immer Deep Learning sein
    Maschinelles Lernen und Autounfälle
    Es muss nicht immer Deep Learning sein

    Nicht nur das autonome Fahren, sondern auch die Fahrzeugsicherheit könnte von KI profitieren - nur ist Deep Learning nicht unbedingt der richtige Ansatz dafür.
    Von Andreas Meier

Du willst dich mit Golem.de beruflich verändern oder weiterbilden?
Zum Stellenmarkt
Zur Akademie
Zum Coaching
  • Schnäppchen, Rabatte und Top-Angebote
    Die besten Deals des Tages
    Daily Deals • Günstig wie nie: Palit RTX 3080 Ti 1.099€, Samsung SSD 2TB m. Kühlkörper (PS5) 219,99€, Samsung Neo QLED TV (2022) 50" 1.139€, AVM Fritz-Box • Asus: Bis 840€ Cashback • MindStar (MSI RTX 3090 Ti 1.299€, AMD Ryzen 7 5800X 288€) • Microsoft Controller (Xbox&PC) 48,99€ [Werbung]
    •  /