Abo
  • Services:
Anzeige

Automatischer Sicherheitsnachweis für Betriebssystemkern

Forscher entwickeln Methode, um Fehlerfreiheit nachzuweisen

Am australischen Forschungsinstitut Nicta haben Mitarbeiter ein Verfahren entwickelt, um die Sicherheit von Programmcode zu beweisen. Die Methode basiert auf mathematischen Berechnungen. Die Forscher haben ihre Methode am Mikrokernel "Secure Embedded L4" erprobt.

Mit ihrem Verfahren wollen die Forscher des Nicta die Sicherheit von Programmcode nachweisen. Die mathematischen Berechnungen sollen verschiedene Fehlerklassen wie Pufferüberläufe ausschließen können. Somit lasse sich beweisen, dass eine Anwendung für kritische Einsatzgebiete wie in Flugzeugen und Autos geeignet sei.

Anzeige

Ausgetestet wurde die Methode am Secure-Embedded-L4-Mikrokernel (seL4). Während frühere Tests nur einzelne Bereiche unter die Lupe nahmen, gelang so der Nachweis über die Korrektheit des kompletten, 7.500 Zeilen langen C-Codes. Die Prüfung erfolgt automatisiert mit einer Software. So soll der seL4 immun gegen gängige Angriffe sein. Pufferüberläufe beispielsweise seien nicht möglich. Mittels der mathematischen Berechnungen sollen sich auch Speicherlecks, Zeigerfehler und weitere Probleme wie arithmetische Überlaufe ausschließen lassen.

Die vom Nicta neu entwickelten Techniken sollen bald an die am Nicta entstandene Firma Open Kernel Labs weitergereicht werden. Die Open Kernel Labs wollen dann ein Produkt auf Basis der mathematischen Methoden entwickeln.

Eine wissenschaftliche Publikation über die Technik soll zum 22. ACM Symposium on Operating Systems Principles im Oktober vorgestellt werden.


eye home zur Startseite
Siga9876 20. Aug 2009

Wenn ich es nicht beweisen kann, darf ich es bei Banken usw. nicht einsetzen. Wäre mal...

Name 20. Aug 2009

Genau den Punkt meinte ich. Eine Zahl ist eine Zahl und der Algorithmus wird wohl nicht...

Name 20. Aug 2009

Wenn Du Pech hast, dann hast Du jetzt eine Patentklage am Hals;-)

Siga9876 20. Aug 2009

Vom Doppelposting bitte eines Löschen. polipo hängt schon mal :-( Danke und Sorry.

DerAkademiker 20. Aug 2009

LISA ist jetzt aber der Roboter an der Uni-Koblenz der im RoboCafe Cola, Fanta und Saft...



Anzeige

Stellenmarkt
  1. über Ratbacher GmbH, München
  2. Hubert Burda Media, Offenburg
  3. CERATIZIT Deutschland GmbH, Empfingen
  4. MCM Klosterfrau Vertriebsgesellschaft mbH, Köln


Anzeige
Blu-ray-Angebote
  1. 17,97€
  2. 12,99€
  3. (u. a. Apollo 13, Insidious, Horns, King Kong, E.T. The Untouchables, Der Sternwanderer)

Folgen Sie uns
       

Anzeige
Whitepaper
  1. Mehr dazu im aktuellen Whitepaper von IBM
  2. Sicherheitsrisiken bei der Dateifreigabe & -Synchronisation
  3. Kritische Bereiche der IT-Sicherheit in Unternehmen


  1. Hololens

    Microsoft holoportiert Leute aus dem Auto ins Büro

  2. Star Wars

    Todesstern kostet 6,25 Quadrilliarden britische Pfund am Tag

  3. NSA-Ausschuss

    Wikileaks könnte Bundestagsquelle enttarnt haben

  4. Transparenzverordnung

    Angaben-Wirrwarr statt einer ehrlichen Datenratenangabe

  5. Urteil zu Sofortüberweisung

    OLG empfiehlt Verbrauchern Einkauf im Ladengeschäft

  6. Hearthstone

    Blizzard schickt Spieler in die Straßen von Gadgetzan

  7. Jolla

    Sailfish OS in Russland als Referenzmodell für andere Länder

  8. Router-Schwachstellen

    100.000 Kunden in Großbritannien von Störungen betroffen

  9. Rule 41

    Das FBI darf jetzt weltweit hacken

  10. Breath of the Wild

    Spekulationen über spielbare Zelda



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Final Fantasy 15 im Test: Weltenrettung mit der Boyband des Wahnsinns
Final Fantasy 15 im Test
Weltenrettung mit der Boyband des Wahnsinns
  1. Square Enix Koop-Modus von Final Fantasy 15 folgt kostenpflichtig

Udacity: Selbstfahrendes Auto selbst programmieren
Udacity
Selbstfahrendes Auto selbst programmieren
  1. Strategiepapier EU fordert europaweite Standards für vernetzte Autos
  2. Autonomes Fahren Comma One veröffentlicht Baupläne für Geohot-Nachrüstsatz
  3. Autonomes Fahren Intel baut Prozessoren für Delphi und Mobileye

Quake (1996): Urknall für Mouselook, Mods und moderne 3D-Grafik
Quake (1996)
Urknall für Mouselook, Mods und moderne 3D-Grafik
  1. Künstliche Intelligenz Doom geht in Deckung

  1. Wie kann man so etwas berechnen ?

    Caturix | 19:01

  2. Re: Damit ist Wikileaks nun endgültig

    teenriot* | 18:58

  3. Re: dauert noch

    nille02 | 18:49

  4. Re: mich hat keiner gefragt

    Faksimile | 18:46

  5. Falsche Fährte?

    vergeben | 18:42


  1. 18:27

  2. 18:01

  3. 17:46

  4. 17:19

  5. 16:37

  6. 16:03

  7. 15:34

  8. 15:08


  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