Jakie są zalety bezpieczeństwa systemu typu?

47

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?

type-systems type-safety

— BłędyWereMade
źródło

Nie jestem pewien, czy systemy typów przynoszą jakiekolwiek korzyści dla języka nieskompilowanego, ale jako długoterminowy użytkownik języków skompilowanych uważam, że języki skompilowane ze staranną kontrolą typów skutecznie zapobiegają wielu rodzajom niejednoznacznego, niezdefiniowanego lub niekompletnego kodu przechodzenie przez etap „kompilacji”. Wydaje mi się, że można powiedzieć, że podpowiedzi i system Lint są cenne dla skryptów sieciowych (JavaScript), a jeśli tak, to jestem pewien, że zobaczymy ich wystarczająco dużo. Dart ktoś? Dynamiczne języki, takie jak Python, nie wydają się gorsze z powodu braku statycznego systemu typów.

— Warren P,

1

Dziś rozumiemy, że pisanie na klawiaturze powinno być behawioralne, a nie strukturalne. Niestety, większość współczesnych języków programowania nie ma sposobu, aby potwierdzić zachowanie danego typu (przeczytaj to pytanie, aby przeczytać). To sprawia, że system typów jest w większości przypadków bezużyteczny, zwłaszcza że proste błędy typu, o których tu wspominają odpowiedzi, mogą zostać złapane przez sprytny linijka, która sprawdza typowe problemy.

— Benjamin Gruenbaum

4

@BenjaminGruenbaum To, co już opisujesz, istnieje w takich językach jak OCaml statycznie. Nazywa się to pisaniem strukturalnym, jest właściwie dość stare, pisanie nominalne jest nowsze.

— jozefg

2

@BenjaminGruenbaum: ... Co !? Oczywiście nie jest to nierozstrzygalne w językach o typie statycznym, inaczej napisanie kompilatora dla tych języków byłoby niemożliwe.

— BlueRaja - Danny Pflughoeft

6

@BenjaminGruenbaum: Twoje komentarze są cenne, a ten artykuł jest interesujący, ale nie potwierdza twojego twierdzenia, że „zwykle jest nierozstrzygalny w językach statycznych, takich jak Java”, ponieważ pokazuje, że jest rozstrzygalny w języku C # i pozostawia otwarte pytanie czy jest to nierozstrzygalne w Javie. (W każdym razie, IME, gdy kompilator dla języka o typie statycznym nie może zdecydować, że coś jest dobrze napisane, odrzuca go (lub nie kompiluje), więc nierozstrzygalność jest raczej uciążliwością niż dziurą w typie bezpieczeństwo.)

— ruakh

82

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

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

— jozefg
źródło

25

+1 za kompilację jako odpowiednik napisania dużej liczby testów.

— Dan Neely

3

@ DanNeely To tylko zilustrowanie, że w dynamicznym języku musisz wykonać wszystkie części kodu, aby wychwycić błędy, które system typów sprawdza za darmo. W języku zależnym od typu można faktycznie całkowicie zastąpić testy typami. Wiele razy trzeba jednak udowodnić dodatkowe twierdzenia o poprawności

— jozefg

3

Jeśli twój system typów udowodnił, że twój program musi się zakończyć, (prawdopodobnie) jest to zrobione przez udowodnienie, że oblicza on funkcję prymitywno-rekurencyjną. To chyba fajne, ale znacznie mniej interesująca klasa złożoności niż ta, którą może rozwiązać prawdziwa Maszyna Turinga. (Nie oznacza to, że wartości pośrednie nie są duże; funkcja Ackermanna jest pierwotnie-rekurencyjna…)

— Donal Fellows

5

@DonalFellows Funkcja Ackermanna nie jest prymitywną rekurencyjną, chociaż jest funkcją obliczalną.

— Taymon

4

@sacundim Dokładnie, języki takie jak agda pozwalają na opcjonalne sprawdzanie całości, aw rzadkich przypadkach, gdy chcesz dowolną rekurencję, możesz ładnie zapytać, jest to dość sprytny system.

— jozefg

17

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.

— MSalters
źródło

15

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.

— Eugene
źródło

5

A sprytny linijka w środowisku IDE, takim jak WebStorm JavaScript, może powiedzieć „Możliwe niezdefiniowane odniesienie do a. Długości dla liczby a”. Nie otrzymujemy tego od posiadania jawnego systemu typów.

— Benjamin Gruenbaum,

4

