am 23. August 2009 um 16:23
Sicherheits-Beweis für Betriebssystem-Kernel
Forscher melden mathematischen Nachweis für fehlerfreien Code
Forscher am australischen IKT-Forschungsinstitut
NICTA haben nach eigenen Angaben den weltweit ersten formellen maschinell geprüften Beweis dafür geliefert, dass ein Betriebssystem-Kernel frei von vielen gängigen Fehlern ist. Dabei wurden 7.500 Zeilen C-Quellcode geprüft. Der so verifizierte Mikrokernel "Secure Embedded L4" (seL4) könnte den Wissenschaftlern zufolge in diversen sicherheitskritischen Embedded-Anwendungen zum Einsatz kommen. "Die Prüfung bietet einen schlüssigen Nachweis, dass fehlerfreie Software möglich ist. Weniger als das sollte in Zukunft in kritischen Bereichen nicht akzeptabel sein", meint Gernot Heiser,
CTO bei Open Kernel (OK) Labs, einem Spezialisten für Virtualisierungslösungen im Embedded-Bereich. Dieser will ein Produkt realisieren, dem ein derart geprüfter Kernel zugrunde liegt.
Mehr dazu findest Du auf
pressetext.com
Kurze URL:
Das könnte Dich auch interessieren:
EU-Parlament stimmt für Austausch sicherheitsrelevanter Passagierdaten
