Securitate bazată pe limbă - Language-based security

În informatică , securitatea bazată pe limbaj ( LBS ) este un set de tehnici care pot fi utilizate pentru a consolida securitatea aplicațiilor la un nivel înalt prin utilizarea proprietăților limbajelor de programare. LBS este considerat a impune securitatea computerului la nivel de aplicație, făcând posibilă prevenirea vulnerabilităților pe care securitatea tradițională a sistemului de operare nu le poate gestiona.

Aplicațiile software sunt de obicei specificate și implementate în anumite limbaje de programare și, pentru a proteja împotriva atacurilor, defectelor și erorilor, codul sursă al unei aplicații ar putea fi vulnerabil, este nevoie de securitate la nivel de aplicație; securitate evaluând comportamentul aplicațiilor în raport cu limbajul de programare. Această zonă este în general cunoscută sub numele de securitate bazată pe limbă.

Motivație

Utilizarea sistemelor software mari, cum ar fi SCADA , are loc în întreaga lume, iar sistemele informatice constituie nucleul multor infrastructuri. Societatea se bazează foarte mult pe infrastructură, cum ar fi apa, energia, comunicațiile și transportul, care, din nou, toate se bazează pe sisteme informatice funcționale. Există câteva exemple binecunoscute ale momentului în care sistemele critice eșuează din cauza erorilor sau erorilor din software, cum ar fi atunci când lipsa de memorie a computerului a cauzat blocarea computerelor LAX și întârzierea sutelor de zboruri (30 aprilie 2014).

În mod tradițional, mecanismele utilizate pentru a controla comportamentul corect al software-ului sunt implementate la nivelul sistemului de operare. Sistemul de operare gestionează mai multe încălcări de securitate posibile, cum ar fi încălcări ale accesului la memorie, încălcări ale depășirii stivei, încălcări ale controlului accesului și multe altele. Aceasta este o parte crucială a securității în sistemele informatice, cu toate acestea, asigurând comportamentul software-ului la un nivel mai specific, se poate realiza o securitate și mai puternică. Deoarece o mulțime de proprietăți și comportament ale software-ului se pierd în compilare, este semnificativ mai dificil de detectat vulnerabilitățile în codul mașinii. Prin evaluarea codului sursă, înainte de compilare, se poate lua în considerare și teoria și implementarea limbajului de programare și pot fi descoperite mai multe vulnerabilități.

"Deci, de ce dezvoltatorii continuă să facă aceleași greșeli? În loc să ne bazăm pe amintirile programatorilor, ar trebui să ne străduim să producem instrumente care să codifice ceea ce se știe despre vulnerabilitățile comune de securitate și să o integreze direct în procesul de dezvoltare."

- D. Evans și D. Larochelle, 2002

Obiectivul securității lingvistice

Prin utilizarea LBS, securitatea software-ului poate fi mărită în mai multe domenii, în funcție de tehnicile utilizate. Erorile obișnuite de programare, cum ar fi permiterea depășirilor de tampon și fluxurilor ilegale de informații, pot fi detectate și interzise în software-ul utilizat de consumator. De asemenea, este de dorit să oferiți o dovadă consumatorului cu privire la proprietățile de securitate ale software-ului, făcându-l în măsură să aibă încredere în software fără a fi nevoie să primească codul sursă și să-l auto-verifice pentru erori.

Un compilator, luând codul sursă ca intrare, efectuează mai multe limbi specifice operațiunilor asupra codului pentru a-l traduce în cod lizibil de mașină. Analiza lexicală , preprocesarea , analiza , analiza semantică , generarea codului și optimizarea codului sunt toate operațiuni utilizate în mod obișnuit în compilatoare. Analizând codul sursă și folosind teoria și implementarea limbajului, compilatorul va încerca să traducă corect codul de nivel înalt în cod de nivel scăzut, păstrând comportamentul programului.

În timpul compilării programelor scrise într -un limbaj sigur de tip , cum ar fi Java , codul sursă trebuie să verifice cu succes înainte de compilare. Dacă verificarea de tip eșuează, compilarea nu va fi efectuată, iar codul sursă trebuie modificat. Aceasta înseamnă că, având în vedere un compilator corect, orice cod compilat dintr-un program sursă verificat cu succes ar trebui să fie clar de erori de atribuire nevalide. Acestea sunt informații care pot avea valoare pentru consumatorul de cod, deoarece oferă un anumit grad de garanție că programul nu se va prăbuși din cauza unei erori specifice.

Un obiectiv al LBS este de a asigura prezența anumitor proprietăți în codul sursă corespunzător politicii de siguranță a software-ului. Informațiile colectate în timpul compilării pot fi utilizate pentru a crea un certificat care poate fi furnizat consumatorului ca dovadă a siguranței în cadrul programului dat. O astfel de dovadă trebuie să implice faptul că consumatorul poate avea încredere în compilatorul utilizat de furnizor și că certificatul, informațiile despre codul sursă, pot fi verificate.

