Automatischer Sicherheitsnachweis für Betriebssystemkern
Mit ihrem Verfahren wollen die Forscher des Nicta(öffnet im neuen Fenster) 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.
Ausgetestet wurde die Methode am Secure-Embedded-L4-Mikrokernel(öffnet im neuen Fenster) (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(öffnet im neuen Fenster) 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(öffnet im neuen Fenster) 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(öffnet im neuen Fenster) im Oktober vorgestellt werden.
- Anzeige Hier geht es zum Handbuch für Softwareentwickler bei Amazon Wenn Sie auf diesen Link klicken und darüber einkaufen, erhält Golem eine kleine Provision. Dies ändert nichts am Preis der Artikel.