Typ säkerhet

Typsystem
Allmänna begrepp
Huvudkategorier
Mindre kategorier

Inom datavetenskap är typsäkerhet och typgodhet i vilken utsträckning ett programmeringsspråk avskräcker eller förhindrar typfel . Typsäkerhet anses ibland alternativt vara en egenskap hos ett datorspråks faciliteter; det vill säga, vissa anläggningar är typsäkra och deras användning kommer inte att resultera i typfel, medan andra anläggningar på samma språk kan vara typosäkra och ett program som använder dem kan stöta på typfel. De beteenden som klassificeras som typfel av ett givet programmeringsspråk är vanligtvis de som är resultatet av försök att utföra operationer på värden som inte är av lämplig datatyp , t.ex. att lägga till en sträng till ett heltal när det inte finns någon definition på hur detta fall ska hanteras . Denna klassificering är delvis baserad på åsikter.

Typtillämpningen kan vara statisk, fånga upp potentiella fel vid kompileringstidpunkten eller dynamisk, associera typinformation med värden vid körning och konsultera dem vid behov för att upptäcka överhängande fel, eller en kombination av båda. Genomförande av dynamisk typ tillåter ofta att program körs som skulle vara ogiltiga under statisk tillämpning.

I samband med system av statiska (kompileringstids)typ innefattar typsäkerhet vanligtvis (bland annat) en garanti för att det slutliga värdet av ett uttryck kommer att vara en legitim medlem av det uttryckets statiska typ. Det exakta kravet är mer subtilt än så — se till exempel subtypning och polymorfism för komplikationer.

Definitioner

Intuitivt fångas typsoundness av Robin Milners pittige uttalande om att

Välskrivna program kan inte "gå fel".

Med andra ord, om ett typsystem är sunt måste uttryck som accepteras av det typsystemet utvärderas till ett värde av lämplig typ (istället för att producera ett värde av någon annan, orelaterade typ eller krascha med ett typfel). Vijay Saraswat tillhandahåller följande, relaterad definition:

Ett språk är typsäkert om de enda operationer som kan utföras på data på språket är de som sanktioneras av typen av data.

Men vad det exakt betyder för ett program att vara "välskrivet" eller att "gå fel" är egenskaperna hos dess statiska och dynamiska semantik , som är specifika för varje programmeringsspråk. Följaktligen beror en exakt, formell definition av typens sundhet på stilen av formell semantik som används för att specificera ett språk. 1994 formulerade Andrew Wright och Matthias Felleisen vad som har blivit standarddefinitionen och bevistekniken för typsäkerhet i språk som definieras av operationssemantics , vilket ligger närmast begreppet typsäkerhet som de flesta programmerare förstår. Enligt detta tillvägagångssätt måste semantiken för ett språk ha följande två egenskaper för att betraktas som typljud:

Framsteg
Ett välskrivet program "fastnar" aldrig: varje uttryck är antingen redan ett värde eller kan reduceras mot ett värde på något väldefinierat sätt. Med andra ord, programmet hamnar aldrig i ett odefinierat tillstånd där inga ytterligare övergångar är möjliga.
Bevarande (eller ämnesreduktion )
Efter varje utvärderingssteg förblir typen av varje uttryck densamma (det vill säga dess typ bevaras ).

Ett antal andra formella behandlingar av typen sundhet har också publicerats i termer av denotationssemantik och strukturell operativ semantik .

Förhållande till andra former av säkerhet

Typgodhet är isolerat en relativt svag egenskap, eftersom den i huvudsak bara säger att reglerna för ett typsystem är internt konsekventa och inte kan undergrävas. Men i praktiken är programmeringsspråk utformade så att välskrivenhet också medför andra, starkare egenskaper, av vilka några inkluderar:

  • Förebyggande av illegal verksamhet. Till exempel kan ett typsystem avvisa uttrycket 3 / "Hello, World" som ogiltigt, eftersom divisionsoperatorn inte är definierad för en strängdivisor .
  • Minnessäkerhet
    • Typsystem kan förhindra vilda pekare som annars skulle kunna uppstå från att en pekare till en typ av objekt behandlas som en pekare till en annan typ.
    • Mer sofistikerade typsystem, som de som stöder beroende typer , kan upptäcka och avvisa out-of-bound åtkomster, vilket förhindrar potentiella buffertspill .
  • Logiska fel som har sitt ursprung i semantiken av olika typer. Till exempel kan tum och millimeter båda lagras som heltal, men bör inte ersättas med varandra eller läggas till. Ett typsystem kan tvinga fram två olika typer av heltal för dem.

