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.

Anzeige

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.

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.


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...

Kommentieren



Anzeige

  1. IT-Service Mitarbeiter (m/w) für den Anwender-Support
    DATAGROUP Köln GmbH, München
  2. Gruppenleitung (m/w) SCADA Wind Power
    Siemens AG, Hamburg
  3. Teamleiter SAP BI/BO (m/w)
    SCHOTT AG, Mainz
  4. IT-Anwendungs­betreuer / -Anwendungs­entwickler (m/w) HR-Informationssysteme
    DR. JOHANNES HEIDENHAIN GmbH, Traunreut

 

Detailsuche


Hardware-Angebote
  1. TIPP: Asus-Cashback-Aktion
    bis zu 45€ Cashback beim Kauf einer Aktions-Grafikkarte
  2. TIPP: Zotac ZT-90101-10P NVIDIA GeForce GTX970 Grafikkarte
    319,04€
  3. TIPP: Alternate Schnäppchen Outlet
    (täglich neue Deals)

 

Weitere Angebote


Folgen Sie uns
       


  1. Sprite

    Fliegende Thermoskanne als Kameradrohne

  2. Android

    Schlüssel werden auf zurückgesetzten Smartphones nicht gelöscht

  3. Aria

    Gerät ermöglicht Smartwatch-Steuerung per Fingerschnippen

  4. Funktechnik

    Daimler und Qualcomm vernetzen das Auto

  5. Projekt Astoria

    Algorithmen gegen Schnüffler im Tor-Netzwerk

  6. Raumfahrt

    Marsrover Curiosity sieht wieder scharf

  7. Server-Prozessor

    Intels Skylake-EX bietet 28 Kerne und sechs Speicherkanäle

  8. Berlin E-Prix

    Motoren, die nach Star Wars klingen

  9. Licht

    Indoor-Navigationssystem führt zu Sonderangeboten im Supermarkt

  10. Handmade

    Amazon bereitet Marktplatz für Handgefertigtes vor



Haben wir etwas übersehen?

E-Mail an news@golem.de



Angriff auf kritische Infrastrukturen: Bundestag, bitte melden!
Angriff auf kritische Infrastrukturen
Bundestag, bitte melden!
  1. Umfrage US-Bürger misstrauen Regierung beim Umgang mit Daten
  2. Spionage NSA wollte Android-App-Stores für Ausspähungen nutzen
  3. Cyberangriff im Bundestag Ausländischer Geheimdienst soll Angriff gestartet haben

BND-Selektorenaffäre: Die stille Löschaktion des W. O.
BND-Selektorenaffäre
Die stille Löschaktion des W. O.
  1. BND-Chef Schindler "Wir sind abhängig von der NSA"
  2. BND-Metadatensuche "Die Nadel im Heuhaufen ist zerbrochen"
  3. Geheimhaltung IT-Experten wollen die NSA austricksen

The Witcher 3 im Grafiktest: Mehr Bonbon am PC
The Witcher 3 im Grafiktest
Mehr Bonbon am PC
  1. Sabotagevorwurf Witcher-3-Streit zwischen AMD und Nvidia
  2. The Witcher 3 im Test Wunderschönes Wohlfühlabenteuer
  3. The Witcher 3 30 weitere Stunden mit Geralt von Riva

  1. Re: Erklärungsanfrage an Golem.de

    lemete | 07:32

  2. Re: alles halb so wild

    elgooG | 07:29

  3. Dieses Jahr noch zu langweilig

    mz_001 | 07:16

  4. Re: Normaler Skylake-Xeon E3?

    HubertHans | 07:13

  5. Re: auch bei alterenativen distros und custom...

    exxo | 07:08


  1. 07:13

  2. 17:47

  3. 13:40

  4. 12:15

  5. 11:28

  6. 11:11

  7. 10:25

  8. 21:43


  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