Typsäkerhet är en egenskap hos ett programmeringsspråk som kännetecknar säkerheten och tillförlitligheten vid tillämpningen av dess typsystem .
Ett typsystem kallas säkert ( eng. säkert ) eller tillförlitligt ( eng. ljud ) om program som har klarat typ -konsistenskontroller ( eng. välskrivna program eller välformade program ) utesluter möjligheten för typkonsistensfel vid körning tid [1 ] [2] [3] [4] [5] [6] .
Typmatchningsfel eller skrivfel ( engelsk typ error ) - inkonsekvens i typerna av uttryckskomponenter i programmet, till exempel ett försök att använda ett heltal som funktion [7] . Saknade typmatchningsfel vid körning kan leda till buggar och till och med krascher . Ett språks säkerhet är inte synonymt med den fullständiga frånvaron av buggar, men de blir åtminstone utforskabara inom språkets semantik (formellt eller informellt) [8] .
Pålitliga typsystem kallas också starka ( eng. stark ) [1] [2] , men tolkningen av denna term mjukas ofta upp, dessutom används den ofta på språk som utför dynamisk typkonsistenskontroll ( stark och svag) skriver ).
Ibland ses säkerhet som en egenskap hos ett visst program snarare än språket som det är skrivet på, av den anledningen att vissa typsäkra språk tillåter att typsystemet kringgås eller kränks om programmeraren utövar dålig typsäkerhet. Det är en allmän uppfattning att sådana möjligheter i praktiken visar sig vara en nödvändighet, men detta är fiktion [9] . Begreppet "programsäkerhet" är viktigt i den meningen att en implementering av ett säkert språk i sig kan vara osäkert. Kompilatorns spin -up löser detta problem, vilket gör språket säkert inte bara i teorin utan även i praktiken.
Robin Milner myntade uttrycket "Program som klarar typkontroll kan inte "gå vilse" [10] . Med andra ord, ett typsäkert system förhindrar avsiktligt felaktiga operationer som involverar ogiltiga typer. Till exempel är uttrycket 3 / "Hello, World"uppenbarligen felaktigt, eftersom aritmetik inte definierar operationen att dividera ett tal med en sträng. Tekniskt sett innebär säkerhet att säkerställa att värdet för varje typkontrollerat uttryckτ av typ är en sann medlem av värdeuppsättningen τ, dvs. kommer att ligga inom det värdeintervall som tillåts av den statiska typen av uttrycket. Faktum är att det finns nyanser i detta krav - se undertyper och polymorfism för komplexa fall.
Dessutom, med stor användning av mekanismer för att definiera nya typer , förhindras logiska fel som är ett resultat av semantiken av olika typer [5] . Till exempel är både millimeter och tum längdenheter och kan representeras som heltal, men det skulle vara ett misstag att subtrahera tum från millimeter, och det utvecklade typsystemet tillåter inte detta (naturligtvis förutsatt att programmeraren använder olika typer för värden uttryckta i olika enheter). data, snarare än att beskriva båda som variabler av heltalstyp). Språksäkerhet innebär med andra ord att språket skyddar programmeraren från hans egna eventuella misstag [9] .
Många systemprogrammeringsspråk (t.ex. Ada , C , C++ ) tillhandahåller osäkra ( osunda ) eller osäkra ( osäkra ) operationer utformade för att kunna bryta mot ( eng . violate ) typsystemet - se typgjutning och ordleksskrivning . I vissa fall tillåts detta endast i begränsade delar av programmet, i andra är det omöjligt att skilja från välskrivna operationer [11] .
I mainstream[ förtydliga ] Det är inte ovanligt att se typsäkerhet begränsas till " minnestypsäkerhet " , vilket betyder att komponenter i objekt av en aggregattyp inte kan komma åt minnesplatser som tilldelats för objekt av en annan typ . Minnesåtkomstsäkerhet innebär att man inte kan kopiera en godtycklig sträng av bitar från ett minnesområde till ett annat. Till exempel, om ett språk tillhandahåller en typ som har ett begränsat intervall av giltiga värden och ger möjlighet att kopiera otypade data till en variabel av den typen, är detta inte typsäkert eftersom det potentiellt tillåter att en typvariabel har ett värde det är inte giltigt för typ . Och i synnerhet om ett sådant osäkert språk tillåter att ett godtyckligt heltalsvärde kan skrivas till en variabel av typen " pointer ", då är osäkerheten i minnesåtkomst uppenbar (se dinglande pekare ). Exempel på osäkra språk är C och C++ [4] . I dessa språks gemenskaper kallas alla operationer som inte direkt får programmet att krascha ofta som "säker" . Minnesåtkomstsäkerhet innebär också att förhindra möjligheten av buffertspill , som att försöka skriva stora objekt till celler som är allokerade för objekt av en annan typ av mindre storlek. ttt
Pålitliga statiska system är konservativa (redundanta) i den meningen att de avvisar även program som skulle köras korrekt. Anledningen till detta är att för alla Turing-komplett språk är uppsättningen av program som kan generera typmatchningsfel vid körning algoritmiskt oavgörbar (se stoppproblemet ) [12] [13] . Som en konsekvens ger sådana typsystem en grad av skydd som är väsentligt högre än vad som är nödvändigt för att säkerställa minnesåtkomstsäkerhet. Å andra sidan kan säkerheten för vissa åtgärder inte bevisas statiskt och måste kontrolleras dynamiskt – till exempel indexering av en array med slumpmässig åtkomst. Sådan kontroll kan utföras antingen av själva språkets runtime- system eller direkt av funktioner som implementerar sådana potentiellt osäkra operationer.
Starkt dynamiskt typade språk (t.ex. Lisp , Smalltalk ) tillåter inte datakorruption på grund av att ett program som försöker konvertera ett värde till en inkompatibel typ ger ett undantag. Fördelarna med stark dynamisk typning framför typsäkerhet inkluderar bristen på konservatism och, som ett resultat, utvidgningen av utbudet av programmeringsuppgifter som ska lösas. Priset för detta är den oundvikliga minskningen av programhastigheten, liksom behovet av ett betydligt större antal testkörningar för att identifiera möjliga fel. Därför kombinerar många språk kapaciteten för statisk och dynamisk typkonsistenskontroll på ett eller annat sätt. [14] [12] [1]
Ada (det mest typsäkra språket i Pascal -familjen ) är fokuserat på utvecklingen av pålitliga inbyggda system , drivrutiner och andra systemprogrammeringsuppgifter . För att implementera kritiska avsnitt tillhandahåller Ada ett antal osäkra konstruktioner vars namn vanligtvis börjar med Unchecked_.
SPARK - språket är en delmängd av Ada. Det tog bort osäkra funktioner men lade till design-by-contract funktioner . SPARK eliminerar möjligheten att dinglande pekare genom att eliminera själva möjligheten till dynamisk minnesallokering. Statiskt verifierade kontrakt har lagts till Ada2012.
Hoare , i en Turing-föreläsning, hävdade att statiska kontroller inte är tillräckligt för att säkerställa tillförlitlighet - tillförlitlighet är främst en konsekvens av enkelhet [15] . Sedan förutspådde han att Adas komplexitet skulle orsaka katastrofer.
BitC är ett hybridspråk som kombinerar lågnivåfunktionerna i C med säkerheten i Standard ML och koncisheten i Scheme . BitC är fokuserat på att utveckla robusta inbyggda system , drivrutiner och andra systemprogrammeringsuppgifter .
Det utforskande språket Cyclone är en säker dialekt av C som lånar många idéer från ML (inklusive typsäker parametrisk polymorfism ). Cyclone är designad för samma uppgifter som C, och efter att ha gjort alla kontroller genererar kompilatorn kod i ANSI C . Cyclone kräver ingen virtuell maskin eller sophämtning för dynamisk säkerhet - istället är den baserad på minneshantering genom regioner . Cyclone sätter en högre stapel för källkodssäkerhet, och på grund av den osäkra naturen hos C kan portering av enkla program från C till Cyclone kräva en del arbete, även om mycket av det kan göras inom C innan du byter kompilator. Därför definieras Cyclone ofta inte som en dialekt av C, utan som " ett språk som syntaktiskt och semantiskt liknar C ".
Många av Cyclones idéer har hittat sin väg in i språket Rust . Förutom stark statisk typning har statisk analys av pekarnas livslängd baserad på begreppet "äganderätt" lagts till språket. Implementerade statiska begränsningar som blockerar potentiellt felaktig minnesåtkomst: inga nollpekare, oinitierade och avinitierade variabler kan inte visas, delning av föränderliga variabler med flera uppgifter är förbjuden. Kontrollera för out-of-bounds array krävs.
Haskell (en ättling till ML ) var ursprungligen designad som ett typfullt rent språk, vilket var tänkt att göra beteendet hos program i det ännu mer förutsägbart än i tidigare dialekter av ML . Men senare i språkstandarden tillhandahölls osäkra operationer [16] [17] , som är nödvändiga i vardagen, även om de är markerade med lämpliga identifierare (som börjar med ) [18] . unsafe
Haskell tillhandahåller också svaga dynamiska skrivfunktioner, och implementeringen av undantagshanteringsmekanismen genom dessa funktioner inkluderades i språkstandarden . Dess användning kan få program att krascha, vilket Robert Harper kallade Haskell för " extremt osäker " [18] . Han anser att det är oacceptabelt att undantag har en typ definierad av användaren i sammanhanget av en typklass Typeable , med tanke på att undantag kastas av säker kod (utanför monaden IO ); och klassificerar kompilatorns interna felmeddelande som olämpligt för Milners slogan . I diskussionen som följde visades hur Standard ML -stil statiskt typsäkra undantag kunde implementeras i Haskell .
"Rent" (minimalt) Lisp är ett språk av en typ (det vill säga alla konstruktioner tillhör typen " S-uttryck ") [19] , även om även de första kommersiella implementeringarna av Lisp gav åtminstone ett visst antal atomer . Familjen av ättlingar till Lisp-språket representeras mestadels av starkt dynamiskt typade språk, men det finns statiskt typade språk som kombinerar båda formerna av maskinskrivning.
Common Lisp är ett starkt dynamiskt skrivet språk, men det ger möjlighet att explicit ( manifest ) tilldela typer (och SBCL- kompilatorn kan härleda dem själv ) , men denna förmåga används för att optimera och genomdriva dynamiska kontroller och innebär inte statisk typsäkerhet. Programmeraren kan ställa in en lägre nivå av dynamiska kontroller för kompilatorn för att förbättra prestandan, och programmet som kompilerats på detta sätt kan inte längre anses vara säkert [20] [21] .
Schema -språket är också ett starkt dynamiskt skrivet språk, men Stalin - härleder statiskt typer och använder dem för att aggressivt optimera program. Språken "Typed Racket" (en förlängning av Racket Scheme ) och Shen är typsäkra . Clojure kombinerar stark dynamisk och statisk typning.
ML - språket utvecklades ursprungligen som ett interaktivt teorembevisande system , och blev först senare ett oberoende sammanställt språk för allmänt ändamål. Mycket ansträngning har ägnats åt att bevisa tillförlitligheten hos det parametriskt polymorfa Hindley-Milner-systemet som ligger bakom ML . Säkerhetsbeviset är byggt för en rent funktionell delmängd ( "Fuctional ML" ), en förlängning av referenstyper ( "Reference ML" ), en förlängning av undantag ( "Exception ML" ), ett språk som kombinerar alla dessa tillägg ( " Core ML" ), och slutligen dess förlängningar med förstklassiga fortsättningar ( "Control ML" ), först monomorf, sedan polymorf [2] .
Konsekvensen av detta är att ML- avkomlingar ofta a priori anses vara typsäkra, även om vissa av dem skjuter upp meningsfulla kontroller till körtid ( OCaml ), eller avviker från den semantik som säkerhetsbeviset är byggt för och uttryckligen innehåller osäkra funktioner ( Haskell ). Språken i ML-familjen kännetecknas av utvecklat stöd för algebraiska datatyper , vars användning avsevärt bidrar till att förhindra logiska fel , vilket också stöder intrycket av typsäkerhet.
Vissa ättlingar till ML är också interaktiva bevisverktyg ( Idris , Mercury , Agda ). Många av dem, även om de skulle kunna användas för direkt utveckling av program med bevisad tillförlitlighet, används oftare för att verifiera program på andra språk - på grund av sådana skäl som hög arbetsintensitet vid användning, låg hastighet, brist på FFI och så vidare. Bland ättlingarna till ML med bevisad tillförlitlighet utmärker sig Standard ML och prototypen av dess vidareutvecklingsefterföljare ML [22] (tidigare känd som "ML2000") som branschorienterade språk .
Standard ML-språket (det äldsta i ML -familjen av språk ) är fokuserat på utvecklingen av storskaliga industriella hastighetsprogram 23] . Språket har en strikt formell definition och dess statiska och dynamiska säkerhet har bevisats [24] . Efter en statisk kontroll av konsistensen av gränssnitten för programkomponenter (inklusive genererade sådana - se ML-funktioner ), stöds ytterligare säkerhetskontroll av runtime- systemet . Som en följd av detta beter sig alltid ett standard ML- program med en bugg som ett ML-program: det kan gå in i beräkningar för alltid eller ge användaren ett felmeddelande, men det kan inte krascha [9] .
Vissa implementeringar ( SML/NJ , Mythryl , MLton ) inkluderar dock icke-standardiserade bibliotek som tillhandahåller vissa osäkra operationer (deras identifierare börjar med Unsafe). Dessa funktioner behövs för det externa språkgränssnittet av dessa implementeringar, vilket ger interaktion med icke-ML-kod (vanligtvis C -kod som implementerar hastighetskritiska programkomponenter), vilket kan kräva en speciell bitrepresentation av data. Dessutom använder många implementeringar av Standard ML , även om de själva är skrivna i sig , ett runtime- system skrivet i C. Ett annat exempel är REPL- läget för SML/NJ kompilatorn , som använder osäkra operationer för att exekvera kod som matas in interaktivt av programmeraren.
Alice - språket är en förlängning av Standard ML , som ger starka dynamiska skrivmöjligheter.