‘Software Fallo 0’, un projecte de la UB per aconseguir un sistema de programació sense errors
Tots els programes informàtics contenen errors; fins i tot els que controlen la indústria aeronàutica o militar tenen errors en el producte final. Aquesta situació és especialment preocupant a causa de la cada vegada major dependència de la programació en processos tan importants com els mecanismes de vot informàtic, les tecnologies mèdiques o les aplicacions que decideixen si una persona compleix o no la llei. Un equip de la Universitat de Barcelona participa en un projecte de quatre anys de durada que impulsa un nou paradigma dins la indústria del software: el desenvolupament per primera vegada a Espanya d’un programari a gran escala sense errors. El projecte ‘Software Fallo 0’ aplicarà una innovadora metodologia de programació per avaluar les dades recollides pel tacògraf, un instrument que monitoritza l’activitat de cada vehicle per detectar quan s’incompleix la normativa. Actualment un software no verificat porta a terme aquesta tasca avaluadora i, com qualsevol software, comet errors que han suposat grans pèrdues a empreses del sector, i fins i tot forts greuges als drets de les persones.
“El mètode per aconseguir aquest programari sense errors suposa no només un canvi abismal en la qualitat del producte final, sinó també un canvi en el paradigma de programació, ja que la programació tradicional fa servir un tipus d’arquitectura que és la responsable de gran part dels errors o bugs”, explica Joost Joosten, professor del Departament de Filosofia de la UB i investigador de l’Institut de Matemàtica de la UB, que lidera el projecte. “La mitjana de la indústria del software sol situar-se entre els 15 i els 50 errors per cada mil línies de codi. El software verificat formalment garanteix zero bugs”, recorda l’investigador.
Un producte per a la Unió Europea, els Estats Units, el Brasil i el Canadà
La primera fase del projecte és la creació d’un programari capaç de reproduir les lleis de transport de mercaderies per carretera a partir de les regulacions de transport de la Unió Europea, els Estats Units, el Brasil i el Canadà, països en els quals el problema tecnològic en aquest camp es troba exactament en el mateix punt. La metodologia per assolir aquest objectiu consisteix a escriure especificacions formals, en aquest cas sobre les lleis del transport, en comptes d’escriure directament el programari, i a traslladar aquestes especificacions a un llenguatge lògico-matemàtic del qual s’extrauria el programari definitiu sense errors.
“A través d’aquest procés s’extreu directament un programa informàtic que garanteix el seguiment de les especificacions basades en la llei. La clau que marca la diferència és que aquest codi s’extreu de demostracions matemàtiques. Aquestes demostracions asseguren al cent per cent la correcció del codi pel que fa a les especificacions detallades al principi del procés “, detalla Joost Joosten.
Programari verificat mitjançant demostracions lògico-matemàtiques
La metodologia parteix del paradigma de programació funcional, que sol utilitzar-se en els sectors en què la fiabilitat és crítica. Posteriorment, l’objectiu és portar l’estàndard de seguretat un pas més enllà i convertir el programa en un codi verificat formalment, i per tant sense errors, i certificat mitjançant un procés lògico-matemàtic. “La principal diferència entre el programari verificat formalment i el programari tradicional és que aquest últim es prova només sobre casos particulars, en un procés que es duu a terme a posteriori del desenvolupament del programa. En canvi, la verificació formal té com a objectiu verificar el conjunt total d’execucions possibles del programa. Per això, el procediment pel qual es verifica formalment un programari és totalment diferent, ja que ha d’anar acompanyat de la força de les demostracions matemàtiques exactes. De fet, el codi resultant és el producte d’aquestes demostracions, i per tant és un procés de prova a priori “, destaca l’investigador.
La verificació formal ha despertat recentment l’interès de la NASA, que pròximament durà a terme el seu 11è. Simposi sobre Mètodes Formals, i ja s’ha implementat en altres projectes. Un dels primers va ser el metro de París sense conductor, RATP. Els seus informes indiquen que la verificació formal del programari va revelar errors que les fases intensives de proves no havien revelat abans. No obstant això, respecte a la metodologia utilitzada a París, la d’aquest projecte, que utilitza un assistent de demostració anomenat Coq, és més ambiciosa, pel fet que és més costosa però alhora més potent, és a dir, capaç de portar la verificació formal a àmbits més complexos. Alguns projectes d’èxit que fan servir aquesta mateixa metodologia són CompCert, un compilador del llenguatge de programació C verificat formalment usant Coq, i el sistema operatiu eChronos RTOS, verificat formalment utilitzant l’assistent de demostració Isabelle.
Darrere totes aquestes tècniques hi ha la teoria de la demostració avançada, que és una branca de la lògica matemàtica. “El que fem és demostrar matemàticament, utilitzant una lògica que es diu lògica constructiva, que hi ha un algoritme amb aquesta o aquella altra propietat, en aquest cas les especificacions obtingudes de la llei del transport. En fer-ho, l’algoritme extret anirà acompanyat d’un certificat que acreditarà que compleix les especificacions. Aquest procés de certificació és llarg, però tots els passos que es fan per completar-lo són molt simples i la correcció es pot verificar amb Coq, un programa que serveix com a assistent de demostració. D’aquesta manera, es comproven els molts però simples passos que confirmen que el programari és correcte”, resumeix Joost Joosten.
Menys burocràcia i menys sancions errònies
El resultat del projecte constituirà un gran avenç, ja que com que no produeix errors s’eliminarà la possibilitat de sancions errònies per fallades del programari que avalua les dades del tacògraf, la qual cosa reduirà processos administratius i judicials i generarà seguretat jurídica tant als professionals del transport com als cossos de seguretat dels estats.
Aquesta iniciativa, que disposa d’un pressupost total que supera els 2.200.000 euros, està inclosa en la convocatòria Retos Colaboración del Ministeri espanyol de Ciència i Innovació i Universitats, l’objectiu de la qual és el finançament de projectes en cooperació entre empreses i organismes de recerca.
A més de la Fundació Bosch i Gimpera de la Universitat de Barcelona, en el consorci del projecte també hi participen Guretruck, una empresa que ofereix a entitats serveis d’enginyeria informàtica i jurídica relacionats amb el món del transport, i Formal Vindications, una empresa especialitzada en la verificació formal d’especificacions tècniques i de programari.
El projecte amb el número d’expedient RTC-2017-6740-7, està cofinançat pel Fons Europeu de Desenvolupament Regional (FEDER) de la Unió Europea.
