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. Optica Abrechnungszentrum Dr. Güldener GmbH, Nittenau Raum Regensburg
  2. BVU Beratergruppe Verkehr + Umwelt GmbH, Freiburg
  3. Daimler AG, Germersheim
  4. Robert Bosch Car Multimedia GmbH, Hildesheim


Anzeige
Blu-ray-Angebote
  1. 139,99€ (Vorbesteller-Preisgarantie)
  2. (u. a. 3 3D-Blu-rays für 30 EUR, Box-Sets u. Serien)
  3. 24,99€ (Vorbesteller-Preisgarantie)

Folgen Sie uns
       

Anzeige
Whitepaper
  1. Mehr dazu im aktuellen Whitepaper von Freudenberg IT
  2. Mehr dazu im aktuellen Whitepaper von Bitdefender
  3. Globale SAP-Anwendungsunterstützung durch Outsourcing


  1. Alternatives Android

    Cyanogen soll zahlreiche Mitarbeiter entlassen

  2. Update

    Onedrive erstellt automatisierte Alben und erkennt Pokémon

  3. Die Woche im Video

    Ausgesperrt, ausprobiert, ausgetüftelt

  4. 100 MBit/s

    Zusagen der Bundesnetzagentur drücken Preis für Vectoring

  5. Insolvenz

    Unister Holding mit 39 Millionen Euro verschuldet

  6. Radeons RX 480

    Die Designs von AMDs Partnern takten höher - und konstanter

  7. Koelnmesse

    Tagestickets für Gamescom ausverkauft

  8. Kluge Uhren

    Weltweiter Smartwatch-Markt bricht um ein Drittel ein

  9. Linux

    Nvidia ist bereit für einheitliche Wayland-Unterstützung

  10. Copyright

    Klage gegen US-Marine wegen 558.466-mal Softwarepiraterie



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Axon 7 vs Oneplus Three im Test: 7 ist besser als 1+3
Axon 7 vs Oneplus Three im Test
7 ist besser als 1+3
  1. Axon 7 im Hands on Oneplus bekommt starke Konkurrenz
  2. Axon 7 ZTEs Topsmartphone kommt für 450 Euro nach Deutschland

Besuch beim HAX Accelerator: Made in Shenzhen
Besuch beim HAX Accelerator
Made in Shenzhen
  1. Superbook Neues Laptop-Dock für Smartphones soll 100 US-Dollar kosten
  2. Kreditkarten Number26 wird Betrug mit Standortdaten verhindern
  3. Bargeld nervt Startups und Kryptowährungen mischen die Finanzbranche auf

Die erste Ransomware: Der Virus des wunderlichen Dr. Popp
Die erste Ransomware
Der Virus des wunderlichen Dr. Popp
  1. Erpressungstrojaner Locky kann jetzt auch offline
  2. Ransomware Ranscam schickt Dateien unwiederbringlich ins Nirwana
  3. Botnet Necurs kommt zurück und bringt Locky millionenfach mit

  1. Re: Maxdome

    nmSteven | 14:54

  2. Re: Einnahmequellen?

    Ebola | 14:53

  3. Re: Das ist schlicht falsch

    Moe479 | 14:52

  4. Ab der kommerziellen Firma..

    SchmuseTigger | 14:51

  5. akute Zahlungsunfähigkeit

    mal_so | 14:44


  1. 14:19

  2. 13:08

  3. 09:01

  4. 18:26

  5. 18:00

  6. 17:00

  7. 16:29

  8. 16:02


  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