Bezpieczeństwo typu - Type safety

W informatyce , bezpieczeństwa typ jest zakres, w jakim język programowania zniechęca lub uniemożliwia typu błędy . Błąd typu to błędne zachowanie programu spowodowane rozbieżnością między różnymi typami danych dla stałych, zmiennych i metod (funkcji) programu, np. traktowanie liczby całkowitej ( int ) jako liczby zmiennoprzecinkowej ( float ) Potrzebny lepszy przykład . Bezpieczeństwo typów jest czasami alternatywnie uważane za właściwość programu komputerowego, a nie język, w którym ten program jest napisany; oznacza to, że niektóre języki mają funkcje bezpiecznego typu, które mogą być ominięte przez programistów, którzy używają innych funkcji typu niebezpiecznego w tym samym języku. Formalna teoretyczna definicja bezpieczeństwa typów jest znacznie silniejsza niż to, co rozumie większość programistów.

Wymuszanie typu może być statyczne, wyłapujące potencjalne błędy w czasie kompilacji lub dynamiczne, kojarzące informacje o typie z wartościami w czasie wykonywania i sprawdzające je w razie potrzeby w celu wykrycia nieuchronnych błędów lub kombinacji obu. Wymuszanie typu dynamicznego zasadniczo pozwala na uruchomienie nieprawidłowego programu.

Zachowania klasyfikowane jako błędy typu przez dany język programowania to zazwyczaj te, które wynikają z prób wykonania operacji na wartościach , które nie mają odpowiedniego typu danych . Ta klasyfikacja jest częściowo oparta na opinii.

W kontekście systemów typów statycznych (w czasie kompilacji) bezpieczeństwo typów zwykle obejmuje (między innymi) gwarancję, że ostateczna wartość dowolnego wyrażenia będzie prawidłowym elementem składowym typu statycznego tego wyrażenia. Dokładne wymaganie jest bardziej subtelne niż to — zobacz na przykład podtypowanie i polimorfizm (informatyka) dla komplikacji.

Bezpieczeństwo typów jest ściśle powiązane z bezpieczeństwem pamięci , ograniczeniem możliwości kopiowania dowolnych wzorców bitowych z jednej lokalizacji pamięci do drugiej. Na przykład w implementacji języka, który ma pewien typ , tak że pewna sekwencja bitów (o odpowiedniej długości) nie reprezentuje prawidłowego członka , jeśli język ten umożliwia kopiowanie danych do zmiennej typu , to nie jest bezpieczny ze względu na typ, ponieważ taka operacja może przypisać do zmiennej inną niż wartość. I odwrotnie, jeśli język nie jest bezpieczny pod względem typu do tego stopnia, że ​​pozwala na użycie dowolnej liczby całkowitej jako wskaźnika , to nie jest bezpieczny w pamięci.

Większość języków statycznie typowanych zapewnia stopień bezpieczeństwa typów, który jest ściślejszy niż bezpieczeństwo pamięci, ponieważ ich systemy typów wymuszają właściwe użycie abstrakcyjnych typów danych zdefiniowanych przez programistów, nawet jeśli nie jest to absolutnie konieczne dla bezpieczeństwa pamięci lub zapobiegania wszelkim rodzajom katastrofalnej awarii.

Definicje

Kod bezpieczny dla typu umożliwia dostęp tylko do tych lokalizacji w pamięci, do których ma dostęp. (W tej dyskusji bezpieczeństwo typów odnosi się w szczególności do bezpieczeństwa typów pamięci i nie powinno być mylone z bezpieczeństwem typów w szerszym zakresie). Na przykład kod bezpieczny dla typu nie może odczytywać wartości z pól prywatnych innego obiektu.

Robin Milner podał następujące hasło opisujące bezpieczeństwo typu:

Dobrze napisane programy nie mogą się „pomylić”.

Odpowiednie sformalizowanie tego hasła zależy od stylu semantyki formalnej zastosowanej dla danego języka. W kontekście semantyki denotacyjnej bezpieczeństwo typów oznacza, że ​​wartość wyrażenia, które jest dobrze wpisane, powiedzmy z typem τ, jest w dobrej wierze członkiem zbioru odpowiadającego τ.

W 1994 roku Andrew Wright i Matthias Felleisen sformułowali to, co jest obecnie standardową definicją i techniką sprawdzania bezpieczeństwa typów w językach zdefiniowanych przez semantykę operacyjną . W tym podejściu bezpieczeństwo typów jest określane przez dwie właściwości semantyki języka programowania:

