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. Softwareentwickler/in innovative Fahrerassistenzsysteme
    Robert Bosch GmbH, Leonberg
  2. Teamleiter Applicationmanagement (m/w)
    IT for Intellectual Property Management GmbH, Berlin
  3. Mitarbeiter PMO und IT Change Management (m/w)
    Commerz Finanz GmbH, München
  4. System Engineer/IT-Ingenieur (m/w)
    Forschungszentrum Jülich GmbH, Jülich

 

Detailsuche


Spiele-Angebote
  1. NEU: Assassin's Creed 3 Download
    5,97€
  2. NEU: Diablo III: Reaper of Souls (Add-on)
    19,97€
  3. TIPP: Xbox One Wired Controller für Windows
    43,99€

 

Weitere Angebote


Folgen Sie uns
       


  1. Smartwatch

    Android Wear soll bald mit iOS sprechen

  2. HTC Re Vive ausprobiert

    Räumt schon mal die Keller leer

  3. Big Maxwell

    Nvidias Geforce GTX Titan X bietet 12 GByte Videospeicher

  4. EU-Datenschutzreform

    Verbraucherschützer warnen vor "Ausverkauf" der Nutzerrechte

  5. DSL/Mobilfunk

    O2 hält Watchever-Nutzung trotz Drosselung für möglich

  6. Anhörung im Bundestag

    Leistungsschutzrecht findet Unterstützer

  7. Branchenbuch

    Was Google und Bing nicht anzeigen, ist wertlos

  8. Globales Transportnetz

    China will längsten Tunnel am Meeresgrund bauen

  9. Google

    Chrome-Support für Android 4.0 wird eingestellt

  10. Valve

    Kostenlose Source-2-Engine bietet Vulkan-Unterstützung



Haben wir etwas übersehen?

E-Mail an news@golem.de



JAP-Netzwerk: Anonymes Surfen für Geduldige
JAP-Netzwerk
Anonymes Surfen für Geduldige
  1. Android 5 Google verzichtet (noch) auf Verschlüsselungszwang
  2. Geheimdienstchef Clapper Cyber-Armageddeon ist nicht zu befürchten
  3. Zertifizierungspflicht Die Übergangsfrist für ISO 27000 läuft ab

MIPS Creator CI20 angetestet: Die Platine zum Pausemachen
MIPS Creator CI20 angetestet
Die Platine zum Pausemachen
  1. Raspberry Pi 2 Fotografieren nur ohne Blitz
  2. Raspberry Pi 2 ausprobiert Schnell rechnen, langsam speichern
  3. Internet der Dinge Windows 10 läuft kostenlos auf dem Raspberry Pi 2

Screamride im Test: Achterbahn mit Zerstörungsdrang
Screamride im Test
Achterbahn mit Zerstörungsdrang
  1. Test The Book of Unwritten Tales 2 Fantasywelt in rosa Plüschgefahr
  2. Test Grow Home Herzallerliebster Roboter
  3. Test Radiation Island Fantastische Spielwelt auf dem Smartphone

  1. Re: Sicher werden Smarties für mich erst sein...

    Tzven | 02:53

  2. Re: Respekt..

    teenriot* | 02:43

  3. Re: fokus auf user generated content

    SelfEsteem | 02:42

  4. Re: Eher aus Prinzip

    Tzven | 02:37

  5. Re: 12 oder 11,5? (kwT)

    Sarkastius | 02:35


  1. 22:28

  2. 21:33

  3. 21:22

  4. 19:04

  5. 18:51

  6. 17:08

  7. 16:52

  8. 16:14


  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