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. ENERCON GmbH, Aurich
  2. Ratbacher GmbH, Hamburg
  3. NKM Noell Special Cranes GmbH, Würzburg, Veitshöchheim
  4. stoba Präzisionstechnik GmbH & Co. KG, Backnang (nahe Stuttgart)


Anzeige
Blu-ray-Angebote
  1. (u. a. Hobbit Trilogie Blu-ray 43,89€ und Batman Dark Knight Trilogy Blu-ray 17,99€)
  2. 29,99€ (Vorbesteller-Preisgarantie)
  3. (u. a. John Wick, Pulp Fiction, Leon der Profi, Good Will Hunting)

Folgen Sie uns
       


  1. U2F

    Yubico bringt winzigen Yubikey für USB-C

  2. Windows 10

    Windows Store wird zum Microsoft Store mit Hardwareangeboten

  3. Kabelnetz

    Eazy senkt Preis für 50-MBit/s-Zugang im Unitymedia-Netz

  4. Nintendo

    Super Mario Run wird umfangreicher und günstiger

  5. Seniorenhandys im Test

    Alter, sind die unpraktisch!

  6. PixelNN

    Mit Machine Learning unscharfe Bilder erkennbar machen

  7. Mobilfunk

    O2 in bayerischer Gemeinde seit 18 Tagen gestört

  8. Elektroauto

    Tesla schafft günstigstes Model S ab

  9. Bundestagswahl 2017

    IT-Probleme verzögerten Stimmübermittlung

  10. Fortnite Battle Royale

    Entwickler von Pubg sorgt sich wegen Unreal Engine



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
Olympus Tough TG5 vs. Nikon Coolpix W300: Die Schlechtwetter-Kameras
Olympus Tough TG5 vs. Nikon Coolpix W300
Die Schlechtwetter-Kameras
  1. Mobilestudio Pro 16 im Test Wacom nennt 2,2-Kilogramm-Grafiktablet "mobil"
  2. HP Z8 Workstation Mit 3 TByte RAM und 56 CPU-Kernen komplexe Bilder rendern
  3. Meeting Owl KI-Eule erkennt Teilnehmer in Meetings

VR: Was HTC, Microsoft und Oculus mit Autos zu tun haben
VR
Was HTC, Microsoft und Oculus mit Autos zu tun haben
  1. Zukunft des Autos "Unsere Elektrofahrzeuge sollen typische Porsche sein"
  2. Concept EQA Mercedes elektrifiziert die Kompaktklasse
  3. GLC F-Cell Mercedes stellt SUV mit Brennstoffzelle und Akku vor

Parkplatz-Erkennung: Bosch und Siemens scheitern mit Pilotprojekten
Parkplatz-Erkennung
Bosch und Siemens scheitern mit Pilotprojekten
  1. Community based Parking Mercedes S-Klasse liefert Daten für Boschs Parkplatzsuche

  1. Re: Verkaufen sich diese CPUs überhaupt?

    ML82 | 15:44

  2. Re: Nutzen von ECC?

    peter.kleibert | 15:43

  3. Familiy Option?

    Tragen | 15:41

  4. Re: Wahlkampf von Flüchtlingspolitik geprägt und...

    Nikolai | 15:39

  5. Re: Android als Seniorensystem?

    Phantom | 15:39


  1. 15:31

  2. 13:28

  3. 13:17

  4. 12:25

  5. 12:02

  6. 11:58

  7. 11:34

  8. 11:19


  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