Forum für Wissenschaft, Industrie und Wirtschaft

Hauptsponsoren:     3M 
Datenbankrecherche:

 

Sicherheits-Beweis für Betriebssystem-Kernel

17.08.2009
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.

Es habe bereits formale Prüfungen einzelner Eigenschaften von kleineren Kernels gegeben, heißt es am NICTA. "Was wir gemacht haben ist aber ein allgemeiner Beweis der funktionellen Fehlerfreiheit, was nie zuvor für reale, hochleistungsfähige Software dieser Komplexität oder Größe gelungen ist", meint Gerwin Klein, Forschungsleiter des NICTA-Teams. Mithilfe eines Computerprogramms wurden 7.500 Code-Zeilen geprüft und in mehr als 200.000 Zeilen formelle Beweise für über 10.000 Theoreme erbracht. Damit wurde gezeigt, dass der Quellcode korrekt gestaltet ist, was hohe Zuverlässigkeit und Sicherheit verspricht. Dem NICTA zufolge wurde nachgewiesen, dass seL4 immun gegen sogenannte Buffer Overflows ist, die Hackern das Einschleusen von Schadcode ermöglichen. OK Labs zufolge können unter anderem auch Zeigerfehler sowie Speicherlecks und -überläufe ausgeschlossen werden.

Das NICTA betont, dass sich nun die Möglichkeit zum mathematischen Nachweis eröffne, dass kritische Software beispielsweise in Sicherheitssystemen in Flugzeugen oder Autos weitgehend fehlerfrei ist, bevor das Verkehrsmittel zum Einsatz kommt. Der seL4-Kernel selbst habe Anwendungspotenzial unter anderem in der Verteidigungsindustrie. Der NICTA-Kernel ist nur ein Vertreter der Mikrokernel-Familie L4 http://www.l4hq.org , die auf den 2001 verstorbenen deutschen Informatiker Jochen Liedtke zurückgeht. Ein L4-Kernel liegt auch OKL4 zugrunde, einer kommerziellen mobilen Virtualisierungsplattform von OK Labs. Als enger Partner des NICTA will OK Labs die Methode des Forschungsinstituts nun nutzen, eine vergleichbare Prüfung für OKL4 durchzuführen. In weiterer Folge soll ein vollständig verifiziertes kommerzielles Produkt entstehen.

Thomas Pichler | pressetext.austria
Weitere Informationen:
http://nicta.com.au
http://www.ok-labs.com

Weitere Nachrichten aus der Kategorie Informationstechnologie:

nachricht Cybersicherheit für die Bahn von morgen
24.03.2017 | Fraunhofer-Institut für Sichere Informationstechnologie SIT

nachricht Schutz vor Angriffen dank flexibler Programmierung
22.03.2017 | FZI Forschungszentrum Informatik am Karlsruher Institut für Technologie

Alle Nachrichten aus der Kategorie: Informationstechnologie >>>

Die aktuellsten Pressemeldungen zum Suchbegriff Innovation >>>

Die letzten 5 Focus-News des innovations-reports im Überblick:

Im Focus: Wegweisende Erkenntnisse für die Biomedizin: NAD⁺ hilft bei Reparatur geschädigter Erbinformationen

Eine internationale Forschergruppe mit dem Bayreuther Biochemiker Prof. Dr. Clemens Steegborn präsentiert in 'Science' neue, für die Biomedizin wegweisende Forschungsergebnisse zur Rolle des Moleküls NAD⁺ bei der Korrektur von Schäden am Erbgut.

Die Zellen von Menschen und Tieren können Schäden an der DNA, dem Träger der Erbinformation, bis zu einem gewissen Umfang selbst reparieren. Diese Fähigkeit...

Im Focus: Designer-Proteine falten DNA

Florian Praetorius und Prof. Hendrik Dietz von der Technischen Universität München (TUM) haben eine neue Methode entwickelt, mit deren Hilfe sie definierte Hybrid-Strukturen aus DNA und Proteinen aufbauen können. Die Methode eröffnet Möglichkeiten für die zellbiologische Grundlagenforschung und für die Anwendung in Medizin und Biotechnologie.

