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. Generaldirektion der Staatlichen Archive Bayerns, München
  2. CTS EVENTIM Solutions GmbH, Bremen

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. mit Gutschein: HARDWARE50 (nur für Neukunden, Warenwert 104 - 1.000 Euro)

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
       


Ubitricity ausprobiert

Das Berliner Unternehmen Ubitricity hat ein eichrechtskonformes System für das Laden von Elektroautos entwickelt. Das Konzept basiert darauf, dass nicht die Säule, sondern der Kunde selbst für die Stromzählung sorgt.

Ubitricity ausprobiert Video aufrufen
Hasskommentare: Wie würde es im Netz aussehen, wenn es uns nicht gäbe?
Hasskommentare
"Wie würde es im Netz aussehen, wenn es uns nicht gäbe?"

Hannes Ley hat vor rund anderthalb Jahren die Online-Initiative #ichbinhier gegründet. Die Facebook-Gruppe schreibt Erwiderungen auf Hasskommentare und hat mittlerweile knapp 40.000 Mitglieder. Im Interview mit Golem.de erklärt Ley, wie er die Idee aus dem Netz in die echte Welt bringen will.
Ein Interview von Jennifer Fraczek

  1. Satelliteninternet Fraunhofer erreicht hohe Datenrate mit Beam Hopping
  2. Nutzungsrechte Einbetten von Fotos muss nicht verhindert werden
  3. Bundesnetzagentur UKW-Abschaltung abgewendet

KI in der Medizin: Keine Angst vor Dr. Future
KI in der Medizin
Keine Angst vor Dr. Future

Mit Hilfe künstlicher Intelligenz können schwer erkennbare Krankheiten früher diagnostiziert und behandelt werden, doch bei Patienten löst die Technik oft Unbehagen aus. Und das ist nicht das einzige Problem.
Ein Bericht von Tim Kröplin

  1. Künstliche Intelligenz Vages wagen
  2. KI Mit Machine Learning neue chemische Reaktionen herausfinden
  3. Elon Musk und Deepmind-Gründer Keine Maschine soll über menschliches Leben entscheiden

Smartphone von Gigaset: Made in Bocholt
Smartphone von Gigaset
Made in Bocholt

Gigaset baut sein Smartphone GS185 in Bocholt - und verpasst dem Gerät trotz kompletter Anlieferung von Teilen aus China das Label "Made in Germany". Der Fokus auf die Region ist aber vorhanden, eine erweiterte Fertigung durchaus eine Option. Wir haben uns das Werk angeschaut.
Ein Bericht von Tobias Költzsch

  1. Bocholt Gigaset baut Smartphone in Deutschland

    •  /