Abo
  • Services:

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. Jade Hochschule Wilhelmshaven/Oldenburg/Elsfleth, Oldenburg
  2. M-net Telekommunikations GmbH, München

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.

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.



Anzeige
Hardware-Angebote
  1. (reduzierte Überstände, Restposten & Co.)
  2. 149,90€ + Versand (im Preisvergleich ab 184,95€)
  3. 1.299,00€

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.

Charlotte77 25. Aug 2015

Mag sein, dass man vielleicht die verlustfreie oder korrekte Datenverarbeitung durch ein...


Folgen Sie uns
       


Red Dead Redemption 2 auf der Xbox One X - Golem.de live

Wir zeigen auf zahlreich geäußerten Wunsch Red Dead Redemption 2 im Livestream auf der Xbox One X. In der Aufzeichung kommen die Details des zum Teil in 4K hereingezoomten Bildausschnittes gut zur Geltung.

Red Dead Redemption 2 auf der Xbox One X - Golem.de live Video aufrufen
Gaming-Tastaturen im Test: Neue Switches für Gamer und Tipper
Gaming-Tastaturen im Test
Neue Switches für Gamer und Tipper

Corsair und Roccat haben neue Gaming-Tastaturen auf den Markt gebracht, die sich vor allem durch ihre Switches auszeichnen. Im Test zeigt sich, dass Roccats Titan Switch besser zum normalen Tippen geeignet ist, aber nicht an die Geschwindigkeit des Corsair-exklusiven Cherry-Switches herankommt.
Ein Test von Tobias Költzsch

  1. Azio RCK Retrotastatur wechselt zwischen Mac und Windows-Layout
  2. OLKB Planck im Test Winzig, gerade, programmierbar - gut!
  3. Alte gegen neue Model M Wenn die Knickfedern wohlig klackern

IT: Frauen, die programmieren und Bier trinken
IT
Frauen, die programmieren und Bier trinken

Fest angestellte Informatiker sind oft froh, nach Feierabend nicht schon wieder in ein Get-together zu müssen. Doch was ist, wenn man kein Team hat und sich selbst Programmieren beibringt? Women Who Code veranstaltet Programmierabende für Frauen, denen es so geht. Golem.de war dort.
Von Maja Hoock

  1. Software-Entwickler CDU will Online-Weiterbildung à la Netflix
  2. Job-Porträt Cyber-Detektiv "Ich musste als Ermittler über 1.000 Onanie-Videos schauen"
  3. Bundesagentur für Arbeit Ausbildungsplätze in der Informatik sind knapp

IMHO: Valves Ka-Ching mit der Brechstange
IMHO
Valves "Ka-Ching" mit der Brechstange

Es klingelt seit Jahren in den Kassen des Unternehmens von Gabe Newell. Dabei ist die Firma tief verschuldet - und zwar in den Herzen der Gamer.
Ein IMHO von Michael Wieczorek

  1. Artifact im Test Zusammengewürfelt und potenziell teuer
  2. Artifact Erste Kritik an Kosten von Valves Sammelkartenspiel
  3. Virtual Reality Valve arbeitet an VR-Headset und Half-Life-Titel

    •  /