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. Winkelmann Group GmbH + Co. KG, Ahlen
  2. über Hanseatisches Personalkontor Mannheim, Mannheim
  3. operational services GmbH & Co. KG, Nürnberg
  4. ENERTRAG Aktiengesellschaft, Dauerthal, Berlin, Edemissen


Anzeige
Spiele-Angebote
  1. 3,49€
  2. (-78%) 8,99€
  3. 1,49€

Folgen Sie uns
       


  1. VLC, Kodi, Popcorn Time

    Mediaplayer können über Untertitel gehackt werden

  2. Engine

    Unity bekommt 400 Millionen US-Dollar Investorengeld

  3. Neuauflage

    Neues Nokia 3310 soll bei Defekt komplett ersetzt werden

  4. Surface Studio

    Microsofts Grafikerstation kommt nach Deutschland

  5. Polar

    Fitnesstracker A370 mit Tiefschlaf- und Pulsmessung

  6. Schutz

    Amazon rechtfertigt Sperrungen von Marketplace-Händlern

  7. CPU-Architektur

    RISC-V-Patches für Linux erstmals eingereicht

  8. FSP Hydro PTM+

    Wassergekühltes PC-Netzteil liefert 1.400 Watt

  9. Matebook X und E im Hands on

    Huawei kann auch Notebooks

  10. Celsius-Workstations

    Fujitsu bringt sichere Notebooks und kabellose Desktops



Haben wir etwas übersehen?

E-Mail an news@golem.de


Anzeige
The Surge im Test: Frust und Feiern in der Zukunft
The Surge im Test
Frust und Feiern in der Zukunft
  1. Computerspiele und Psyche Wie Computerspieler zu Süchtigen erklärt werden sollen
  2. Wirtschaftssimulation Pizza Connection 3 wird gebacken
  3. Mobile-Games-Auslese Untote Rundfahrt und mobiles Seemannsgarn

Redmond Campus Building 87: Microsofts Area 51 für Hardware
Redmond Campus Building 87
Microsofts Area 51 für Hardware
  1. Windows on ARM Microsoft erklärt den kommenden x86-Emulator im Detail
  2. Azure Microsoft betreut MySQL und PostgreSQL in der Cloud
  3. Microsoft Azure bekommt eine beeindruckend beängstigende Video-API

3D-Druck bei der Bahn: Mal eben einen Kleiderhaken für 80 Euro drucken
3D-Druck bei der Bahn
Mal eben einen Kleiderhaken für 80 Euro drucken
  1. Bahnchef Richard Lutz Künftig "kein Ticket mehr für die Bahn" notwendig
  2. Flatrate Öffentliches Fahrradleihen kostet 50 Euro im Jahr
  3. Nextbike Berlins neues Fahrradverleihsystem startet

  1. Re: Für Vermögende die kreativ sein wollen..

    awgher | 05:24

  2. Re: Wannacry? Linux lacht :)

    ArcherV | 04:13

  3. Re: 1400W... für welche Hardware?

    ArcherV | 04:10

  4. Re: Warum überhaupt VLC nutzen

    ve2000 | 03:26

  5. Re: Unix, das Betriebssystem von Entwicklern, für...

    __destruct() | 03:26


  1. 18:58

  2. 18:20

  3. 17:59

  4. 17:44

  5. 17:20

  6. 16:59

  7. 16:30

  8. 15:40


  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