Jakie są zalety bezpieczeństwa systemu typu?

W JavaScript: Dobre części Douglasa Crockforda wspomina w swoim rozdziale dotyczącym dziedziczenia:

Inną zaletą klasycznego dziedziczenia jest to, że obejmuje specyfikację systemu typów. To głównie uwalnia programistę od konieczności pisania jawnych operacji rzutowania, co jest bardzo dobrą rzeczą, ponieważ podczas rzutowania tracone są zalety bezpieczeństwa systemu typów.

Przede wszystkim, czym właściwie jest bezpieczeństwo? ochrona przed uszkodzeniem danych, hakerami, awariami systemu itp.?

Jakie są zalety bezpieczeństwa systemu typu? Co wyróżnia system typów, który pozwala mu zapewnić te korzyści bezpieczeństwa?

Systemy typów zapobiegają błędom

Systemy typów eliminują nielegalne programy. Rozważ następujący kod Python.

 a = 'foo'
 b = True
 c = a / b

W Pythonie ten program nie działa; rzuca wyjątek. W języku takim jak Java, C #, Haskell , cokolwiek, nie jest to nawet legalny program. Całkowicie unikasz tych błędów, ponieważ po prostu nie są one możliwe w zestawie programów wejściowych.

Podobnie lepszy system typów wyklucza więcej błędów. Jeśli przejdziemy do super zaawansowanych systemów typów, możemy powiedzieć coś takiego:

 Definition divide x (y : {x : integer | x /= 0}) = x / y

Teraz system typów gwarantuje, że nie będzie żadnych błędów dzielenia przez 0.

Jakie błędy

Oto krótka lista rodzajów błędów, którym mogą zapobiec systemy

1. Błędy poza zakresem
2. Wstrzyknięcie SQL
3. Uogólniając 2, wiele problemów związanych z bezpieczeństwem (po co sprawdzanie skażenia w Perlu )
4. Błędy poza sekwencją (zapominanie o wywołaniu init)
5. Wymuszanie użycia podzbioru wartości (na przykład tylko liczby całkowite większe niż 0)
6. Niegrzeczne kocięta (Tak, to był żart)
7. Błędy utraty precyzji
8. Błędy oprogramowania pamięci transakcyjnej (STM) (wymaga to czystości, która wymaga również typów)
9. Uogólniając 8, kontrolując efekty uboczne
10. Niezmienniki ponad strukturami danych (czy drzewo binarne jest zrównoważone?)
11. Zapominanie wyjątku lub rzucanie niewłaściwego

I pamiętaj, że jest to również w czasie kompilacji . Nie musisz pisać testów ze 100% pokryciem kodu, aby po prostu sprawdzić błędy typu, kompilator to zrobi za Ciebie :)

Studium przypadku: Wpisany rachunek lambda

Dobra, przyjrzyjmy się najprostszemu ze wszystkich systemów typów, po prostu typowi rachunku lambda .

Zasadniczo istnieją dwa typy,

Type = Unit | Type -> Type

Wszystkie terminy są zmiennymi, lambdami lub aplikacjami. Na tej podstawie możemy udowodnić, że każdy dobrze napisany program kończy się. Nigdy nie ma sytuacji, w której program utknie lub zapętli się na zawsze. Nie jest to możliwe do udowodnienia w normalnym rachunku lambda, ponieważ cóż, to nieprawda.

Pomyśl o tym, możemy użyć systemów typów, aby zagwarantować, że nasz program nie zapętla się wiecznie, a raczej fajnie, prawda?

Objazd do typów dynamicznych

Systemy typu dynamicznego mogą oferować identyczne gwarancje jak systemy typu statycznego, ale w czasie wykonywania, a nie w czasie kompilacji. W rzeczywistości, ponieważ jest to środowisko wykonawcze, możesz zaoferować więcej informacji. Tracisz jednak pewne gwarancje, w szczególności dotyczące właściwości statycznych, takich jak zakończenie.

Dlatego typy dynamiczne nie wykluczają niektórych programów, ale raczej kierują źle sformułowane programy do dobrze zdefiniowanych akcji, takich jak zgłaszanie wyjątków.

TLDR

