Type sikkerhed - Type safety

Typesystemer
Generelle begreber
Store kategorier
Mindre kategorier

I datalogi , typen sikkerhed er, i hvilket omfang et programmeringssprog fraråder eller forhindrer skrive fejl . En typefejl er en forkert programadfærd forårsaget af en uoverensstemmelse mellem forskellige datatyper for programmets konstanter, variabler og metoder (funktioner), f.eks. Behandling af et heltal ( int ) som et flydende tal ( float ) Bedre eksempel er påkrævet . Typesikkerhed anses undertiden alternativt for at være en ejendom for et computerprogram frem for det sprog, som programmet er skrevet på; det vil sige, at nogle sprog har typesikre faciliteter, der kan omgås af programmører, der bruger andre type-usikre faciliteter på samme sprog. Den formelle typeteoretiske definition af typesikkerhed er betydeligt stærkere end hvad de fleste programmører forstår.

Typehåndhævelse kan være statisk, fange potentielle fejl på kompileringstidspunktet eller dynamisk, forbinde typeoplysninger med værdier i løbetid og konsultere dem efter behov for at opdage overhængende fejl eller en kombination af begge. Dynamisk typehåndhævelse tillader i det væsentlige et ugyldigt program at køre.

Den adfærd, der er klassificeret som typefejl ved et givet programmeringssprog, er normalt dem, der skyldes forsøg på at udføre operationer på værdier , der ikke er af den relevante datatype . Denne klassifikation er delvist baseret på mening.

I forbindelse med statiske (kompileringstid) typesystemer indebærer typesikkerhed normalt (blandt andet) en garanti for, at den eventuelle værdi af ethvert udtryk vil være et legitimt medlem af dette udtryks statiske type. Det præcise krav er mere subtilt end dette - se f.eks. Subtyping og Polymorphism (datalogi) for komplikationer.

Typesikkerhed er tæt forbundet med hukommelsessikkerhed , en begrænsning af muligheden for at kopiere vilkårlige bitmønstre fra et hukommelsessted til et andet. For eksempel i en implementering af et sprog, der har en eller anden type , sådan at en række bits (af den passende længde) ikke repræsenterer et legitimt medlem af , hvis dette sprog tillader data at blive kopieret til en variabel af typen , så er det er ikke typesikker, fordi en sådan handling kan tildele en variabel en ikke- værdi. Omvendt, hvis sproget er type-usikkert i den grad, at et vilkårligt heltal kan bruges som en markør , så er det ikke hukommelsessikkert.

De fleste statisk typede sprog giver en grad af typesikkerhed, der er strengt stærkere end hukommelsessikkerhed, fordi deres typesystemer håndhæver korrekt brug af abstrakte datatyper defineret af programmører, selvom dette ikke er strengt nødvendigt for hukommelsessikkerhed eller for at forhindre enhver form af katastrofalt svigt.

Definitioner

Typesikker kode får kun adgang til de hukommelsessteder, som den er autoriseret til at få adgang til. (I denne diskussion henviser typesikkerhed specifikt til hukommelsestypesikkerhed og må ikke forveksles med typesikkerhed i en større henseende.) Typesikker kode kan for eksempel ikke læse værdier fra et andet objekts private felter.

Robin Milner gav følgende slogan for at beskrive typesikkerhed:

Godt typede programmer kan ikke "gå galt".

Den passende formalisering af dette slogan afhænger af den formelle form for semantik, der bruges til et bestemt sprog. I forbindelse med denotationssemantik betyder typesikkerhed , at værdien af ​​et udtryk, der er velskrevet, f.eks. Med typen τ, er et bona fide- medlem af det sæt, der svarer til τ.

I 1994 formulerede Andrew Wright og Matthias Felleisen , hvad der nu er standarddefinitionen og bevisteknikken for typesikkerhed på sprog defineret af operativ semantik . Under denne tilgang bestemmes typesikkerhed af to egenskaber ved semantikken i programmeringssproget:

