„Moodsad ühiskonnad naalduvad paljude fundamentaalsete ülesannete täitmiseks aina enam väga tugevalt erinevatele masinatele,” ütleb Firenze Ülikoolis matemaatikat õppinud ja Kopenhaageni IT-ülikoolis järeldoktorantuuris teemat uurinud Veltri. „Kuna me masinaid väga usaldame, siis eeldame alati, et need töötavad korrektselt. Rikked neis süsteemides ja masinates võivad tuua kaasa nii märkimisväärseid rahalisi kaotusi kui suuremaid probleeme kogu ühiskonnale. Näiteks võivad sattuda rünnaku alla meile olulised turvasüsteemid, lekkida võib delikaatne või isiklik informatsioon, tehniliste vigadega või valesti programmeeritud liiklusvahendid võivad sattuda avalikkuse kätte.” 

Teadur lisab, et enamiku kasulike masinate juhtimiseks on arendatud vastav arvutitarkvara, et tagada täpne ja probleemivaba töötamine. 

„Sellest tulenevalt on tähtis kogu maailmas olevat riist- ja tarkvara pidevalt ning süsteemselt formaalmeetodite põhjal tõendada,” ütleb ta. „Selline tõendamine tagab nende süsteemide usaldusväärse toimimise ja aina enam tarkvaraarendajaid on võtnud suuna luua iseend kontrolliv tarkvara.” Ta lisab, et ka Eesti IT-ettevõtted on näinud suure kindlusega tarkvara vajalikkust ning asunud selle nimel arendusi tegema. 

„See tähendab aina suuremaid rahalisi investeeringuid nendesse osakondadesse ja töögruppidesse, mis kasutavad analüüsimiseks, sertifitseerimiseks ja kontrollimiseks formaalmeetodeid, kaasa arvatud tarkvara, mis on loodud analüüsima teisi loodavaid programme,” selgitab Veltri. 

Arenev tarkvara programmide analüüsiks 

Veltri uurimustöö EXCITE projekti raames ringleb selle ümber, et arendada välja meetodid arvutisüsteemide formaalseks tõendamiseks, kasutades selleks peamiselt erinevaid loogilisi ja matemaatilisi tehnikaid. 

„Minu töövahendid on interaktiivsed teoreemitõestajad,” selgitab ta. „Need on väga väljendusrikkad programmeerimiskeeled, mida saab kasutada paljude arvutiteaduses sageli kasutatavate matemaatiliste struktuuride lahtikodeerimises. Nende abil püüavad selle valdkonna teadlased luua arvutisüsteemide tarbeks konkreetseid matemaatilisi mudeleid, millega saaks omakorda simuleerida ja ennustada nende arvutisüsteemide käitumist. Tulemuseks on mudelid, mis on sertifitseeritud, kuna nende korrektsuse ja töökindluse on tõestanud masinad ise. See omakorda tagab lõppkasutajale kindluse, et süsteem toimib korrektselt ja on usaldusväärne. 

Veltri lisab, et idee teisi programme kontrollivate programmide, tõestajate või keelte arendamisest ei ole uus, kuid kuna aina suurem osa meie elust kolib arvutitesse, siis on hiljuti kasvanud vajadus nende järele täielikult uude kõrgusse. Teadur lisab, et kuna arvutisüsteemid lähevad pidevalt keerulisemaks ja laiahaardelisemaks, siis ei ole inimestel võimalik enam ise kõiki süsteeme ja koodiridu kontrollida, kuna see on äärmiselt kulukas. Küll aga saab rakendada masinaid kasuliku töövahendina nende keeruliste süsteemide ja programmide õigsuse tõendamiseks. 

Veltri lisab, et formaalse tõendamise tarkvara hakati arendama juba 1960ndate lõpus, kuid toona oli tegemist pigem vaid akadeemilise ülesandega. Tõsisemalt tõusis teoreemitõestajate vajadus fookusesse 1990. aastatel, kui arvutid muutusid võimsamaks, laienesid kõikidesse eluvaldkondadesse ja ettevõtted hakkasid saama rahalist kahju, kuna ei olnud võimelised nägema ette võimalikke probleeme. Sellised probleemid võivad esineda näiteks uute programmeerimiskeelte toimimisega uutel arvutitel, kui need peaksid mõne aasta jooksul mitu korda võimsamaks muutuma, või vastupidi tarkvara puhul, kui uued kirjutatud programmid nõuavad protsessorilt järjest enam võimsust. 

„Näitena võib tuua juhtumi ühest maailma suurimast arvutikiipide tootjast Intel, mis valmistas mitukümmend tuhat uut protsessorit, millelt avastati aga alles hiljem tootmise järel märkimisväärne viga. Viga oli tekkinud seetõttu, et kiibi tootmisel ei suudetud ette näha kõiki esineda võivaid vigu. Teoreemitõestajad oleksid suutnud sellise vea tänu simulatsioonile enne kiibi turule viimist üles leida ning ettevõte oleks saanud vea kõrvaldada. On võimalik, et tulevikus on need tõestajad nii targad, et suudavad leida ja lahendada sarnaseid probleeme iseseisvalt, kuid hetkel ei oleks see ei rahaliselt ega ajaliselt kasulik, kui vea oleks saanud formaalse tõendamise faasis parandada inimene,” selgitab Veltri. 

Veltri tööl on kaks suunda: esimene on teoreetiliselt arendada tarkvara formaalseks tõendamiseks uusi teoreemitõestajaid, mis oleks võimelised suhtlema suure hulga programmeerimiskeeltega. Üks viis on mõelda teoreemitõestajatest kui ülinutikatest märkmikest. Kasutajad saavad sisestada matemaatilisi võrrandeid ja tõestada teoreeme, mille tõesust hindab tõestaja. Kasutajad saavad paluda süsteemil tõestada neile ka mõnd tulemust ning tõestaja saab sageli selle tööga edukalt hakkama. 