Długa i krótka jest to, że systemy typów wykluczają niektóre programy. Wiele programów jest w jakiś sposób zepsutych, dlatego w systemach typu unikamy tych zepsutych programów.

Sama rzeczywistość jest wpisana. Nie można dodawać długości do ciężarów. I chociaż możesz dodawać stopy do metrów (oba są jednostkami długości), powinieneś skalować co najmniej jeden z dwóch. Niezastosowanie się do tego może dosłownie zepsuć misję Marsa.

W systemie typu bezpieczny dodanie dwóch długości wyrażonych w różnych jednostkach byłoby błędem lub spowodowałoby automatyczne rzucanie.

System typów pomaga uniknąć prostych błędów kodowania, a raczej pozwala kompilatorowi wychwycić te błędy.

Na przykład w JavaScript i Python następujący problem często zostanie wykryty tylko w czasie wykonywania - i w zależności od testowania jakości / rzadkości warunku może faktycznie dojść do produkcji:

if (someRareCondition)
     a = 1
else
     a = {1, 2, 3}

// 10 lines below
k = a.length

Podczas gdy mocno pisany język zmusi cię do jawnego stwierdzenia, że ajest tablicą i nie pozwoli ci przypisać liczby całkowitej. W ten sposób, nie ma żadnych szans anie będzie miał length- nawet w rzadkich przypadkach.

Im wcześniej w cyklu tworzenia oprogramowania można wykryć błąd, tym tańsze jest jego naprawienie. Rozważ błąd, który powoduje, że największy klient lub wszyscy klienci tracą dane. Taki błąd może być końcem Twojej firmy, jeśli zostanie wykryty dopiero po utracie danych przez prawdziwych klientów! Znalezienie i usunięcie tego błędu przed przeniesieniem go do produkcji jest zdecydowanie tańsze .

Nawet w przypadku mniej kosztownych błędów zużywa się więcej czasu i energii, jeśli zaangażowani są testerzy, niż jeśli programiści mogą je znaleźć i naprawić. Jest to tańsze, jeśli nie zostanie poddane kontroli źródła, gdzie inni programiści mogą budować oprogramowanie, które na nim polega. Bezpieczeństwo typu zapobiega nawet kompilacji niektórych klas błędów, eliminując w ten sposób prawie cały potencjalny koszt tych błędów.

Ale to nie jest cała historia. Jak powie każdy programista w dynamicznym języku, czasami fajnie jest, jeśli Twój program po prostu się skompiluje, abyś mógł wypróbować jego część bez wykonywania najmniejszych szczegółów. Istnieje kompromis między bezpieczeństwem a wygodą. Testy jednostkowe mogą zmniejszyć część ryzyka używania dynamicznego języka, ale pisanie i utrzymywanie dobrych testów jednostkowych ma swój własny koszt, który może być wyższy niż koszt używania języka bezpiecznego dla typu.

Jeśli eksperymentujesz, jeśli Twój kod zostanie użyty tylko raz (na przykład jednorazowy raport), lub jeśli znajdujesz się w sytuacji, w której nie zawracałbyś sobie głowy pisaniem testu jednostkowego, to dynamiczny język jest prawdopodobnie idealny dla Was. Jeśli masz dużą aplikację i chcesz zmienić jedną część, nie niszcząc jej pozostałych, bezpieczeństwo typu jest ratowaniem życia. Rodzaje błędów typu blokady bezpieczeństwa są dokładnie rodzajem błędów, które ludzie przeoczają lub się mylą podczas refaktoryzacji.

Wprowadzenie

Bezpieczeństwo typów można osiągnąć za pomocą języków o typie statycznym (skompilowanym, statycznym sprawdzaniu typu) i / lub w środowisku wykonawczym (ewaluowanym, dynamicznym sprawdzaniu typów). Według Wikipedii „... silny system typów jest opisany jako taki, w którym nie ma możliwości niezaznaczonego błędu typu środowiska wykonawczego (ed Luca Cardelli). Innymi słowy, brak niesprawdzonych błędów w czasie wykonywania określa się jako bezpieczeństwo lub bezpieczeństwo typu ... ”

Bezpieczeństwo - sprawdzanie typu statycznego

