Czy można programowo ocenić bezpieczeństwo dla dowolnego kodu?

Ostatnio dużo myślałem o bezpiecznym kodzie. Bezpieczny dla wątków. Bezpieczny dla pamięci. Bezpieczny, nie wybuchnie w twarz. Ale dla jasności w tym pytaniu zastosujmy model bezpieczeństwa Rust jako naszą definicję.

Często zapewnienie bezpieczeństwa jest trochę problemem, jak duży jest Internet, ponieważ, jak dowodzi potrzeba Rust unsafe, istnieją pewne bardzo rozsądne pomysły programistyczne, takie jak współbieżność, których nie można wdrożyć w Rust bez użycia unsafesłowa kluczowego . Mimo że współbieżność można całkowicie zabezpieczyć za pomocą blokad, muteksów, kanałów i izolacji pamięci lub tego, co masz, wymaga to pracy poza modelem bezpieczeństwa Rust z unsafe, a następnie ręcznego zapewnienia kompilatorowi, że: „Tak, wiem, co robię To wygląda na niebezpieczne, ale matematycznie udowodniłem, że jest całkowicie bezpieczne. ”

Ale zazwyczaj sprowadza się to do ręcznego tworzenia modeli tych rzeczy i udowodnienia, że ​​są bezpieczne dzięki dowodom twierdzeń . Zarówno z perspektywy informatyki (czy to możliwe), jak i praktycznej (czy to zajmie życie wszechświata), czy uzasadnione jest wyobrażenie sobie programu, który pobiera dowolny kod w dowolnym języku i ocenia, czy to „ Bezpieczny dla rdzy ”?

Ostrzeżenia :

• Łatwo jest zauważyć, że program może być nieszkodliwy i dlatego problem zatrzymania zawodzi nas. Powiedzmy, że każdy program dostarczony do czytnika z pewnością się zatrzyma
• Chociaż celem jest „dowolny kod w dowolnym języku”, jestem oczywiście świadomy, że zależy to od znajomości programu przez wybrany język, którą weźmiemy za dany

Ostatecznie mówimy tutaj o czasie kompilacji a czasie wykonywania.

Błędy czasu kompilacji, jeśli się nad tym zastanowić, ostatecznie sprowadzają się do tego, że kompilator jest w stanie określić, jakie problemy masz w swoim programie, zanim jeszcze zostanie uruchomiony. Oczywiście nie jest to kompilator „dowolnego języka”, ale wrócę do tego wkrótce. Kompilator, w całej swej nieskończonej mądrości, nie wymienia jednak wszystkich problemów, które może określić kompilator. Zależy to częściowo od tego, jak dobrze napisany jest kompilator, ale głównym tego powodem jest to, że wiele rzeczy jest określanych w czasie wykonywania .

Błędy uruchomieniowe, jak dobrze wiesz, jestem pewien, że tak jak ja, to każdy rodzaj błędu, który pojawia się podczas wykonywania samego programu. Obejmuje to dzielenie przez zero, wyjątki zerowego wskaźnika, problemy ze sprzętem i wiele innych czynników.

Charakter błędów w czasie wykonywania oznacza, że ​​nie można przewidzieć tych błędów w czasie kompilacji. Jeśli możesz, prawie na pewno zostaną sprawdzone podczas kompilacji. Jeśli możesz zagwarantować, że liczba jest równa zero w czasie kompilacji, możesz wykonać pewne logiczne wnioski, takie jak podzielenie dowolnej liczby przez tę liczbę spowoduje błąd arytmetyczny spowodowany dzieleniem przez zero.

Jako taki, w bardzo realny sposób, wróg programowo gwarantujący prawidłowe funkcjonowanie programu wykonuje kontrole czasu wykonywania w przeciwieństwie do kontroli czasu kompilacji. Przykładem może być dynamiczne rzutowanie na inny typ. Jeśli jest to dozwolone, to ty, programista, zasadniczo przesłonisz zdolność kompilatora do sprawdzenia, czy jest to bezpieczne. Niektóre języki programowania zdecydowały, że jest to akceptowalne, podczas gdy inne przynajmniej ostrzegą cię podczas kompilacji.