(Typ-) zachowanie lub redukcja tematu
„Dokładność typowania” („typowalność”) programów pozostaje niezmienna w ramach reguł przejściowych (tj. reguł oceny lub reguł redukcji) języka.
Postęp
Dobrze napisany (możliwy do wpisania) program nigdy się nie „zacina”, co oznacza, że wyrażenia w programie będą albo wartościowane do wartości , albo istnieje dla tego reguła przejścia; innymi słowy, program nigdy nie wchodzi w niezdefiniowany stan, w którym nie są możliwe dalsze przejścia.

Te właściwości nie istnieją w próżni; są one powiązane z semantyką języka programowania, który opisują, i istnieje duża liczba różnych języków, które mogą spełniać te kryteria, ponieważ pojęcie „dobrze napisanego” programu jest częścią statycznej semantyki języka programowania i pojęcia „utknięcie” (lub „pomyłka”) jest właściwością jego dynamicznej semantyki .

Vijay Saraswat podaje następującą definicję:

„Język jest bezpieczny dla typu, jeśli jedyne operacje, które można wykonać na danych w języku, to te, które są usankcjonowane przez typ danych”.

Związek z innymi formami bezpieczeństwa

Bezpieczeństwo typu ma ostatecznie na celu wykluczenie innych problemów, np.:-

  • Zapobieganie nielegalnym operacjom. Na przykład możemy zidentyfikować wyrażenie 3 / "Hello, World"jako nieważne, ponieważ zasady arytmetyki nie określają sposobu dzielenia liczby całkowitej przez łańcuch .
  • Bezpieczeństwo pamięci
    • Dzikie wskaźniki mogą powstać, gdy wskaźnik do jednego obiektu typu jest traktowany jako wskaźnik do innego typu. Na przykład rozmiar obiektu zależy od typu, więc jeśli wskaźnik zostanie zwiększony przy niewłaściwych poświadczeniach, w końcu będzie wskazywał na jakiś losowy obszar pamięci.
    • Przepełnienie buforu — zapisy poza zakresem mogą uszkodzić zawartość obiektów już obecnych na stercie. Może się to zdarzyć, gdy większy obiekt jednego typu zostanie z grubsza skopiowany do mniejszego obiektu innego typu.
  • Błędy logiczne pochodzące z różnych typów semantyki . Na przykład cale i milimetry mogą być przechowywane jako liczby całkowite, ale nie należy ich zastępować ani dodawać. System typów może wymusić dla nich dwa różne typy liczb całkowitych.

Języki z bezpiecznym i niebezpiecznym typem

Bezpieczeństwo typów jest zwykle wymogiem dla każdego języka-zabawki proponowanego w akademickich badaniach nad językiem programowania. Z drugiej strony, wiele języków jest zbyt obszernych dla dowodów bezpieczeństwa generowanych przez człowieka, ponieważ często wymagają one sprawdzenia tysięcy przypadków. Niemniej jednak niektóre języki, takie jak Standard ML , który ma rygorystycznie zdefiniowaną semantykę, spełniają jedną definicję bezpieczeństwa typów. Niektóre inne języki takie jak HaskellUważa się spotkać jakąś definicję bezpieczeństwa typu, pod warunkiem pewne „uciec” funkcje nie są używane (np Haskell za unsafePerformIO , używany do „ucieczki” od zwykłej ograniczonym środowisku, w którym I / O jest możliwe obejście system typów, a więc może być użyty do złamania bezpieczeństwa typów ) . Niezależnie od właściwości definicji języka, pewne błędy mogą wystąpić w czasie wykonywania z powodu błędów w implementacji lub w połączonych bibliotekach napisanych w innych językach; takie błędy mogą w pewnych okolicznościach spowodować, że dany typ implementacji stanie się niebezpieczny. Wczesna wersja wirtualnej maszyny Java firmy Sun była podatna na tego rodzaju problem.

Mocne i słabe pisanie

Języki programowania są często potocznie klasyfikowane jako silnie lub słabo typowane (również luźno typowane), aby odnosić się do pewnych aspektów bezpieczeństwa typów. W 1974 roku Liskov i Zilles zdefiniowali język silnie typizowany jako taki, w którym „za każdym razem, gdy obiekt jest przekazywany z funkcji wywołującej do funkcji wywoływanej, jego typ musi być zgodny z typem zadeklarowanym w wywoływanej funkcji”. W 1977 roku Jackson napisał: „W mocno typizowanym języku każdy obszar danych będzie miał odrębny typ, a każdy proces określi swoje wymagania komunikacyjne w odniesieniu do tych typów”. W przeciwieństwie do tego, słabo typizowany język może dawać nieprzewidywalne wyniki lub może wykonywać niejawną konwersję typu.

