CertiKOS

CertiKOS este un proiect dezvoltat de Zhong Shao, profesor la Universitatea Yale , Connecticut , cu participarea unei echipe de alți 6 cercetători. CertiKOS ( Kit de sisteme de operare certificate ) este un instrument metodologic pentru proiectarea și dezvoltarea sistemelor de operare certificate. Abordarea sa se bazează pe definirea și certificarea straturilor de abstractizare , ele însele bazate pe semantică bogată în specificații (specificații profunde). Aceste procese răspund la ceea ce poate fi considerat o lege fundamentală, un puternic rafinament contextual. Această metodologie nu numai pentru certificarea tuturor semanticii (de către asistentul de probă al Coq ), ci și pentru certificarea compilării prin utilizarea CompCertX. CertiKOS permite dezvoltarea unui hipervizor și a mai multor miezuri certificate, inclusiv mC2. Acesta din urmă acceptă procesoare multi-core , precum și execuția întrețesută a modulelor kernel / utilizator pe diferite straturi de abstractizare (concurență).

Motivații și provocări

Cele miezurile , sisteme de operare , hipervizori (etc) sunt software / programe , o serie de linii de cod , care atunci când sunt compilate și interpretate de către mașină, face un serviciu pentru utilizator. Ele se găsesc astăzi în noastre smartphone - uri , masini, trântori , calculatoare, avioane, sisteme sau servicii bancare de automatizare acasă ... Potrivit raportului 2017 de Linux Foundation , în Linux de operare sistemul efectuează aproape 90% din volumul de muncă. Al publicului nor , acoperă 62% din cota de piață a tehnologiei încorporate și 99% din cea a supercomputerelor . Este prezent pe 82% dintre smartphone-uri. International Data Corporation (IDC) , rapoartele pe care le - a vandut aproximativ 355,2 milioane de smartphone - uri la nivel mondial în 3 - lea trimestru din 2018, aproape 45 de smartphone - uri pe secunda. Prin urmare, impactul este semnificativ, dar și miza financiară este prezentă. De exemplu, potrivit The Transparency Market Research (TMR), piața sistemelor încorporate la nivel mondial, care cântărea aproape 153 miliarde dolari în 2014, ar putea crește până la aproape 223 miliarde dolari în 2021. Omniprezența și dependența tot mai mare a societăților noastre moderne de aceste diferite sisteme, fac esențială dezvoltarea unui software sigur și sigur .

Sistemele de operare sunt coloana vertebrală a sistemelor software și a componentelor deosebit de importante pentru securitatea globală. Într-adevăr, aceste sisteme nu permit întotdeauna mașinii să furnizeze serviciul pentru care sunt proiectate. Acest lucru se poate datora defectelor de scriere în cod, defectelor de proiectare sau chiar interacțiunilor cu alte programe software. Aceste defecte pot da naștere la bug-uri . Exploatarea unora dintre aceste defecte poate permite, de asemenea, terților să devieze utilizarea lor pentru a recupera date și a interfera cu funcționarea sistemelor. Aceste erori constituie apoi încălcări ale securității (a se vedea linkurile externe: „Buletine informative, încălcări ale securității”). Aceste defecțiuni sunt evidențiate printr-o verificare a codului, corectarea lor se face prin patch-uri corective. Această soluție banală implică parcurgerea fiecărei linii de cod și testarea fiecărui scenariu posibil. Deși această soluție este fezabilă, devine rapid plictisitoare și exponențială pe măsură ce se acumulează liniile de cod. De exemplu, kernelul Linux Versiunea 4.13 conține 24.766.703 linii de cod. Potrivit lui Edsger W. Dijkstra , „Testele programului pot fi folosite pentru a arăta prezența bug-urilor, dar niciodată pentru a arăta absența lor”. Alternativa constă într-o verificare prin metodă formală (deductivă). Potrivit contribuitorilor seL4, „o verificare formală completă este singura modalitate cunoscută de a vă asigura că un sistem este lipsit de erori de programare”. . Acestea din urmă au fost în special primele care au produs dovada corecției funcționale pentru un micro-nucleu. CertiKOS este poziționat deschis în această perspectivă, pentru a certifica un sistem de operare, mai degrabă decât pentru a-l face o verificare banală. Cu toate acestea, nu se concentrează asupra acestui obiectiv. Încearcă să ofere cea mai bună metodologie pentru proiectarea și dezvoltarea sistemelor de operare eficiente, fiabile și sigure. CertiKOS caută, de asemenea, să producă un nucleu certificat, capabil să suporte simultan și mașini multi-core.

