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
