Abo
  • Services:
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.

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.

Anzeige

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



Anzeige

Stellenmarkt
  1. Fraunhofer-Institut für Solare Energiesysteme ISE, Freiburg
  2. über Robert Half Technology, Hamburg
  3. congatec AG, Deggendorf
  4. Schaeffler Technologies AG & Co. KG, Herzogenaurach


Anzeige
Hardware-Angebote
  1. (u. a. Asus GTX 1070 Strix OC, MSI GTX 1070 Gaming X 8G und Aero 8G OC)
  2. 49,90€

Folgen Sie uns
       

Anzeige
Whitepaper
  1. Sicherheitskonzeption für das App-getriebene Geschäft
  2. Mehr dazu im aktuellen Whitepaper von IBM
  3. Mit digitalen Workflows Geschäftsprozesse agiler machen


  1. Videocodec

    Für Netflix ist H.265 besser als VP9

  2. Weltraumforschung

    DFKI-Roboter soll auf dem Jupitermond Europa abtauchen

  3. World of Warcraft

    Sechste Erweiterung Legion ist online

  4. Ripper

    Geldautomaten-Malware gibt bis zu 40 Scheine aus

  5. Europäische Union

    Irlands Steuervorteile für Apple sollen unzulässig sein

  6. Linux-Paketmanager

    RPM-Entwicklung verläuft chaotisch

  7. Neuseeland

    Kim Dotcom überträgt Gerichtsverhandlung im Netz

  8. Leitlinien vereinbart

    Regulierer schwächen Vorgaben zu Netzneutralität ab

  9. Kartendienst

    Microsoft und Amazon könnten sich an Here beteiligen

  10. Draufsicht

    Neuer 5er BMW mit Überwachungskameras



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Lernroboter-Test: Besser Technik lernen mit drei Freunden
Lernroboter-Test
Besser Technik lernen mit drei Freunden
  1. Kinderroboter Myon Einauge lernt, Einauge hat Körper
  2. Landwirtschaft 4.0 Swagbot hütet das Vieh
  3. Künstliche Muskeln Skelettroboter klappert mit den Zähnen

Mobilfunk: Eine Woche in Deutschland im Funkloch
Mobilfunk
Eine Woche in Deutschland im Funkloch
  1. Netzwerk Mehrere regionale Mobilfunkausfälle bei Vodafone
  2. Hutchison 3 Google-Mobilfunk Project Fi soll zwanzigmal schneller werden
  3. RWTH Ericsson startet 5G-Machbarkeitsnetz in Aachen

No Man's Sky im Test: Interstellare Emotionen durch schwarze Löcher
No Man's Sky im Test
Interstellare Emotionen durch schwarze Löcher
  1. No Man's Sky für PC Läuft nicht, stottert, nervt
  2. No Man's Sky Onlinedienste wegen Überlastung offline
  3. Hello Games No Man's Sky bekommt Raumstationsbau

  1. Re: Halbe Milliarde

    My1 | 12:43

  2. Re: Speicherung der Daten u. gerichtliche...

    Peter Brülls | 12:42

  3. Europäische Union einmischen

    A. T. R. | 12:41

  4. Dark Zero

    cyablo | 12:40

  5. Re: Druckverhältnisse in 100 km Tiefe?

    Vollstrecker | 12:40


  1. 12:31

  2. 12:07

  3. 11:51

  4. 11:25

  5. 10:45

  6. 10:00

  7. 09:32

  8. 09:00


  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