Teine, praktilisem suund, millega teadur tegeleb, on samade teoreemitõestajate kasutamine olemasolevate programmeerimiskeelte formaalseks tõestamiseks ja uute keelte arendamiseks. See ülesanne tagab programmide õigsuse nende kavandatud käitumist kirjeldavate spetsifikatsioonide suhtes. See omakorda võimaldab arvutisüsteeme ennetavalt täiustada ja uuendada, tagades nende sujuva toimimise, mis on tänapäeva digitaalses kliimas paljude igapäevaelu oluliste tegevuste jaoks ülioluline. 

„Seda on keeruline selgitada, kuid suund on muuta tarkvaraarendus lihtsamaks, kontrollitavamaks ja sellega ka paremaks,” ütleb Veltri. „Praegu loome veel teoreetilisi lahendusi, kuid oleme natukene asja ka praktikasse viinud. Küll hetkel väga väiksel tasemel, kuid esimesed tulemused on paljulubavad.” 

Milline valdkond võidaks enim? 

Pikas perspektiivis võiks teoreemitõestajaid kasutada kõik arendajad iga programmi analüüsis. Hetkel võib aga näha, et suurimat huvi nende formaalmeetodite vastu näitavad üles kõige kriitilisemat täpsust vajavad valdkonnad, kuid ka need, kus on mängus palju raha. Veltri toob teoreemi tõestajate kasutamisest kasusaajatena esile isesõitvad autod ja lennunduse, aga ka kindlustuse, panganduse ja meditsiini. 

„Võtame näiteks isesõitva auto. Ühest küljest on selle tööks vaja äärmiselt suurt infomahtu ning samas ülimalt täpset ning alati korrektselt toimivat riist- ja tarkvarasüsteemi,” selgitab Veltri. „Isesõitva auto tarkvara õigsust saab hinnata süsteemi miljoneid kordi testides, kuid tõeliselt hinnata saab seda ainult formaalse tõestamise abil. Põhieesmärk inimelude eest vastutavate kriitiliste süsteemide puhul, nagu näiteks isesõitvad sõidukid, on loomulikult tagada õigsus. Teoreemitõestajate idee ongi olla piltlikult „selgeltnägijad”, kes kinnitavad süsteemide õigsust. Neid võib kasutada ka vigade leidmiseks ning sellest lähtuvalt süsteemide endi parandamiseks.” 

Ka panganduses ja meditsiinis, milles liigub meeletus koguses salajast, krüpteeritud ja piiratud ligipääsulubadega informatsiooni, millest enamik on delikaatsed isikuandmed, peavad süsteemid toimima selliselt, et ühegi viga kasutamisel sisse ei tule. Enamik maailma suuri infolekkeid ongi olnud seotud vääralt ehitatud süsteemidega, mitte häkkerluse või pahatahtlikkusega. 

„Huvitav on see, et väga paljude ettevõtete juurde tekivad aina kiiremini üksused, mis nende probleemidega tegelevad. On arusaadav, et Eestis on sellised üksused näiteks Skype‘i, Guardtime‘i või Bolti juures, kuid ka pangad ja kindlustusagentuurid ei ole jäänud sellest arengust puutumata. Kõik töötavad selleks, et need firmad saaksid olla 100% kindlad, et nende arendatud või tellitud tarkvara – aga ka riistvara – toimiks nii, nagu toimima peaks. Küsimus on alati lisagarantiides nii organisatsiooni kui ka klientide jaoks,” lisab Veltri. 

Tulemus on turvalisem digiühiskond 

Veltri arvab, et 30 aasta pärast on uute kõrge kindlusega tarkvara ja formaalmeetodite põhise tõendamise tulemusel viidud meie digiühiskond täiesti uuele turvalisuse ja töökindluse tasemele. Aga mida võidab sellest kõigest tavainimene? 

„Just arvutiprogrammide põhine riigile oluliste kriitiliste arvutisüsteemide kontrollimine tänapäevase elu kõige fundamentaalsemates aspektides – e-valimised, pangandus, meditsiin – on see, mis annab inimestele tagasi usalduse tehnoloogia ja teaduse vastu. Usalduse, mis on hetkel pigem ebastabiilne ja kasin. See usaldus aga omakorda viib meid parema elukvaliteedini igas eluvaldkonnas,” lisab ta. 

Veltri mainib, et tipptasemel tehnoloogia on tarkvara analüüsiks ja kontrollimiseks kasutusel juba paljudes edukates IT-ettevõtetes nii Eestis kui ka mujal maailmas. Järgmiste aastakümnete jooksul on oodata, et see fenomen aina kasvab ja laieneb. Arvata on, et formaalmeetodite abil programmide kontrollimine muutub igas tarkvarafirmas ja arvutisüsteeme loovas riigiasutuses standardprotseduuriks ja põhisuunaks. 

„Selle tulemusel saavad lisakindluse nii arendajad, nende kliendid, kuid mis peamine, ka lõppkasutajad, et programmid, mis meie elu juhivad ja mida iga päev kasutame, töötavad korrektselt,” selgitab Veltri. 

Artikkel ilmus Eesti IT Tippkeskuse EXCITE ajakirjas 2021. aastal. Loe veebiversiooni.

Tutvu Eesti IT Tippkeskusega EXCITE: www.excite.it.ee

Fotod: Hendrik Osula; Shutterstock

Excite-t rahastatakse Euroopa Regionaalarengu Fondi vahenditest.