Typsäkra och typosäkra språk

Typsäkerhet är vanligtvis ett krav för alla leksaksspråk (dvs. esoteriska språk ) som föreslås i akademisk programmeringsspråksforskning. Många språk, å andra sidan, är för stora för mänskligt genererade säkerhetsbevis, eftersom de ofta kräver kontroll av tusentals fall. Ändå har vissa språk som Standard ML , som har strikt definierat semantik, visat sig uppfylla en definition av typsäkerhet. Vissa andra språk som Haskell tros [ diskutera ] uppfylla någon definition av typsäkerhet, förutsatt att vissa "flykt"-funktioner inte används (till exempel Haskells unsafePerformIO , som används för att "rymma" från den vanliga begränsade miljön där I/O är möjligt, kringgår typsystemet och kan därför användas för att bryta typsäkerheten.) Typpunning är ett annat exempel på en sådan "flykt"-funktion. Oavsett egenskaperna hos språkdefinitionen kan vissa fel uppstå under körning på grund av buggar i implementeringen eller i länkade bibliotek skrivna på andra språk; sådana fel kan göra en given implementeringstyp osäker under vissa omständigheter. En tidig version av Suns virtuella Java-maskin var sårbar för denna typ av problem.

Starkt och svagt skrivande

Huvudartikel: Starkt och svagt skrivande

Programmeringsspråk klassificeras ofta i vardagsspråk som starkt skrivna eller svagt skrivna (även löst skrivna) för att hänvisa till vissa aspekter av typsäkerhet. 1974 Liskov och Zilles ett starkt typat språk som ett där "när ett objekt överförs från en anropande funktion till en anropad funktion, måste dess typ vara kompatibel med den typ som deklareras i den anropade funktionen." 1977 skrev Jackson, "I ett starkt skrivet språk kommer varje dataområde att ha en distinkt typ och varje process kommer att ange sina kommunikationskrav i termer av dessa typer." Däremot kan ett svagt skrivet språk ge oförutsägbara resultat eller kan utföra implicit typkonvertering.

Minneshantering och typsäkerhet

Typsäkerhet är nära kopplat till minnessäkerhet . Till exempel, i en implementering av ett språk som har någon typ som tillåter vissa bitmönster men inte andra, tillåter ett dinglande pekarminne att skriva ett bitmönster som inte representerar en legitim medlem av till en död variabel av typen , vilket orsakar ett typfel när variabeln läses. Omvänt, om språket är minnessäkert, kan det inte tillåta att ett godtyckligt heltal används som en pekare , därför måste det finnas en separat pekare eller referenstyp.

Som ett minimalt villkor får ett typsäkert språk inte tillåta dinglande pekare över tilldelningar av olika typer. Men de flesta språk tvingar fram korrekt användning av abstrakta datatyper definierade av programmerare även när detta inte är strikt nödvändigt för minnessäkerhet eller för att förhindra någon form av katastrofala misslyckanden. Tilldelningar ges en typ som beskriver dess innehåll, och denna typ är fast under tilldelningens varaktighet. Detta gör att typbaserad aliasanalys kan dra slutsatsen att tilldelningar av olika typer är distinkta.

De flesta typsäkra språk använder sophämtning . Pierce säger, "det är extremt svårt att uppnå typsäkerhet i närvaro av en explicit deallokeringsoperation", på grund av problemet med hängande pekare. Men Rust anses generellt vara typsäker och använder en låna checker för att uppnå minnessäkerhet, istället för sophämtning.

Skriv säkerhet i objektorienterade språk

I objektorienterade språk är typsäkerhet vanligtvis inneboende i det faktum att ett typsystem finns på plats. Detta uttrycks i termer av klassdefinitioner.