Figura ilustrează modul în care certificarea și verificarea codului de nivel scăzut ar putea fi stabilite prin utilizarea unui compilator de certificare. Furnizorul de software câștigă avantajul că nu trebuie să dezvăluie codul sursă, iar consumatorul rămâne cu sarcina de a verifica certificatul, care este o sarcină ușoară în comparație cu evaluarea și compilarea codului sursă în sine. Verificarea certificatului necesită doar o bază de cod de încredere limitată care să conțină compilatorul și verificatorul.

Tehnici

Analiza programului

Principalele aplicații ale analizei programului sunt optimizarea programului (timp de rulare, cerințe de spațiu, consum de energie etc.) și corectitudinea programului (bug-uri, vulnerabilități de securitate etc.). Analiza programului poate fi aplicată la compilare ( analiză statică ), timp de execuție ( analiză dinamică ) sau ambelor. În securitatea bazată pe limbă, analiza programului poate oferi mai multe caracteristici utile, cum ar fi: verificarea tipului (static și dinamic), monitorizarea , verificarea taintului și analiza fluxului de control .

Analiza fluxului informațional

Analiza fluxului de informații poate fi descrisă ca un set de instrumente utilizate pentru a analiza controlul fluxului de informații într-un program, pentru a păstra confidențialitatea și integritatea acolo unde mecanismele regulate de control al accesului sunt scurte.

"Prin decuplarea dreptului de acces la informații de dreptul de a le difuza, modelul fluxului depășește modelul matricei de acces prin capacitatea sa de a specifica fluxul sigur de informații. Un sistem practic are nevoie atât de control de acces, cât și de flux pentru a satisface toate cerințele de securitate."

- D. Denning, 1976

Controlul accesului impune verificarea accesului la informații, dar nu este preocupat de ceea ce se întâmplă după aceea. Un exemplu: un sistem are doi utilizatori, Alice și Bob. Alice are un fișier secret.txt , care poate fi citit și editat doar de către ea și preferă să păstreze aceste informații pentru sine. În sistem, există și un fișier public.txt , care poate fi citit și editat gratuit pentru toți utilizatorii din sistem. Acum, să presupunem că Alice a descărcat accidental un program rău intenționat. Acest program poate accesa sistemul ca Alice, ocolind verificarea controlului accesului pe secret.txt . Programul rău intenționat copiază apoi conținutul secret.txt și îl plasează în public.txt , permițându-i lui Bob și tuturor celorlalți utilizatori să îl citească. Aceasta constituie o încălcare a politicii de confidențialitate a sistemului.

Neamestec

Noninterferența este o proprietate a programelor care nu scurg sau dezvăluie informații despre variabilele cu o clasificare de securitate mai mare , în funcție de introducerea variabilelor cu o clasificare de securitate mai mică . Un program care satisface neinterferența ar trebui să producă aceeași ieșire ori de câte ori se utilizează aceeași intrare corespunzătoare pentru variabilele inferioare . Aceasta trebuie să fie valabilă pentru fiecare valoare posibilă a intrării. Acest lucru implică faptul că, chiar dacă variabilele superioare din program au valori diferite de la o execuție la alta, acest lucru nu ar trebui să fie vizibil pe variabilele inferioare .

Un atacator ar putea încerca să execute un program care nu satisface neinterferența în mod repetat și sistematic pentru a încerca să-și mapeze comportamentul. Mai multe iterații ar putea duce la dezvăluirea unor variabile mai mari și ar permite atacatorului să învețe informații sensibile despre, de exemplu, starea sistemelor.

Dacă un program satisface sau nu neinterferența poate fi evaluat în timpul compilării, presupunând prezența sistemelor de tip securitate .

Sistem de tip securitate

Un sistem de tip securitate este un tip de sistem tip care poate fi utilizat de dezvoltatorii de software pentru a verifica proprietățile de securitate ale codului lor. Într-un limbaj cu tipuri de securitate, tipurile de variabile și expresii se referă la politica de securitate a aplicației, iar programatorii pot specifica politica de securitate a aplicației prin declarații de tip. Tipurile pot fi folosite pentru a argumenta diferite tipuri de politici de securitate, inclusiv politici de autorizare (precum controlul accesului sau capabilități) și securitatea fluxului de informații. Sistemele de tip securitate pot fi legate în mod oficial de politica de securitate de bază, iar un sistem de tip securitate este solid dacă toate programele care verifică tipul satisfac politica în sens semantic. De exemplu, un sistem de tip securitate pentru fluxul de informații ar putea impune neinterferența, ceea ce înseamnă că verificarea tipului relevă dacă există vreo încălcare a confidențialității sau integrității în program.

Securizarea codului de nivel scăzut

