Sprogbaseret sikkerhed - Language-based security

I datalogi er sprogbaseret sikkerhed ( LBS ) et sæt teknikker, der kan bruges til at styrke applikationssikkerheden på et højt niveau ved at bruge egenskaberne til programmeringssprog. LBS anses for at håndhæve computersikkerhed på applikationsniveau, hvilket gør det muligt at forhindre sårbarheder, som traditionel operativsystemsikkerhed ikke er i stand til at håndtere.

Softwareapplikationer er typisk specificeret og implementeret på visse programmeringssprog , og for at beskytte mod angreb, fejl og fejl kan en applikations kildekode være sårbar over for, er der behov for sikkerhed på applikationsniveau; sikkerhed evaluering af applikationsadfærd med hensyn til programmeringssprog. Dette område er generelt kendt som sprogbaseret sikkerhed.

Motivering

Brugen af ​​store softwaresystemer, såsom SCADA , finder sted overalt i verden, og computersystemer udgør kernen i mange infrastrukturer. Samfundet er meget afhængig af infrastruktur såsom vand, energi, kommunikation og transport, som igen alle er afhængige af fuldt fungerende computersystemer. Der er flere velkendte eksempler på, hvornår kritiske systemer mislykkes på grund af fejl eller softwarefejl, f.eks. Når mangel på computerhukommelse fik LAX-computere til at gå ned og hundreder af flyvninger blev forsinket (30. april 2014).

Traditionelt implementeres de mekanismer, der bruges til at kontrollere den korrekte opførsel af software, på operativsystemniveau. Operativsystemet håndterer flere mulige sikkerhedsovertrædelser såsom overtrædelser af hukommelsesadgang, overtrædelser af stackoverløb, overtrædelser af adgangskontrol og mange andre. Dette er en vigtig del af sikkerheden i computersystemer, men ved at sikre softwares adfærd på et mere specifikt niveau kan der opnås endnu stærkere sikkerhed. Da mange egenskaber og opførsel af softwaren går tabt i kompilering, er det betydeligt sværere at opdage sårbarheder i maskinkoden. Ved at evaluere kildekoden før kompilering kan teorien og implementeringen af ​​programmeringssproget også overvejes, og flere sårbarheder kan afdækkes.

"Så hvorfor fortsætter udviklere med at lave de samme fejl? I stedet for at stole på programmørernes minder, skal vi stræbe efter at producere værktøjer, der kodificerer det, der er kendt om almindelige sikkerhedssårbarheder, og integrerer det direkte i udviklingsprocessen."

- D. Evans og D. Larochelle, 2002

Formål med sprogbaseret sikkerhed

Ved at bruge LBS kan sikkerhedens sikkerhed øges på flere områder afhængigt af de anvendte teknikker. Almindelige programmeringsfejl, såsom at tillade bufferoverløb og ulovlige informationsstrømme, kan opdages og ikke tillades i den software, der bruges af forbrugeren. Det er også ønskeligt at give forbrugeren noget bevis på softwarens sikkerhedsegenskaber, hvilket gør forbrugeren i stand til at stole på softwaren uden at skulle modtage kildekoden og selv kontrollere den for fejl.

En kompilator, der tager kildekoden som input, udfører flere sprogspecifikke operationer på koden for at oversætte den til maskinlæsbar kode. Lexikalisk analyse , forbehandling , parsing , semantisk analyse , kodegenerering og kodeoptimering er alle almindeligt anvendte operationer i kompilatorer. Ved at analysere kildekoden og bruge teorien og implementeringen af ​​sproget, vil compileren forsøge korrekt at oversætte koden på højt niveau til koden på lavt niveau og dermed bevare programmets opførsel.

Under kompilering af programmer, der er skrevet på et typesikkert sprog, såsom Java , skal kildekoden typecheck med succes inden kompilering. Hvis typekontrollen mislykkes, udføres kompileringen ikke, og kildekoden skal ændres. Dette betyder, at givet en korrekt kompilator, skal enhver kode, der er kompileret fra et vellykket typekontrolleret kildeprogram, være fri for ugyldige tildelingsfejl. Dette er information, der kan være af værdi for kodeforbrugeren, da det giver en vis grad af garanti for, at programmet ikke går ned på grund af en bestemt fejl.

Et mål for LBS er at sikre tilstedeværelsen af ​​visse egenskaber i kildekoden svarende til softwarepolitikken. Oplysninger, der indsamles under udarbejdelsen, kan bruges til at oprette et certifikat, der kan leveres til forbrugeren som bevis for sikkerhed i det givne program. Et sådant bevis skal antyde, at forbrugeren kan stole på den kompilator, der bruges af leverandøren, og at certifikatet, oplysningerne om kildekoden, kan verificeres.

