Abo
  • IT-Karriere:

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. Enertrag Aktiengesellschaft, Dauerthal, Berlin
  2. Wirecard Technologies GmbH, Aschheim near Munich

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. 279,90€
  2. 229€ (Bestpreis!)
  3. (u. a. beide Spiele zu Ryzen 9 3000 oder 7 3800X Series, eines davon zu Ryzen 7 3700X/5 3600X/7...

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
       


55-Zoll-OLED-Monitor von Alienware - Test

Mit 120 Hz, 4K-Auflösung und 55-Zoll-Panel ist der AW5520qf ein riesiger Gaming-Monitor. Darauf macht es besonders Spaß, Monster in Borderlands 3 zu besiegen. Wäre da nicht die ziemlich niedrige Ausleuchtung.

55-Zoll-OLED-Monitor von Alienware - Test Video aufrufen
WLAN-Kameras ausgeknipst: Wer hat die Winkekatze geklaut?
WLAN-Kameras ausgeknipst
Wer hat die Winkekatze geklaut?

Weg ist die Winkekatze - und keine unserer vier Überwachungskameras hat den Dieb gesehen. Denn WLAN-Cams von Abus, Nest, Yi Technology und Arlo lassen sich ganz einfach ausschalten.
Von Moritz Tremmel

  1. Wi-Fi 6 Router und Clients für den neuen WLAN-Standard
  2. Wi-Fi 6 und 802.11ax Was bringt der neue WLAN-Standard?
  3. Brandenburg Vodafone errichtet 1.200 kostenlose WLAN-Hotspots

SSD-Kompendium: AHCI, M.2, NVMe, PCIe, Sata, U.2 - ein Überblick
SSD-Kompendium
AHCI, M.2, NVMe, PCIe, Sata, U.2 - ein Überblick

Heutige SSDs gibt es in allerhand Formfaktoren mit diversen Anbindungen und Protokollen, selbst der verwendete Speicher ist längst nicht mehr zwingend NAND-Flash. Wir erläutern die Unterschiede und Gemeinsamkeiten der Solid State Drives.
Von Marc Sauter

  1. PM1733 Samsungs PCIe-Gen4-SSD macht die 8 GByte/s voll
  2. PS5018-E18 Phisons PCIe-Gen4-SSD-Controller liefert 7 GByte/s
  3. Ultrastar SN640 Western Digital bringt SSD mit 31 TByte im E1.L-Ruler-Format

Banken: Die Finanzbranche braucht eine neue Strategie für ihre IT
Banken
Die Finanzbranche braucht eine neue Strategie für ihre IT

Ob Deutsche Bank, Commerzbank oder DKB: Immer wieder wackeln Server und Anwendungen bei großen Finanzinstituten. Viele Kernbanksysteme sind zu alt für aktuelle Anforderungen. Die Branche sucht nach Auswegen.
Eine Analyse von Manuel Heckel

  1. Bafin Kunden beklagen mehr Störungen beim Online-Banking
  2. PSD2 Giropay soll bald nahezu allen Kunden zur Verfügung stehen
  3. Klarna Der Schrecken der traditionellen Banken

    •  /