Bezpieczeństwo pamięci oparte na typach bez ręcznego zarządzania pamięcią lub zbierania elementów w czasie wykonywania?

Powiedzmy, że chcieliśmy typowego, czysto funkcjonalnego języka programowania, takiego jak Haskell lub Idris, który jest przeznaczony do programowania systemów bez wyrzucania elementów bezużytecznych i nie ma środowiska wykonawczego (a przynajmniej nie więcej niż „środowiska wykonawcze” C i Rust). Coś, co może działać mniej więcej na gołym metalu.

Jakie są niektóre opcje statycznego bezpieczeństwa pamięci, które nie wymagają ręcznego zarządzania pamięcią lub usuwania śmieci w środowisku wykonawczym, i jak można rozwiązać problem za pomocą systemu typów o czystej funkcjonalności podobnej do Haskell lub Idris?

Z grubsza mówiąc, istnieją dwie główne strategie bezpiecznego ręcznego zarządzania pamięcią.

1. Pierwsze podejście polega na użyciu pewnej logiki podstrukturalnej, takiej jak logika liniowa, do kontrolowania wykorzystania zasobów. Pomysł ten krążył w zasadzie od początku logiki liniowej i zasadniczo działa na podstawie obserwacji, że zakazując strukturalnej reguły skurczu, każda zmienna jest używana co najwyżej raz, a więc nie ma aliasingu. W rezultacie różnica między aktualizacją w miejscu a ponownym przydziałem jest niewidoczna dla programu, dzięki czemu można wdrożyć swój język za pomocą ręcznego zarządzania pamięcią.

   To właśnie robi Rust (używa systemu typu afinicznego). Jeśli interesuje Cię teoria języków w stylu Rust, jednym z najlepszych artykułów do przeczytania jest L3: A Linear Language with Locations Ahmeda i innych . Nawiasem mówiąc, wspomniany rachunek LFPL Damiano Mazza jest również liniowy, ma pełny język pochodzący z niego w języku RAML .

   Jeśli interesuje Cię weryfikacja w stylu Idris, powinieneś spojrzeć na język ATS Xi i innych , który jest językiem w stylu Rust / L3 z obsługą weryfikacji opartej na typach indeksowanych w stylu Haskell, tylko uczyniono niepoprawnym i liniowym, aby dać więcej kontrola wydajności.

   Jeszcze bardziej agresywnie zależnym podejściem jest język F-star opracowany w Microsoft Research, który jest w pełni zależną teorią typów. Ten język ma monadyczny interfejs z warunkami wstępnymi i końcowymi w duchu teorii typów Hoare'a Nanevskiego i in. (Lub nawet moich własnych integrujących typów liniowych i zależnych ) i ma zdefiniowany podzbiór, który można skompilować do niskiego poziomu kodu C - w rzeczywistości wysyłają już zweryfikowany kod kryptograficzny jako część Firefoksa!

   Żeby było jasne, ani gwiazda F, ani HTT nie są językami o typie liniowym, ale język indeksu dla ich monad zwykle opiera się na logice separacji Reynolda i O'Hearn'a , która jest logiką podstrukturalną związaną z logiką liniową, która odniosła wielki sukces jako język asercji dla logiki Hoare dla programów wskaźnikowych.

2. Drugim podejściem jest po prostu określenie, co robi zespół (lub cokolwiek, co chcesz na niskim poziomie IR), a następnie użycie jakiejś logiki liniowej lub separacyjnej, aby bezpośrednio uzasadnić swoje zachowanie w asystencie dowodu. Zasadniczo możesz użyć asystenta sprawdzania lub języka pisanego zależnie jako bardzo fantazyjnego asemblera makr, który generuje tylko poprawne programy.

   Jensen i wsp. Logika separacji wysokiego poziomu dla kodu niskopoziomowego jest tego szczególnie czystym przykładem - buduje logikę separacji dla asemblera x86! Istnieje jednak wiele projektów w tym stylu, takich jak Verified Software Toolchain w Princeton i projekt CertiKOS w Yale.