(Type-) bevarelse eller motivreduktion
"Welltypedness" ("typability") af programmer forbliver uændret under sprogets overgangsregler (dvs. evalueringsregler eller reduktionsregler).
Fremskridt
Et velskrevet (skrivbart) program bliver aldrig "fast", hvilket betyder, at udtrykkene i programmet enten vil blive evalueret til en værdi , eller der er en overgangsregel for det; med andre ord, programmet kommer aldrig i en udefineret tilstand, hvor der ikke er mulighed for yderligere overgange.

Disse egenskaber eksisterer ikke i et vakuum; de er knyttet til semantikken i det programmeringssprog, de beskriver, og der er et stort rum med forskellige sprog, der kan passe til disse kriterier, da begrebet "velskrevet" program er en del af programmeringssprogets statiske semantik og forestillingen at "sidde fast" (eller "gå galt") er en egenskab ved dens dynamiske semantik .

Vijay Saraswat giver følgende definition:

"Et sprog er typesikkert, hvis de eneste handlinger, der kan udføres på data på sproget, er dem, der er sanktioneret af datatypen."

Forhold til andre former for sikkerhed

Typesikkerhed er i sidste ende rettet mod at udelukke andre problemer, f.eks .:-

  • Forebyggelse af ulovlige operationer. For eksempel kan vi identificere et udtryk 3 / "Hello, World"som ugyldig, fordi reglerne for aritmetiske ikke angiver, hvordan man opdele et heltal med en snor .
  • Hukommelsessikkerhed
    • Vilde pointer kan opstå, når en markør til en type objekt behandles som en markør til en anden type. For eksempel afhænger størrelsen af ​​et objekt på typen, så hvis en markør øges under de forkerte legitimationsoplysninger, vil det ende med at pege på et vilkårligt område af hukommelsen.
    • Bufferoverløb - Out -of bound -skrivninger kan ødelægge indholdet af objekter, der allerede findes på bunken. Dette kan forekomme, når et større objekt af en type groft kopieres til mindre objekt af en anden type.
  • Logiske fejl, der stammer fra semantikken af forskellige typer. F.eks. Kan inches og millimeter begge gemmes som heltal, men bør ikke erstattes af hinanden eller tilføjes. Et typesystem kan håndhæve to forskellige typer heltal for dem.

Typesikre og usikre sprog

Typesikkerhed er normalt et krav for ethvert legetøjssprog, der foreslås i forskning i programmeringssprog. Mange sprog er derimod for store til menneskeskabte typesikkerhedsbeviser, da de ofte kræver kontrol af tusindvis af sager. Ikke desto mindre har nogle sprog som Standard ML , der har nøje defineret semantik, vist sig at opfylde en definition af typesikkerhed. Nogle andre sprog som Haskell er menes at møde nogle definitionen af type sikkerhed, forudsat visse "flygte" funktioner er ikke anvendes (f.eks Haskell s unsafePerformIO , bruges til at "flygte" fra den sædvanlige begrænset miljø, hvor I / O er muligt, omgår typesystemet og kan derfor bruges til at bryde typesikkerheden .) Type punning er et andet eksempel på sådan en "flugt" -funktion. Uanset egenskaberne ved sprogdefinitionen kan der opstå visse fejl i løbetid på grund af fejl i implementeringen eller i sammenkædede biblioteker skrevet på andre sprog; sådanne fejl kan under visse omstændigheder gøre en given implementeringstype usikker. En tidlig version af Suns virtuelle Java -maskine var sårbar over for denne slags problemer.

Stærk og svag skrivning

Hovedartikel: Stærk og svag skrivning

Programmeringssprog klassificeres ofte i daglig tale som stærkt typede eller svagt typede (også løst typede) for at henvise til visse aspekter af typesikkerhed. I 1974 definerede Liskov og Zilles et stærkt tastet sprog som et sprog, hvor "når et objekt sendes fra en kaldende funktion til en kaldet funktion, skal dets type være kompatibel med den type, der er deklareret i den kaldte funktion." I 1977 skrev Jackson: "I et stærkt indtastet sprog vil hvert dataområde have en særskilt type, og hver proces angiver sine kommunikationskrav med hensyn til disse typer." I modsætning hertil kan et svagt indtastet sprog frembringe uforudsigelige resultater eller udføre implicit typekonvertering.

Skriv sikkerhed i objektorienterede sprog