Bezpieczeństwo pisania w językach obiektowych

W językach obiektowych bezpieczeństwo typów jest zwykle nierozerwalnie związane z faktem, że istnieje system typów . Wyraża się to w definicjach klas.

Klasy zasadniczo określa strukturę przedmiotów pochodzących z niego oraz API jako zamówienia do obsługi tych obiektów. Za każdym razem, gdy tworzony jest nowy obiekt, będzie on zgodny z tą umową.

Każda funkcja, która wymienia obiekty pochodzące z określonej klasy lub implementująca określony interfejs , będzie przestrzegać tego kontraktu: stąd w tej funkcji operacje dozwolone na tym obiekcie będą tylko operacjami zdefiniowanymi przez metody klasy implementowanej przez obiekt. Zagwarantuje to zachowanie integralności obiektu.

Wyjątkiem są języki zorientowane obiektowo, które umożliwiają dynamiczną modyfikację struktury obiektu lub wykorzystanie odbicia do modyfikacji zawartości obiektu w celu przezwyciężenia ograniczeń nałożonych przez definicje metod klas.

Wpisz kwestie bezpieczeństwa w określonych językach

Ada

Ada została zaprojektowana tak, aby była odpowiednia dla systemów wbudowanych , sterowników urządzeń i innych form programowania systemowego , ale także zachęcała do programowania bezpiecznego typu. Aby rozwiązać te sprzeczne cele, Ada ogranicza typ-unsafety do pewnego zestawu specjalnych konstrukcji, których nazwy zwykle zaczynają się od ciągu Unchecked_ . Unchecked_Deallocation może zostać skutecznie zbanowany z jednostki tekstu Ady poprzez zastosowanie pragmy Pure do tej jednostki. Oczekuje się, że programiści będą używać konstrukcji Unchecked_ bardzo ostrożnie i tylko wtedy, gdy będzie to konieczne; programy, które ich nie używają, są bezpieczne dla typu.

Język programowania SPARK jest podzbiorem Ady, eliminującym wszystkie jego potencjalne niejasności i niepewności, jednocześnie dodając statycznie sprawdzane kontrakty do dostępnych funkcji językowych. SPARK pozwala uniknąć problemów z nieaktualnymi wskaźnikami, całkowicie uniemożliwiając alokację w czasie wykonywania.

Ada2012 dodaje do samego języka kontrakty sprawdzane statycznie (w postaci warunków wstępnych i końcowych oraz niezmienników typu).

C

Język programowania C jest bezpieczny dla typów w ograniczonych kontekstach; na przykład błąd czasu kompilacji jest generowany podczas próby przekonwertowania wskaźnika na jeden typ struktury na wskaźnik na inny typ struktury, chyba że jest używane jawne rzutowanie. Jednak wiele bardzo typowych operacji nie jest bezpiecznych dla typu; na przykład, zwykłym sposobem wypisania liczby całkowitej jest coś takiego jak printf("%d", 12), gdzie w czasie wykonywania %dnakazuje printfoczekiwać argumentu liczby całkowitej. (Coś w rodzaju printf("%s", 12), który mówi funkcji, aby oczekiwała wskaźnika do ciągu znaków, a jednocześnie dostarcza argument w postaci liczby całkowitej, może być zaakceptowane przez kompilatory, ale da niezdefiniowane wyniki.) Jest to częściowo łagodzone przez niektóre kompilatory (takie jak gcc) sprawdzanie typ korespondencji między argumentami printf a ciągami formatu.

Ponadto C, podobnie jak Ada, zapewnia nieokreślone lub niezdefiniowane jawne konwersje; i w przeciwieństwie do Ady, idiomy używające tych konwersji są bardzo powszechne i pomogły w nadaniu C reputacji niebezpiecznego typu. Na przykład standardowym sposobem alokacji pamięci na stercie jest wywołanie funkcji alokacji pamięci, takiej jak malloc, z argumentem wskazującym, ile bajtów jest wymaganych. Funkcja zwraca wskaźnik bez typu (type void *), który kod wywołujący musi jawnie lub niejawnie rzutować na odpowiedni typ wskaźnika. Wstępnie standaryzowane implementacje języka C wymagały w tym celu jawnego rzutowania, dlatego kod stał się przyjętą praktyką. (struct foo *) malloc(sizeof(struct foo))

C++

Niektóre cechy C++, które promują bardziej bezpieczny typ kodu:

C#

