Téma disertační práce

Přesná a dobře škálující statická analýza programů se složitými datovými a/nebo řídicími strukturami

Ak. rok 2021/2022

Školitel: Vojnar Tomáš, prof. Ing., Ph.D.

Ústav: Ústav inteligentních systémů FIT VUT v Brně

Obecným cílem výzkumu v rámci zadání je výrazně posunout vpřed současný stav poznání ve světě v oblasti statické analýzy programů, a to jak v oblasti principů, tak i nástrojů alespoň potenciálně využitelných v praxi.

Statická analýza postavená na formálních základech je moderním a rychle se rozvíjejícím přístupem k ověřování korektnosti počítačových systémů, resp. pro vyhledávání chyb v nich. Existuje a dále se rozvíjí mnoho přístupů k takové analýze či verifikaci: analýza toku dat, pokročilé typové analýzy, abstraktní interpretace, model checking apod. Značná pozornost je těmto přístupům věnována nejen v akademické oblasti, ale také řadou špičkových velkých průmyslových společností (např. Facebook, Google, Amazon, Apple, Microsoft, Oracle, Red Hat apod.) i neustále vznikajících specializovaných firem (např. Coverity, GrammaTech, AbsInt, DiffBlue apod.), často následně zakoupených velkými technologickými leadery. Přes tento zájem univerzit i průmyslových společností je však v oblasti statické analýzy stále zapotřebí vyřešit celou řadu teoretických i praktických problémů. Jedním z těchto problémů, na který by se měla práce zaměřit, je škálovatelnost, a to i pro hlubší analýzy, které se zaměřují na komplexní datové či řídicí struktury. Na oltář škálovatelnosti by ale neměla být obětována přesnost analýzy, jak se tomu v průmyslové praxi často děje -- jde tedy o nalezení vhodné rovnováhy mezi přesností (tj. procentem falešných hlášení) a efektivností.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT automatizovanou analýzou a verifikací, zejména pak doc. A. Rogalewiczem, dr. L. Holíkem, dr. O. Lengálem, dr. P. Peringerem, Ing. T. Fiedorem, Ing. M. Hruškou, Ing. V. Šokovou či Ing. V. Malíkem. Je zde rovněž možnost úzké spolupráce s různými zahraničními partnery VeriFIT: TU Vienna, Rakousko (dr. F. Zuleger), Uppsala University, Švédsko (prof. P.A. Abdulla, prof. B. Jonsson, doc. P. Rümmer); Verimag, Grenoble, Francie (doc. R. Iosif), IRIF, Paříž, Francie (prof. A. Bouajjani, doc. C. Enea, doc. P. Habermehl), LSV, ENS Paris-Saclay, Francie (prof. M. Sighireanu), Academia Sinica, Tchaj-wan (prof. Y.-F. Chen), TU Kaiserslautern, Německo (prof. A.W. Lin) či TU Braunschweig, Německo (prof. R. Meyer). Téma je zajímavé také z pohledu spolupráce s průmyslovými společnostmi, zejména pak DiffBlue z Velké Británie (dr. P. Schrammel), která vyvíjí mj. statický analyzátor 2LS, do jehož vývoje se již tým VeriFIT zapojil v několika oblastech. Dalšími možnými průmyslovými partnery jsou např. Red Hat, Honeywell či Facebook.

V oblasti statické analýzy programů dosáhla skupina VeriFIT mnoha originálních výsledků publikovaných na špičkových konferencích (např. v oblasti analýzy programů s dynamickými datovými strukturami, parametrickými datovými strukturami, neomezenými poli, řetězci či parametrickým počtem procesů). Řada z dosažených výsledků byla implementována v nástrojích (např. Predator, Forester či 2LS), které získaly řadu ocenění např. na mezinárodní soutěži ve verifikaci software SV-COMP. V nedávné době začali členové skupiny vyvíjet také analyzátory do generických prostředí, jako jsou Facebook Infer či Frama-C.

Konkrétní výzkum v rámci tématu zahrne práci na nových abstraktních doménách vhodných např. pro práci s dynamickými datovými strukturami (včetně např. tzv. překrývajících se datových struktur, které jsou v současné době pokryty analýzami jen velmi omezeně, přestože se běžně vyskytují např. v systémovém kódu), řetězci, poli a/nebo paralelismem (včetně pokročilých konstrukcí, jako jsou bezzámkové struktury či synchronizace typu RCU) a nových výpočetních smyček pro vlastní analýzu (např. abdukce či použití souhrnů funkcí počítaných od listů stromu volání) tak, aby byla zajištěna lepší škálovatelnost, než je tomu u současných přístupů. Cílem analýzy nemusí přitom být jen ověřování absence klasických chyb, ale také např. chyb ve výkonnosti programů.

V případě zodpovědného přístupu a kvalitních výsledků je zde možnost zapojení do grantových projektů (např. český projekt GAČR Snappy, evropské projekty H2020 ECSEL Arrowhead Tools a Valu3S či TAČR Aufover ve spolupráci s Honeywell a Red Hat), možnost vycestování na spolupracující zahraniční pracoviště a kontaktu se spolupracujícími průmyslovými společnostmi.

Nahoru