Typová bezpečnost je vlastnost programovacího jazyka , která charakterizuje bezpečnost a spolehlivost při aplikaci jeho typového systému .
Typový systém se nazývá bezpečný ( angl. safe ) nebo spolehlivý ( eng. sound ), pokud programy, které prošly kontrolou konzistence typu ( angl. dobře napsané programy nebo dobře vytvořené programy ), vylučují možnost chyb typové konzistence při spuštění. čas [1 ] [2] [3] [4] [5] [6] .
Chyba při shodě typu nebo chyba při psaní ( English type error ) - nekonzistence v typech výrazových komponent v programu, například pokus o použití celého čísla jako funkce [7] . Chybějící chyby při porovnávání typů za běhu mohou vést k chybám a dokonce k selháním . Bezpečnost jazyka není synonymem pro úplnou absenci chyb, ale přinejmenším se stávají prozkoumatelnými v rámci sémantiky jazyka (formální nebo neformální) [8] .
Systémy spolehlivého typu se také nazývají silné ( eng. strong ) [1] [2] , ale výklad tohoto termínu je často změkčený, navíc je často aplikován na jazyky, které provádějí dynamickou kontrolu konzistence typu ( silný a slabý psaní ).
Někdy je bezpečnost považována za vlastnost konkrétního programu spíše než za jazyk, ve kterém je napsán, z toho důvodu, že některé typově bezpečné jazyky umožňují obejít nebo narušit typový systém , pokud programátor praktikuje špatnou bezpečnost typu. Obecně se má za to, že takové příležitosti se v praxi ukazují jako nutnost, ale to je fikce [9] . Koncept „bezpečnosti programu“ je důležitý v tom smyslu, že samotná implementace bezpečného jazyka může být nebezpečná. Tento problém řeší spin-up kompilátoru , díky kterému je jazyk bezpečný nejen teoreticky, ale i prakticky.
Robin Milner razil frázi „Programy, které projdou kontrolou typu, nemohou ‚sejít z cesty‘“ [10] . Jinými slovy, typově bezpečný systém zabraňuje záměrně chybným operacím zahrnujícím neplatné typy. Například výraz 3 / "Hello, World"je zjevně chybný, protože aritmetika nedefinuje operaci dělení čísla řetězcem. Technicky bezpečnost znamená zajistit, že hodnota jakéhokoli typově kontrolovaného výrazuτ typu je skutečným členem sady hodnot τ, tj. bude ležet v rozsahu hodnot povolených statickým typem daného výrazu. Tento požadavek má ve skutečnosti nuance – viz podtypy a polymorfismus pro složité případy.
Navíc při intenzivním používání mechanismů pro definování nových typů se předchází logickým chybám vyplývajícím ze sémantiky různých typů [5] . Například milimetry i palce jsou jednotky délky a lze je reprezentovat jako celá čísla, ale byla by chyba odečítat palce od milimetrů a vyvinutý typový systém to neumožní (samozřejmě za předpokladu, že programátor používá různé typy pro hodnoty vyjádřené v různých jednotkách). Jinými slovy, jazyková bezpečnost znamená, že jazyk chrání programátora před jeho vlastními možnými chybami [9] .
Mnoho systémových programovacích jazyků (např. Ada , C , C++ ) poskytuje nebezpečné ( nezdravé ) nebo nebezpečné ( nebezpečné ) operace navržené tak, aby byly schopny narušit ( anglicky narušit ) typový systém – viz přelévání a psaní slovních hříček . V některých případech je to povoleno pouze v omezených částech programu, v jiných je to k nerozeznání od dobře napsaných operací [11] .
V hlavním proudu[ ujasnit ] Není neobvyklé vidět typovou bezpečnost zúženou na „ bezpečnost typu paměti “, což znamená, že komponenty objektů jednoho agregovaného typu nemají přístup k paměťovým místům přiděleným pro objekty jiného typu . Zabezpečení přístupu do paměti znamená, že nelze zkopírovat libovolný řetězec bitů z jedné oblasti paměti do druhé. Pokud například jazyk poskytuje typ , který má omezený rozsah platných hodnot, a poskytuje možnost kopírovat netypizovaná data do proměnné tohoto typu, pak to není typově bezpečné, protože potenciálně umožňuje proměnné typu mít hodnotu to neplatí pro typ . A zvláště, pokud takový nebezpečný jazyk umožňuje zapsat libovolnou celočíselnou hodnotu do proměnné typu " ukazatel ", pak je nebezpečnost přístupu do paměti zřejmá (viz visící ukazatel ). Příklady nebezpečných jazyků jsou C a C++ [4] . V komunitách těchto jazyků je každá operace, která přímo nezpůsobí pád programu, často označována jako „bezpečná“ . Zabezpečení přístupu do paměti také znamená zamezení možnosti přetečení vyrovnávací paměti , jako je pokus o zápis velkých objektů do buněk přidělených pro objekty jiného typu menší velikosti. ttt
Spolehlivé systémy statického typu jsou konzervativní (nadbytečné) v tom smyslu, že odmítají i programy, které by se správně prováděly. Důvod pro toto je to, pro nějaký Turing-kompletní jazyk, soubor programů, které mohou generovat typ-odpovídající chyby za běhu je algoritmicky nerozhodnutelný (viz problém zastavení ) [12] [13] . V důsledku toho systémy takového typu poskytují stupeň ochrany, který je podstatně vyšší, než je nezbytné pro zajištění bezpečnosti přístupu do paměti. Na druhou stranu bezpečnost některých akcí nelze staticky prokázat a musí být řízena dynamicky – například indexování pole s náhodným přístupem. Takové řízení může být prováděno buď samotným runtime systémem jazyka, nebo přímo funkcemi, které implementují takové potenciálně nebezpečné operace.
Silně dynamicky typované jazyky (např . Lisp , Smalltalk ) neumožňují poškození dat kvůli skutečnosti, že program, který se snaží převést hodnotu na nekompatibilní typ, vyvolá výjimku. Mezi výhody silného dynamického psaní oproti bezpečnosti typu patří nedostatek konzervatismu a v důsledku toho rozšíření řady programovacích úloh, které je třeba řešit. Cenou za to je nevyhnutelné snížení rychlosti programů a také nutnost podstatně většího počtu testovacích běhů pro identifikaci případných chyb. Proto mnoho jazyků tak či onak kombinuje možnosti statického a dynamického řízení konzistence typu. [14] [12] [1]
Ada (typově nejbezpečnější jazyk v rodině Pascal ) se zaměřuje na vývoj spolehlivých vestavěných systémů , ovladačů a dalších úloh systémového programování . Pro implementaci kritických sekcí poskytuje Ada řadu nebezpečných konstrukcí, jejichž názvy obvykle začínají Unchecked_.
Jazyk SPARK je podmnožinou Ada. Odstranil nebezpečné funkce, ale přidal funkce navržené podle smlouvy . SPARK eliminuje možnost zavěšení ukazatelů tím, že eliminuje samotnou možnost dynamické alokace paměti. Do Ada2012 byly přidány staticky ověřené smlouvy .
Hoare v Turingově přednášce tvrdil, že statické kontroly nestačí k zajištění spolehlivosti – spolehlivost je především důsledkem jednoduchosti [15] . Pak předpověděl, že složitost Ady způsobí katastrofy.
BitC je hybridní jazyk, který kombinuje nízkoúrovňové funkce jazyka C s bezpečností Standard ML a stručností Scheme . BitC se zaměřuje na vývoj robustních vestavěných systémů , ovladačů a dalších úloh programování systémů .
Průzkumný jazyk Cyclone je bezpečný dialekt jazyka C , který si půjčuje mnoho myšlenek z ML (včetně typově bezpečného parametrického polymorfismu ). Cyclone je navržen pro stejné úkoly jako C a po provedení všech kontrol kompilátor vygeneruje kód v ANSI C . Cyclone pro dynamické zabezpečení nevyžaduje virtuální stroj nebo shromažďování odpadků – místo toho je založen na správě paměti prostřednictvím regionů . Cyclone nastavuje vyšší laťku zabezpečení zdrojového kódu a kvůli nezabezpečené povaze jazyka C může přenos i jednoduchých programů z jazyka C do Cyclone vyžadovat určitou práci, i když mnoho z toho lze provést v jazyce C před změnou kompilátorů. Proto je Cyclone často definován ne jako dialekt C, ale jako „ jazyk syntakticky a sémanticky podobný C “.
Mnoho z myšlenek Cyclone si našlo cestu do jazyka Rust . Kromě silného statického typování byla do jazyka přidána statická analýza životnosti ukazatelů založená na konceptu „vlastnictví“. Implementovaná statická omezení, která blokují potenciálně nesprávný přístup k paměti: žádné nulové ukazatele, neinicializované a deinicializované proměnné se nemohou objevit, sdílení proměnných proměnných několika úlohami je zakázáno. Je vyžadována kontrola pole mimo hranice.
Haskell (potomek ML ) byl původně navržen jako typově plně čistý jazyk, což mělo učinit chování programů v něm ještě předvídatelnějším než v dřívějších dialektech ML . Později však byly v jazykové normě poskytnuty nebezpečné operace [16] [17] , které jsou v každodenní praxi nezbytné, přestože jsou označeny příslušnými identifikátory (začínající na ) [18] . unsafe
Haskell také poskytuje slabé funkce dynamického psaní a implementace mechanismu zpracování výjimek prostřednictvím těchto funkcí byla zahrnuta do jazykového standardu . Jeho použití může způsobit pád programů, pro které Robert Harper nazval Haskell " extrémně nezabezpečeným " [18] . Považuje za nepřijatelné, aby výjimky měly typ definovaný uživatelem v kontextu třídy typu Typeable , vzhledem k tomu, že výjimky jsou vyvolány bezpečným kódem (mimo monad IO ); a klasifikuje interní chybovou zprávu kompilátoru jako nevhodnou pro Milnerův slogan . V diskusi, která následovala, bylo ukázáno, jak lze v Haskell implementovat staticky typově bezpečné výjimky ve stylu Standard ML .
„Čistý“ (minimální) Lisp je jednotypový jazyk (to znamená, že jakýkoli konstrukt patří do typu „ S-výraz “) [19] , ačkoli již první komerční implementace Lisp poskytovaly alespoň určitý počet atomů . Rodina potomků jazyka Lisp je reprezentována převážně silně dynamicky typovanými jazyky, existují však staticky typované jazyky, které kombinují obě formy psaní.
Common Lisp je silně dynamicky typovaný jazyk, ale poskytuje možnost explicitně ( manifest ) přiřazovat typy (a kompilátor SBCL je schopen je sám odvodit ) , nicméně tato schopnost se používá k optimalizaci a vynucení dynamických kontrol a neznamená bezpečnost statického typu. Programátor může nastavit nižší úroveň dynamických kontrol pro kompilátor za účelem zlepšení výkonu a takto zkompilovaný program již nelze považovat za bezpečný [20] [21] .
Jazyk Scheme je také silně dynamicky typovaný jazyk, ale Stalin staticky odvozuje typy a používá je k agresivní optimalizaci programů. Jazyky „Typed Racket“ (rozšíření Racket Scheme ) a Shen jsou typově bezpečné. Clojure kombinuje silné dynamické a statické psaní.
Jazyk ML byl původně vyvinut jako interaktivní systém dokazování teorémů a teprve později se stal nezávislým kompilovaným jazykem pro všeobecné použití. Mnoho úsilí bylo věnováno prokázání spolehlivosti parametricky polymorfního systému typu Hindley-Milner, který je základem ML . Důkaz bezpečnosti je vytvořen pro čistě funkční podmnožinu ( „Fuctional ML“ ), rozšíření o typy odkazů ( „Reference ML“ ), rozšíření o výjimky ( „Exception ML“ ), jazyk, který kombinuje všechna tato rozšíření ( „ Core ML" ), a konečně jeho rozšíření s prvotřídními pokračováními ( "Control ML" ), nejprve monomorfní, poté polymorfní [2] .
Důsledkem toho je, že potomci ML jsou často a priori považováni za typově bezpečné, i když některé z nich odkládají smysluplné kontroly na běhové prostředí ( OCaml ), nebo se odchylují od sémantiky, pro kterou je vytvořen důkaz o bezpečnosti, a výslovně obsahují nebezpečné funkce ( Haskell ). Jazyky rodiny ML se vyznačují vyvinutou podporou algebraických datových typů , jejichž použití výrazně přispívá k prevenci logických chyb , což také podporuje dojem typové bezpečnosti.
Někteří potomci ML jsou také interaktivní důkazové nástroje ( Idris , Mercury , Agda ). Mnohé z nich, přestože by mohly být použity pro přímý vývoj programů s prokázanou spolehlivostí, se častěji používají k ověřování programů v jiných jazycích - z důvodů, jako je vysoká pracnost použití, nízká rychlost, nedostatek FFI a tak dále. Mezi potomky ML s prokázanou spolehlivostí vynikají jako průmyslově orientované jazyky Standard ML a prototyp jeho dalšího vývojového nástupce ML [22] (dříve známý jako „ML2000“) .
Jazyk Standard ML (nejstarší v rodině jazyků ML ) je zaměřen na vývoj rozsáhlých průmyslových programů rychlosti 23] . Jazyk má přísnou formální definici a byla prokázána jeho statická i dynamická bezpečnost [24] . Po statické kontrole konzistence rozhraní programových komponent (včetně generovaných - viz ML funktory ) je další kontrola bezpečnosti podporována runtime systémem . V důsledku toho se dokonce i standardní program ML s chybou vždy chová jako program ML: může navždy přejít do výpočtů nebo dát uživateli chybovou zprávu, ale nemůže spadnout [9] .
Některé implementace ( SML/NJ , Mythryl , MLton ) však obsahují nestandardní knihovny , které poskytují určité nebezpečné operace (jejich identifikátory začínají Unsafe). Tyto schopnosti jsou potřebné pro externí jazykové rozhraní těchto implementací, které poskytuje interakci s ne-ML kódem (obvykle C kód , který implementuje komponenty programu kritické pro rychlost), což může vyžadovat zvláštní bitovou reprezentaci dat. Kromě toho mnoho implementací Standard ML , i když samy o sobě jsou napsány , používá runtime systém napsaný v C. Dalším příkladem je režim REPL kompilátoru SML/NJ , který používá nebezpečné operace ke spuštění kódu zadaného interaktivně programátorem.
Jazyk Alice je rozšířením standardu ML a poskytuje silné možnosti dynamického psaní.