C# jest bezpieczny dla typu (ale nie statycznie bezpieczny dla typu). Posiada wsparcie dla wskaźników bez typu, ale musi być dostępny za pomocą słowa kluczowego "unsafe", które może być zabronione na poziomie kompilatora. Ma wbudowane wsparcie dla walidacji rzutowania w czasie wykonywania. Rzuty można zweryfikować za pomocą słowa kluczowego „as”, które zwróci odwołanie o wartości null, jeśli rzutowanie jest nieprawidłowe, lub za pomocą rzutowania w stylu C, które zgłosi wyjątek, jeśli rzutowanie jest nieprawidłowe. Zobacz Operatory konwersji C Sharp .

Nadmierne poleganie na typie obiektu (z którego pochodzą wszystkie inne typy) wiąże się z ryzykiem pokonania celu systemu typów C#. Zwykle lepszą praktyką jest rezygnacja z odwołań do obiektów na rzecz generyków , podobnie jak szablony w C++ i generyki w Javie .

Jawa

Język Java został zaprojektowany w celu wymuszenia bezpieczeństwa typów. Wszystko w Javie dzieje się wewnątrz obiektu i każdy obiekt jest instancją klasy .

Aby zaimplementować wymuszanie bezpieczeństwa typów , każdy obiekt przed użyciem musi zostać przydzielony . Java pozwala na używanie typów pierwotnych, ale tylko wewnątrz odpowiednio przydzielonych obiektów.

Czasami część bezpieczeństwa typu jest implementowana pośrednio: np. klasa BigDecimal reprezentuje liczbę zmiennoprzecinkową o dowolnej precyzji, ale obsługuje tylko liczby, które można wyrazić skończoną reprezentacją. Operacja BigDecimal.divide() oblicza nowy obiekt jako dzielenie dwóch liczb wyrażonych jako BigDecimal.

W tym przypadku, jeśli dzielenie nie ma skończonej reprezentacji, tak jak podczas obliczania np. 1/3=0,33333..., metoda divide() może zgłosić wyjątek, jeśli nie zdefiniowano trybu zaokrąglania dla operacji. Dlatego biblioteka, a nie język, gwarantuje, że obiekt przestrzega kontraktu zawartego w definicji klasy.

Standardowy ML

Standard ML ma rygorystycznie zdefiniowaną semantykę i wiadomo, że jest bezpieczny dla typów. Jednak niektóre implementacje, w tym Standard ML of New Jersey (SML/NJ), jego wariant składniowy Mythryl i MLton , zapewniają biblioteki oferujące niebezpieczne operacje. Te udogodnienia są często używane w połączeniu z interfejsami funkcji obcych tych implementacji do interakcji z kodem innym niż ML (takim jak biblioteki C), który może wymagać danych ułożonych w określony sposób. Innym przykładem jest sam interaktywny najwyższy poziom SML/NJ , który musi używać niebezpiecznych operacji do wykonania kodu ML wprowadzonego przez użytkownika.

Moduł-2

Modula-2 to silnie typizowany język, którego filozofia projektowania wymaga, aby wszelkie niebezpieczne obiekty były wyraźnie oznaczone jako niebezpieczne. Osiąga się to poprzez „przenoszenie” takich obiektów do wbudowanej pseudobiblioteki o nazwie SYSTEM, z której muszą zostać zaimportowane przed użyciem. Dzięki temu import jest widoczny, gdy takie udogodnienia są używane. Niestety nie zostało to konsekwentnie zaimplementowane w oryginalnym raporcie językowym i jego implementacji. Nadal pozostały niebezpieczne udogodnienia, takie jak składnia rzutowania typów i rekordy wariantów (odziedziczone po Pascalu), których można było używać bez wcześniejszego importu. Trudność w przeniesieniu tych udogodnień do pseudomodułu SYSTEM polegała na braku jakiegokolwiek identyfikatora dla obiektu, który mógłby być następnie zaimportowany, ponieważ można zaimportować tylko identyfikatory, ale nie składnię.

IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *)
VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS;
addr := SYSTEM.ADR(word);

(* but type cast syntax can be used without such import *)
VAR i : INTEGER; n : CARDINAL;
n := CARDINAL(i); (* or *) i := INTEGER(n);

Norma ISO Modula-2 poprawiła to dla funkcji rzutowania typów, zmieniając składnię rzutowania typów na funkcję o nazwie CAST, która musi być importowana z pseudomodułu SYSTEM. Jednak inne niebezpieczne udogodnienia, takie jak zapisy wariantów, pozostały dostępne bez importu z pseudomodułu SYSTEM.

IMPORT SYSTEM;
VAR i : INTEGER; n : CARDINAL;
i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)

