Bug-urile: De la frustrare la succes
Blocarea computerului şi bug-urile din componentele software ale acestuia sunt enervante şi ele ne învaţă, de obicei tardiv, cât de important este să efectuăm un backup regulat al calculatorului. Dar ar putea deveni toate acestea de domeniul trecutului?
Vă amintiţi de cei care v-au spus să vă salvaţi datele? Credit: Sybren A. Stuvel/Flickr
Cu toţii ştim că munca noastră timp de mai multe zile sau săptămâni se poate pierde într-o clipă. Indiferent că a fost vorba despre un editor de texte care s-a blocat sau de un sistem de operare în care, la un moment dat, a apărut o eroare, fişierele de lucru din computerul vostru se pot pierde (acestea putând conţine rezultate de laborator sau diferite rapoarte întocmite de voi…).
Dar ce se întâmplă dacă software-ul este responsabil pentru mai mult decât de nişte date dintr-un computer? Ce se întâmplă dacă banii sau chiar viaţa voastră depind de o componentă software?
Bursele de valori şi sistemele bancare sunt controlate prin software şi de fiecare dată când conduceţi o maşină sau zburaţi cu avionul practic vă puneţi viaţa în mâinile unor sisteme software.
Desigur, sistemele critice de siguranță sunt realizate cu mult mai multă grijă decât un software obișnuit, dar asta nu înseamnă că nu există bug-uri. Testarea bug-urilor, principala metodă de verificare software utilizată în prezent, se confruntă cu următoarea problemă: chiar dacă la un moment dat nu au fost identificate bug-uri, asta nu înseamnă că acestea nu există. Poate că, pur și simplu, nu le-am căutat suficient de mult timp sau poate că nu am fost suficienţi de atenţi la ele.
Deci, ce putem face în legătură cu această problemă?
Ei bine, mai există o altă metodă denumită „verificarea formală”. Software-ul este doar o formă de logică. Folosind un argument matematic se poate demonstra că o componentă software se va comporta întotdeauna într-un anumit fel.
Acest proces, cunoscut sub numele de verificare formală, ne poate indica lipsa unor bug-uri într-un software, dar şi această tehnică are propriile sale limite. Până de curând a fost mult prea greu să se aplice această metodă, în mod direct, într-un cod de program având orice complexitate.
Aceasta este ceea ce a făcut echipa noastră din cadrul NICTA și UNSW: am reuşit să evidenţiem o dovadă formală de corectitudine pentru un cod complex, critic, în cazul unui microkernel denumit seL4. Un microkernel reprezintă nucleul unui sistem de operare minimal care controlează hardware-ul și memoria de acces pentru restul sistemului de operare.
Având aproximativ 10.000 de linii de cod, mărimea lui seL4 este tipică pentru o componentă software critică, chiar dacă această mărime este mică în comparaţie cu cea a unui sistem de operare (Linux, de exemplu, conţine milioane de linii de cod).
Sarcina principală a lui SeL4 este aceea de a oferi o protecţie la erori: dacă două componente dintr-un sistem cum ar fi, de exemplu, o interfaţă pentru utilizator şi un senzor medical sunt controlate prin acest microkernel, chiar dacă interfaţa pentru utilizator se blochează, senzorul medical nu va fi afectat.
Aceasta este o strategie foarte bună pentru gestiunea bug-urilor dintr-un software: dacă nu le putem elimina în întregime, cel puţin să ne asigurăm că acestea nu sunt letale, chiar dacă pot fi enervante.
Chiar dacă nu există nicio garanţie finală că un anumit calculator va rula codul nostru în mod corect, noi am reuşit să creştem în mod semnificativ nivelul de încredere al software-ului din cadrul lui seL4.
De mai mult de 30 de ani s-a încercat să se obţină ceva de genul ăsta şi acum, în cele din urmă, acest lucru a devenit o realitate.
Această tehnologie se poate aplica într-o gamă largă de aplicaţii privind:
– îmbunătăţirea securităţii și a siguranței produselor software existente
– funcţionarea programelor financiare care rulează în siguranță pe un hardware existent
– asigurarea unor comunicații mobile sigure
– îmbunătățirea dispozitivelor de implant medical
Dezvoltarea aplicațiilor comerciale pe baza acestui cod va continua în viitor, dar amintiți-vă că puteți evita (măcar în parte) bug-urile enervante și blocajul calculatorului prin realizarea, în mod regulat, a unor copii de siguranţă a datelor din computerul vostru.
Traducere şi adaptare după Frustration to salvation: a code to end computer crashes