Desoxyribonukleinsäure – besser bekannt unter der englischen Abkürzung DNA – ist die Trägerin unserer Erbinformation. Für Prof. Hendrik Dietz und Florian...

Im Focus: Fliegende Intensivstationen: Ultraschallgeräte in Rettungshubschraubern können Leben retten

Etwa 21 Millionen Menschen treffen jährlich in deutschen Notaufnahmen ein. Im Kampf zwischen Leben und Tod zählt für diese Patienten jede Minute. Wenn sie schon kurz nach dem Unfall zielgerichtet behandelt werden können, verbessern sich ihre Überlebenschancen erheblich. Damit Notfallmediziner in solchen Fällen schnell die richtige Diagnose stellen können, kommen in den Rettungshubschraubern der DRF Luftrettung und zunehmend auch in Notarzteinsatzfahrzeugen mobile Ultraschallgeräte zum Einsatz. Experten der Deutschen Gesellschaft für Ultraschall in der Medizin e.V. (DEGUM) schulen die Notärzte und Rettungsassistenten.

Mit mobilen Ultraschallgeräten können Notärzte beispielsweise innere Blutungen direkt am Unfallort identifizieren und sie bei Bedarf auch für Untersuchungen im...

Im Focus: Gigantische Magnetfelder im Universum

Astronomen aus Bonn und Tautenburg in Thüringen beobachteten mit dem 100-m-Radioteleskop Effelsberg Galaxienhaufen, das sind Ansammlungen von Sternsystemen, heißem Gas und geladenen Teilchen. An den Rändern dieser Galaxienhaufen fanden sie außergewöhnlich geordnete Magnetfelder, die sich über viele Millionen Lichtjahre erstrecken. Sie stellen die größten bekannten Magnetfelder im Universum dar.

Die Ergebnisse werden am 22. März in der Fachzeitschrift „Astronomy & Astrophysics“ veröffentlicht.

Galaxienhaufen sind die größten gravitativ gebundenen Strukturen im Universum, mit einer Ausdehnung von etwa zehn Millionen Lichtjahren. Im Vergleich dazu ist...

Im Focus: Giant Magnetic Fields in the Universe

Astronomers from Bonn and Tautenburg in Thuringia (Germany) used the 100-m radio telescope at Effelsberg to observe several galaxy clusters. At the edges of these large accumulations of dark matter, stellar systems (galaxies), hot gas, and charged particles, they found magnetic fields that are exceptionally ordered over distances of many million light years. This makes them the most extended magnetic fields in the universe known so far.

The results will be published on March 22 in the journal „Astronomy & Astrophysics“.

Galaxy clusters are the largest gravitationally bound structures in the universe. With a typical extent of about 10 million light years, i.e. 100 times the...

Alle Focus-News des Innovations-reports >>>

Anzeige

Anzeige

IHR
JOB & KARRIERE
SERVICE
im innovations-report
in Kooperation mit academics
Veranstaltungen

Rund 500 Fachleute aus Wissenschaft und Wirtschaft diskutierten über technologische Zukunftsthemen

24.03.2017 | Veranstaltungen

Lebenswichtige Lebensmittelchemie

23.03.2017 | Veranstaltungen

Die „Panama Papers“ aus Programmierersicht

22.03.2017 | Veranstaltungen

 
VideoLinks
B2B-VideoLinks
Weitere VideoLinks >>>
Aktuelle Beiträge

Rund 500 Fachleute aus Wissenschaft und Wirtschaft diskutierten über technologische Zukunftsthemen

24.03.2017 | Veranstaltungsnachrichten

Förderung des Instituts für Lasertechnik und Messtechnik in Ulm mit rund 1,63 Millionen Euro

24.03.2017 | Förderungen Preise

TU-Bauingenieure koordinieren EU-Projekt zu Recycling-Beton von über sieben Millionen Euro

24.03.2017 | Förderungen Preise