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. Software Entwickler (m/w)
    M-net Telekommunikations GmbH, München
  2. SAP Specialist (m/w)
    SoftwareONE Deutschland GmbH, Heilbronn
  3. IT-MA System Administrator / Support (m/w)
    BWT Pharma & Biotech GmbH, Bietigheim-Bissingen
  4. Java / JEE Softwareentwickler (m/w)
    Commerz Finanz GmbH, München

 

Detailsuche


Spiele-Angebote
  1. The Witcher 3: Wild Hunt
    44,99€ USK 18
  2. PS4-Spiele reduziert
    (u. a. Lego der Hobbit 26,72€, The Crew 29,19€, Assassins Creed Unity 29,19€, The Wolf Among...
  3. Games-Downloads Angebote
    (u. a. Bioshock Infinite 7,49€, Xcom Enemy Unknown 4,99€, Boderlands 2 7,49€)

 

Weitere Angebote


Folgen Sie uns
       


  1. Apple Music

    iCloud verpasst der eigenen Musik einen Kopierschutz

  2. Ex-Minister Pofalla

    NSA-Affäre war doch nicht beendet

  3. Grüne

    Rechtsanspruch auf Breitband soll 12 Milliarden Euro kosten

  4. Überwachung

    BND-Akten zeigen die Sorglosigkeit deutscher Diplomaten

  5. Management

    Intel-Präsidentin tritt zurück und Mobile-Chef muss gehen

  6. Digital

    Paypal-Käuferschutz auch für Downloads

  7. UI-Framework

    Qt 5.5 vereinfacht 3D-Darstellungen

  8. Security

    Viele VPN-Dienste sind unsicher

  9. Anna's Quest im Test

    Mit Telekinese gegen die böse Hexe

  10. Österreich

    Provider müssen illegale Filmportale sperren



Haben wir etwas übersehen?

E-Mail an news@golem.de



PGP: Hochsicher, kaum genutzt, völlig veraltet
PGP
Hochsicher, kaum genutzt, völlig veraltet
  1. OpenPGP Facebook verschlüsselt E-Mails
  2. Geheimhaltung IT-Experten wollen die NSA austricksen
  3. Security Wie Google Android sicher macht

Urheberrecht: Die Panoramafreiheit ist bedroht
Urheberrecht
Die Panoramafreiheit ist bedroht
  1. EU-Urheberrecht Wikipedia fürchtet Abschaffung der Panoramafreiheit
  2. Experten Filesharing-Urteil des Bundesgerichtshofs für Musikindustrie
  3. Privatkopie Österreich will Downloads von illegalen Quellen verbieten

Unity: "Inzwischen entstehen viele tolle Spiele ohne Programmierer"
Unity
"Inzwischen entstehen viele tolle Spiele ohne Programmierer"
  1. Unity Technologies 56.289 Engine-Tests in einer Nacht
  2. Engine Unity 5.1 mit neuer Rendering-Pipeline für Virtual Reality
  3. Microsoft Hololens setzt auf die Unity-Engine

  1. Was ein Scheiß...

    Clarissa1986 | 01:07

  2. Re: Qt in eigene Projekte einbinden? Idealerweise...

    Abenglut | 01:04

  3. Was interessiert mich mein Geschwätz von gestern ...

    luarix | 01:01

  4. Re: Rechtsanspruch auf Breitband - Rundfunkgebühr...

    DrWatson | 00:58

  5. Re: Zockende Banken und ein desolates...

    DrWatson | 00:53


  1. 00:09

  2. 23:14

  3. 18:34

  4. 17:58

  5. 16:50

  6. 15:30

  7. 15:24

  8. 15:18


  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