Siguranța de tip este o proprietate a unui limbaj de programare care caracterizează siguranța și fiabilitatea în aplicarea sistemului său de tip .
Un sistem de tip se numește sigur ( ing. safe ) sau fiabil ( ing. sunet ) dacă programele care au trecut verificările de consecvență de tip ( ing. programe bine tipizate sau programe bine formate ) exclud posibilitatea apariției erorilor de consecvență de tip la rulare timp [1 ] [2] [3] [4] [5] [6] .
Eroare de potrivire de tip sau eroare de tastare ( Eroare de tip engleză ) - inconsecvență în tipurile de componente ale expresiei din program, de exemplu, o încercare de a utiliza un număr întreg ca funcție [7] . Lipsa erorilor de potrivire a tipurilor la timpul de execuție poate duce la erori și chiar la blocări . Securitatea unei limbi nu este sinonimă cu absența completă a bug-urilor, dar cel puțin acestea devin explorabile în cadrul semanticii limbajului (formal sau informal) [8] .
Sistemele de tip de încredere sunt numite și puternice ( ing. strong ) [1] [2] , dar interpretarea acestui termen este adesea atenuată, în plus, este adesea aplicată limbilor care efectuează verificarea dinamică a consistenței tipului ( puternic și slab ). tastarea ).
Uneori, siguranța este văzută ca o proprietate a unui anumit program, mai degrabă decât limba în care este scris, din motivul că unele limbaje sigure de tip permit ocolirea sau încălcarea sistemului de tip dacă programatorul practică o siguranță de tip slabă. Se crede larg că astfel de oportunități în practică se dovedesc a fi o necesitate, dar aceasta este ficțiune [9] . Conceptul de „siguranță a programului” este important în sensul că o implementare a unui limbaj sigur poate fi ea însăși nesigură. Spin-up-ul compilatorului rezolvă această problemă, făcând limbajul sigur nu numai în teorie, ci și în practică.
Robin Milner a inventat sintagma „Programele care trec verificarea tipului nu pot „a rătăci” [10] . Cu alte cuvinte, un sistem sigur de tip previne operațiunile eronate în mod deliberat care implică tipuri nevalide. De exemplu, expresia 3 / "Hello, World"este evident eronată, deoarece aritmetica nu definește operația de împărțire a unui număr la un șir. Din punct de vedere tehnic, siguranța înseamnă asigurarea faptului că valoarea oricărei expresii de tip verificată τeste un membru adevărat al setului de valori τ, adică se va afla în intervalul de valori permis de tipul static al expresiei respective. De fapt, această cerință are nuanțe - vezi subtipurile și polimorfismul pentru cazuri complexe.
În plus, prin utilizarea intensă a mecanismelor de definire a noilor tipuri , sunt prevenite erorile logice rezultate din semantica diferitelor tipuri [5] . De exemplu, atât milimetrii , cât și inci sunt unități de lungime și pot fi reprezentați ca numere întregi, dar ar fi o greșeală să scădem inci din milimetri, iar sistemul de tip dezvoltat nu va permite acest lucru (desigur, cu condiția ca programatorul să folosească tipuri diferite). pentru valori exprimate în unități diferite). date, mai degrabă decât să le descrie pe ambele ca variabile de tip întreg). Cu alte cuvinte, securitatea limbajului înseamnă că limbajul protejează programatorul de propriile greșeli posibile [9] .
Multe limbaje de programare a sistemului (de exemplu , Ada , C , C++ ) oferă operațiuni nesigure ( nesigure ) sau nesigure ( nesigure ) concepute pentru a putea încălca ( eng . încălca ) sistemul de tip - vezi tipul de turnare și scrierea de cuvinte . În unele cazuri, acest lucru este permis numai în părți limitate ale programului, în altele nu se poate distinge de operațiunile bine tipizate [11] .
În mainstream[ clarificați ] Nu este neobișnuit să vedeți siguranța tipului restrânsă la „ siguranța tipului de memorie ”, ceea ce înseamnă că componentele obiectelor de un tip agregat nu pot accesa locațiile de memorie alocate pentru obiecte de alt tip . Securitatea accesului la memorie înseamnă a nu putea copia un șir arbitrar de biți dintr-o zonă de memorie în alta. De exemplu, dacă o limbă furnizează un tip care are o gamă limitată de valori valide și oferă posibilitatea de a copia date netipizate într-o variabilă de acel tip, atunci acest tip nu este sigur pentru că poate permite unei variabile de tip să aibă o valoare care nu este valabil pentru tipul . Și, în special, dacă un astfel de limbaj nesigur permite scrierea unei valori întregi arbitrare într-o variabilă de tip „ pointer ”, atunci nesiguranța accesului la memorie este evidentă (vezi indicatorul suspendat ). Exemple de limbaje nesigure sunt C și C++ [4] . În comunitățile acestor limbi, orice operațiune care nu provoacă în mod direct blocarea programului este adesea denumită „sigură” . Securitatea accesului la memorie înseamnă, de asemenea, prevenirea posibilității de depășire a memoriei tampon , cum ar fi încercarea de a scrie obiecte mari în celulele alocate pentru obiecte de alt tip de dimensiune mai mică. ttt
Sistemele fiabile de tip static sunt conservatoare (redundante) în sensul că resping chiar și programele care s-ar executa corect. Motivul pentru aceasta este că, pentru orice limbaj Turing-complet , setul de programe care pot genera erori de potrivire de tip în timpul rulării este algoritmic indecidabil (vezi problema opririi ) [12] [13] . În consecință, astfel de sisteme de tip oferă un grad de protecție substanțial mai mare decât este necesar pentru a asigura siguranța accesului la memorie. Pe de altă parte, siguranța unor acțiuni nu poate fi dovedită static și trebuie controlată dinamic, de exemplu, indexarea unei matrice cu acces aleatoriu. Un astfel de control poate fi efectuat fie de sistemul runtime al limbajului în sine, fie direct de funcții care implementează astfel de operațiuni potențial nesigure.
Limbile tip puternic dinamic (de ex. Lisp , Smalltalk ) nu permit coruperea datelor din cauza faptului că un program care încearcă să convertească o valoare într-un tip incompatibil aruncă o excepție. Avantajele tastării dinamice puternice față de siguranța tipului includ lipsa de conservatorism și, ca urmare, extinderea gamei de sarcini de programare care trebuie rezolvate. Prețul acesteia este scăderea inevitabilă a vitezei programelor, precum și necesitatea unui număr semnificativ mai mare de rulări de testare pentru a identifica posibile erori. Prin urmare, multe limbi combină capabilitățile de control static și dinamic al consistenței tipului într-un fel sau altul. [14] [12] [1]
Ada (cel mai sigur limbaj din familia Pascal ) se concentrează pe dezvoltarea de sisteme încorporate fiabile , drivere și alte sarcini de programare a sistemului . Pentru a implementa secțiuni critice, Ada oferă o serie de constructe nesigure ale căror nume încep de obicei cu Unchecked_.
Limbajul SPARK este un subset al Ada. A eliminat funcțiile nesigure, dar a adăugat caracteristici proiectate prin contract . SPARK elimină posibilitatea de a agăța pointerii prin eliminarea însăși posibilitatea alocării dinamice a memoriei. Contractele verificate static au fost adăugate la Ada2012.
Hoare , într-o prelegere Turing, a susținut că verificările statice nu sunt suficiente pentru a asigura fiabilitatea - fiabilitatea este în primul rând o consecință a simplității [15] . Apoi a prezis că complexitatea Adei va provoca catastrofe.
BitC este un limbaj hibrid care combină caracteristicile de nivel scăzut ale C cu securitatea Standard ML și concizia Scheme . BitC se concentrează pe dezvoltarea de sisteme încorporate robuste , drivere și alte sarcini de programare a sistemelor .
Limbajul explorator Cyclone este un dialect sigur al C care împrumută multe idei din ML (inclusiv polimorfismul parametric sigur de tip ). Cyclone este proiectat pentru aceleași sarcini ca și C și, după ce a efectuat toate verificările, compilatorul generează cod în ANSI C. Cyclone nu necesită o mașină virtuală sau o colectare a gunoiului pentru securitate dinamică - în schimb, se bazează pe gestionarea memoriei prin regiuni . Cyclone stabilește o bară mai înaltă pentru securitatea codului sursă și, din cauza naturii nesigure a lui C, portarea chiar și a programelor simple din C în Cyclone poate necesita ceva muncă, deși multe din acestea pot fi făcute în C înainte de a schimba compilatoarele. Prin urmare, Cyclone este adesea definit nu ca un dialect al lui C, ci ca „ o limbă similară sintactic și semantic cu C ”.
Multe dintre ideile lui Cyclone și-au găsit drumul în limbajul Rust . Pe lângă tastarea statică puternică, limbajului a fost adăugată analiza statică a duratei de viață a indicatorilor bazată pe conceptul de „proprietate”. Implementarea restricțiilor statice care blochează accesul la memorie potențial incorect: nu pot apărea indicatori nuli, nu pot apărea variabile neinițializate și deinițializate, partajarea variabilelor mutabile de către mai multe sarcini este interzisă. Este necesară verificarea matricei în afara limitelor.
Haskell (un descendent al ML ) a fost conceput inițial ca un limbaj pur cu tipul complet , care trebuia să facă comportamentul programelor din acesta și mai previzibil decât în dialectele anterioare ale ML . Totuși, mai târziu în standardul lingvistic au fost prevăzute operațiuni nesigure [16] [17] , care sunt necesare în practica de zi cu zi, deși sunt marcate cu identificatorii corespunzători (începând cu ) [18] . unsafe
Haskell oferă, de asemenea, caracteristici slabe de tastare dinamică , iar implementarea mecanismului de gestionare a excepțiilor prin aceste caracteristici a fost inclusă în standardul lingvistic . Utilizarea acestuia poate provoca blocarea programelor, pentru care Robert Harper l-a numit pe Haskell „ extrem de nesigur ” [18] . Consideră inacceptabil ca excepțiile să aibă un tip definit de utilizator în contextul unei clase de tip Typeable , dat fiind că excepțiile sunt aruncate prin cod sigur (în afara monadei IO ); și clasifică mesajul de eroare intern al compilatorului ca fiind nepotrivit pentru sloganul lui Milner . În discuția care a urmat, s-a arătat cum ar putea fi implementate în Haskell excepțiile de tip static tip static în stil standard ML .
Lisp „pur” (minimal) este un limbaj de tip unic (adică orice construct aparține tipului „ expresie S ”) [19] , deși chiar și primele implementări comerciale ale lui Lisp prevedeau cel puțin un anumit număr de atomi . Familia de descendenți ai limbajului Lisp este reprezentată mai ales de limbi puternic tipate dinamic , dar există limbi tipizate static care combină ambele forme de tastare.
Common Lisp este un limbaj puternic tip dinamic, dar oferă capacitatea de a atribui în mod explicit ( manifest ) tipuri (și compilatorul SBCL este capabil să le deducă el însuși ) , totuși, această abilitate este folosită pentru a optimiza și a impune verificări dinamice și nu implică siguranță de tip static. Programatorul poate seta un nivel mai scăzut de verificări dinamice pentru compilator pentru a îmbunătăți performanța, iar programul compilat în acest fel nu mai poate fi considerat sigur [20] [21] .
Limbajul Scheme este, de asemenea, un limbaj puternic tip dinamic, dar Stalin deduce static tipuri, utilizându-le pentru a optimiza agresiv programele. Limbile „Typed Racket” (o extensie a Racket Scheme ) și Shen sunt sigure de tip. Clojure combină tastarea dinamică și statică puternică.
Limbajul ML a fost dezvoltat inițial ca un sistem interactiv de demonstrare a teoremei și abia mai târziu a devenit un limbaj compilat independent de uz general. S-au dedicat mult efort pentru a demonstra fiabilitatea sistemului de tip Hindley-Milner polimorf parametric care stau la baza ML . Dovada siguranței este construită pentru un subset pur funcțional ( "Fuctional ML" ), o extensie prin tipuri de referință ( "Reference ML" ), o extensie prin excepții ( "Exception ML" ), un limbaj care combină toate aceste extensii ( " Core ML" ) și, în final, extensiile sale cu continuări de primă clasă ( "Control ML" ), mai întâi monomorfe, apoi polimorfe [2] .
Consecința acestui lucru este că descendenții ML sunt adesea considerați a priori a fi siguri de tip, chiar dacă unii dintre ei amână verificările semnificative la timpul de execuție ( OCaml ) sau se abat de la semantica pentru care este construită dovada siguranței și conțin în mod explicit nesigure. caracteristici ( Haskell ). Limbile familiei ML se caracterizează prin suport dezvoltat pentru tipuri de date algebrice , a căror utilizare contribuie în mod semnificativ la prevenirea erorilor logice , ceea ce susține și impresia de siguranță a tipului.
Unii descendenți ai ML sunt, de asemenea, instrumente de demonstrare interactive ( Idris , Mercury , Agda ). Multe dintre ele, deși ar putea fi folosite pentru dezvoltarea directă a programelor cu fiabilitate dovedită, sunt mai des folosite pentru a verifica programe în alte limbi - din motive precum intensitatea ridicată a muncii, viteza scăzută, lipsa FFI și așa mai departe. Printre descendenții ML cu fiabilitate dovedită, Standard ML și prototipul succesorului său de dezvoltare ulterioară ML [22] (cunoscut anterior ca „ML2000”) se remarcă ca limbaje orientate spre industrie .
Limbajul Standard ML (cel mai vechi din familia de limbaje ML ) este axat pe dezvoltarea de programe industriale de viteză la scară largă 23] . Limbajul are o definiție formală strictă și securitatea sa statică și dinamică a fost dovedită [24] . După o verificare statică a consistenței interfețelor componentelor programului (inclusiv a celor generate - vezi functorii ML ), sistemul de rulare susține un control suplimentar de securitate . În consecință, chiar și un program ML Standard cu un bug se comportă întotdeauna ca un program ML: poate intra în calcule pentru totdeauna sau poate da utilizatorului un mesaj de eroare, dar nu se poate bloca [9] .
Cu toate acestea, unele implementări ( SML/NJ , Mythryl , MLton ) includ biblioteci non-standard care oferă anumite operațiuni nesigure (identificatorii lor încep cu Unsafe). Aceste capabilități sunt necesare pentru interfața de limbaj extern a acestor implementări, care oferă interacțiune cu cod non-ML (de obicei cod C care implementează componente de program critice pentru viteză), care poate necesita o reprezentare particulară de biți a datelor. În plus, multe implementări ale Standardului ML , deși sunt scrise în sine , folosesc un sistem de rulare scris în C. Un alt exemplu este modul REPL al compilatorului SML/NJ , care folosește operațiuni nesigure pentru a executa codul introdus interactiv de către programator.
Limbajul Alice este o extensie a Standard ML , oferind capabilități puternice de tastare dinamică .