En klass definierar i huvudsak strukturen för de objekt som härrör från den och ett API som ett kontrakt för att hantera dessa objekt. Varje gång ett nytt objekt skapas kommer det att följa det kontraktet.

Varje funktion som utbyter objekt som härrör från en specifik klass, eller implementerar ett specifikt gränssnitt , kommer att följa det kontraktet: i den funktionen kommer de operationer som tillåts på det objektet endast att vara de som definieras av metoderna för klassen objektet implementerar. Detta kommer att garantera att objektets integritet kommer att bevaras.

Undantag från detta är objektorienterade språk som tillåter dynamisk modifiering av objektstrukturen, eller användning av reflektion för att modifiera innehållet i ett objekt för att övervinna de begränsningar som ställs av klassmetodernas definitioner.

Skriv säkerhetsproblem på specifika språk

Ada

Ada designades för att vara lämplig för inbyggda system , drivrutiner och andra former av systemprogrammering , men också för att uppmuntra typsäker programmering. För att lösa dessa motstridiga mål begränsar Ada typosäkerhet till en viss uppsättning speciella konstruktioner vars namn vanligtvis börjar med strängen Unchecked_ . Unchecked_Deallocation kan effektivt förbjudas från en enhet av Ada-text genom att tillämpa pragma Pure på denna enhet. Det förväntas att programmerare kommer att använda Unchecked_- konstruktioner mycket noggrant och endast när det är nödvändigt; program som inte använder dem är typsäkra.

Programmeringsspråket SPARK är en delmängd av Ada som eliminerar alla dess potentiella oklarheter och osäkerheter samtidigt som det lägger till statiskt kontrollerade kontrakt till de tillgängliga språkfunktionerna. SPARK undviker problemen med hängande pekare genom att inte tillåta allokering under körning helt.

Ada2012 lägger till statiskt kontrollerade kontrakt till själva språket (i form av för- och eftervillkor, samt typinvarianter).

C

Programmeringsspråket C är typsäkert i begränsade sammanhang; till exempel genereras ett kompileringstidsfel när ett försök görs att konvertera en pekare till en typ av struktur till en pekare till en annan typ av struktur, om inte en explicit cast används. Ett antal mycket vanliga operationer är dock icke typsäkra; till exempel är det vanliga sättet att skriva ut ett heltal ungefär som printf("%d", 12) , där %d talar om för printf vid körning att förvänta sig ett heltalsargument. (Något som printf("%s", 12) , som talar om för funktionen att förvänta sig en pekare till en teckensträng och ändå tillhandahåller ett heltalsargument, kan accepteras av kompilatorer, men kommer att ge odefinierade resultat.) Detta mildras delvis. genom att vissa kompilatorer (som gcc) kontrollerar typöverensstämmelser mellan printf-argument och formatsträngar.

Dessutom tillhandahåller C, liksom Ada, ospecificerade eller odefinierade explicita omvandlingar; och till skillnad från i Ada är idiom som använder dessa omvandlingar mycket vanliga och har bidragit till att ge C ett typosäkert rykte. Till exempel är standardsättet att allokera minne på heapen att anropa en minnesallokeringsfunktion, såsom malloc , med ett argument som anger hur många byte som krävs. Funktionen returnerar en otypad pekare (typ void * ), som den anropande koden måste explicit eller implicit casta till lämplig pekartyp. Förstandardiserade implementeringar av C krävde en explicit cast för att göra det, därför blev koden ( struct foo *) malloc( sizeof (struct foo)) den accepterade praxisen.

C++

Några funktioner i C++ som främjar mer typsäker kod:

C#

C# är typsäker (men inte statiskt typsäker). Den har stöd för otypade pekare, men detta måste nås med nyckelordet "osäkra" som kan förbjudas på kompilatornivå. Den har inneboende stöd för run-time cast-validering. Cast kan valideras genom att använda nyckelordet "som" som kommer att returnera en nollreferens om casten är ogiltig, eller genom att använda en C-stil cast som ger ett undantag om casten är ogiltig. Se C Sharp-konverteringsoperatorer .

Otillbörligt beroende av objekttypen (från vilken alla andra typer härrör) riskerar att motverka syftet med C#-systemet. Det är vanligtvis bättre praxis att överge objektreferenser till förmån för generika , liknande mallar i C++ och generiska i Java .

