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. STAHLGRUBER GmbH, Poing bei München
  2. NOWIS GmbH, Oldenburg
  3. Siemens Postal, Parcel & Airport Logistics GmbH, Düsseldorf
  4. Robert Bosch Start-up GmbH, Renningen


Anzeige
Hardware-Angebote
  1. 2099,99€ statt 2399,99€ bei razerzone.com
  2. und Destiny 2 gratis erhalten
  3. täglich neue Deals

Folgen Sie uns
       


  1. Smartphones

    Huawei installiert ungefragt Zusatz-App

  2. Android 8.0

    Oreo-Update für Oneplus Three und 3T ist da

  3. Musikstreaming

    Amazon Music für Android unterstützt Google Cast

  4. Staingate

    Austauschprogramm für fleckige Macbooks wird verlängert

  5. Digitale Infrastruktur

    Ralph Dommermuth kritisiert deutsche Netzpolitik

  6. Elektroauto

    VW will weitere Milliarden in Elektromobilität investieren

  7. Elektroauto

    Walmart will den Tesla-Truck

  8. Die Woche im Video

    Ausgefuchst, abgezockt und abgefahren

  9. Siri-Lautsprecher

    Apple versemmelt den Homepod-Start

  10. Open Routing

    Facebook gibt interne Plattform für Backbone-Routing frei



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Smartphoneversicherungen im Überblick: Teuer und meistens überflüssig
Smartphoneversicherungen im Überblick
Teuer und meistens überflüssig
  1. Winphone 5.0 Trekstor will es nochmal mit Windows 10 Mobile versuchen
  2. Librem 5 Das freie Linux-Smartphone ist finanziert
  3. Aquaris-V- und U2-Reihe BQ stellt neue Smartphones ab 180 Euro vor

Erneuerbare Energien: Siemens leitet die neue Steinzeit ein
Erneuerbare Energien
Siemens leitet die neue Steinzeit ein
  1. Siemens und Schunk Akkufahrzeuge werden mit 600 bis 1.000 Kilowatt aufgeladen
  2. Parkplatz-Erkennung Bosch und Siemens scheitern mit Pilotprojekten

Cubesats: Startup steuert riesigen Satellitenschwarm von Berlin aus
Cubesats
Startup steuert riesigen Satellitenschwarm von Berlin aus
  1. Arkyd-6 Planetary Resources startet bald ein neues Weltraumteleskop
  2. SAEx Internet-Seekabel für Südatlantikinsel St. Helena
  3. Sputnik Piep, piep, kleiner Satellit

  1. Re: Usenet-Links? Wasdas?

    Apfelbrot | 18:47

  2. Re: Wieder mal Anwalt Solmecke...

    Apfelbrot | 18:46

  3. Re: Minus iOS

    derdiedas | 18:43

  4. Re: Frontantrieb...

    oliver.n.herzog | 18:38

  5. Re: "Qualität" ... aus einer Blechdose

    Dietbert | 18:36


  1. 11:55

  2. 11:21

  3. 10:43

  4. 17:14

  5. 13:36

  6. 12:22

  7. 10:48

  8. 09:02


  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