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. Statistisches Bundesamt, Wiesbaden
  2. KeyIdentity GmbH, Weiterstadt

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
Hardware-Angebote
  1. 120,84€ + Versand
  2. 106,34€ + 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
       


Golem.de lässt Alexa schlecht lachen und rappen

Alexa kann komisch lachen und schlecht rappen - wie man im Video hört.

Golem.de lässt Alexa schlecht lachen und rappen Video aufrufen
Grenzenloser Datenzugriff: Was der Cloud-Act für EU-Bürger bedeutet
Grenzenloser Datenzugriff
Was der Cloud-Act für EU-Bürger bedeutet

Neue Gesetze in den USA und der EU könnten den Weg für einen ungehinderten und schnellen weltweiten Datenzugriff von Ermittlungsbehörden ebnen. Datenschützer und IT-Wirtschaft sehen die Pläne jedoch sehr kritisch.
Ein Bericht von Friedhelm Greis

  1. Elektronische Beweise EU-Kommission fordert weltweiten Zugriff auf Daten
  2. Panera Bread Café-Kette exponiert Millionen Kundendaten im Netz
  3. Soziale Netzwerke Datenschlampereien mit HIV-Status und Videodateien

Ancestors Legacy angespielt: Mittelalter für Echtzeit-Strategen
Ancestors Legacy angespielt
Mittelalter für Echtzeit-Strategen

Historisch mehr oder weniger akkurate Spiele sind angesagt, nach Assassin's Creed Origins und Kingdom Come Deliverance will nun auch Ancestors Legacy mit Geschichte punkten. Golem.de hat eine Beta des im Mittelalter angesiedelten Strategiespiels ausprobiert.

  1. Into the Breach im Test Strategiespaß im Quadrat

Klimaschutz: Unter der Erde ist das Kohlendioxid gut aufgehoben
Klimaschutz
Unter der Erde ist das Kohlendioxid gut aufgehoben

Die Kohlendioxid-Emissionen steigen und steigen. Die auf der UN-Klimakonferenz in Paris vereinbarten Ziele sind so kaum zu schaffen. Fachleute fordern daher den Einsatz von Techniken, die Kohlendioxid in Kraftwerken abscheiden oder sogar aus der Luft filtern.
Ein Bericht von Daniel Hautmann

  1. Xiaoice und Zo Microsoft erforscht menschlicher wirkende Sprachchat-KIs
  2. Hyperschallgeschwindigkeit Projektil schießt sich durch den Boden
  3. Materialforschung Stanen - ein neues Wundermaterial?

    •  /