Tyyppiturvallisuus on ohjelmointikielen ominaisuus , joka luonnehtii turvallisuutta ja luotettavuutta sen tyyppijärjestelmän soveltamisessa .
Tyyppijärjestelmää kutsutaan turvalliseksi ( eng. safe ) tai luotettavaksi ( eng. sound ) , jos ohjelmat, jotka ovat läpäisseet tyyppiyhdenmukaisuustarkastukset ( eng. hyvin kirjoitetut ohjelmat tai hyvin muodostetut ohjelmat ) sulkevat pois tyyppiyhdenmukaisuusvirheiden mahdollisuuden ajon aikana aika [1 ] [2] [3] [4] [5] [6] .
Type matching error tai kirjoitusvirhe ( englanniksi type error ) - ohjelman lausekekomponenttien tyyppien epäjohdonmukaisuus , esimerkiksi yritys käyttää kokonaislukua funktiona [7] . Puuttuvat ajonaikaiset tyyppivastaavuusvirheet voivat johtaa virheisiin ja jopa kaatumisiin . Kielen turvallisuus ei ole synonyymi virheiden täydelliselle puuttumiselle, mutta ainakin niistä tulee tutkittavia kielen semantiikan (muodollisen tai epämuodollisen) puitteissa [8] .
Luotettavia tyyppijärjestelmiä kutsutaan myös vahvaksi ( eng. strong ) [1] [2] , mutta tämän termin tulkintaa on usein pehmennetty, lisäksi sitä sovelletaan usein kieliin, jotka suorittavat dynaamista tyyppiyhdenmukaisuuden tarkistusta ( vahva ja heikko ). kirjoittamalla ).
Joskus turvallisuus nähdään tietyn ohjelman ominaisuutena pikemminkin kuin kielenä, jolla se on kirjoitettu, siitä syystä, että jotkin tyyppiturvalliset kielet sallivat tyyppijärjestelmän ohituksen tai rikkomisen , jos ohjelmoija noudattaa huonoa tyyppiturvallisuutta. Yleisesti uskotaan, että tällaiset mahdollisuudet osoittautuvat käytännössä välttämättömiksi, mutta tämä on fiktiota [9] . Käsite "ohjelmaturvallisuus" on tärkeä siinä mielessä, että turvallisen kielen toteutus voi itsessään olla vaarallinen. Kääntäjän spin -up ratkaisee tämän ongelman ja tekee kielestä turvallisen paitsi teoriassa myös käytännössä.
Robin Milner loi lauseen "Ohjelmat, jotka läpäisevät tyyppitarkistuksen, eivät voi "mennä harhaan" [10] . Toisin sanoen tyyppiturvallinen järjestelmä estää tahallaan virheelliset toiminnot, joihin liittyy virheellisiä tyyppejä. Esimerkiksi lauseke 3 / "Hello, World"on ilmeisen virheellinen, koska aritmetiikka ei määrittele luvun jakamista merkkijonolla. Teknisesti turvallisuus tarkoittaa sen varmistamista, että minkä tahansa tyyppitarkistetun tyypin lausekkeenτ arvo on arvojoukon todellinen jäsen, eli se on kyseisen lausekkeen staattisen tyypinτ sallimien arvojen alueella . Itse asiassa tässä vaatimuksessa on vivahteita - katso alatyypit ja polymorfismi monimutkaisille tapauksille.
Lisäksi uusien tyyppien määrittelymekanismien voimakkaalla käytöllä estetään eri tyyppien semantiikasta aiheutuvat loogiset virheet [5] . Esimerkiksi sekä millimetrit että tuumat ovat pituusyksiköitä ja ne voidaan esittää kokonaislukuina, mutta olisi virhe vähentää tuumaa millimetreistä, eikä kehitetty tyyppijärjestelmä salli tätä (tietenkin edellyttäen, että ohjelmoija käyttää eri tyyppejä arvoille, jotka on ilmaistu eri yksiköissä). Toisin sanoen kieliturva tarkoittaa sitä, että kieli suojaa ohjelmoijaa hänen omilta mahdollisilta virheiltä [9] .
Monet järjestelmän ohjelmointikielet (esim. Ada , C , C++ ) tarjoavat vaarallisia ( epäturvallisia ) tai vaarallisia ( ei turvallisia ) toimintoja, jotka on suunniteltu rikkomaan ( eng . loukkaamaan ) tyyppijärjestelmää - katso tyypin casting ja sanakirjoitus . Joissakin tapauksissa tämä on sallittua vain rajoitetuissa ohjelman osissa, toisissa sitä ei voi erottaa hyvin kirjoitetuista toiminnoista [11] .
Valtavirrassa[ selventää ] Ei ole harvinaista nähdä tyyppisuojauksen supistuminen " muistityypin turvallisuuteen " , mikä tarkoittaa , että yhden aggregaattityypin objektien komponentit eivät pääse käsiksi toisen tyyppisille objekteille varattuihin muistipaikkoihin . Muistin käyttösuojaus tarkoittaa, että ei pysty kopioimaan mielivaltaista bittijonoa yhdeltä muistialueelta toiselle. Jos esimerkiksi kieli tarjoaa tyypin , jolla on rajoitettu alue kelvollisia arvoja ja joka tarjoaa mahdollisuuden kopioida kirjoittamatonta dataa kyseisen tyypin muuttujaan, tämä ei ole tyyppiturvallinen, koska se mahdollistaa tyyppimuuttujan arvon. joka ei kelpaa tyypille . Ja erityisesti, jos tällainen vaarallinen kieli sallii mielivaltaisen kokonaislukuarvon kirjoittamisen " osoitin "-tyypin muuttujaan, muistin käytön vaarallisuus on ilmeistä (katso roikkuva osoitin ). Esimerkkejä vaarallisista kielistä ovat C ja C++ [4] . Näiden kielten yhteisöissä kaikkia toimintoja, jotka eivät suoraan aiheuta ohjelman kaatumista, kutsutaan usein "turvallisiksi" . Muistin käyttösuojaus tarkoittaa myös puskurin ylivuotojen estämistä , kuten suurten objektien kirjoittamista soluihin, jotka on varattu muun tyyppisille, pienempikokoisille objekteille. ttt
Luotettavat staattiset järjestelmät ovat konservatiivisia (redundantteja) siinä mielessä, että ne hylkäävät jopa ohjelmat, jotka suoriutuisivat oikein. Syynä tähän on se, että millä tahansa Turing-täydellisellä kielellä ohjelmien joukko, joka voi tuottaa tyyppisovitusvirheitä ajon aikana, on algoritmisesti ratkaisematon (katso pysäytysongelma ) [12] [13] . Tämän seurauksena tällaiset järjestelmät tarjoavat suojaustason, joka on huomattavasti korkeampi kuin on tarpeen muistin käytön turvallisuuden varmistamiseksi. Toisaalta joidenkin toimien turvallisuutta ei voida todistaa staattisesti, ja niitä on ohjattava dynaamisesti – esimerkiksi indeksoimalla satunnaispääsymatriisi. Tällaisen ohjauksen voi suorittaa joko itse kielen ajonaikainen järjestelmä tai suoraan toiminnot, jotka toteuttavat tällaisia mahdollisesti vaarallisia toimintoja.
Voimakkaasti dynaamisesti kirjoitetut kielet (esim . Lisp , Smalltalk ) eivät salli tietojen korruptoitumista, koska ohjelma, joka yrittää muuntaa arvon yhteensopimattomaksi tyypiksi, tekee poikkeuksen. Vahvan dynaamisen konekirjoituksen etuja tyyppiturvallisuuteen verrattuna ovat konservatiivisuuden puute ja sen seurauksena ratkaistavien ohjelmointitehtävien laajeneminen. Tämän hinta on väistämätön ohjelmien nopeuden hidastuminen sekä tarve tehdä huomattavasti suurempi määrä testiajoja mahdollisten virheiden tunnistamiseksi. Siksi monet kielet yhdistävät tavalla tai toisella staattisen ja dynaamisen tyyppiyhdenmukaisuuden hallinnan ominaisuudet. [14] [12] [1]
Ada ( Pascal -perheen tyyppiturvallisin kieli ) on keskittynyt luotettavien sulautettujen järjestelmien , ohjainten ja muiden järjestelmän ohjelmointitehtävien kehittämiseen . Kriittisten osien toteuttamiseksi Ada tarjoaa useita vaarallisia rakenteita, joiden nimet alkavat yleensä kirjaimella Unchecked_.
SPARK - kieli on Adan osajoukko. Se poisti vaaralliset ominaisuudet, mutta lisäsi suunnittelukohtaisia ominaisuuksia . SPARK eliminoi roikkuvien osoittimien mahdollisuuden eliminoimalla dynaamisen muistin varauksen mahdollisuuden. Staattisesti varmennettuja sopimuksia on lisätty Ada2012:een.
Hoare väitti Turingin luennossa, että staattiset tarkastukset eivät riitä varmistamaan luotettavuutta - luotettavuus on ensisijaisesti seurausta yksinkertaisuudesta [15] . Sitten hän ennusti, että Adan monimutkaisuus aiheuttaisi katastrofeja.
BitC on hybridikieli, joka yhdistää C : n matalan tason ominaisuudet Standard ML :n turvallisuuteen ja Scheme :n ytimekkyyteen . BitC on keskittynyt kehittämään kestäviä sulautettuja järjestelmiä , ohjaimia ja muita järjestelmän ohjelmointitehtäviä .
Tutkiva kieli Cyclone on C :n turvallinen murre, joka lainaa monia ideoita ML:stä (mukaan lukien tyyppiturvallinen parametrinen polymorfismi ). Cyclone on suunniteltu samoihin tehtäviin kuin C, ja kaikkien tarkistusten tekemisen jälkeen kääntäjä luo koodin ANSI C :ssä . Cyclone ei vaadi virtuaalikoneita tai roskienkeruuta dynaamista turvallisuutta varten - sen sijaan se perustuu muistinhallintaan alueiden kautta . Cyclone asettaa korkeamman rajan lähdekoodin turvallisuudelle, ja C:n epävarman luonteen vuoksi jopa yksinkertaisten ohjelmien siirtäminen C:stä Cyclone-ohjelmaan saattaa vaatia työtä, vaikka suuri osa siitä voidaan tehdä C:ssä ennen kääntäjien vaihtamista. Siksi Cyclonea ei usein määritellä C:n murteeksi, vaan " kieleksi, joka on syntaktisesti ja semanttisesti samanlainen kuin C ".
Monet Cyclonen ideat ovat löytäneet tiensä ruosteen kieleen . Vahvan staattisen kirjoituksen lisäksi kieleen on lisätty "omistus"-käsitteeseen perustuva staattinen osoittimien eliniän analyysi. Toteutetut staattiset rajoitukset, jotka estävät mahdollisesti virheellisen muistin käytön: ei nollaosoittimia, alustamattomia ja deinitialisoituja muuttujia ei voi ilmestyä, muuttuvien muuttujien jakaminen useiden tehtävien kesken on kielletty. On tarkistettava rajojen ulkopuolinen taulukko.
Haskell (ML:n jälkeläinen ) suunniteltiin alun perin tyypiltään puhtaaksi kieleksi, jonka piti tehdä siinä olevien ohjelmien käyttäytymisestä vieläkin ennakoitavampaa kuin aiemmissa ML :n murteissa . Myöhemmin kielistandardissa esiteltiin kuitenkin vaarallisia operaatioita [16] [17] , jotka ovat välttämättömiä jokapäiväisessä käytännössä, vaikka ne on merkitty asianmukaisilla tunnisteilla (alkaen ) [18] . unsafe
Haskell tarjoaa myös heikkoja dynaamisia kirjoitusominaisuuksia, ja poikkeusten käsittelymekanismin toteutus näiden ominaisuuksien kautta sisällytettiin kielistandardiin . Sen käyttö voi aiheuttaa ohjelmien kaatumisen, jota varten Robert Harper kutsui Haskellia " erittäin epävarmaksi " [18] . Hän pitää mahdottomana hyväksyä, että poikkeuksilla on tyyppi, jonka käyttäjä on määrittänyt tyyppiluokan Typeable yhteydessä , koska poikkeukset heitetään turvakoodilla ( monadin IO ulkopuolella ); ja luokittelee kääntäjän sisäisen virheilmoituksen sopimattomaksi Milnerin sloganille . Seuranneessa keskustelussa esitettiin, kuinka Standard ML -tyylisiä staattisesti tyyppiturvallisia poikkeuksia voidaan toteuttaa Haskellissa .
"Puhas" (minimaalinen) Lisp on yksityyppinen kieli (eli mikä tahansa rakennelma kuuluu tyyppiin " S-lauseke ") [19] , vaikka Lispin ensimmäiset kaupalliset toteutukset tarjosivatkin ainakin tietyn määrän atomeja. . Lisp-kielen jälkeläisperhettä edustavat enimmäkseen vahvasti dynaamisesti tyypitetyt kielet, mutta on staattisesti kirjoitettuja kieliä, joissa yhdistyvät molemmat kirjoitusmuodot.
Common Lisp on vahvasti dynaamisesti kirjoitettu kieli, mutta se tarjoaa mahdollisuuden nimenomaisesti ( manifest ) määrittää tyyppejä (ja SBCL- kääntäjä pystyy päättelemään ne itse ) , mutta tätä kykyä käytetään optimoimaan ja pakottamaan dynaamisia tarkistuksia ja ei tarkoita staattista tyyppistä turvallisuutta. Ohjelmoija voi asettaa kääntäjälle alemman dynaamisten tarkistusten tason suorituskyvyn parantamiseksi, eikä tällä tavalla käännettyä ohjelmaa voida enää pitää turvallisena [20] [21] .
Scheme - kieli on myös vahvasti dynaamisesti tyypitetty kieli, mutta Stalinin päättelee tyypit staattisesti ja käyttää niitä ohjelmien aggressiiviseen optimointiin. Kielet "Typed Racket" ( Racket Schemin laajennus ) ja Shen ovat tyyppiturvallisia . Clojure yhdistää vahvan dynaamisen ja staattisen kirjoittamisen.
ML-kieli kehitettiin alun perin interaktiiviseksi teoreemojen todistamisjärjestelmäksi , ja vasta myöhemmin siitä tuli itsenäinen yleiskäyttöinen käännöskieli. Paljon työtä on omistettu ML :n taustalla olevan parametrisesti polymorfisen Hindley-Milner-tyyppisen järjestelmän luotettavuuden osoittamiseksi . Turvallisuustodistus on rakennettu puhtaasti toiminnalliselle osajoukolle ( "Fuctional ML" ), laajennukselle viitetyypeillä ( "Reference ML" ), laajennukselle poikkeuksilla ( "Exception ML" ), kielelle, joka yhdistää kaikki nämä laajennukset ( " Core ML" ), ja lopuksi sen laajennukset ensiluokkaisilla jatkoilla ( "Control ML" ), ensin monomorfisia, sitten polymorfisia [2] .
Tämän seurauksena ML :n jälkeläisiä pidetään usein a priori tyyppiturvallisina, vaikka jotkin niistä lykkäävät tarkoituksenmukaiset tarkistukset ajonaikaiseen ( OCaml ) tai poikkeavat semantiikasta, jota varten turvallisuustodistus on rakennettu, ja sisältävät eksplisiittisesti vaarallisia. ominaisuuksia. ( Haskell ). ML-perheen kielille on ominaista kehitetty tuki algebrallisille tietotyypeille , joiden käyttö edistää merkittävästi loogisten virheiden ehkäisyä , mikä tukee myös tyyppiturvallisuuden vaikutelmaa.
Jotkut ML :n jälkeläiset ovat myös interaktiivisia todistustyökaluja ( Idris , Mercury , Agda ). Monia niistä, vaikka niitä voitaisiinkin käyttää ohjelmien suoraan kehittämiseen, joiden luotettavuus on todistettu, käytetään useammin muilla kielillä olevien ohjelmien varmentamiseen - johtuen sellaisista syistä kuin korkea käyttöintensiteetti, alhainen nopeus, FFI :n puute ja niin edelleen. Luotettaviksi todistetuista ML : n jälkeläisistä Standard ML ja sen jatkokehityksen seuraajan prototyyppi ML [22] (tunnetaan aiemmin nimellä "ML2000") erottuvat alalle suuntautuneina kielinä .
Standard ML -kieli ( ML - kieliperheen vanhin ) on keskittynyt laajamittaisten teollisten nopeusohjelmien kehittämiseen 23 ] . Kielellä on tiukka muodollinen määritelmä ja sen staattinen ja dynaaminen turvallisuus on todistettu [24] . Ohjelmakomponenttien (mukaan lukien generoidut - katso ML-funktiot ) liitäntöjen yhtenäisyyden staattisen tarkistuksen jälkeen ajonaikainen järjestelmä tukee lisäturvallisuuden valvontaa . Tästä johtuen jopa standardi ML- ohjelma, jossa on virhe, käyttäytyy aina kuten ML-ohjelma: se voi mennä laskelmiin ikuisesti tai antaa käyttäjälle virheilmoituksen, mutta se ei voi kaatua [9] .
Jotkut toteutukset ( SML/NJ , Mythryl , MLton ) sisältävät kuitenkin standardista poikkeavia kirjastoja , jotka tarjoavat tiettyjä vaarallisia toimintoja (niiden tunnisteet alkavat kirjaimella Unsafe). Näitä ominaisuuksia tarvitaan näiden toteutusten ulkoiselle kielirajapinnalle , joka tarjoaa vuorovaikutuksen ei-ML-koodin kanssa (yleensä C -koodi, joka toteuttaa nopeuskriittisiä ohjelmakomponentteja), mikä saattaa vaatia omituista datan bittiesitystä . Lisäksi monet Standard ML :n toteutukset , vaikka ne on kirjoitettu itsessään , käyttävät C - kielellä kirjoitettua ajonaikaista järjestelmää . Toinen esimerkki on SML/NJ -kääntäjän REPL -tila , joka käyttää vaarallisia toimintoja ohjelmoijan interaktiivisesti syöttämän koodin suorittamiseen.
Alice - kieli on Standard ML :n laajennus , joka tarjoaa vahvat dynaamiset kirjoitusominaisuudet.