Wszystkie te podejścia będą „przypominać” Rust, ponieważ śledzenie własności poprzez ograniczenie użycia zmiennych jest dla nich kluczowe.

Typy liniowe i logika separacji są świetne, ale mogą wymagać sporo wysiłku programisty. Na przykład napisanie bezpiecznej listy w Rust może być dość trudne.

Ale istnieje alternatywa, która wymaga znacznie mniej wysiłku programisty, choć z mniej surowymi gwarancjami. (Dość stary) strumień pracy ma zagwarantować bezpieczeństwo pamięci przy użyciu (zwykle stosu) regionów. Korzystając z wnioskowania o regionie, kompilator może statycznie zadecydować, do którego regionu powinna wejść część przydzielonych danych, i cofnąć przydział regionu, gdy wykracza on poza zakres.

Wnioskowanie regionu jest możliwe do udowodnienia, że ​​jest bezpieczne (nie może cofnąć przydziału dostępnej pamięci) i wymaga minimalnej ingerencji programisty, ale nie jest „całkowite” (tzn. Wciąż może przeciekać pamięć, chociaż zdecydowanie znacznie lepiej niż „nic nie robić”), więc zwykle jest łączone z GC w praktyce. TheMLtonKompilator ML Kit wykorzystuje regiony do eliminacji większości wywołań GC, ale nadal ma GC, ponieważ w przeciwnym razie nadal przeciekałby pamięć. Według niektórych pierwszych pionierów w regionie wnioskowanie o regiony nie zostało w rzeczywistości wymyślone w tym celu (chyba automatycznej paralelizacji); ale właśnie się okazało, że można go również wykorzystać do zarządzania pamięcią.

Na początek chciałbym napisać artykuł „Implementacja typowego rachunku λ według wartości przy użyciu stosu regionów” autorstwa Madsa Tofte i Jean-Pierre Talpin. Aby uzyskać więcej artykułów na temat wnioskowania na temat regionu, poszukaj innych artykułów M. Tofte i J.-P. Talpin, niektóre prace Pierre'a Jouvelota, a także Greg Morrisett, Mike Hicks i seria artykułów Dana Grossmana na temat Cyklonu.

Trywialnym schematem dla systemów typu „bare metal” jest po prostu uniemożliwienie przydziałów pamięci wykonawczej. Pamiętaj, że nawet malloc/freepara C wymaga biblioteki wykonawczej. Ale nawet gdy wszystkie obiekty są zdefiniowane w czasie kompilacji, można je zdefiniować w bezpieczny sposób.

Głównym problemem tutaj jest fikcja niezmiennych wartości w czysto funkcjonalnych językach, które są tworzone podczas działania programu. Prawdziwy sprzęt (a na pewno systemy typu bare metal) opiera się na zmiennej pamięci RAM, która jest ograniczona. Środowisko wykonawcze implementacji języka funkcjonalnego w praktyce dynamicznie przydziela pamięć RAM, gdy tworzone są nowe wartości „niezmienne”, a śmieci je gromadzą, gdy wartość „niezmienna” nie jest już potrzebna.

W przypadku najciekawszych problemów czas życia przynajmniej niektórych wartości zależy od danych wejściowych środowiska wykonawczego (użytkownika), więc okresów życia nie można ustalić statycznie. Ale nawet jeśli czas życia nie zależy od danych wejściowych, może być wysoce nietrywialny. Weź prosty program, wielokrotnie wyszukując liczby pierwsze, po prostu sprawdzając każdą liczbę w kolejności, sprawdzając względem wszystkich liczb pierwszych do sqrt(N). Wyraźnie taka potrzeba zachowuje liczby pierwsze i może odzyskać pamięć używaną dla liczb pierwszych.