Abo
  • Services:
Anzeige

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.

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.

Anzeige

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.


eye home zur Startseite
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...



Anzeige

Stellenmarkt
  1. dSPACE GmbH, Paderborn
  2. Landespolizeiamt Schleswig-Holstein, Kiel
  3. über Provadis Professionals GmbH, Frankfurt am Main
  4. Daimler AG, Böblingen


Anzeige
Blu-ray-Angebote
  1. (u. a. The Hateful 8 7,97€, The Revenant 8,97€, Interstellar 7,97€)
  2. (u. a. Forrest Gump 9,97€, Gods of Egypt 9,97€, Creed 8,99€, Cloud Atlas 8,94€)
  3. 6,99€

Folgen Sie uns
       

Anzeige
Whitepaper
  1. Globale SAP-Anwendungsunterstützung durch Outsourcing
  2. Praxiseinsatz, Nutzen und Grenzen von Hadoop und Data Lakes


  1. Ungepatchte Sicherheitslücke

    Google legt sich erneut mit Microsoft an

  2. Torus

    CoreOS gibt weitere Eigenentwicklung auf

  3. Hololens

    Verbesserte AR-Brille soll nicht vor 2019 kommen

  4. Halo Wars 2 im Test

    Echtzeit-Strategie für Supersoldaten

  5. Autonome Systeme

    Microsoft stellt virtuelle Testplattform für Drohnen vor

  6. Limux

    Die tragische Geschichte eines Leuchtturm-Projekts

  7. Betriebssysteme

    Linux 4.10 beschleunigt und verbessert

  8. Supercomputer

    Der erste Exaflop-Rechner wird in China gebaut

  9. Thomas de Maizière

    Doch keine Vorratsdatenspeicherung für Whatsapp

  10. Automatisierung

    Europaparlament fordert Roboterregeln



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Pure Audio: Blu-ray-Audioformate kommen nicht aus der Nische
Pure Audio
Blu-ray-Audioformate kommen nicht aus der Nische

Prey angespielt: Das Monster aus der Kaffeetasse
Prey angespielt
Das Monster aus der Kaffeetasse
  1. Bethesda Softworks Prey bedroht die Welt im Mai 2017
  2. Ausblicke Abenteuer in Andromeda und Galaxy

Kernfusion: Angewandte Science-Fiction
Kernfusion
Angewandte Science-Fiction
  1. Kernfusion Wendelstein 7-X funktioniert nach Plan

  1. Re: Keine Werbung für Kinder

    tha_specializt | 16:38

  2. Re: Und was macht die Boulevardpresse draus?

    crack_monkey | 16:38

  3. Re: technisch möglich? einziger sinn?

    triplekiller | 16:38

  4. Re: Die geliebten kleinen Pausen

    Potrimpo | 16:37

  5. Re: Firefox funktioniert nicht mehr (ganz richtig)

    bjs | 16:36


  1. 16:38

  2. 16:27

  3. 15:23

  4. 14:00

  5. 13:12

  6. 12:07

  7. 12:06

  8. 11:59


  1. Themen
  2. A
  3. B
  4. C
  5. D
  6. E
  7. F
  8. G
  9. H
  10. I
  11. J
  12. K
  13. L
  14. M
  15. N
  16. O
  17. P
  18. Q
  19. R
  20. S
  21. T
  22. U
  23. V
  24. W
  25. X
  26. Y
  27. Z
  28. #
 
    •  / 
    Zum Artikel