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. Quality Assurance & Security Manager (m/w)
    FRITZ & MACZIOL group, deutschlandweit
  2. IT-Sicherheitsbeauftragter (m/w)
    MAX-DELBRÜCK-CENTRUM FÜR MOLEKULARE MEDIZIN, Berlin
  3. Datenanalyst im Gesundheitswesen (m/w)
    Arbeitsgemeinschaft Wirtschaftlichkeitsprüfung Berlin GbR, Berlin
  4. Prozessexperte SAP-Logistik (m/w)
    Max Bögl Bauservice GmbH & Co. KG, Neumarkt (Metropolregion Nürnberg)

Detailsuche


Hardware-Angebote
  1. Sapphire Radeon R9 Fury Tri-X
    ab 546,75€
  2. Sandisk 16-GB-USB-3.0-Stick
    8,94€
  3. DANK IOS-APP ANDROID WEAR JETZT AUCH IPHONE-KOMPATIBEL: LG Watch Urbane Smartwatch
    269,74€

Weitere Angebote


Folgen Sie uns
       


  1. Me Pro im Hands on

    Gigasets Einstieg in den Smartphone-Markt

  2. iOS

    Jailbreak-Malware greift 225.000 Nutzerdaten ab

  3. Wettbewerbszentrale

    Abmahnung für Zalando wegen vorgetäuschter Knappheit

  4. Nextbit Robin angeschaut

    Das Smartphone mit der intelligenten Cloud

  5. Netzneutralität

    Bund will Spezialdienste für autonome Autos - egal wozu

  6. Streaming

    Amazon-Prime-Inhalte jetzt für alle herunterladbar

  7. Epic Games

    Unreal Engine 4.9 mit mehr Grafikeffekten auf Mobilegeräten

  8. Hypervisor

    OpenBSD bekommt native Virtualisierung

  9. Streamingbox

    Amazon bereitet wohl neues Fire TV vor

  10. Elliptische Umlaufbahn

    Galileo-Satelliten werden für die Forschung eingesetzt



Haben wir etwas übersehen?

E-Mail an news@golem.de



Game Writer: Warum Quereinsteiger selten gute Storys für Spiele schreiben
Game Writer
Warum Quereinsteiger selten gute Storys für Spiele schreiben
  1. This War of Mine Krieg mit The Little Ones auf Konsole
  2. Swapster Deutsche Börse plant Handelsplattform für Spieler
  3. Ninja Theory Hellblade und eine Heldin mit Trauma

20 Jahre im Einsatz: Lebenserhaltende Maßnahmen bei Windows 95
20 Jahre im Einsatz
Lebenserhaltende Maßnahmen bei Windows 95
  1. Windows-Insider-Programm Chrome hat Probleme mit Windows 10 Build 10525
  2. Internet Explorer Notfall-Patch für Microsofts Browser
  3. Microsoft Erster Insider-Build seit dem Erscheinen von Windows 10

Helium-3: Kommt der Energieträger der Zukunft vom Mond?
Helium-3
Kommt der Energieträger der Zukunft vom Mond?
  1. Stratolaunch Carrier Größtes Flugzeug der Welt soll 2016 erstmals starten
  2. Escape Dynamics Mikrowellen sollen Raumgleiter von der Erde aus antreiben
  3. Raumfahrt Transformer sollen den Mond beleuchten

  1. Re: Toll o2 netz

    Clarissa1986 | 20:05

  2. Warum noch Smartphones mit dem Snapdragon 810?

    kvoram | 20:03

  3. Re: omg...

    Clarissa1986 | 19:59

  4. Re: Selbst SSD einbauen?

    Legacyleader | 19:58

  5. Re: Es könnte auch sein, ...

    Astorek | 19:56


  1. 18:29

  2. 17:52

  3. 17:08

  4. 16:00

  5. 15:57

  6. 15:40

  7. 15:25

  8. 13:28


  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