Typesikkerhed er en egenskab ved et programmeringssprog, der karakteriserer sikkerheden og pålideligheden ved anvendelsen af dets typesystem .
Et typesystem kaldes sikkert ( eng. sikker ) eller pålidelig ( eng. lyd ), hvis programmer, der har bestået type- konsistenstjek ( eng. well-typed programs eller well-formed programs ) udelukker muligheden for type-konsistensfejl ved kørsel tid [1 ] [2] [3] [4] [5] [6] .
Typematching error eller typing error ( engelsk type error ) - inkonsistens i typerne af udtrykskomponenter i programmet, for eksempel et forsøg på at bruge et heltal som en funktion [7] . Manglende runtime type-matching fejl kan føre til fejl og endda nedbrud . Et sprogs sikkerhed er ikke synonymt med fuldstændigt fravær af fejl, men de bliver i det mindste udforskbare inden for sprogets semantik (formelle eller uformelle) [8] .
Pålidelige typesystemer kaldes også stærke ( eng. strong ) [1] [2] , men fortolkningen af dette udtryk er ofte blødgjort, derudover anvendes det ofte på sprog, der udfører dynamisk typekonsistenskontrol ( stærk og svag ) skrive ).
Nogle gange ses sikkerhed som en egenskab ved et bestemt program snarere end det sprog, det er skrevet på, af den grund, at nogle typesikre sprog tillader typesystemet at blive omgået eller krænket , hvis programmøren praktiserer dårlig typesikkerhed. Det er en udbredt opfattelse, at sådanne muligheder i praksis viser sig at være en nødvendighed, men dette er fiktion [9] . Begrebet "programsikkerhed" er vigtigt i den forstand, at en implementering af et sikkert sprog i sig selv kan være usikker. Compiler-spin- up'en løser dette problem, hvilket gør sproget sikkert ikke kun i teorien, men også i praksis.
Robin Milner opfandt sætningen "Programmer, der passerer typekontrol, kan ikke 'gå på afveje'" [10] . Med andre ord forhindrer et typesikkert system bevidst fejlagtige operationer, der involverer ugyldige typer. For eksempel er udtrykket 3 / "Hello, World"åbenlyst forkert, da aritmetik ikke definerer operationen med at dividere et tal med en streng. Teknisk set betyder sikkerhed at sikre, at værdien af ethvert typekontrolleret udtrykτ er et sandt medlem af værdisættet τ, dvs. vil ligge inden for det værdiområde, der tillades af den statiske type af det pågældende udtryk. Faktisk er der nuancer til dette krav - se undertyper og polymorfi for komplekse sager.
Hertil kommer, at med stor brug af mekanismer til at definere nye typer , forhindres logiske fejl som følge af semantikken af forskellige typer [5] . For eksempel er både millimeter og tommer længdeenheder og kan repræsenteres som heltal, men det ville være en fejl at trække tommer fra millimeter, og det udviklede typesystem vil ikke tillade dette (selvfølgelig forudsat at programmøren bruger forskellige typer for værdier udtrykt i forskellige enheder). data, snarere end at beskrive begge som variable af en heltalstype). Sprogsikkerhed betyder med andre ord, at sproget beskytter programmøren mod hans egne mulige fejl [9] .
Mange systemprogrammeringssprog (f.eks. Ada , C , C++ ) sørger for usikre ( usunde ) eller usikre ( usikre ) operationer designet til at være i stand til at krænke ( eng . violate ) typesystemet - se typecasting og pun typing . I nogle tilfælde er dette kun tilladt i begrænsede dele af programmet, i andre kan det ikke skelnes fra velskrevne operationer [11] .
I mainstream[ klargør ] Det er ikke ualmindeligt at se typesikkerhed indsnævret til " hukommelsestypesikkerhed ", hvilket betyder, at komponenter af objekter af en samlet type ikke kan få adgang til hukommelsesplaceringer, der er allokeret til objekter af en anden type . Hukommelsesadgangssikkerhed betyder ikke at være i stand til at kopiere en vilkårlig streng af bits fra et hukommelsesområde til et andet. For eksempel, hvis et sprog leverer en type , der har et begrænset område af gyldige værdier, og giver mulighed for at kopiere utypedata til en variabel af den type, så er dette ikke type sikkert, fordi det potentielt tillader en typevariabel at have en værdi det er ikke gyldigt for type . Og især, hvis et sådant usikkert sprog tillader, at en vilkårlig heltalværdi skrives til en variabel af typen " pointer ", så er usikkerheden ved hukommelsesadgang indlysende (se dinglende pointer ). Eksempler på usikre sprog er C og C++ [4] . I disse sprogs fællesskaber omtales enhver handling, der ikke direkte får programmet til at gå ned , ofte som "sikker" . Hukommelsesadgangssikkerhed betyder også at forhindre muligheden for bufferoverløb , såsom forsøg på at skrive store objekter til celler, der er allokeret til objekter af en anden type af mindre størrelse. ttt
Pålidelige statiske systemer er konservative (redundante) i den forstand, at de afviser selv programmer, der ville køre korrekt. Årsagen til dette er, at for ethvert Turing-komplet sprog er det sæt af programmer, der kan generere typetilpasningsfejl under kørsel, algoritmisk uafgørligt (se stopproblemet ) [12] [13] . Som følge heraf giver sådanne typesystemer en grad af beskyttelse, der er væsentligt højere end nødvendigt for at sikre hukommelsesadgangssikkerhed. På den anden side kan sikkerheden af nogle handlinger ikke bevises statisk og skal styres dynamisk - for eksempel indeksering af et array med tilfældig adgang. Sådan kontrol kan udføres enten af selve sprogets runtime- system eller direkte af funktioner, der implementerer sådanne potentielt usikre operationer.
Stærkt dynamisk indtastede sprog (f.eks . Lisp , Smalltalk ) tillader ikke datakorruption på grund af det faktum, at et program, der forsøger at konvertere en værdi til en inkompatibel type, giver en undtagelse. Fordelene ved stærk dynamisk skrivning frem for typesikkerhed omfatter manglen på konservatisme og som et resultat udvidelsen af rækken af programmeringsopgaver, der skal løses. Prisen for dette er det uundgåelige fald i programmernes hastighed, samt behovet for et betydeligt større antal testkørsler for at identificere mulige fejl. Derfor kombinerer mange sprog mulighederne for statisk og dynamisk typekonsistenskontrol på en eller anden måde. [14] [12] [1]
Ada (det mest typesikre sprog i Pascal- familien ) er fokuseret på udvikling af pålidelige indlejrede systemer , drivere og andre systemprogrammeringsopgaver . For at implementere kritiske sektioner giver Ada en række usikre konstruktioner, hvis navne normalt begynder med . Unchecked_
SPARK - sproget er en delmængde af Ada. Det fjernede usikre funktioner, men tilføjede design-for-kontrakt funktioner . SPARK eliminerer muligheden for hængende pointere ved at eliminere selve muligheden for dynamisk hukommelsesallokering. Statisk verificerede kontrakter er blevet tilføjet til Ada2012.
Hoare argumenterede i et Turing-foredrag, at statiske kontroller ikke er nok til at sikre pålidelighed - pålidelighed er primært en konsekvens af enkelhed [15] . Så forudsagde han, at kompleksiteten af Ada ville forårsage katastrofer.
BitC er et hybridsprog, der kombinerer C -funktionerne på lavt niveau med sikkerheden i Standard ML og det kortfattede i Scheme . BitC er fokuseret på at udvikle robuste indlejrede systemer , drivere og andre systemprogrammeringsopgaver .
Det udforskende sprog Cyclone er en sikker dialekt af C , der låner mange ideer fra ML (herunder typesikker parametrisk polymorfi ). Cyclone er designet til de samme opgaver som C, og efter at have udført alle kontroller, genererer compileren kode i ANSI C. Cyclone kræver ikke en virtuel maskine eller affaldsopsamling for dynamisk sikkerhed - i stedet er den baseret på hukommelsesstyring gennem regioner . Cyclone sætter en højere streg for kildekodesikkerhed, og på grund af den usikre karakter af C, kan portering af selv simple programmer fra C til Cyclone kræve noget arbejde, selvom meget af det kan gøres inden for C, før du skifter compilere. Derfor defineres Cyclone ofte ikke som en dialekt af C, men som " et sprog, der syntaktisk og semantisk ligner C ".
Mange af Cyclones ideer har fundet vej til Rust -sproget . Ud over stærk statisk typning er der tilføjet en statisk analyse af pointers levetid baseret på begrebet "ejerskab" til sproget. Implementerede statiske begrænsninger, der blokerer potentielt ukorrekt hukommelsesadgang: ingen null-pointere, uinitialiserede og deinitialiserede variabler kan ikke vises, deling af variable variable med flere opgaver er forbudt. Check for out-of-bounds-array er påkrævet.
Haskell (en efterkommer af ML ) blev oprindeligt designet som et typefuldt rent sprog, som skulle gøre opførselen af programmer i det endnu mere forudsigelig end i tidligere dialekter af ML . Men senere i sprogstandarden blev der tilvejebragt usikre operationer [16] [17] , som er nødvendige i daglig praksis, selvom de er markeret med passende identifikatorer (startende med ) [18] . unsafe
Haskell leverer også svage dynamiske skrivefunktioner, og implementering af undtagelseshåndteringsmekanismen gennem disse funktioner var inkluderet i sprogstandarden . Dets brug kan få programmer til at gå ned, som Robert Harper kaldte Haskell for " ekstremt usikker " [18] . Han anser det for uacceptabelt, at undtagelser har en type defineret af brugeren i sammenhæng med en typeklasse Typeable , givet at undtagelser er smidt af sikker kode (uden for monaden IO ); og klassificerer compilerens interne fejlmeddelelse som upassende for Milners slogan . I den efterfølgende diskussion blev det vist, hvordan Standard ML - stil statisk typesikre undtagelser kunne implementeres i Haskell .
"Ren" (minimal) Lisp er et enkelt-type sprog (det vil sige, at enhver konstruktion tilhører typen " S-udtryk ") [19] , selvom selv de første kommercielle implementeringer af Lisp sørgede for mindst et vist antal atomer . Familien af efterkommere af Lisp-sproget er for det meste repræsenteret af stærkt dynamisk indtastede sprog, men der er statisk maskinskrevne sprog, der kombinerer begge former for maskinskrivning.
Common Lisp er et stærkt dynamisk skrevet sprog, men det giver mulighed for eksplicit ( manifest ) at tildele typer (og SBCL- kompileren er i stand til selv at udlede dem ) , men denne evne bruges til at optimere og håndhæve dynamiske kontroller og indebærer ikke statisk type sikkerhed. Programmøren kan indstille et lavere niveau af dynamiske kontroller for compileren for at forbedre ydeevnen, og programmet kompileret på denne måde kan ikke længere betragtes som sikkert [20] [21] .
Skema-sproget er også et stærkt dynamisk skrevet sprog, men Stalin - udleder statisk typer og bruger dem til aggressivt at optimere programmer. Sprogene "Typed Racket" (en udvidelse af Racket Scheme ) og Shen er typesikre . Clojure kombinerer stærk dynamisk og statisk typning.
ML-sproget blev oprindeligt udviklet som et interaktivt teorembevissystem og blev først senere et uafhængigt kompileret sprog til generelle formål. Der er blevet brugt mange kræfter på at bevise pålideligheden af det parametrisk polymorfe Hindley-Milner type system, der ligger til grund for ML . Sikkerhedsbeviset er bygget til en rent funktionel delmængde ( "Fuctional ML" ), en udvidelse efter referencetyper ( "Reference ML" ), en udvidelse med undtagelser ( "Exception ML" ), et sprog, der kombinerer alle disse udvidelser ( " Core ML" ), og endelig dens udvidelser med førsteklasses fortsættelser ( "Control ML" ), først monomorfe, derefter polymorfe [2] .
Konsekvensen af dette er, at ML -efterkommere ofte på forhånd anses for at være typesikre, selvom nogle af dem udsætter meningsfulde kontroller til runtime ( OCaml ), eller afviger fra den semantik, som sikkerhedsbeviset er bygget til, og eksplicit indeholder usikre funktioner ( Haskell ). Sprogene i ML-familien er kendetegnet ved udviklet understøttelse af algebraiske datatyper , hvis brug bidrager væsentligt til at forhindre logiske fejl , hvilket også understøtter indtrykket af typesikkerhed.
Nogle efterkommere af ML er også interaktive bevisværktøjer ( Idris , Mercury , Agda ). Mange af dem, selvom de kunne bruges til direkte udvikling af programmer med dokumenteret pålidelighed, bruges oftere til at verificere programmer på andre sprog - på grund af sådanne årsager som høj arbejdsintensitet, lav hastighed, mangel på FFI og så videre. Blandt efterkommerne af ML med dokumenteret pålidelighed skiller Standard ML og prototypen af dets videreudviklingsefterfølger ML [22] (tidligere kendt som "ML2000") sig ud som industriorienterede sprog .
Standard ML-sproget (det ældste i ML -sprogfamilien ) er fokuseret på udviklingen af industrielle hastighedsprogrammer i stor skala 23] . Sproget har en streng formel definition og dets statiske og dynamiske sikkerhed er bevist [24] . Efter en statisk kontrol af konsistensen af programkomponenternes grænseflader (inklusive genererede - se ML -funktioner ), understøttes yderligere sikkerhedskontrol af runtime- systemet . Som en konsekvens heraf opfører selv et Standard ML -program med en fejl sig altid som et ML-program: det kan gå i beregninger for evigt eller give brugeren en fejlmeddelelse, men det kan ikke gå ned [9] .
Nogle implementeringer ( SML/NJ , Mythryl , MLton ) inkluderer dog ikke-standardiserede biblioteker , der giver visse usikre operationer (deres identifikatorer begynder med Unsafe). Disse muligheder er nødvendige for den eksterne sproggrænseflade af disse implementeringer, som giver interaktion med ikke-ML-kode (normalt C -kode , der implementerer hastighedskritiske programkomponenter), hvilket kan kræve en ejendommelig bitrepræsentation af data. Derudover bruger mange implementeringer af Standard ML , selvom de er skrevet i sig selv , et runtime- system skrevet i C. Et andet eksempel er REPL -tilstanden for SML/NJ compileren , som bruger usikre operationer til at udføre kode, der er indtastet interaktivt af programmøren.
Alice - sproget er en udvidelse af Standard ML , der giver stærke dynamiske skriveegenskaber.