I objektorienterede sprog er typesikkerhed sædvanligvis iboende i, at et typesystem er på plads. Dette udtrykkes i form af klasse definitioner.

En klasse definerer i det væsentlige strukturen af ​​de objekter, der stammer fra den, og en API som en kontrakt for håndtering af disse objekter. Hver gang et nyt objekt oprettes, vil det overholde denne kontrakt.

Hver funktion, der udveksler objekter, der stammer fra en bestemt klasse, eller implementerer en bestemt grænseflade , vil overholde denne kontrakt: derfor vil den tilladte handling på dette objekt kun være dem, der er defineret af metoderne i den klasse, objektet implementerer. Dette vil garantere, at objektets integritet bevares.

Undtagelser fra dette er objektorienterede sprog, der tillader dynamisk ændring af objektstrukturen eller brug af refleksion til at ændre indholdet af et objekt for at overvinde de begrænsninger, der er pålagt af klassemetodedefinitionerne.

Skriv sikkerhedsproblemer på bestemte sprog

Ada

Ada var designet til at være velegnet til integrerede systemer , enhedsdrivere og andre former for systemprogrammering , men også for at tilskynde til programmering med sikkerhed. For at løse disse modstridende mål begrænser Ada type-usikkerhed til et bestemt sæt specielle konstruktioner, hvis navne normalt begynder med strengen Unchecked_ . Unchecked_Deallocation kan effektivt udelukkes fra en enhed med Ada -tekst ved at anvende pragma Pure på denne enhed. Det forventes, at programmører vil bruge Unchecked_ -konstruktioner meget omhyggeligt og kun når det er nødvendigt; programmer, der ikke bruger dem, er typesikre.

Det sprog SPARK programmering er en delmængde af Ada eliminere alle potentielle tvetydigheder og usikkerhed, mens på samme tid tilføjer statisk kontrolleret kontrakter til sproget funktioner til rådighed. SPARK undgår problemerne med dinglende tips ved helt at afvise tildeling i løbetid.

Ada2012 tilføjer statisk kontrollerede kontrakter til selve sproget (i form af forud- og efterbetingelser samt type invarianter).

C

Det sprog C programmering er type sikkert i begrænsede sammenhænge; for eksempel genereres en kompileringstidsfejl, når der gøres et forsøg på at konvertere en markør til en type struktur til en markør til en anden type struktur, medmindre der bruges en eksplicit cast. En række meget almindelige operationer er imidlertid ikke-typesikre; for eksempel er den sædvanlige måde at udskrive et helt tal noget i stil med printf("%d", 12), hvor %dtellerne printfved løbetid forventer et heltalsargument. (Noget lignende printf("%s", 12), der fortæller funktionen at forvente en markør til en tegnstreng og alligevel leverer et heltalsargument, kan accepteres af kompilatorer, men vil producere udefinerede resultater.) Dette formindskes delvist af nogle kompilatorer (f.eks. Gcc) -kontrol skriv korrespondancer mellem printf -argumenter og formatstrenge.

Derudover giver C, ligesom Ada, uspecificerede eller udefinerede eksplicitte konverteringer; og i modsætning til i Ada er formsprog, der bruger disse konverteringer, meget almindelige og har været med til at give C et type-usikkert omdømme. For eksempel er standardmåden at allokere hukommelse på bunken at påberåbe en hukommelsesallokeringsfunktion, f.eks. mallocMed et argument, der angiver, hvor mange bytes der kræves. Funktionen returnerer en ikke -indtastet markør (type void *), som opkaldskoden eksplicit eller implicit skal caste til den relevante markørtype. Pre-standardiserede implementeringer af C krævede en eksplicit cast for at gøre det, derfor blev koden den accepterede praksis. (struct foo *) malloc(sizeof(struct foo))

C ++

Nogle funktioner i C ++, der fremmer mere typesikker kode:

C#

C# er typesikker (men ikke statisk typesikker). Det har understøttelse af ikke -typede pointers, men dette skal tilgås ved hjælp af det "usikre" søgeord, som kan være forbudt på kompilerniveau. Det har iboende understøttelse af validering af run-time cast. Cast kan valideres ved at bruge søgeordet "som", der returnerer en null-reference, hvis casten er ugyldig, eller ved at bruge en cast i C-stil, der kaster en undtagelse, hvis casten er ugyldig. Se C Sharp -konverteringsoperatører .