Java

Java -språket är utformat för att upprätthålla typsäkerhet. Allt i Java händer inuti ett objekt och varje objekt är en instans av en klass .

För att implementera typsäkerhetsupprätthållandet måste varje objekt, före användning, allokeras . Java tillåter användning av primitiva typer men endast inuti korrekt allokerade objekt.

Ibland implementeras en del av typen säkerhet indirekt: t.ex. representerar klassen BigDecimal ett flyttal med godtycklig precision, men hanterar endast tal som kan uttryckas med en finit representation. Operationen BigDecimal.divide() beräknar ett nytt objekt som divisionen av två tal uttryckta som BigDecimal.

I det här fallet om divisionen inte har någon finit representation, som när man beräknar t.ex. 1/3=0,33333..., kan divide()-metoden skapa ett undantag om inget avrundningsläge är definierat för operationen. Därför garanterar biblioteket, snarare än språket, att objektet respekterar kontraktet som är implicit i klassdefinitionen.

Standard ML

Standard ML har strikt definierad semantik och är känd för att vara typsäker. Vissa implementeringar, inklusive Standard ML från New Jersey (SML/NJ), dess syntaktiska variant Mythryl och MLton , tillhandahåller bibliotek som erbjuder osäkra operationer. Dessa faciliteter används ofta i samband med dessa implementeringars främmande funktionsgränssnitt för att interagera med icke-ML-kod (som C-bibliotek) som kan kräva data utlagda på specifika sätt. Ett annat exempel är den interaktiva SML/NJ- toppnivån själv, som måste använda osäkra operationer för att exekvera ML-kod som angetts av användaren.

Modula-2

Modula-2 är ett starkt skrivet språk med en designfilosofi att kräva att alla osäkra anläggningar uttryckligen markeras som osäkra. Detta uppnås genom att "flytta" sådana faciliteter till ett inbyggt pseudobibliotek som kallas SYSTEM varifrån de måste importeras innan de kan användas. Importen gör det alltså synligt när sådana anläggningar används. Tyvärr implementerades detta inte i den ursprungliga språkrapporten och dess genomförande. Det återstod fortfarande osäkra anläggningar som typcast syntax och variantposter (ärvt från Pascal) som kunde användas utan föregående import. Svårigheten med att flytta dessa faciliteter till SYSTEM-pseudomodulen var avsaknaden av någon identifierare för anläggningen som sedan kunde importeras eftersom endast identifierare kan importeras, men inte syntax.

  
      
  


      
       IMPORTSYSTEM  ;  _  (* tillåter användning av vissa osäkra faciliteter: *)  VAR  -ord  :  SYSTEM  .  ORD  ;  addr  :  SYSTEM  .  ADRESS  ;  addr  :=  SYSTEM  .  ADR  (  ord  );  (* men typ cast-syntax kan användas utan sådan import *)  VAR  i  :  INTEGER  ;  n  :  KARDINAL  ;  n  :=  KARDINAL  (  i  );  (* eller *)  i  :=  HELTAL  (  n  );

ISO Modula-2-standarden korrigerade detta för typcast-anläggningen genom att ändra typcast-syntaxen till en funktion som kallas CAST som måste importeras från pseudomodul SYSTEM. Andra osäkra anläggningar som variantposter förblev dock tillgängliga utan någon import från pseudomodul SYSTEM.

 
      
     IMPORTSYSTEM  ;  _  VAR  i  :  HELTAL  ;  n  :  KARDINAL  ;  i  :=  SYSTEM  .  CAST  (  HELTAL  ,  n  );  (* Typ gjuten i ISO Modula-2 *)

