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.

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.


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

Kommentieren



Anzeige

  1. Trainee (m/w) IT-Anwendungen
    Süwag Energie AG, Frankfurt am Main
  2. IT-Scrum Master Payment Solutions (m/w)
    Media-Saturn IT Services GmbH, Ingolstadt
  3. Technical Manager (m/w)
    Cambaum GmbH, Baden-Baden
  4. Projektmanager (m/w)
    T-Systems International GmbH, Berlin, Bonn, Darmstadt, München, Münster

Detailsuche



Anzeige

Folgen Sie uns
       


  1. Section Control

    Bremsen vor Blitzern soll nicht mehr vor Bußgeld schützen

  2. Beam

    ISS-Modul erfolgreich aufgeblasen

  3. Arbeitsbedingungen

    Apple-Store-Mitarbeiterin gewährt Blick hinter die Kulissen

  4. Modulares Smartphone

    Project-Ara-Ideengeber hat von Google mehr erwartet

  5. Telekom-Konzernchef

    "Vectoring schafft Wettbewerb"

  6. Model S

    Teslas Autopilot verursacht Auffahrunfall

  7. Security

    Microsoft will Passwort 'Passwort' verbieten

  8. Boston Dynamics

    Google will Roboterfirma an Toyota verkaufen

  9. Oracle-Anwältin nach Niederlage

    "Google hat die GPL getötet"

  10. Selbstvermessung

    Jawbone steigt offenbar aus Fitnesstracker-Geschäft aus



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Oracle vs. Google: Wie man Geschworene am besten verwirrt
Oracle vs. Google
Wie man Geschworene am besten verwirrt
  1. Java-Rechtsstreit Oracle verliert gegen Google
  2. Oracle vs. Google Wie viel Fair Use steckt in 11.000 Codezeilen?

GPD XD im Test: Zwischen Nintendo 3DS und PS Vita ist noch Platz
GPD XD im Test
Zwischen Nintendo 3DS und PS Vita ist noch Platz
  1. Xbox Scorpio Schneller als Playstation Neo und mit Rift-Unterstützung
  2. Playstation 4 Rennstart für Gran Turismo Sport im November 2016
  3. AMD Drei Konsolen-Chips für 2017 angekündigt

Intels Compute Stick im Test: Der mit dem Lüfter streamt (2)
Intels Compute Stick im Test
Der mit dem Lüfter streamt (2)
  1. Stratix 10 MX Alteras Chips nutzen HBM2 und Intels Interposer-Technik
  2. Apple Store Apple darf keine Geschäfte in Indien eröffnen
  3. HBM2 eSilicon zeigt 14LPP-Design mit High Bandwidth Memory

  1. Re: lowcarb funktioniert auch .. (ganz ohne Sport)

    pk_erchner | 15:21

  2. Re: wer kauft denn heute noch im laden?

    Maatze | 15:21

  3. Re: Das gibts doch schon ewig?

    ad (Golem.de) | 15:20

  4. Re: Stimme Hackens 98,7% zu!

    deus-ex | 15:19

  5. Re: 80 GB pro Film, netter Kopierschutz :-)

    lemmer | 15:18


  1. 12:45

  2. 12:12

  3. 11:19

  4. 09:44

  5. 14:15

  6. 13:47

  7. 13:00

  8. 12:30


  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