Innym dobrym przykładem może być dopuszczenie, aby wartości null były częścią języka, ponieważ wyjątki wskaźnika zerowego mogą się zdarzyć, jeśli zezwolisz na wartości null. Niektóre języki całkowicie wyeliminowały ten problem, uniemożliwiając, aby zmienne, które nie zostały jawnie zadeklarowane, mogły przechowywać deklarowane wartości zerowe bez natychmiastowego przypisywania wartości (na przykład Kotlin). Chociaż nie można wyeliminować błędu czasu wykonania wyjątku wskaźnika zerowego, można temu zapobiec, usuwając dynamiczną naturę języka. W Kotlinie można oczywiście wymusić zachowanie wartości zerowych, ale nie trzeba dodawać, że jest to metaforyczna „uwaga kupujących”, ponieważ należy to wyraźnie określić.

Czy możesz koncepcyjnie mieć kompilator, który może sprawdzać błędy w każdym języku? Tak, ale prawdopodobnie byłby to niezgrabny i wysoce niestabilny kompilator, w którym musiałbyś koniecznie podać język kompilacji wcześniej. Nie mógł również wiedzieć wielu rzeczy o twoim programie, tak jak kompilatory dla określonych języków nie wiedzą o nim pewnych rzeczy, takich jak wspomniany problem zatrzymania. Jak się okazuje, nie da się zebrać wielu informacji, które mogą być interesujące dla programu. Zostało to udowodnione, więc prawdopodobnie nie zmieni się w najbliższym czasie.

Wracając do pierwotnego punktu. Metody nie są automatycznie wątkowo bezpieczne. Istnieje praktyczny powód tego, że metody bezpieczeństwa wątku są również wolniejsze, nawet gdy wątki nie są używane. Rust decyduje, że może wyeliminować problemy w czasie wykonywania, domyślnie czyniąc metody wątkami bezpiecznymi, i to jest ich wybór. To jednak kosztuje.

Możliwe jest matematyczne udowodnienie poprawności programu, ale z zastrzeżeniem, że masz dosłownie zero cech środowiska uruchomieniowego w języku. Będziesz mógł przeczytać ten język i wiedzieć, co on robi bez żadnych niespodzianek. Język prawdopodobnie wyglądałby bardzo matematycznie i prawdopodobnie nie jest to przypadek. Drugim zastrzeżeniem jest to, że nadal występują błędy czasu wykonywania , które mogą nie mieć nic wspólnego z samym programem. Dlatego program można udowodnić, że jest poprawny, zakładając, że szereg założeń dotyczących komputera, na którym jest uruchamiany, są dokładne i nie zmieniają się, co oczywiście zawsze się zdarza i często.

System typów jest automatycznie weryfikowalnymi dowodami niektórych aspektów poprawności. Na przykład system typów Rust'a może udowodnić, że odwołanie nie przeżywa obiektu, do którego się odwołuje, lub że obiekt, do którego się odwołuje, nie jest modyfikowany przez inny wątek.

Ale systemy typów są dość ograniczone:

• Szybko napotykają problemy rozstrzygalności. W szczególności sam system typów powinien być rozstrzygalny, jednak wiele praktycznych systemów typu przypadkowo jest Turing Complete (w tym C ++ z powodu szablonów i Rust z powodu cech). Ponadto, niektóre właściwości weryfikowanego programu mogą być nierozstrzygalne w ogólnym przypadku, najsłynniej, czy jakiś program się zatrzymuje (czy rozbiega).

• Ponadto systemy typów powinny działać szybko, najlepiej w czasie liniowym. Nie wszystkie możliwe dowody powinny być przedstawione w systemie typów. Np. Zwykle unika się analizy całego programu, a dowody obejmują pojedyncze moduły lub funkcje.

