A típusbiztonság egy programozási nyelv olyan tulajdonsága, amely jellemzi típusrendszerének alkalmazásának biztonságát és megbízhatóságát .
Egy típusrendszert biztonságosnak ( eng. safe ) vagy megbízhatónak ( eng. sound ) nevezünk , ha azok a programok, amelyek átmentek a típuskonzisztencia ellenőrzésen ( jól beírt programok vagy jól formázott programok ) kizárják a típuskonzisztencia hibáinak lehetőségét futás közben idő [1 ] [2] [3] [4] [5] [6] .
Típusillesztési hiba vagy gépelési hiba ( English type error ) - a programban található kifejezés-összetevők típusainak inkonzisztenciája , például egy egész szám függvényként való használatának kísérlete [7] . A hiányzó futásidejű típusegyezési hibák hibákhoz , sőt összeomláshoz vezethetnek . Egy nyelv biztonsága nem egyet jelent a hibák teljes hiányával, de legalább a nyelv (formális vagy informális) szemantikáján belül feltárhatóvá válnak [8] .
A megbízható típusrendszereket erősnek ( eng. strong ) is nevezik [1] [2] , de ennek a kifejezésnek az értelmezése gyakran lágyul, emellett gyakran alkalmazzák olyan nyelvekre, amelyek dinamikus típuskonzisztencia-ellenőrzést végeznek ( erős és gyenge gépelés ).
Néha a biztonságot egy adott program tulajdonságának tekintik, nem pedig annak a nyelvnek, amelyen meg van írva, abból az okból kifolyólag, hogy egyes típusbiztos nyelvek lehetővé teszik a típusrendszer megkerülését vagy megsértését , ha a programozó rossz típusbiztonságot gyakorol. Elterjedt az a vélemény, hogy az ilyen lehetőségek a gyakorlatban szükségszerűnek bizonyulnak, de ez fikció [9] . A „programbiztonság” fogalma abból a szempontból fontos, hogy egy biztonságos nyelv megvalósítása maga is nem biztonságos. A fordító spin -up megoldja ezt a problémát, így a nyelv nem csak elméletben, hanem gyakorlatban is biztonságossá válik.
Robin Milner megalkotta a „Típusellenőrzésen átmenő programok nem tévedhetnek el” kifejezést [10] . Más szavakkal, a típusbiztos rendszer megakadályozza a szándékosan hibás műveleteket, amelyek érvénytelen típusokat tartalmaznak. Például a kifejezés 3 / "Hello, World"nyilvánvalóan hibás, mivel az aritmetika nem határozza meg a szám karakterlánccal való elosztásának műveletét. Technikailag a biztonság azt jelenti, hogy a típus bármely típus-ellenőrzött kifejezésénekτ értéke az értékkészlet valódi tagja legyen , azaz az adott kifejezés statikus típusaτ által megengedett értéktartományon belül legyen . Valójában ennek a követelménynek vannak árnyalatai – lásd az altípusokat és a polimorfizmust az összetett eseteknél.
Ezen túlmenően, az új típusok meghatározására szolgáló mechanizmusok intenzív használatával a különféle típusok szemantikájából eredő logikai hibák kivédhetők [5] . Például a milliméter és a hüvelyk is hosszegységek, és egész számokként is ábrázolhatók, de hiba lenne a milliméterből kivonni a hüvelykeket, és a kifejlesztett típusrendszer ezt nem teszi lehetővé (persze, feltéve, hogy a programozó különböző típusokat használ különböző mértékegységekben kifejezett értékek esetén). Más szóval a nyelvi biztonság azt jelenti, hogy a nyelv megvédi a programozót a saját esetleges hibáitól [9] .
Számos rendszerprogramozási nyelv (pl. Ada , C , C++ ) nem biztonságos ( nem biztonságos ) vagy nem biztonságos ( nem biztonságos ) műveleteket tesz lehetővé, amelyek célja a típusrendszer megsértése ( angol . sérti ) – lásd a típusöntést és a szóhasználatot . Egyes esetekben ez csak a program korlátozott részeiben megengedett, máskor meg nem különböztethető a jól tipizált műveletektől [11] .
A mainstreamben[ pontosítás ] Nem ritka , hogy a típusbiztonságot a " memóriatípus biztonságára " szűkítik , ami azt jelenti , hogy az egyik aggregált típusú objektumok komponensei nem férhetnek hozzá a másik típusú objektumok számára lefoglalt memóriahelyekhez . A memóriahozzáférés biztonsága azt jelenti, hogy nem lehet tetszőleges bitsort átmásolni egyik memóriaterületről a másikra. Például, ha egy nyelv olyan típust biztosít , amelynek korlátozott az érvényes értékek tartománya, és lehetőséget ad a típusolatlan adatok bemásolására egy ilyen típusú változóba, akkor ez nem típusbiztos, mert potenciálisan lehetővé teszi, hogy a típusváltozónak értéke legyen. típusra nem érvényes . És különösen, ha egy ilyen nem biztonságos nyelv lehetővé teszi egy tetszőleges egész érték írását egy " pointer " típusú változóba, akkor nyilvánvaló a memóriaelérés nem biztonságos (lásd: lógó mutató ). Példák a nem biztonságos nyelvekre a C és a C++ [4] . Ezeknek a nyelveknek a közösségeiben minden olyan műveletet, amely nem okoz közvetlenül a program összeomlását , gyakran "biztonságosnak" nevezik . A memóriahozzáférés biztonsága azt is jelenti, hogy meg kell akadályozni a puffertúlcsordulás lehetőségét , például a nagy objektumok megkísérlését más típusú, kisebb méretű objektumok számára lefoglalt cellákba írni. ttt
A megbízható statikus típusú rendszerek konzervatívak (redundánsak) abban az értelemben, hogy még azokat a programokat is elutasítják, amelyek megfelelően futnának. Ennek az az oka, hogy bármely Turing-teljes nyelv esetében algoritmikusan eldönthetetlen azon programok halmaza, amelyek futás közben típusillesztési hibákat generálnak (lásd a leállítási problémát ) [12] [13] . Következésképpen az ilyen típusú rendszerek lényegesen magasabb szintű védelmet biztosítanak, mint ami a memóriaelérés biztonságához szükséges. Másrészt bizonyos műveletek biztonsága nem igazolható statikusan, és dinamikusan kell ellenőrizni – például egy véletlen hozzáférésű tömb indexelésével. Az ilyen vezérlést vagy maga a nyelv futtatórendszere , vagy közvetlenül az ilyen potenciálisan nem biztonságos műveleteket végrehajtó függvények hajthatják végre .
Az erősen dinamikusan beírt nyelvek (pl . Lisp , Smalltalk ) nem engedik meg az adatsérülést, amiatt, hogy egy értéket inkompatibilis típusra konvertálni próbáló program kivételt dob. Az erős dinamikus tipizálás előnyei a típusbiztonsággal szemben a konzervativizmus hiánya, és ennek eredményeként a megoldandó programozási feladatok körének bővülése. Ennek az ára a programok sebességének elkerülhetetlen csökkenése, valamint a lényegesen nagyobb számú próbaüzem szükségessége az esetleges hibák felderítésére. Ezért sok nyelv ilyen vagy olyan módon egyesíti a statikus és dinamikus típuskonzisztencia-vezérlés képességeit. [14] [12] [1]
Az Ada (a Pascal család leginkább típusbiztos nyelve ) megbízható beágyazott rendszerek , illesztőprogramok és egyéb rendszerprogramozási feladatok fejlesztésére összpontosít . A kritikus szakaszok megvalósításához az Ada számos nem biztonságos konstrukciót biztosít, amelyek neve általában -val kezdődik Unchecked_.
A SPARK nyelv az Ada egy részhalmaza. Eltávolította a nem biztonságos funkciókat, de szerződés szerinti tervezési funkciókat adott hozzá . A SPARK kiküszöböli a mutató lógásának lehetőségét azáltal, hogy kiküszöböli a dinamikus memóriafoglalás lehetőségét. Statikusan ellenőrzött szerződések kerültek az Ada2012-be.
Hoare egy Turing-előadásban amellett érvelt, hogy a statikus ellenőrzések nem elegendőek a megbízhatóság biztosításához – a megbízhatóság elsősorban az egyszerűség következménye [15] . Aztán megjósolta, hogy Ada bonyolultsága katasztrófákat fog okozni.
A BitC egy hibrid nyelv, amely egyesíti a C alacsony szintű szolgáltatásait a Standard ML biztonságával és a Scheme tömörségével . A BitC a robusztus beágyazott rendszerek , illesztőprogramok és egyéb rendszerprogramozási feladatok fejlesztésére összpontosít .
A Cyclone felfedező nyelv a C biztonságos dialektusa, amely számos ötletet kölcsönzött az ML -ből (beleértve a típusbiztos parametrikus polimorfizmust is ). A Cyclone ugyanazokra a feladatokra készült, mint a C, és az összes ellenőrzés elvégzése után a fordító kódot generál ANSI C -ben . A Cyclone nem igényel virtuális gépet vagy szemétgyűjtést a dinamikus biztonság érdekében – ehelyett a régiókon keresztüli memóriakezelésen alapul . A Cyclone magasabb lécet tesz a forráskód biztonságára, és a C nem biztonságos természete miatt még az egyszerű programok C-ből Cyclone-ba történő portolása is igényelhet némi munkát, bár a fordítók cseréje előtt sokat meg lehet tenni C-n belül. Ezért a Cyclone-t gyakran nem a C nyelvjárásaként definiálják, hanem mint „ szintaktikailag és szemantikailag a C-hez hasonló nyelvet ”.
A Cyclone sok ötlete utat talált a Rust nyelvbe . Az erős statikus tipizálás mellett a mutatók élettartamának statikus elemzése is a "tulajdonjog" fogalma alapján került a nyelvbe. Megvalósított statikus korlátozások, amelyek blokkolják az esetlegesen helytelen memóriaelérést: nincsenek nullmutatók, nem jelenhetnek meg inicializálatlan és deinicializált változók, tilos a változó változók több feladat általi megosztása. A határokon kívüli tömb ellenőrzése kötelező.
A Haskell (az ML leszármazottja ) eredetileg egy típusteljes tiszta nyelvnek készült, ami a benne lévő programok viselkedését még kiszámíthatóbbá kellett volna tenni, mint az ML korábbi dialektusaiban . Később azonban a nyelvi szabványban megjelentek a nem biztonságos műveletek [16] [17] , amelyek a mindennapi gyakorlatban szükségesek, bár a megfelelő azonosítókkal vannak jelölve (-től kezdve ) [18] . unsafe
A Haskell gyenge dinamikus gépelési szolgáltatásokat is biztosít , és a kivételkezelési mechanizmus megvalósítása ezeken a szolgáltatásokon keresztül bekerült a nyelvi szabványba . Használata a programok összeomlását okozhatja, amiért Robert Harper „ rendkívül bizonytalannak ” nevezte a Haskellt [18] . Elfogadhatatlannak tartja, hogy a kivételeknek legyen egy típusa, amelyet a felhasználó a type class kontextusában határoz meg , mivel a kivételeket biztonságos kód dobja (a monadon kívül ); és a fordító belső hibaüzenetét Milner szlogenje szempontjából nem megfelelőnek minősíti . Az ezt követő beszélgetés során bemutatták, hogyan lehet a Haskellben megvalósítani a Standard ML stílusú statikusan típusbiztos kivételeket . Typeable IO
A "tiszta" (minimális) Lisp egy egytípusú nyelv (azaz bármely konstrukció az " S-kifejezés " típushoz tartozik) [19] , bár még a Lisp első kereskedelmi megvalósításai is biztosítottak legalább bizonyos számú atomot. . A Lisp nyelv leszármazottainak családját többnyire erősen dinamikusan tipizált nyelvek képviselik, de vannak statikusan tipizált nyelvek, amelyek a gépelés mindkét formáját egyesítik.
A Common Lisp egy erősen dinamikusan tipizált nyelv, de lehetőséget biztosít a típusok explicit ( manifeszt ) hozzárendelésére (és az SBCL fordító maga is képes következtetni rájuk ) , azonban ezt a képességet a dinamikus ellenőrzések és ellenőrzések optimalizálására és kikényszerítésére használják. nem jelent statikus típusú biztonságot. A programozó a teljesítmény javítása érdekében alacsonyabb szintű dinamikus ellenőrzéseket állíthat be a fordító számára, és az így lefordított program már nem tekinthető biztonságosnak [20] [21] .
A Scheme nyelv is erősen dinamikusan tipizált nyelv, de a Sztálin statikusan következtet a típusokra, és a programok agresszív optimalizálására használja őket. A „Typed Racket” (a Racket Scheme kiterjesztése ) és a Shen nyelvek típusbiztosak . A Clojure az erőteljes dinamikus és statikus gépelést egyesíti.
Az ML nyelvet eredetileg interaktív tételbizonyító rendszerként fejlesztették ki , és csak később vált önálló, általános célú fordított nyelvvé. Sok erőfeszítést fordítottak az ML alapjául szolgáló parametrikusan polimorf Hindley-Milner típusú rendszer megbízhatóságának bizonyítására . A biztonság igazolása egy tisztán funkcionális részhalmazra ( "Fukciós ML" ), egy hivatkozási típusok szerinti kiterjesztésre ( "Reference ML" ), egy kivételes kiterjesztésre ( "Exception ML" ), egy nyelvre, amely ezeket a kiterjesztéseket egyesíti ( " Core ML" ), és végül annak első osztályú folytatásaival ( "Control ML" ), először monomorf, majd polimorf [2] kiterjesztései .
Ennek az a következménye, hogy az ML leszármazottjait gyakran eleve típusbiztonságosnak tekintik, még akkor is, ha némelyikük az értelmes ellenőrzéseket a futási időre halasztja ( OCaml ), vagy eltér attól a szemantikától, amelyre a biztonsági igazolás készült, és kifejezetten nem biztonságos. ( Haskell ). Az ML család nyelveit az algebrai adattípusok fejlett támogatása jellemzi , melynek használata jelentősen hozzájárul a logikai hibák megelőzéséhez , ami a típusbiztonság benyomását is alátámasztja.
Az ML egyes leszármazottai interaktív bizonyító eszközök is ( Idris , Mercury , Agda ). Sok közülük, bár bizonyítottan megbízható programok közvetlen fejlesztésére használhatók, gyakrabban használják más nyelvű programok ellenőrzésére - olyan okok miatt, mint a használat nagy munkaintenzitása, alacsony sebesség, FFI hiánya és így tovább. Az ML bizonyítottan megbízható leszármazottai közül a Standard ML és a továbbfejlesztett utódjának prototípusa, az ML [22] (korábbi nevén "ML2000") kiemelkedik iparág-orientált nyelvként .
A Standard ML nyelv (a legrégebbi az ML nyelvcsaládban) a nagyszabású ipari sebességű programok fejlesztésére összpontosít 23] . A nyelvnek szigorú formális definíciója van, statikus és dinamikus biztonsága bizonyított [24] . A programkomponensek interfészeinek konzisztenciájának statikus ellenőrzése után (beleértve a generáltakat is – lásd az ML függvényeket ), a további biztonsági ellenőrzést a futásidejű rendszer támogatja . Következésképpen még egy hibával rendelkező Standard ML program is mindig úgy viselkedik, mint egy ML program: örökre belemegy a számításokba, vagy hibaüzenetet küld a felhasználónak, de nem tud összeomlani [9] .
Egyes megvalósítások ( SML/NJ , Mythryl ] , MLton ) azonban nem szabványos könyvtárakat is tartalmaznak , amelyek bizonyos nem biztonságos műveleteket biztosítanak (az azonosítóik -vel kezdődnek Unsafe). Ezek a képességek szükségesek ezen implementációk külső nyelvi interfészéhez , amely interakciót biztosít nem ML kóddal (általában C kóddal , amely sebességkritikus programkomponenseket valósít meg), amihez szükség lehet az adatok sajátos bitreprezentációjára . Ezenkívül a Standard ML számos implementációja , bár önmagában íródott , C nyelven írt futásidejű rendszert használ . Egy másik példa az SML/NJ fordító REPL módja , amely nem biztonságos műveleteket használ a programozó által interaktívan bevitt kód végrehajtására.
Az Alice nyelv a Standard ML kiterjesztése , amely erőteljes dinamikus gépelési képességeket biztosít.