Klasycznie, bezpieczeństwo typów było synonimem pisania statycznego, w takich językach jak C, C ++ i Haskell, które mają na celu wykrywanie niezgodności typów podczas ich kompilacji. Ma to tę zaletę, że pozwala uniknąć potencjalnie niezdefiniowanych lub podatnych na błędy warunków podczas wykonywania programu. Może to być nieocenione, gdy istnieje ryzyko, że typy wskaźników mogą być źle dopasowane, na przykład sytuacja, która może prowadzić do katastrofalnych konsekwencji, jeśli nie zostanie wykryta. W tym sensie pisanie statyczne jest uważane za synonim bezpieczeństwa pamięci.

Pisanie statyczne nie jest jednak całkowicie bezpieczne, ale zwiększa bezpieczeństwo . Nawet systemy o typie statycznym mogą mieć katastrofalne konsekwencje. Wielu ekspertów uważa, że ​​typowanie statyczne może służyć do pisania bardziej niezawodnych i mniej podatnych na błędy (krytycznych dla misji) systemów.

Języki o typie statycznym mogą pomóc zmniejszyć ryzyko utraty danych lub utraty dokładności w pracy numerycznej, które może wystąpić z powodu niewłaściwego lub obciętego podwójnego do zmiennoprzecinkowego lub niewłaściwego dopasowywania typów całkowitych i zmiennoprzecinkowych.

Zaletą używania języków o typie statycznym jest zwiększenie wydajności i szybkości wykonywania. Środowisko wykonawcze korzysta z braku konieczności określania typów podczas wykonywania.

Bezpieczeństwo - sprawdzanie typu środowiska wykonawczego

Na przykład Erlang jest deklaratywnym typem, dynamicznie sprawdzanym językiem, który działa na maszynie wirtualnej. Kod Erlanga można skompilować bajtowo. Erlang jest uważany za prawdopodobnie najważniejszy dostępny język o znaczeniu krytycznym, odporny na awarie, i donosi się, że Erlang ma niezawodność na poziomie 9 9 (99,9999999% lub nie więcej niż 31,5 ms rocznie).

Niektóre języki, takie jak Common Lisp, nie są wpisywane statycznie, ale w razie potrzeby można zadeklarować typy, co może poprawić szybkość i wydajność. Należy również zauważyć, że wiele powszechnie używanych języków interpretowanych, takich jak Python, pod pętlą oceny są pisane w językach o typie statycznym, takich jak C lub C ++. Zarówno Commom Lisp, jak i Python są uważane za bezpieczne typu zgodnie z powyższą definicją.

utracone zostają zalety bezpieczeństwa systemu typu.

Przede wszystkim, czym właściwie jest bezpieczeństwo? ochrona przed uszkodzeniem danych, hakerami, awariami systemu itp.?

Jakie są zalety bezpieczeństwa systemu typu? Co wyróżnia system typów, który pozwala mu zapewnić te korzyści bezpieczeństwa?

Czuję, że systemy typu mają tak negatywny pogląd. System typów polega bardziej na zapewnieniu gwarancji niż na udowodnieniu braku błędów. To ostatnie jest konsekwencją systemu typów. System typów dla języka programowania jest sposobem na uzyskanie w czasie kompilacji dowodu, że program spełnia pewną specyfikację.

Rodzaj specyfikacji, którą można zakodować jako typ, zależy od języka, lub bardziej bezpośrednio, od siły systemu typów języka.

Najbardziej podstawowym rodzajem specyfikacji jest gwarancja dotycząca wejściowego / wyjściowego zachowania funkcji i ważności wnętrza ciała funkcji. Rozważ nagłówek funkcji

f : (Int,Int) -> String

Dobry system typów upewni się, że f zostanie zastosowane tylko do obiektów, które podczas oceny będą wytwarzały parę Int, i zagwarantuje, że f zawsze wytworzy łańcuch.

Niektóre instrukcje w języku, takie jak bloki if-then, nie mają zachowania wejścia / wyjścia; tutaj system typów gwarantuje, że każda deklaracja lub instrukcja w bloku jest ważna; to znaczy stosuje operacje na obiektach właściwego rodzaju. Gwarancje te można łączyć.

