Abo
  • Services:

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.

Artikel veröffentlicht am , Julius Stiebert

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.

Stellenmarkt
  1. Tecmata GmbH, Mannheim
  2. 10X Innovation GmbH & Co. KG, Berlin

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.



Anzeige
Top-Angebote
  1. 43,99€ (Bestpreis!)
  2. (u. a. DOOM für 6,99€ und Civilization VI - Digital Deluxe Edition für 25,99€)
  3. (heute OK. OPK 1000 Partybox mit LED-Show für 99€)
  4. (heute u. a. AZZA Chroma 410A für 69,90€ + Versand)

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


Folgen Sie uns
       


BMW stellt seinen Formel-E-Rennwagen vor - Bericht

BMW setzt auf elektrischen Motorsport: Die Münchener treten als zweiter deutscher Autohersteller in der Rennserie Formel E an. BMW hat in München das Fahrzeug für die Saison 2018/19 vorgestellt.

BMW stellt seinen Formel-E-Rennwagen vor - Bericht Video aufrufen
Gigabit: 5G-Planungen gehen völlig an den Nutzern vorbei
Gigabit
5G-Planungen gehen völlig an den Nutzern vorbei

Fast täglich hören wir Erklärungen aus der Telekommunikationsbranche, was 5G erfüllen müsse und warum sonst das Ende der Welt drohe. Wir haben die Konzerngruppen nach Interessenlage kartografiert.
Ein IMHO von Achim Sawall

  1. Fixed Wireless Access Nokia bringt mehrere 100 MBit/s mit LTE ins Festnetz
  2. Funklöcher Telekom bietet freiwillig hohe 5G-Netzabdeckung an
  3. 5G Telekom hat ihr Mobilfunknetz mit Glasfaser versorgt

Apple Watch im Test: Auch ohne EKG die beste Smartwatch
Apple Watch im Test
Auch ohne EKG die beste Smartwatch

Apples vierte Watch verändert das Display-Design leicht - zum Wohle des Nutzers. Die Uhr bietet immer noch mit die beste Smartwatch-Erfahrung, auch wenn eine der neuen Funktionen in Deutschland noch nicht funktioniert.
Ein Test von Tobias Költzsch

  1. Skydio R1 Apple Watch zur Drohnensteuerung verwendet
  2. Smartwatch Apple Watch Series 4 mit EKG und Sturzerkennung
  3. Smartwatch Apple Watch Series 4 nur mit sechs Modellen

Shine 3: Neuer Tolino-Reader bringt mehr Lesekomfort
Shine 3
Neuer Tolino-Reader bringt mehr Lesekomfort

Die Tolino-Allianz bringt das Nachfolgemodell des Shine 2 HD auf den Markt. Das Shine 3 erhält mehr Ausstattungsdetails aus der E-Book-Reader-Oberklasse. Vor allem beim Lesen macht sich das positiv bemerkbar.
Ein Hands on von Ingo Pakalski

  1. E-Book-Reader Update macht Tolino-Geräte unbrauchbar

    •  /