Figuren illustrerer, hvordan certificering og verifikation af lavt niveau kode kunne etableres ved brug af en certificerende kompilator. Softwareleverandøren får fordelen ved ikke at skulle afsløre kildekoden, og forbrugeren har opgaven med at verificere certifikatet, hvilket er en nem opgave sammenlignet med evaluering og kompilering af selve kildekoden. Bekræftelse af certifikatet kræver kun en begrænset pålidelig kodebase, der indeholder compileren og verifikatoren.

Teknikker

Programanalyse

De vigtigste anvendelser af programanalyse er programoptimering (driftstid, pladsbehov, strømforbrug osv.) Og programkorrekthed (fejl, sikkerhedssårbarheder osv.). Programanalyse kan anvendes til kompilering ( statisk analyse ), run-time ( dynamisk analyse ) eller begge dele. I sprogbaseret sikkerhed kan programanalyser give flere nyttige funktioner, såsom: typekontrol (statisk og dynamisk), overvågning , pletkontrol og kontrol-flow-analyse .

Analyse af informationsflow

Informationsflowanalyse kan beskrives som et sæt værktøjer, der bruges til at analysere informationsflowkontrollen i et program for at bevare fortrolighed og integritet, hvor regelmæssige adgangskontrolmekanismer kommer til kort.

"Ved at afkoble retten til adgang til information fra retten til at formidle den går flowmodellen ud over adgangsmatrixmodellen i sin evne til at specificere sikker informationsstrøm. Et praktisk system har brug for både adgangs- og flowkontrol for at opfylde alle sikkerhedskrav."

- D. Denning, 1976

Adgangskontrol håndhæver kontrol af adgang til information, men er ikke bekymret for, hvad der sker efter det. Et eksempel: Et system har to brugere, Alice og Bob. Alice har en fil secret.txt , som kun er tilladt at læse og redigere af hende, og hun foretrækker at opbevare disse oplysninger for sig selv. I systemet findes der også en fil public.txt , som er gratis at læse og redigere for alle brugere i systemet. Antag nu, at Alice ved et uheld har downloadet et ondsindet program. Dette program kan få adgang til systemet som Alice og omgå adgangskontrolkontrollen på secret.txt . Det ondsindede program kopierer derefter indholdet af secret.txt og placerer det i public.txt , så Bob og alle andre brugere kan læse det. Dette udgør en overtrædelse af systemets påtænkte fortrolighedspolitik.

Ikke-interferens

Ikke-interferens er en egenskab ved programmer, der ikke lækker eller afslører information om variabler med en højere sikkerhedsklassifikation, afhængigt af input af variabler med en lavere sikkerhedsklassifikation. Et program, der tilfredsstiller ikke-interferens, skal producere den samme output, når den tilsvarende samme input på de lavere variabler bruges. Dette skal gælde for enhver mulig værdi på input. Dette indebærer, at selvom højere variabler i programmet har forskellige værdier fra en udførelse til en anden, bør dette ikke være synligt på de lavere variabler.

En angriber kan prøve at udføre et program, der ikke tilfredsstiller ikke-interferens gentagne gange og systematisk for at forsøge at kortlægge dets adfærd. Flere gentagelser kan føre til afsløring af højere variabler og lade angriberen lære følsomme oplysninger om f.eks. Systemtilstanden.

Om et program opfylder ikke-interferens eller ej, kan evalueres under kompilering forudsat tilstedeværelsen af sikkerhedstypesystemer .

Sikkerhedstypesystem

Et sikkerhedstypesystem er en slags typesystem, der kan bruges af softwareudviklere for at kontrollere sikkerhedsegenskaberne for deres kode. På et sprog med sikkerhedstyper vedrører typerne af variabler og udtryk applikationens sikkerhedspolitik, og programmører kan muligvis specificere applikationssikkerhedspolitikken via typedeklarationer. Typer kan bruges til at ræsonnere om forskellige slags sikkerhedspolitikker, herunder autorisationspolitikker (som adgangskontrol eller funktioner) og informationsflowsikkerhed. Sikkerhedstypesystemer kan formelt være relateret til den underliggende sikkerhedspolitik, og et sikkerhedstypesystem er sundt, hvis alle programmer, der typecheck tilfredsstiller politikken i semantisk forstand. For eksempel kan et sikkerhedstypesystem til informationsstrøm håndhæve ikke-interferens, hvilket betyder, at typekontrol afslører, om der er nogen krænkelse af fortrolighed eller integritet i programmet.

Sikring af lavt niveau kode

Sårbarheder i lavt niveau kode er fejl eller mangler, der fører programmet til en tilstand, hvor yderligere opførsel af programmet er udefineret af kildens programmeringssprog. Opførelsen af ​​programmet på lavt niveau afhænger af compiler, runtime-system eller operativsystemdetaljer. Dette giver en angriber mulighed for at køre programmet mod en udefineret tilstand og udnytte systemets opførsel.

