Das Unternehmen Amazon und die Rust Foundation haben eine Initiative vorgestellt, die darauf abzielt, die Sicherheit der Standardbibliothek der Programmiersprache Rust zu erhöhen. Ziel ist die Überprüfung der Zuverlässigkeit und Sicherheit von Funktionen, in denen das Schlüsselwort „unsafe“ verwendet wird, das unsichere Speicheroperationen wie das Dereferenzieren von Zeigern, das Modifizieren von statischen Variablen und den Zugriff auf externe C/C++-Bibliotheken zulässt. Es wird darauf hingewiesen, dass die Standardbibliothek von Rust derzeit etwa 35.000 Funktionen umfasst, von denen 7.500 Codeabschnitte enthalten, die im Kontext von „unsafe“ ausgeführt werden. In den letzten drei Jahren wurden in der Bibliothek 57 Probleme mit der Korrektheit festgestellt, von denen 20 als Sicherheitsanfälligkeiten gekennzeichnet wurden.
Die Arbeit zur Überprüfung der Bibliothek erfolgt in Form eines Wettbewerbs, bei dem den Teilnehmern verschiedene Aufgaben angeboten werden, die sich mit der Durchführung bestimmter Prüfungen zur Bestätigung der sicheren Arbeit mit dem Speicher von Rust-Bibliotheken oder der Entwicklung von Tools zur Automatisierung solcher Prüfungen befassen. Der erfolgreiche Abschluss des Prüfungsziels (Bereitstellung eines formalen Nachweises der Zuverlässigkeit) sieht eine Belohnung vor. Ein Repository, das eine Abspaltung des Standard-Rust-Repositories darstellt, wurde eingerichtet, um Experimente durchzuführen und die Ergebnisse zu veröffentlichen.
Derzeit wurden 13 Aufgaben zur Lösung vorgeschlagen. Zum Beispiel wird in einer der Aufgaben gefordert, die Sicherheit der Arbeit mit Raw-Zeigern in den Funktionen des Moduls core::ptr zu überprüfen und einen formalen Nachweis der Korrektheit der Operationen mit Zeigern zu erbringen. Zur Verifikation können bestehende Werkzeuge wie Aeneas, Kani, Gillian, Verus und Creusot verwendet werden, oder es können neue vorgeschlagen werden. Beispiele für ausgeführte Aufgaben.
Quelle: opennet.ru