Vulnerabilitățile din codul de nivel scăzut sunt erori sau defecte care vor duce programul într-o stare în care comportamentul suplimentar al programului este nedefinit de limbajul de programare sursă. Comportamentul programului de nivel inferior va depinde de detalii despre compilator, runtime sau despre sistemul de operare. Acest lucru permite unui atacator să conducă programul către o stare nedefinită și să exploateze comportamentul sistemului.

Exploatările obișnuite ale codului de nivel scăzut nesigur permit unui atacator să efectueze citiri sau scrieri neautorizate la adrese de memorie. Adresele de memorie pot fi aleatorii sau alese de atacator.

Folosind limbi sigure

O abordare pentru a obține un cod sigur la nivel scăzut este utilizarea limbajelor sigure la nivel înalt. Un limbaj sigur este considerat a fi complet definit de manualul programatorilor săi. Orice eroare care ar putea duce la un comportament dependent de implementare într-un limbaj sigur, fie va fi detectată în momentul compilării, fie va duce la un comportament de eroare bine definit la runtime. În Java , dacă accesați o matrice în afara limitelor, va fi aruncată o excepție. Exemple de alte limbi sigure sunt C # , Haskell și Scala .

Executarea defensivă a limbajelor nesigure

În timpul compilării unui limbaj nesigur, verificările în timpul rulării sunt adăugate la codul de nivel scăzut pentru a detecta comportamentul nedefinit la nivel de sursă. Un exemplu este utilizarea canarilor , care pot termina un program atunci când descoperă încălcări ale limitelor. Un dezavantaj al utilizării verificărilor în timp de execuție, cum ar fi verificarea limitelor, este că acestea impun o performanță considerabilă.

Protecția memoriei , cum ar fi utilizarea stivei și / sau heap-ului neexecutabil, poate fi, de asemenea, văzută ca verificări suplimentare în timp de rulare. Aceasta este folosită de multe sisteme de operare moderne.

Executarea izolată a modulelor

Ideea generală este de a identifica codul sensibil din datele aplicației prin analiza codului sursă. Odată ce acest lucru este făcut, diferitele date sunt separate și plasate în module diferite. Când se presupune că fiecare modul are control total asupra informațiilor sensibile pe care le conține, este posibil să se specifice când și cum ar trebui să părăsească modulul. Un exemplu este un modul criptografic care poate împiedica cheile să lase vreodată modulul necriptat.

Compilare certificare

Compilarea certificării este ideea de a produce un certificat în timpul compilării codului sursă, folosind informațiile din semantica limbajului de programare la nivel înalt. Acest certificat trebuie anexat la codul compilat pentru a oferi consumatorului o formă de dovadă că codul sursă a fost compilat conform unui anumit set de reguli. Certificatul poate fi produs în diferite moduri, de exemplu, prin intermediul codului de transport al dovezilor (PCC) sau al limbajului de asamblare tipizat (TAL).

Cod de probă

Principalele aspecte ale PCC pot fi rezumate în următorii pași:

1. Furnizorul oferă un program executabil cu diferite adnotări produse de un compilator de certificare .
2. Consumatorul oferă o condiție de verificare, pe baza unei politici de securitate . Aceasta este trimisă furnizorului.
3. Furnizorul se execută condiția de verificare într - un demonstrator de teoreme pentru a produce o dovadă consumatorului că programul de fapt satisface politica de securitate.
4. Consumatorul rulează apoi dovada într-un verificator pentru a verifica validitatea dovezii.

Un exemplu de compilator de certificare este compilatorul Touchstone , care oferă o dovadă formală PCC a siguranței tipului și memoriei pentru programele implementate în Java.

Limbaj de asamblare tastat

TAL se aplică limbajelor de programare care utilizează un sistem de tip . După compilare, codul obiectului va purta o adnotare de tip care poate fi verificată de un verificator de tip obișnuit. Adnotarea produsă aici este în multe feluri similară adnotărilor furnizate de PCC, cu unele limitări. Cu toate acestea, TAL poate gestiona orice politică de securitate care poate fi exprimată de restricțiile sistemului de tip, care pot include siguranța memoriei și fluxul de control, printre altele.

Seminarii

• Seminarul Dagstuhl 03411 , Securitate bazată pe limbă, 5-10 octombrie 2003.

Referințe

Cărți

• G. Barthe, B. Grégoire, T. Rezk, Compilarea certificatelor , 2008
• Brian Chess și Gary McGraw, Analiza statică pentru securitate , 2004.

Lecturi suplimentare

• Dexter Kozen, Language Based Security , Cornell University, 1999
• Pieter Agten et al., Recent Developments in Low-Level Software Security , Universiteit Leuven
• Andrei Sabelfeld și Andrew C. Myers, Language-Based Information-Flow Security
• Fred B. Schneider și colab., A Language-Based Approach to Security , Carnegie Mellon University, 2000