Almindelig udnyttelse af usikker kode på lavt niveau lader en hacker udføre uautoriserede læsninger eller skrivninger til hukommelsesadresser. Hukommelsesadresserne kan enten være tilfældige eller vælges af angriberen.

Brug af sikre sprog

En tilgang til at opnå sikker kode på lavt niveau er at bruge sikre sprog på højt niveau. Et sikkert sprog anses for at være fuldstændig defineret i programmørhåndbogen. Enhver fejl, der kan føre til implementeringsafhængig adfærd på et sikkert sprog, opdages enten på kompileringstidspunktet eller fører til en veldefineret fejladfærd ved kørselstid. Hvis du får adgang til en matrix uden for grænserne i Java , kastes en undtagelse i Java . Eksempler på andre sikre sprog er C # , Haskell og Scala .

Defensiv udførelse af usikre sprog

Under kompilering af et usikkert sprog tilføjes run-time-kontrol til koden på lavt niveau for at opdage udefineret adfærd på kildeniveau. Et eksempel er brugen af kanariefugle , som kan afslutte et program, når man opdager grænser. En ulempe ved at bruge kørselstimer, f.eks. Inden for grænsekontrol, er, at de pålægger betydelig ydeevne overhead.

Hukommelsesbeskyttelse , såsom brug af ikke-eksekverbar stak og / eller bunke, kan også ses som yderligere kørselstider. Dette bruges af mange moderne operativsystemer.

Isoleret udførelse af moduler

Den generelle idé er at identificere følsom kode fra applikationsdata ved at analysere kildekoden. Når dette er gjort, adskilles de forskellige data og placeres i forskellige moduler. Når man antager, at hvert modul har total kontrol over de følsomme oplysninger, det indeholder, er det muligt at specificere, hvornår og hvordan man skal forlade modulet. Et eksempel er et kryptografisk modul, der kan forhindre nøgler i at lade modulet være ukrypteret.

Certificering af kompilering

Certificering af kompilering er ideen om at producere et certifikat under kompilering af kildekode ved hjælp af oplysningerne fra semantikken på programmeringssprog på højt niveau. Dette certifikat skal vedlægges den kompilerede kode for at give forbrugeren en form for bevis for, at kildekoden blev kompileret i henhold til et bestemt sæt regler. Certifikatet kan produceres på forskellige måder, f.eks. Gennem Proof-carrying code (PCC) eller Typed assemblingsprog (TAL).

Bevisbærende kode

De vigtigste aspekter af PCC kan opsummeres i følgende trin:

1. Leverandøren leverer et eksekverbart program med forskellige annoteringer produceret af en certificerende compiler .
2. Forbrugeren stiller en verifikationsbetingelse baseret på en sikkerhedspolitik . Dette sendes til leverandøren.
3. Leverandøren kører verifikationsbetingelsen i en sætningsprover for at fremlægge et bevis for forbrugeren om, at programmet faktisk opfylder sikkerhedspolitikken.
4. Forbrugeren kører derefter beviset i en kontrolkontrol for at kontrollere bevisets gyldighed.

Et eksempel på en certificerende kompilator er Touchstone-kompilatoren , der giver et formelt PCC-bevis for type- og hukommelsessikkerhed for programmer implementeret i Java.

Typet samlingssprog

TAL gælder for programmeringssprog, der bruger et typesystem . Efter kompilering vil objektkoden bære en typebetegnelse, der kan kontrolleres af en almindelig typekontrol. Den annotering, der produceres her, ligner på mange måder de kommentarer, der leveres af PCC, med nogle begrænsninger. TAL kan dog håndtere enhver sikkerhedspolitik, der kan udtrykkes af typesystemets begrænsninger, som blandt andet kan omfatte hukommelsessikkerhed og kontrolflow.

Seminarer

• Dagstuhl Seminar 03411 , Sprogbaseret sikkerhed, 5. - 10. oktober 2003.

Referencer

Bøger

• G. Barthe, B. Grégoire, T. Rezk, udarbejdelse af certifikater , 2008
• Brian Chess og Gary McGraw, Statisk analyse for sikkerhed , 2004.

Yderligere læsning

• Dexter Kozen, sprogbaseret sikkerhed , Cornell University, 1999
• Pieter Agten et al., Nyere udvikling inden for softwaresikkerhed på lavt niveau , Universiteit Leuven
• Andrei Sabelfeld og Andrew C. Myers, sprogbaseret informationsstrømningssikkerhed
• Fred B. Schneider et al., A Language-Based Approach to Security , Carnegie Mellon University, 2000