Firma Amazon i organizacja Rust Foundation wprowadziły inicjatywę mającą na celu zwiększenie bezpieczeństwa standardowej biblioteki języka Rust. Celem jest sprawdzenie niezawodności i bezpieczeństwa funkcji, w których używane jest słowo kluczowe „unsafe”, zezwalające na operacje niebezpiecznie pracujące z pamięcią, takie jak dereferencja wskaźników, modyfikacja zmiennych statycznych i wywołania do zewnętrznych bibliotek w C/C++. Podkreśla się, że obecnie standardowa biblioteka Rust zawiera około 35 tysięcy funkcji, z czego w 7500 występują bloki kodu wykonywane w kontekście „unsafe”. W ciągu ostatnich trzech lat w bibliotece zidentyfikowano 57 problemów związanych z poprawnością działania, z których 20 zostało oznaczonych jako luki.
Prace związane z weryfikacją biblioteki są organizowane w formie konkursu, w którym uczestnicy są zapraszani do rozwiązywania różnych zadań związanych z wykonywaniem określonych kontroli w celu potwierdzenia bezpiecznej pracy z pamięcią bibliotek Rust lub do opracowania narzędzi do automatyzacji podobnych weryfikacji. Sukces w osiągnięciu celu weryfikacji (zapewnienie formalnego dowodu niezawodności) przewiduje wypłatę nagrody. Do przeprowadzania eksperymentów i publikowania wyników stworzono repozytorium będące rozwidleniem oficjalnego repozytorium Rust.
Obecnie zaproponowano 13 zadań. Na przykład, w jednym z zadań uczestnicy są zachęcani do upewnienia się co do bezpieczeństwa pracy z wskaźnikami raw w funkcjach modułu core::ptr oraz do dostarczenia formalnego dowodu poprawności operacji na wskaźnikach. Do weryfikacji można używać istniejących narzędzi, takich jak Aeneas, Kani, Gillian, Verus i Creusot, lub zaproponować nowe. Przykłady zrealizowanych zadań.
Źródło: opennet.ru