Uberettiget afhængighed af objekttypen (hvorfra alle andre typer stammer) risikerer at besejre formålet med C# -typesystemet. Det er normalt bedre praksis at opgive objektreferencer til fordel for generika , svarende til skabeloner i C ++ og generika i Java .

Java

Den Java-sproget er designet til at håndhæve typen sikkerhed. Alt i Java sker inde i et objekt, og hvert objekt er en forekomst af en klasse .

At gennemføre typen sikkerhed håndhævelse, hvert objekt, før brug, skal fordeles . Java tillader brug af primitive typer, men kun inde i korrekt tildelte objekter.

Nogle gange implementeres en del af typesikkerheden indirekte: f.eks. Klassen BigDecimal repræsenterer et flydende antal med vilkårlig præcision, men håndterer kun tal, der kan udtrykkes med en endelig repræsentation. Operationen BigDecimal.divide () beregner et nyt objekt som division af to tal udtrykt som BigDecimal.

I dette tilfælde, hvis divisionen ikke har en endelig repræsentation, som når man beregner f.eks. 1/3 = 0,33333 ..., kan metoden divide () rejse en undtagelse, hvis der ikke er defineret nogen afrundingstilstand for operationen. Derfor garanterer biblioteket frem for sproget, at objektet respekterer kontrakten, der er implicit i klassedefinitionen.

Standard ML

Standard ML har nøje defineret semantik og er kendt for at være typesikker. Nogle implementeringer, herunder Standard ML of New Jersey (SML/NJ), dens syntaktiske variant Mythryl og MLton , giver imidlertid biblioteker, der tilbyder usikre operationer. Disse faciliteter bruges ofte i forbindelse med disse implementeringers udenlandske funktionsgrænseflader til at interagere med ikke-ML-kode (f.eks. C-biblioteker), der kan kræve data, der er opstillet på bestemte måder. Et andet eksempel er selve SML/NJ interaktive toplevel , som skal bruge usikre operationer til at udføre ML -kode, der er indtastet af brugeren.

Modula-2

Modula-2 er et stærkt skrevet sprog med en designfilosofi, der kræver, at usikre faciliteter eksplicit markeres som usikre. Dette opnås ved at "flytte" sådanne faciliteter til et indbygget pseudobibliotek kaldet SYSTEM, hvorfra de skal importeres, før de kan bruges. Importen gør den således synlig, når sådanne faciliteter bruges. Desværre blev dette ikke derfor implementeret i den originale sprograpport og dens implementering. Der var stadig usikre faciliteter, f.eks. Typen cast syntaks og variantposter (arvet fra Pascal), der kunne bruges uden forudgående import. Vanskeligheden ved at flytte disse faciliteter ind i SYSTEM-pseudomodulet var manglen på nogen identifikator for anlægget, der derefter kunne importeres, da kun identifikatorer kan importeres, men ikke syntaks. 

IMPORT SYSTEM; (* allows the use of certain unsafe facilities: *)
VAR word : SYSTEM.WORD; addr : SYSTEM.ADDRESS;
addr := SYSTEM.ADR(word);

(* but type cast syntax can be used without such import *)
VAR i : INTEGER; n : CARDINAL;
n := CARDINAL(i); (* or *) i := INTEGER(n);

ISO Modula-2-standarden korrigerede dette for typen cast-facilitet ved at ændre type cast-syntaksen til en funktion kaldet CAST, som skal importeres fra pseudomodul SYSTEM. Andre usikre faciliteter, såsom variantposter, forblev imidlertid tilgængelige uden import fra pseudomodul SYSTEM. 

IMPORT SYSTEM;
VAR i : INTEGER; n : CARDINAL;
i := SYSTEM.CAST(INTEGER, n); (* Type cast in ISO Modula-2 *)