1. Statycznie niezbyt silnie 2. @BenjaminGruenbaum Tak, ale dzieje się to poprzez ściganie wykresu zadań w tle, pomyśl o tym jak o mini-tłumaczu próbującym dowiedzieć się, dokąd zmierzają. Znacznie trudniej niż wtedy, gdy typy dają ci to za darmo

— jozefg

6

@BenjaminGruenbaum: Nie myl niejawnego / jawnego z silnym / słabym. Na przykład Haskell ma niewiarygodnie silny system pisma, który zawstydza większość innych języków, ale z powodu pewnych podjętych decyzji dotyczących projektowania języka jest również w stanie niemal całkowicie uniwersalne wnioskowanie o typie, co zasadniczo czyni go silnie niejawnym językiem pisma z obsługą wyraźnego pisania (Powinieneś tego użyć, ponieważ inferencja typu może wywnioskować tylko z tego, co napisałeś, a nie to, co miałeś na myśli!)

— Phoshi,

6

„Silnie napisany język zmusi cię do jednoznacznego stwierdzenia, że a jest tablicą” To źle. Python jest silnie napisany i nie wymaga tego. Nawet statycznie i silnie typowane języki nie wymagają tego, jeśli obsługują wnioskowanie o typie (a większość współczesnych języków tak robi, przynajmniej częściowo).

— Konrad Rudolph

1

@BenjaminGruenbaum: Ach, wystarczy. Mimo to wystąpią przypadki, w których żaden analizator statyczny JS nie będzie w stanie wykonać tego samego rodzaju kontroli typu, który zapewniłby język silnie typowany, co rozwiąże to w ogólnym przypadku wymaga rozwiązania problemu zatrzymania. Haskell musiał podjąć sporo decyzji projektowych, aby uzyskać prawie 100% wnioskowanie na temat typu, a C # / Scala nie może wywnioskować wszystkiego. Oczywiście w takich przypadkach nie ma to znaczenia, ponieważ możesz po prostu jawnie określić typy - w Javascripcie oznacza to, że nawet najlepszy analizator statyczny nie może dłużej sprawdzać twojego kodu.

— Phoshi

5

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.

— GlenPeterson
źródło

To sprzedaje krótkie pisanie dynamiczne, nie wspominając o jego głównych zaletach (te wymienione są przydatne przez stosunkowo nieistotne). Wydaje się również, że implikuje to coś dziwnego w testach jednostkowych - tak, są one trudne do zrobienia i wiążą się z nimi koszty, i dotyczy to także języków o typie statycznym. Co to próbuje powiedzieć? Nie wspomina również o ograniczeniach (zgodnie z projektem) obecnych systemów typu, zarówno pod względem tego, co mogą wyrazić, jak i błędów, które mogą wykryć.

@MattFenwick, jakie według Ciebie są główne zalety pisania dynamicznego?

— GlenPeterson,

Typowe systemy typu statycznego odrzucają wiele dobrze napisanych programów z założenia. ( alternatywa ) (BTW, moja krytyka

4

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ą.

— AsymLabs
źródło

2

Sprzeciwiam się „silnemu wpisaniu”. Masz na myśli wpisanie statyczne. Silnie napisany typ nie ma większego znaczenia,

— zwykło się

@ jozefg Dobra uwaga. Poprawię post.

— AsymLabs

3

Nie jest również przydatne mówienie językiem interpretowanym ... o implementacji języka tak, ale nie sam język. Każdy język może być interpretowany lub kompilowany. I nawet po edycji używasz terminów silnego i słabego pisania.

— Esailija

3

@ jozefg: Zawsze myślałem, że silnie wpisane oznaczało, że każda wartość ma ustalony typ (np. liczba całkowita, ciąg itp.), podczas gdy słabo wpisane oznacza, że wartość można przekonwertować na wartość innego typu, jeśli uważa się to za wygodne więc. Np. W Pythonie (silnie typowany) 1 + "1"generuje wyjątek, podczas gdy w PHP (słabo typowany) 1 + "1"tworzy 2(łańcuch "1"jest automatycznie konwertowany na liczbę całkowitą 1).

— Giorgio

1

@Giorgio z taką definicją, na przykład Java, nie jest mocno wpisany. Ale w wielu przypadkach tak się twierdzi. Te słowa nie mają znaczenia. Mocne / słabe typy mają znacznie dokładniejszą definicję, jak „Lubię ten język”, jak mówi Józef.

— Esailija

1

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.

— Jonathan Gallagher
źródło

1

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.

— supercat
źródło

0

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 .

— naasking
źródło