Das Unternehmen Amazon und die Rust Foundation haben eine Initiative zur Verbesserung der Sicherheit der Standardbibliothek der Programmiersprache Rust vorgestellt. Ziel ist die ĂberprĂŒfung der ZuverlĂ€ssigkeit und Sicherheit von Funktionen, die das SchlĂŒsselwort "unsafe" verwenden, welches unsichere Speicheroperationen wie das Dereferenzieren von Zeigern, das Modifizieren von statischen Variablen und den Zugriff auf externe Bibliotheken in C/C++ zulĂ€sst. Es wird festgestellt, dass die Standardbibliothek von Rust derzeit etwa 35.000 Funktionen umfasst, von denen in 7.500 Codeblöcke im Kontext von "unsafe" ausgefĂŒhrt werden. In den letzten drei Jahren wurden in der Bibliothek 57 Korrektheitsprobleme identifiziert, von denen 20 als SicherheitsanfĂ€lligkeiten eingestuft wurden.
Die Arbeit an der ĂberprĂŒfung der Bibliothek wird in Form eines Wettbewerbs organisiert, bei dem den Teilnehmern verschiedene Aufgaben angeboten werden, die sich mit der DurchfĂŒhrung bestimmter Tests zur BestĂ€tigung der sicheren Arbeit mit dem Speicher von Rust-Bibliotheken oder mit der Entwicklung von Werkzeugen zur Automatisierung solcher Tests befassen. Das erfolgreiche Erreichen des PrĂŒfungsziels (Bereitstellung eines formalen Nachweises der ZuverlĂ€ssigkeit) sieht die Zahlung einer Belohnung vor. FĂŒr Experimente und die Veröffentlichung von Arbeitsergebnissen wurde ein Repository erstellt, das einen Fork des Standard-Repositories von Rust darstellt.
Derzeit sind 13 Aufgaben zur Lösung vorgeschlagen. Beispielsweise wird in einer Aufgabe angeboten, die Sicherheit der Arbeit mit raw-Pointern in Funktionen des Moduls core::ptr sicherzustellen und einen formalen Nachweis der Korrektheit der Operationen mit Zeigern vorzulegen. Zur Verifizierung können bestehende Werkzeuge wie Aeneas, Kani, Gillian, Verus und Creusot verwendet oder neue vorgeschlagen werden. Beispiele fĂŒr gelöste Aufgaben.
Quelle: opennet.ru