En nylig revision af sproget anvendte den originale designfilosofi grundigt. For det første blev pseudomodul SYSTEM omdøbt til UNSAFE for at gøre den usikre karakter af faciliteter importeret derfra mere eksplicit. Derefter blev alle tilbageværende usikre faciliteter fjernet helt (f.eks. Variantposter) eller flyttet til pseudomodul UNSAFE. For faciliteter, hvor der ikke er nogen identifikator, der kunne importeres, blev der introduceret aktiverende identifikatorer. For at muliggøre en sådan facilitet skal dens tilsvarende aktiverings-id importeres fra pseudomodulet UNSAFE. Der er ingen usikre faciliteter tilbage på det sprog, der ikke kræver import fra UNSAFE. 

IMPORT UNSAFE;
VAR i : INTEGER; n : CARDINAL;
i := UNSAFE.CAST(INTEGER, n); (* Type cast in Modula-2 Revision 2010 *)

FROM UNSAFE IMPORT FFI; (* enabling identifier for foreign function interface facility *)
<*FFI="C"*> (* pragma for foreign function interface to C *)

Pascal

Pascal har haft en række typesikkerhedskrav, hvoraf nogle opbevares i nogle kompilatorer. Hvor en Pascal -kompilator dikterer "streng indtastning", kan to variabler ikke tildeles hinanden, medmindre de enten er kompatible (f.eks. Konvertering af heltal til reel) eller tildelt den identiske undertype. For eksempel, hvis du har følgende kodefragment: 

type
  TwoTypes = record
     I: Integer;
     Q: Real;
  end;

  DualTypes = record
    I: Integer;
    Q: Real;
  end;

var
  T1, T2:  TwoTypes;
  D1, D2:  DualTypes;

Under streng indtastning er en variabel, der er defineret som TwoTypes , ikke kompatibel med DualTypes (fordi de ikke er identiske, selvom komponenterne i den brugerdefinerede type er identiske), og en tildeling af {{{1}}} er ulovlig. En tildeling af {{{1}}} ville være lovlig, fordi de undertyper, de er defineret til, er identiske. En opgave som f.eks. {{{1}}} er imidlertid lovlig.

Almindelig Lisp

Generelt er Common Lisp et typesikkert sprog. En Common Lisp -compiler er ansvarlig for at indsætte dynamiske kontroller for operationer, hvis typesikkerhed ikke kan bevises statisk. Imidlertid kan en programmør angive, at et program skal kompileres med et lavere niveau af dynamisk typekontrol. Et program, der er sammensat i en sådan tilstand, kan ikke betragtes som typesikkert.

C ++ eksempler

Følgende eksempler illustrerer, hvordan C ++ støbte operatører kan bryde typesikkerheden, når de bruges forkert. Det første eksempel viser, hvordan grundlæggende datatyper kan være forkert castet: 

#include <iostream>
using namespace std;

int main () {
    int   ival = 5;                              // integer value
    float fval = reinterpret_cast<float&>(ival); // reinterpret bit pattern
    cout << fval << endl;                        // output integer as float
    return 0;
}

I dette eksempel reinterpret_castforhindrer eksplicit kompilatoren i at udføre en sikker konvertering fra heltal til floating-point værdi. Når programmet kører, udsender det en skraldende flydende værdi. Problemet kunne have været undgået ved i stedet at skrivefloat fval = ival;

Det næste eksempel viser, hvordan objektreferencer kan være forkert nedslidte: 

#include <iostream>
using namespace std;

class Parent {
public:
    virtual ~Parent() {} // virtual destructor for RTTI
};

class Child1 : public Parent {
public:
    int a;
};

class Child2 : public Parent {
public:
    float b;
};

int main () {
    Child1 c1;
    c1.a = 5;
    Parent & p = c1;                     // upcast always safe
    Child2 & c2 = static_cast<Child2&>(p); // invalid downcast
    cout << c2.b << endl;          // will output garbage data
    return 0;
}

De to børneklasser har medlemmer af forskellige typer. Når en forældreklassemarkør nedskrives til en underklassemarkør, peger den resulterende markør muligvis ikke på et gyldigt objekt af korrekt type. I eksemplet fører dette til, at affaldsværdi udskrives. Problemet kunne have været undgået ved at erstatte static_castmed det, dynamic_castder kaster en undtagelse på ugyldige kast.

Se også

Noter

Referencer