Ostatnia zmiana języka rygorystycznie zastosowała oryginalną filozofię projektowania. Po pierwsze, pseudomoduł SYSTEM został przemianowany na UNSAFE, aby uwydatnić niebezpieczny charakter importowanych stamtąd obiektów. Następnie wszystkie pozostałe niebezpieczne obiekty zostały całkowicie usunięte (na przykład rekordy wariantów) lub przeniesione do pseudomodułu UNSAFE. Dla obiektów, w których nie ma identyfikatora, który można by zaimportować, wprowadzono identyfikatory umożliwiające. Aby włączyć taką funkcję, odpowiedni identyfikator włączenia musi zostać zaimportowany z pseudomodułu UNSAFE. W języku nie ma żadnych niebezpiecznych obiektów, które nie wymagają importu z UNSAFE.

IMPORT UNSAFE;
VAR i : INTEGER; n : CARDINAL;
i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)

FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *)
<*FFI="C"*> (* pragma for foreign function interface to C *)

Pascal

Pascal ma szereg wymagań dotyczących bezpieczeństwa typów, z których część jest przechowywana w niektórych kompilatorach. Tam, gdzie kompilator Pascala dyktuje „ścisłe wpisywanie”, dwie zmienne nie mogą być przypisane do siebie, chyba że są kompatybilne (takie jak konwersja liczb całkowitych na rzeczywiste) lub przypisane do identycznego podtypu. Na przykład, jeśli masz następujący fragment kodu:

type
  TwoTypes = record
     I: Integer;
     Q: Real;
  end;

  DualTypes = record
    I: Integer;
    Q: Real;
  end;

var
  T1, T2:  TwoTypes;
  D1, D2:  DualTypes;

Przy ścisłym typowaniu zmienna zdefiniowana jako TwoTypes nie jest kompatybilna z DualTypes (ponieważ nie są one identyczne, nawet jeśli komponenty tego typu zdefiniowanego przez użytkownika są identyczne), a przypisanie {{{1}}} jest niedozwolone. Przypisanie {{{1}}} byłoby legalne, ponieważ zdefiniowane podtypy identyczne. Jednak zlecenie takie jak {{{1}}} byłoby legalne.

Wspólne seplenienie

Ogólnie rzecz biorąc, Common Lisp jest językiem bezpiecznym dla typów. Kompilator Common Lisp jest odpowiedzialny za wstawianie dynamicznych kontroli dla operacji, których bezpieczeństwa typu nie można udowodnić statycznie. Jednak programista może wskazać, że program powinien być skompilowany z niższym poziomem dynamicznego sprawdzania typu. Program skompilowany w takim trybie nie może być uważany za bezpieczny dla typu.

Przykłady C++

Poniższe przykłady ilustrują, jak C++ operatory rzutowania mogą złamać bezpieczeństwo typu, gdy są używane niepoprawnie. Pierwszy przykład pokazuje, w jaki sposób podstawowe typy danych mogą być niepoprawnie rzutowane:

#include <iostream>
using namespace std;

int main () {
    int   ival = 5;                              // integer value
    float fval = reinterpret_cast<float&>(ival); // reinterpret bit pattern
    cout << fval << endl;                        // output integer as float
    return 0;
}

W tym przykładzie reinterpret_castjawnie uniemożliwia kompilatorowi wykonanie bezpiecznej konwersji z liczby całkowitej na wartość zmiennoprzecinkową. Gdy program zostanie uruchomiony, wyświetli wartość zmiennoprzecinkową śmieci. Problemu można było uniknąć, pisząc zamiast tegofloat fval = ival;

Następny przykład pokazuje, w jaki sposób odwołania do obiektów mogą być niepoprawnie odrzucane:

#include <iostream>
using namespace std;

class Parent {
public:
    virtual ~Parent() {} // virtual destructor for RTTI
};

class Child1 : public Parent {
public:
    int a;
};

class Child2 : public Parent {
public:
    float b;
};

int main () {
    Child1 c1;
    c1.a = 5;
    Parent & p = c1;                     // upcast always safe
    Child2 & c2 = static_cast<Child2&>(p); // invalid downcast
    cout << c2.b << endl;          // will output garbage data
    return 0;
}

Dwie klasy podrzędne mają członków różnych typów. Podczas obniżania wskaźnika klasy nadrzędnej do wskaźnika klasy podrzędnej, wynikowy wskaźnik może nie wskazywać na prawidłowy obiekt prawidłowego typu. W tym przykładzie prowadzi to do wypisania wartości śmieci. Problemu można było uniknąć, zastępując static_castgo, dynamic_castktóry zgłasza wyjątek w przypadku nieprawidłowych rzutów.

Zobacz też

Uwagi

Bibliografia