Filozofia Certikos

Sistemul de operare , sau OS ( Sistem de operare ), este un set de programe care fac interfața între hardware - ul calculatorului și a programelor de utilizator. Este coloana vertebrală a unui sistem informatic. Acest sistem este construit și se bazează pe un nucleu ( Kernel în engleză), care gestionează resursele hardware. Acesta din urmă oferă mecanisme de abstractizare între software și hardware.

Certificarea unui program constă în demonstrarea, pe baza unei metode formale, că Efectuează de program, fără erori și în toate cazurile posibile, sarcina încredințată. Această metodă se bazează pe o analiză statică a programului, permițând un raționament riguros pentru a demonstra validitatea unui program în raport cu specificațiile acestuia. Raționamentul se face pe semantica programului.

Certificare de bază

CertiKOS își propune să certifice un sistem de operare. Această noțiune se bazează pe probabilitatea verificării de către mașină, într-un mod explicit și formal. Acest efort de probă este cu atât mai complicat, având în vedere calitatea probei și riscul controversei. Echipa seL4 a fost prima care a construit o dovadă a corecției funcționale, pentru un microkernel . CertiKOS l-a folosit, de asemenea, folosind asistentul de probă al cocoșului și definirea unui rafinament contextual puternic.

Metodologia CertiKOS intervine din etapa de conceptualizare a sistemului și urmărește în special să definească specificații precise, dând naștere la comportamente observabile. Aceste specificații sunt transformate în formule logice. Prin demonstrarea matematică a acestor formule, putem apoi să certificăm programul . Utilizarea Certikos își propune să definească specificații bogate și detaliate, bazându-se pe noțiunea de specificații profunde, printr-o suprapunere a diferitelor straturi de abstractizare logică.

Rafinarea contextuală a CertiKOS indică faptul că implementarea fiecărei funcții a nucleului se comportă ca și specificația sa în orice interacțiune dintre nucleu și program ( contextul utilizatorului ). Astfel, luând în considerare K pentru nucleu, P pentru program și S pentru specificația funcțională a nucleului, combinația codurilor K și P afin S și P. CertiKOS încearcă să descompună verificarea sistemului de operare în mai multe sub- sarcini, mai mici și ele însele controlabile, pe baza specificațiilor lor profunde. Prin urmare, este certificarea acestor diferite straturi de abstractizare, care permit certificarea sistemului de operare. Definiția rafinamentului contextual în CertiKOS este definită după cum urmează: luați L0 și L1 ca două interfețe (straturi de abstractizare) și P pentru un program. L0 rafinează contextual L1, dacă și numai dacă pentru toate P, P este valid pe L1, indiferent de configurație. Rafinarea contextuală implică, de asemenea, că pentru toate P, P este valabil pe L1, indiferent de configurație și că orice comportament observabil al lui P pe L0, în anumite configurații, este de asemenea observat pe L1, indiferent de configurație.

Specificații profunde

Sistemele de operare constituie o multitudine de straturi suprapuse de abstractizare: nuclee (Kernel), piloți (Drivers), Hypervisors (etc.). Fiecare dintre aceste straturi formează o interfață, care ascunde detaliile de implementare ale unui set de caracteristici ale stratului subiacent. De programe clienții construite pe partea de sus a fiecărui strat poate fi înțeleasă numai în ceea ce privește interfețele lor și independente de punerea în aplicare a stratului. În ciuda importanței lor evidente, straturile de abstractizare au fost în general tratate ca un concept de sistem; nu au fost niciodată specificate sau verificate formal. Acest lucru face dificilă stabilirea unor proprietăți de corecție puternice și verificarea programului pe mai multe straturi. Importanța definirii precise a specificațiilor funcționale ale diferitelor straturi de abstractizare este strâns legată de certificarea acestora din urmă.

Cu toate acestea, este vorba de certificarea unui întreg, deci de luarea în considerare a relațiilor dintre straturi. Acesta este motivul pentru care CertiKOS definește specificații mai bogate, specificații profunde. Aceste specificații iau în considerare implementarea de bază, captează funcționalitățile sale precise, dar și efectele posibile ale implementării asupra contextelor clienților săi.

Este posibil să se reprezinte conceptul de specificație cu următoarele exemple:

Acest exemplu ilustrează, într-un mod simplu, aspectul detaliat al specificației profunde. Obiectivul bogăției detaliilor specificației profunde este de a surprinde cu precizie comportamentele observabile în contextul implementării, dar independent de acesta. Luați în considerare două implementări (de exemplu, M1 și M2) ale aceleiași specificații profunde (de exemplu, L), acestea trebuie să aibă comportamente echivalente contextual. Această proprietate a independenței de implementare a specificațiilor profunde face posibilă verificarea modulară a proprietăților de corecție, cum ar fi specificațiile de programare de tip sau contract.

Independența implementării specificației profunde (încercare de popularizare): considerați sistemul de frânare (pedala de frână) a unei mașini ca o interfață (L1), între șofer (P) și plăcuțele de frână (interfața L0). R, reflectând relația contextuală dintre L1 și M (1 și 2), este reprezentat de presiunea pedalei. Specificația profundă a interfeței L1 este ABS, M1 (modulul kernel care implementează interfața L1 pe baza specificațiilor sale) este o mașină Citroen C1. În cele din urmă, M2 (modulul kernel care implementează interfața L1 pe baza specificațiilor sale) este o mașină Citroen C3. M1 și M2 vor avea presiunea lui P pe frână ca funcție, cu posibilitatea declanșării ABS.

Certificare cod computer: CompCertX

CertiKOS lucrează pentru a proiecta micronucleele, deoarece verificările lor sunt inerent mai puțin împovărătoare. Cele Nucleele de sisteme de operare nu sunt nimic mai mult sau mai puțin de calculator programe scrise într - un limbaj de programare C și / sau în programare limbaj de asamblare. Orice limbaj de programare constituie în sine un strat de abstractizare, deoarece nu este direct interpretabil de către mașină.

Pentru a certifica acest nou strat de abstractizare, pentru a asigura buna funcționare a unui kernel, este necesar, prin urmare, să certificați că liniile de cod vor putea fi compilate corect, pentru a nu genera bug-uri. În acest scop, CertiKOS folosește CompCertX „CompCert eXtended”, dezvoltat de Gu et al și bazat pe CompCert . Utilizarea CompCert nu dovedește corectitudinea compilării straturilor individuale sau a modulelor utilizate de CertiKOS. Acesta din urmă poate face acest lucru doar pentru programe întregi. Prin urmare, a fost adaptat.

CompCertX implementează ClightX (o variantă a limbajului sursă al CompCert, Clight) și un limbaj de asamblare , LAsm. Cele operaționale Semantica ale CompCertX, cum ar fi CompCert, este dată de relațiile de tranziție în pași mici, care au stări inițiale și finale. Cu toate acestea, în cazul straturilor sau modulelor individuale, și nu al programelor întregi, definiția acestor stări a trebuit să fie adaptată. De exemplu, pentru starea inițială, CompCertX ia memoria inițială, lista argumentelor și indicatorul funcției care trebuie apelate ca parametri. Pentru starea finală, este valoarea returnată și starea memoriei, atunci când părăsim funcția, care sunt utilizate ca parametri. Starea finală a memoriei este observabilă deoarece este returnată apelantului. Astfel, în CompCertX, este necesar în diagramele de simulare să se ia în considerare transformările memoriei, atunci când se raportează stările finale.

De certificare straturi de abstractizare în CertiKOS este gestionat și livrat de CompCertX (cod sursă de asamblare). Cu toate acestea, ansamblul CompCertX care permite conversia unui ansamblu în codul mașinii nu este verificat. Se presupune corectitudinea corectorului Coq și a mecanismului său de extragere a codului.

Implementarea CertiKOS

Prin intermediul unui hipervizor certificat

Odată cu dezvoltarea semnificativă a soluțiilor de stocare și a tipului de cazare Cloud (Amazon EC2, Salesforce, Rackspace), a devenit din ce în ce mai important să securizăm datele, astfel încât clienții să poată avea încredere în aceste soluții. Cu toate acestea, a fost complex să se certifice că un hipervizor a fost 100% sigur, datorită complexității și dimensiunii sale. Prin urmare, a fost imposibil să se certifice și să se garanteze că funcționarea sa va fi corectă.

Unul dintre primele defecte de securitate într-un mediu cloud este software-ul de gestionare în sine. Într-adevăr, acest software face posibilă alocarea și revocarea resurselor de pe serverele puse la dispoziție pentru a găzdui datele și, prin urmare, acest software poate avea acces la informațiile găsite pe servere.

