Abo
  • Services:
Anzeige
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)

Crash-Toleranz: MIT arbeitet an mathematisch bewiesenem Dateisystem

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)

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.

Anzeige

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.

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.


eye home zur Startseite
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...



Anzeige

Stellenmarkt
  1. IKOR Management- und Systemberatung GmbH, deutschlandweit
  2. über Hanseatisches Personalkontor Mannheim, Mannheim
  3. Bundesdruckerei GmbH, Berlin
  4. Hornetsecurity GmbH, Hannover


Anzeige
Spiele-Angebote
  1. 28,99€
  2. 389,99€
  3. 35,00€ (nur für Prime-Mitglieder)

Folgen Sie uns
       


  1. Virb 360

    Garmins erste 360-Grad-Kamera nimmt 5,7K-Videos auf

  2. Digitalkamera

    Ricoh WG-50 soll Fotos bei extremen Bedingungen ermöglichen

  3. Wemo

    Belkin erweitert Smart-Home-System um Homekit-Bridge

  4. Digital Paper DPT-RP1

    Sonys neuer E-Paper-Notizblock wird 700 US-Dollar kosten

  5. USB Typ C Alternate Mode

    Thunderbolt-3-Docks von Belkin und Elgato ab Juni

  6. Sphero Lightning McQueen

    Erst macht es Brummbrumm, dann verdreht es die Augen

  7. VLC, Kodi, Popcorn Time

    Mediaplayer können über Untertitel gehackt werden

  8. Engine

    Unity bekommt 400 Millionen US-Dollar Investorengeld

  9. Neuauflage

    Neues Nokia 3310 soll bei Defekt komplett ersetzt werden

  10. Surface Studio

    Microsofts Grafikerstation kommt nach Deutschland



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
The Surge im Test: Frust und Feiern in der Zukunft
The Surge im Test
Frust und Feiern in der Zukunft
  1. Computerspiele und Psyche Wie Computerspieler zu Süchtigen erklärt werden sollen
  2. Wirtschaftssimulation Pizza Connection 3 wird gebacken
  3. Mobile-Games-Auslese Untote Rundfahrt und mobiles Seemannsgarn

Redmond Campus Building 87: Microsofts Area 51 für Hardware
Redmond Campus Building 87
Microsofts Area 51 für Hardware
  1. Windows on ARM Microsoft erklärt den kommenden x86-Emulator im Detail
  2. Azure Microsoft betreut MySQL und PostgreSQL in der Cloud
  3. Microsoft Azure bekommt eine beeindruckend beängstigende Video-API

3D-Druck bei der Bahn: Mal eben einen Kleiderhaken für 80 Euro drucken
3D-Druck bei der Bahn
Mal eben einen Kleiderhaken für 80 Euro drucken
  1. Bahnchef Richard Lutz Künftig "kein Ticket mehr für die Bahn" notwendig
  2. Flatrate Öffentliches Fahrradleihen kostet 50 Euro im Jahr
  3. Nextbike Berlins neues Fahrradverleihsystem startet

  1. Re: Tastatur für Entwickler / Programmierer...

    Teebecher | 07:37

  2. Re: Schwachsinn: 2x 4K-Monitore nur mit extra...

    msdong71 | 07:37

  3. Re: Was mich grundsätzlich bei WaKü stört...

    ChoMar | 07:22

  4. Re: 700$ - Ich hätte da eine bessere Lösung...

    forenuser | 07:11

  5. Re: Alternativen?

    herrwusel | 07:10


  1. 07:16

  2. 07:08

  3. 18:10

  4. 10:10

  5. 09:59

  6. 09:00

  7. 18:58

  8. 18:20


  1. Themen
  2. A
  3. B
  4. C
  5. D
  6. E
  7. F
  8. G
  9. H
  10. I
  11. J
  12. K
  13. L
  14. M
  15. N
  16. O
  17. P
  18. Q
  19. R
  20. S
  21. T
  22. U
  23. V
  24. W
  25. X
  26. Y
  27. Z
  28. #
 
    •  / 
    Zum Artikel