En nyligen genomförd översyn av språket tillämpade den ursprungliga designfilosofin rigoröst. Först döptes pseudomodul SYSTEM om till UNSAFE för att göra den osäkra karaktären hos anläggningar som importerades därifrån mer tydlig. Sedan togs alla återstående osäkra anläggningar antingen bort helt (till exempel variantposter) eller flyttades till pseudomodulen UNSAFE. För anläggningar där det inte finns någon identifierare som skulle kunna importeras, infördes möjliggörande identifierare. För att möjliggöra en sådan möjlighet måste dess motsvarande aktiveringsidentifierare importeras från pseudomodulen UNSAFE. Inga osäkra anläggningar finns kvar på språket som inte kräver import från UNSAFE.

 
      
    

    
  IMPORTERA  OSÄKERT  ;  VAR  i  :  HELTAL  ;  n  :  KARDINAL  ;  i  :=  OSÄKERT  .  CAST  (  HELTAL  ,  n  );  (* Typgjuten i Modula-2 Revision 2010 *)  FRÅN  OSÄKER  IMPORT  FFI  ;  (* möjliggörande identifierare för gränssnitt för främmande funktioner *)  <*FFI="C">  (* pragma för gränssnitt för främmande funktioner till C *)

Pascal

Pascal har haft ett antal typsäkerhetskrav, av vilka några finns kvar i vissa kompilatorer. Där en Pascal-kompilator dikterar "strikt typning" kan två variabler inte tilldelas varandra om de inte är antingen kompatibla (som omvandling av heltal till reellt) eller tilldelas den identiska undertypen. Till exempel, om du har följande kodfragment: 


    
      
      
  

    
     
     
  


     
      typ  TwoTypes  =  post  I  :  Heltal  ;  F  :  Verkligt  ;  slut  ;  DualTypes  =  post  I  :  Heltal  ;  F  :  Verkligt  ;  slut  ;  var  T1  ,  T2  :  TwoTypes  ;  D1  ,  D2  :  DualTypes  ;

är en variabel definierad som TwoTypes inte kompatibel med DualTypes (eftersom de inte är identiska, även om komponenterna i den användardefinierade typen är identiska) och en tilldelning av T1 := D2; är olagligt. En tilldelning av T1 := T2; skulle vara lagligt eftersom undertyperna de är definierade till är identiska. Men en uppgift som T1.Q := D1.Q; skulle vara lagligt.

Vanlig Lisp

I allmänhet är Common Lisp ett typsäkert språk. En Common Lisp-kompilator ansvarar för att infoga dynamiska kontroller för operationer vars typsäkerhet inte kan bevisas statiskt. En programmerare kan dock indikera att ett program bör kompileras med en lägre nivå av dynamisk typkontroll. Ett program som kompilerats i ett sådant läge kan inte anses typsäkert.

C++ exempel

Följande exempel illustrerar hur C++ gjutoperatorer kan bryta typsäkerheten när de används felaktigt. Det första exemplet visar hur grundläggande datatyper kan castas felaktigt:

 
  

   
                                       
        
                                
     0
 #include  <iostream>  med  namnutrymme  std  ;  int  main  ()  {  int  ival  =  5  ;  // heltalsvärde  float  fval  =  reinterpret_cast  <  float  &>  (  ival  );  // omtolka bitmönster  cout  <<  fval  <<  endl  ;  // mata ut heltal som flytande  retur  ;  }

I det här exemplet förhindrar reinterpret_cast uttryckligen kompilatorn från att utföra en säker konvertering från heltal till flyttal. När programmet körs kommer det att mata ut ett flyttal för skräp. Problemet kunde ha undvikits genom att istället skriva float fval = ival;

Nästa exempel visar hur objektreferenser kan nedkastas felaktigt:

 
  

  

       


     

     


     

     


   
     
      
                             
         
                  
     0
 #include  <iostream>  med  namnutrymme  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  ;  Förälder  &  p  =  c1  ;  // upcast alltid säker  Child2  &  c2  =  static_cast  <  Child2  &>  (  p  );  // invalid downcast  cout  <<  c2  .  b  <<  endl  ;  // kommer att mata ut skräpdata  retur  ;  }

De två barnklasserna har medlemmar av olika slag. När du sänker en överordnad klasspekare till en underordnad klasspekare, kanske den resulterande pekaren inte pekar på ett giltigt objekt av korrekt typ. I exemplet leder detta till att skräpvärde skrivs ut. Problemet kunde ha undvikits genom att ersätta static_cast med dynamic_cast som ger ett undantag på ogiltiga casts.

Se även

Anteckningar

Hämtad från " https://en.wikipedia.org/w/index.php?title=Type_safety&oldid=1136507167 "