Software-ul de gestionare a furnizorilor utilizează interfețe de încredere pentru delegarea kernelului pentru a aloca și revoca resursele în conformitate cu politica furnizorului. La rândul său, nucleul de încredere își actualizează înregistrările de proprietate pentru a restricționa în mod adecvat accesul la resurse în fiecare domeniu de încredere utilizând tehnici standard de protecție și virtualizare.

Alocarea, gestionarea și revocarea resurselor conform CertiKOS Hypervisor

CertiKOS alocă resursele CPU spațial, la granularitatea de bază. În timpul primei versiuni a CertiKOS, un nucleu CPU a fost atribuit unui invitat. Ulterior, hipervizorul CertiKOS a fost ajustat pentru a face alocarea CPU mai flexibilă. CertiKOS oferă interfețe pentru software-ul de management pentru a aloca nucleele procesorului către clienți și pentru a le revoca.

CertiKOS extrage atât memoria RAM, cât și unitățile de stocare ca spațiu de memorie pentru software-ul de gestionare și clienții de încredere. Nucleul nu include un sistem de fișiere, lăsând această funcționalitate unui software invitat de încredere. CertiKOS expune doar interfețele care acceptă delegarea și accesul protejat la memorie și stocare pe disc.

CertiKOS oferă interfețe pentru software-ul de gestionare a furnizorului pentru a oferi clienților acces la infrastructura de rețea partajată a furnizorului. Designul actual presupune că hardware-ul serverului oferă suficiente NIC-uri fizice și / sau NIC-uri virtualizate pentru a dedica cel puțin o NIC fiecărui client fără multiplexare software. CertiKOS ar putea fi îmbunătățit în viitor pentru a oferi propria sa multiplexare dinamică a interfețelor de rețea, dar aceasta nu este o prioritate absolută, deoarece virtualizarea plăcii de rețea bazată pe hardware devine mai obișnuită și mai ieftină.

În timpul rulării, CertiKOS își folosește înregistrările de proprietăți pentru a verifica autorizarea tuturor cererilor de acces explicit și pentru a configura mecanisme de protecție bazate pe hardware, cum ar fi hardware-ul MMU și IOMMU. În acest fel, CertiKOS aplică izolarea resurselor între aplicații și previne scurgerile de informații.

Prin intermediul unui nucleu certificat: mCertiKOS, mC2

Odată ce hipervizorul a fost dezvoltat, cercetătorii au întâmpinat unele dificultăți. Într-adevăr, hipervizorul lor nu a fost neapărat adaptat la un kernel Linux standard sau altul. Prin urmare, acest lucru a făcut ca utilizarea hipervizorului să fie învechită. Apoi au decis să dezvolte pe deplin un nucleu (Kernel), mai ușor în comparație cu un nucleu Linux, dar permițând validarea funcționării corecte a hipervizorului lor. Mai mult decât atât, pentru a dezvolta acest nucleu, au folosit și metode de certificare , astfel încât nucleul să fie verificat și hipervizorul să ofere performanțe optime.

Datorită semanticii sale de compoziție a straturilor, CertiKOS a rezultat în mai multe miezuri certificate, dintre care cele mai de succes sunt mCertikos și mC2. Mc2 este capabil să accepte mașini multi-core și concurență, precum și intercalarea nucleului și a modulului de rulare a utilizatorului, pe diferite straturi de abstractizare. Miezul mC2 este o evoluție a mCertikos dezvoltată inițial ca parte a unui amplu proiect de cercetare, finanțat de DARPA , pentru vehiculele terestre fără pilot. Acesta din urmă este proiectat secvențial, în 4 module totalizând 28 de straturi de abstractizare certificate pentru versiunea sa de bază și 5 module în total 37 de straturi de abstractizare certificate pentru versiunea sa cu hipervizor. Fiecare strat este compilat și certificat de CompCertX. Acest nucleu reprezintă 3000 de linii de cod și vă permite să porniți un sistem Linux.

Începând de la mCertikos și adăugând diferite funcționalități (module) la acesta, cum ar fi gestionarea dinamică a memoriei, suport pentru containere pentru controlul consumului de resurse, suport pentru virtualizare hardware Intel, memorie partajată IPC , blocări IPC , ticket sincron și MCS (un spinlock prin excludere reciprocă) (etc.), Certikos a dat naștere mC2.

