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. IT-Security Architect (m/w/d)
    MITTELDEUTSCHER RUNDFUNK Anstalt des öffentlichen Rechts, Leipzig
  2. SAP Logistik-Berater (m/w/x) mit Fokus auf SD
    über duerenhoff GmbH, Raum Darmstadt
Detailsuche

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.

Bitte aktivieren Sie Javascript.
Oder nutzen Sie das Golem-pur-Angebot
und lesen Golem.de
  • ohne Werbung
  • mit ausgeschaltetem Javascript
  • mit RSS-Volltext-Feed


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.



Aktuell auf der Startseite von Golem.de
Openweather
Eine Wetter-Uhr auf dem Raspberry Pi

Wir zeigen auf einem 64-x-64-LED-Panel mithilfe eines Raspberry Pi außer der Uhrzeit auch Wetterinformationen an. Die Programmierung erfolgt in C#.
Eine Anleitung von Michael Bröde

Openweather: Eine Wetter-Uhr auf dem Raspberry Pi
Artikel
  1. Toyota, CATL etc.: China schließt Fabriken wegen Hitzewelle
    Toyota, CATL etc.
    China schließt Fabriken wegen Hitzewelle

    Unter anderem Chinas größter Batteriehersteller muss seine Fabriken in Sichuan für eine Woche schließen - Grund ist eine Hitzewelle.

  2. Hybride Arbeit: Das Schlechteste aus zwei Welten?
    Hybride Arbeit
    Das Schlechteste aus zwei Welten?

    Frust plus Probleme statt Arbeiten im Grünen plus Kollegenkontakt: Hybrides Arbeiten misslingt oft - muss es aber nicht.
    Ein Ratgebertext von Jakob Rufus Klimkait und Kristin Ottlinger

  3. J.R.R. Tolkien: The Embracer Group kauft Der Herr der Ringe
    J.R.R. Tolkien
    The Embracer Group kauft Der Herr der Ringe

    Bis auf die Buchrechte gehört Der Herr der Ringe künftig zu The Embracer Group. Nebenbei kauft der Publisher mal wieder ein paar Spielestudios.

Du willst dich mit Golem.de beruflich verändern oder weiterbilden?
Zum Stellenmarkt
Zur Akademie
Zum Coaching
  • Schnäppchen, Rabatte und Top-Angebote
    Die besten Deals des Tages
    Daily Deals • 10%-Gaming-Gutschein bei eBay • Grafikkarten zu Tiefpreisen (Palit RTX 3090 Ti 1.391,98€, Zotac RTX 3090 1.298,99€, MSI RTX 3080 Ti 1.059€) • PS5 bei Amazon • HP HyperX Gaming-Maus 29€ statt 99€ • MindStar (ASRock RX 6900XT 869€) • Bester 2.000€-Gaming-PC [Werbung]
    •  /