Z powodu tych ograniczeń systemy typów mają tendencję do sprawdzania tylko dość słabych właściwości, które można łatwo udowodnić, np. Że funkcja jest wywoływana z wartościami poprawnego typu. Jednak nawet to znacznie ogranicza ekspresję, więc często stosuje się obejścia (jak interface{}w Go, dynamicw C #, Objectw Javie, void*w C), a nawet w językach, które całkowicie unikają pisania statycznego.

Im silniejsze właściwości zweryfikujemy, tym mniej wyrazisty będzie zwykle język. Jeśli napisałeś Rust, poznasz te momenty „walki z kompilatorem”, w których kompilator odrzuca pozornie poprawny kod, ponieważ nie był w stanie udowodnić poprawności. W niektórych przypadkach nie można wyrazić określonego programu w Rust, nawet jeśli uważamy, że możemy udowodnić jego poprawność. unsafeMechanizm w Rust lub C # pozwala na ucieczkę granicach systemu typu. W niektórych przypadkach odroczenie kontroli w czasie wykonywania może być inną opcją - ale oznacza to, że nie możemy odrzucić niektórych niepoprawnych programów. To kwestia definicji. Program Rust, który wpada w panikę jest bezpieczny, jeśli chodzi o system typów, ale niekoniecznie z perspektywy programisty lub użytkownika.

Języki są projektowane razem z ich systemem typów. Rzadko zdarza się, aby nowy system typów został narzucony na istniejący język (ale patrz np. MyPy, Flow lub TypeScript). Język będzie próbował ułatwić pisanie kodu zgodnego z systemem typów, np. Oferując adnotacje typu lub wprowadzając łatwe do udowodnienia struktury przepływu sterowania. Różne języki mogą kończyć się różnymi rozwiązaniami. Np. Java ma pojęcie finalzmiennych, które są przypisywane dokładnie raz, podobnie jak mutzmienne Rust :

final int x;
if (...) { ... }
else     { ... }
doSomethingWith(x);

Java ma reguły systemowe typu, które określają, czy wszystkie ścieżki przypisują zmienną, czy kończą funkcję, zanim zmienna będzie dostępna. W przeciwieństwie do tego Rust upraszcza ten dowód, ponieważ nie ma zadeklarowanych, ale niezaprojektowanych zmiennych, ale umożliwia zwracanie wartości z instrukcji przepływu sterowania:

let x = if ... { ... } else { ... };
do_something_with(x)

Wygląda to na naprawdę drobną kwestię przy ustalaniu zadania, ale jasne określenie zakresu jest niezwykle ważne w przypadku dowodów związanych z życiem.

Gdybyśmy zastosowali system Java w stylu Rust, mielibyśmy o wiele większe problemy: obiekty Java nie są opatrzone adnotacjami o czasach istnienia, więc musielibyśmy traktować je jak &'static SomeClasslub Arc<dyn SomeClass>. Osłabiłoby to wszelkie wynikające z tego dowody. Java ma też żadnego pojęcia typu poziomowego niezmienności więc nie możemy odróżnić &i &mutrodzaje. Musielibyśmy traktować każdy obiekt jako komórkę lub muteks, chociaż może to zakładać silniejsze gwarancje niż faktycznie oferuje Java (zmiana pola Java nie jest bezpieczna dla wątków, chyba że jest zsynchronizowana i niestabilna). Wreszcie Rust nie ma pojęcia dziedziczenia implementacji w stylu Java.

Systemy typu TL; DR: są dowodami twierdzeń. Są one jednak ograniczone problemami rozstrzygalności i problemami z wydajnością. Nie można po prostu wziąć jednego systemu typów i zastosować go w innym języku, ponieważ składnia języka docelowego może nie zapewniać niezbędnych informacji i ponieważ semantyka może być niezgodna.

Jak bezpieczny jest bezpieczny?

Tak, prawie możliwe jest napisanie takiego weryfikatora: twój program musi tylko zwrócić stałą UNSAFE. Będziesz miał 99% czasu

Ponieważ nawet jeśli uruchomisz bezpieczny program Rust, ktoś nadal może wyciągnąć wtyczkę podczas jego wykonywania: więc twój program może się zatrzymać, nawet jeśli teoretycznie nie powinien.

I nawet jeśli twój serwer działa w faradayowej klatce w bunkrze, sąsiedni proces może wykonać exploit młota rowkowego i zrobić trochę przewrotu w jednym z rzekomo bezpiecznych programów Rust.

Próbuję powiedzieć, że twoje oprogramowanie będzie działać w środowisku niedeterministycznym, a na działanie może mieć wpływ wiele czynników zewnętrznych.

Żart na bok, automatyczna weryfikacja

Istnieją już statyczne analizatory kodu, które potrafią wykryć ryzykowne konstrukcje programistyczne (niezainicjowane zmienne, przepełnienie bufora itp.). Działają one, tworząc wykres programu i analizując propagację ograniczeń (typy, zakresy wartości, sekwencjonowanie).

Tego rodzaju analizy są również przeprowadzane przez niektóre kompilatory w celu optymalizacji.

Z pewnością można pójść o krok dalej, a także przeanalizować współbieżność i dokonać dedukcji dotyczących propagacji ograniczeń w kilku wątkach, synchronizacji i warunków wyścigowych. Jednak bardzo szybko wpadłbyś na problem kombinatorycznej eksplozji między ścieżkami wykonywania i wieloma niewiadomymi (operacje we / wy, planowanie systemu operacyjnego, dane wejściowe użytkownika, zachowanie programów zewnętrznych, przerwy itp.), Które rozwiążą znane ograniczenia minimum i bardzo utrudniają wyciągnięcie jakichkolwiek przydatnych automatycznych wniosków na temat dowolnego kodu.

Turing zajął się tym w 1936 r., Pisząc o problemie zatrzymania. Jednym z rezultatów jest to, że po prostu niemożliwym jest napisanie algorytmu, który w 100% przypadków może analizować kod i poprawnie ustalić, czy się zatrzyma, czy nie, niemożliwe jest napisanie algorytmu, który potrafi w 100% poprawnie określ, czy kod ma jakąś konkretną właściwość, czy nie, w tym „bezpieczeństwo”, jednak chcesz to zdefiniować.

Jednak wynik Turinga nie wyklucza możliwości, że program, który w 100% przypadków może (1) absolutnie określić kod jest bezpieczny, (2) bezwzględnie ustalić, że kod jest niebezpieczny, lub (3) antropomorficznie podnieść ręce i powiedzieć: „Cholera, nie wiem”. Kompilator Rust, ogólnie mówiąc, należy do tej kategorii.

Jeśli program jest całkowity (nazwa techniczna programu, który gwarantuje zatrzymanie), teoretycznie możliwe jest udowodnienie dowolnej arbitralnej własności w stosunku do programu przy wystarczających zasobach. Możesz po prostu zbadać każdy potencjalny stan, w którym program może wejść, i sprawdzić, czy którykolwiek z nich narusza twoją własność. TLA + język modelu sprawdzanie wykorzystuje wariant tej metody, za pomocą teorii mnogości, by sprawdzić właściwości przeciw zestawów potencjalnych stanów programu, zamiast obliczania wszystkie stany.

Technicznie rzecz biorąc, każdy program wykonywany na dowolnym praktycznym sprzęcie fizycznym ma albo całkowitą, albo możliwą do udowodnienia pętlę, ponieważ masz tylko ograniczoną ilość dostępnej pamięci, więc istnieje tylko skończona liczba stanów, w których komputer może się znaleźć. komputer jest w rzeczywistości skończoną maszyną stanu, nie Turing jest kompletny, ale przestrzeń stanu jest tak duża, że ​​łatwiej jest udawać, że się kończy.

Problem z tym podejściem polega na tym, że ma wykładniczą złożoność w stosunku do ilości pamięci i wielkości programu, co czyni go niepraktycznym dla niczego innego niż rdzeń algorytmów i niemożliwym do zastosowania w przypadku znacznych baz kodu w całości.

Zdecydowana większość badań koncentruje się na dowodach. Korespondencja Curry'ego-Howarda stwierdza, że ​​dowód poprawności i system typów to jedno i to samo, dlatego większość praktycznych badań nosi nazwę systemów typów. Szczególnie istotne w tej dyskusji są Coq i Idriss, oprócz rdzy, o której już wspomniałeś. Coq podchodzi do problemu inżynieryjnego z drugiej strony. Biorąc dowód poprawności dowolnego kodu w języku Coq, może wygenerować kod, który wykonuje sprawdzony program. Tymczasem Idriss używa systemu typów zależnych do udowodnienia dowolnego kodu w języku podobnym do języka Haskell. Oba te języki spychają trudne problemy z wygenerowaniem sprawdzającego dowodu na pisarz, umożliwiając sprawdzanie typów skoncentrowanie się na sprawdzaniu dowodu. Sprawdzenie dowodu jest znacznie prostszym problemem, ale sprawia to, że języki są znacznie trudniejsze do pracy.

Oba te języki zostały specjalnie zaprojektowane w celu ułatwienia prób, wykorzystując czystość do kontrolowania stanu, który jest istotny dla poszczególnych części programu. W przypadku wielu głównych języków samo udowodnienie, że część stanu jest nieistotna dla dowodu części programu, może być złożonym problemem ze względu na charakter skutków ubocznych i zmiennych wartości.