Kernel-ul mC2 este o versiune mai avansată, care include 6500 C și linii de asamblare x86 . Dovedește că este posibilă acuratețea funcțională a unui nucleu de sistem de operare simultan complet și versatil, cu blocare cu granulație fină (MCS).

Nucleul mC2 include o bază de bază cu specificații reduse pentru a simplifica procesul de revizuire și a minimiza erorile. Această bază reprezintă aproape 1400 de linii, inclusiv 943 de linii pentru straturile inferioare, constituind teoria axiomatică a mașinii fizice și 450 de linii pentru interfețele de apel ale sistemului abstract. În afară de această bază, există specificații suplimentare: 5246 linii, pentru diferitele funcții ale nucleului și aproape 40.000 de linii, pentru a defini diverse teoreme, leme și invarianți.

CertiKOS a dovedit proprietatea rafinării contextuale a nucleului său mC2, în raport cu o specificație profundă, la nivel înalt. Acest rafinament este definit după cum urmează: pentru orice program (P), interacțiunea nucleului (K) și P, în semantica mașinii x86, implică același comportament ca P în semantica mașinii mC2: ∀P, [[P⋉K]] x86 ⊆ [[P]] mC2. Proprietatea de echivalență comportamentală pentru P este deci diferențiată. Toate întreruperile și apelurile de sistem respectă strict specificațiile de nivel înalt. Acestea sunt întotdeauna executate în siguranță (și în cele din urmă terminate), așa cum este indicat de această proprietate de remediere funcțională. Nu există depășire de tampon , niciun atac de injectare de cod , depășire de număr întreg sau acces nul la pointer etc.

Kernel-ul mC2 nu este încă la fel de complet ca un sistem Linux. În prezent nu are un sistem de stocare certificat. Mai mult, se bazează pe un încărcător de boot care inițializează procesoare și periferice, care nu este încă verificat.

Referințe

  1. LinuxFoundation 2017 , p.  3
  2. Auffray 2018 , p.  1
  3. TMR 2018 , p.  1
  4. Shao 2016 , p.  653
  5. Toyota 2013 , p.  1
  6. Dennis Burke Toate circuitele sunt ocupate acum: rețeaua AT&T de lungă distanță din 1990 se prăbușește
  7. Kalagiakos 2012 , p.  6
  8. US-CERT și 2018 VMware-Releases-Security-Updates
  9. US-CERT și 2018 Microsoft-Releases-November-2018-Security-Updates
  10. US-CERT și 2018 Cisco-Releases-Security-Updates
  11. US-CERT și 2018 Apple-Releases-Security-Updates-iCloud-iOS
  12. SUA-CERT și 2018 Apache-Releases-Security-Update-Apache-Tomcat-JK-Connectors
  13. FR-CERT și 2018 Vulnerabilități multiple de scurgere de informații în procesoare
  14. Vulnerabilitate FR-CERT și 2018 în Wallix AdminBastion
  15. FR-CERT și 2018 Vulnerabilități multiple în nucleul Ubuntu Linux
  16. Dijkstra 1979 , p.  6
  17. Klein 2009 , p.  207
  18. Gu 2015 , p.  596-2
  19. Shao 2016 , p.  666
  20. Shao 2016 , p.  655
  21. De Millo 1979 , p.  279
  22. Shao 2016 , p.  654
  23. Guithub Teorema celor patru culori și dovezi ale computerului
  24. CNRS Un computer pentru verificarea dovezilor matematice
  25. Shao 2016 , p.  607
  26. Apel 2016 , p.  2
  27. Gu 2015 , p.  595-1
  28. Pierce 2016 , p.  1
  29. Shao 2016 , p.  654-2
  30. Shao 2016 , p.  658
  31. Gu 2015 , p.  595
  32. Gu 2015 , p.  604
  33. Shao 2016 , p.  656
  34. CompCert C a verificat compilatorul 2018 , p.  1
  35. Shao 2016 , p.  657-5
  36. Vaynberg2011 2011 , p.  4
  37. Vaynberg2011 2011 , p.  2
  38. Shao 2016 , p.  656-657
  39. Gu 2015 , p.  596
  40. Shao 2016 , p.  663
  41. Shao 2016 , p.  664
  42. Shao 2016 , p.  655-655
  43. Shao 2016 , p.  657

Bibliografie

linkuri externe

Buletin informativ: defecțiuni la computer https://www.us-cert.gov/ https://www.cert.ssi.gouv.fr