Daje to również pewien rodzaj bezpieczeństwa pamięci. Cytat, z którym masz do czynienia, dotyczy castingu. W niektórych przypadkach rzutowanie jest w porządku, na przykład rzutowanie 32-bitowego Int na 64-bitowy Int. Jednak generalnie powoduje awarię systemu typów.

Rozważać

Foo x = new Foo(3,4,5,6);
f((Int)x,(Int)x);

Z powodu rzutowania x zamienia się w Int, więc technicznie powyższe sprawdza typ; jednak tak naprawdę nie spełnia celu sprawdzania typu.

Jedną rzeczą, która mogłaby stworzyć inny i lepszy system typów, jest niedopuszczenie rzutów (A) x, gdzie x przed skrzynką jest typu B, chyba że B jest podtypem (lub podobiektem) A. Idee teorii podtypów zostały wykorzystane w bezpieczeństwie w celu usunięcia możliwości ataków przepełnienia / niedopełnienia liczb całkowitych.

Podsumowanie

System typów jest sposobem na udowodnienie, że program spełnia pewną specyfikację. Korzyści, jakie może zapewnić system typów, zależą od siły zastosowanego systemu typów.

Jedna z niewymienionych zalet systemu typów polega na tym, że wiele programów jest czytanych więcej niż jest napisanych, aw wielu przypadkach system typów może pozwalać na sprecyzowanie dużej ilości informacji w sposób zwięzły i łatwo dostępny strawione przez kogoś czytającego kod. Podczas gdy typy parametrów nie zastępują opisowych komentarzy, większość osób szybciej je przeczyta: „int Distance;” lubDistance As Int32niż przeczytać „Odległość musi być liczbą całkowitą +/- 2147483647”; przekazywanie ułamków może dawać niespójne wyniki. ”Ponadto typy parametrów mogą pomóc zmniejszyć różnicę między tym, co dzieje się w konkretnej implementacji interfejsu API, a tym, na czym mogą polegać osoby wywołujące. Na przykład, jeśli konkretna implementacja interfejsu JavaScript w interfejsie API używa jego parametrów w taki sposób, by zmuszenia strun do postaci cyfrowej, mogą być jasne, czy wywołujący mogą polegać na takie działania, czy inne implementacje awarii API potęgę jeśli danych napisów. obejmujący sposób, którego parametr określa się jako DoublebĘDZIE wyjaśnij, że przed przekazaniem wartości wywołujące muszą zostać wymuszone przez osobę wywołującą; mając metodę z przeciążeniem, która akceptuje, Doublei inną, która akceptujeString uczyniłoby to nieco jaśniejszym, że dzwoniący posiadający ciągi znaków będą mogli przekazać je jako takie.

Przede wszystkim, czym właściwie jest bezpieczeństwo? Ochrona przed uszkodzeniem danych, hakerami, awariami systemu itp.?

Wszystkie pozostałe odpowiedzi i więcej. Zasadniczo „bezpieczeństwo typu” oznacza po prostu, że żaden program, który kompilator pomyślnie skompiluje, nie będzie zawierał błędów typu.

Co to jest błąd typu? Zasadniczo można określić dowolną niepożądaną właściwość jako błąd typu, a niektóre systemy typów będą w stanie statycznie upewnić się, że żaden program nie ma takiego błędu.

Przez „właściwość” powyżej rozumiem pewną logiczną propozycję, która dotyczy twojego programu, na przykład „wszystkie indeksy mieszczą się w granicach tablicy”. Inne typy właściwości obejmują: „wszystkie niepoprawne wskaźniki są poprawne”, „ten program nie wykonuje żadnych operacji we / wy” lub „ten program wykonuje operacje we / wy tylko do / dev / null” itp. Prawie każdy rodzaj można określić właściwość i sprawdzić typ w ten sposób, w zależności od ekspresyjności systemu typów.

Zależne systemy typów należą do najbardziej ogólnych systemów typów, dzięki którym można egzekwować prawie dowolne właściwości. Niekoniecznie jest to jednak łatwe, ponieważ wyrafinowane właściwości podlegają niekompletności dzięki uprzejmości Gödela .