Formális szoftver verifikáció a gyakorlatban: kísérleti kiértékelés és analízis

A formális szoftver verifikáció egyre nagyobb jelentőséggel bír, különösen biztonságkritikus rendszerek területén. Ugyanakkor a formális módszerek számításigényesek és összetettek, ezért számos különféle hatékony technika került kifejlesztésre a különböző alkalmazási területekre szabva. A Theta egy általános, konfigurálható keretrendszer, mely több különböző algoritmust fog össze és a Gazer nevű frontenddel képes C programok ellenőrzésére. Habár a keretrendszer hatékonyságát és sokszínűségét már korábbi vizsgálatok bizonyították, annak eldöntése, hogy egy adott programon mely konfiguráció fog várhatóan a legjobban teljesíteni, mély elméleti hozzáértést igényel.

Ezen munka integrálja a Theta és Gazer keretrendszereket az SV-Comp (International Competition on Software Verification) futtatókörnyezetébe. Az SV-Comp több ezer verifikálandó C programot fog össze, így akadémiai és ipari körökben egyaránt mint de-facto tesztkészlet tartják számon. Egyrészt az integrációhoz különféle gyakorlati kihívásokat kellett megoldanunk, beleértve egy szabványos interfész megvalósítását és verifikálható hibajelentések (program végrehajtások) produkálását a hibás programok esetén.

Másrészt, ugyan az integráció a Theta rendszer több ezer programon való futtatásának lehetőségét nyújtja, a lehetséges konfigurációk nagy száma miatt az összes konfiguráció minden feladaton való futtatása nem lenne kivitelezhető a gyakorlatban. A különböző konfigurációk erősségeinek és gyengeségeinek meghatározásához így egy szisztematikusan megtervezett, iteratív méréssorozatot hajtottunk végre. Az eredmények részletes elemzése után kiválasztottuk a konfigurációk egy szűk részhalmazát, melyek szekvenciális kombinációja egy stabil, átfogóan jó eredményt adó portfóliót biztosít. Továbbá ezt kibővítettük olyan utólagos feldolgozó lépésekkel, melyek segítenek a hamis riasztások (false negative) kiküszöbölésében. Az eredmények alapján a munkánk automatizált és könnyen alkalmazható, mégis hatékony megoldást nyújt formális szoftver verifikációra.

szerző

Ádám Zsófia
Mérnök informatikus szak, alapképzés
alapképzés (BA/BSc)

konzulens

Dr. Hajdu Ákos
Software engineer, Meta (külső)