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. Fraunhofer-Institut für Arbeitswirtschaft und Organisation IAO, Stuttgart, Esslingen
  2. eco Verband der Internetwirtschaft e.V., Köln

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
Blu-ray-Angebote
  1. (u. a. ES Blu-ray 10,83€, Die nackte Kanone Blu-ray-Box-Set 14,99€)
  2. (u. a. 3 Blu-rays für 15€, 2 Neuheiten für 15€)

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
       


Nubia X - Hands on (CES 2019)

Das Nubia X hat nicht einen, sondern gleich zwei Bildschirme. Wie der Hersteller die Dual-Screen-Lösung umgesetzt hat, haben wir uns auf der CES 2019 angeschaut.

Nubia X - Hands on (CES 2019) Video aufrufen
Padrone angesehen: Eine Mausalternative, die funktioniert
Padrone angesehen
Eine Mausalternative, die funktioniert

CES 2019 Ein Ring soll die Computermaus ersetzen: Am Zeigefinger getragen macht Padrone jede Oberfläche zum Touchpad. Der Prototyp fühlt sich bei der Bedienung überraschend gut an.
Von Tobias Költzsch

  1. Videostreaming Plex will Filme und Serien kostenlos und im Abo anbieten
  2. People Mover Rollende Kisten ohne Fahrer
  3. Solar Cow angesehen Elektrische Kuh gibt Strom statt Milch

Nubia Red Magic Mars im Hands On: Gaming-Smartphone mit Top-Ausstattung für 390 Euro
Nubia Red Magic Mars im Hands On
Gaming-Smartphone mit Top-Ausstattung für 390 Euro

CES 2019 Mit dem Red Magic Mars bringt Nubia ein interessantes und vor allem verhältnismäßig preiswertes Gaming-Smartphone nach Deutschland. Es hat einen Leistungsmodus und Schulter-Sensortasten, die beim Zocken helfen können.
Ein Hands on von Tobias Költzsch

  1. ATH-ANC900BT Audio Technica zeigt neuen ANC-Kopfhörer
  2. Smart Clock Lenovo setzt bei Echo-Spot-Variante auf Google Assistant
  3. Smart Tab Lenovo zeigt Mischung aus Android-Tablet und Echo Show

Datenleak: Die Fehler, die 0rbit überführten
Datenleak
Die Fehler, die 0rbit überführten

Er ließ sich bei einem Hack erwischen, vermischte seine Pseudonyme und redete zu viel - Johannes S. hinterließ viele Spuren. Trotzdem brauchte die Polizei offenbar einen Hinweisgeber, um ihn als mutmaßlichen Täter im Politiker-Hack zu überführen.

  1. Datenleak Bundestagsabgeordnete sind Zwei-Faktor-Muffel
  2. Datenleak Telekom und Politiker wollen härtere Strafen für Hacker
  3. Datenleak BSI soll Frühwarnsystem für Hackerangriffe aufbauen

    •  /