Automatická analýza programů v C
Jan Strejček, Vincent Mihalkovič a Lukáš Zaoral skupina Statica, laboratoř Formela
2. května 2022
Navrhujeme algoritmy a vyvíjíme nástroje pro automatickou analýzu programů v C.
co děláme
Navrhujeme algoritmy a vyvíjíme nástroje pro automatickou analýzu programů v C.
cílem analýz je
■ rozhodnout, zda v programu může nastat určitý typ chyby
■ nalézt běh, v kterém tato chyba nastává
■ automatické generování testů s vysokým pokrytím kódu
■ odhad délky běhu programu v závislosti na vstupech
2/8
co děláme
Navrhujeme algoritmy a vyvíjíme nástroje pro automatickou analýzu programů v C.
cílem analýz je
■ rozhodnout, zda v programu může nastat určitý typ chyby
■ nalézt běh, v kterém tato chyba nastává
■ automatické generování testů s vysokým pokrytím kódu
■ odhad délky běhu programu v závislosti na vstupech
zkoumané typy chyb
■ porušení assertu
■ přetečení celých čísel se znaménkem (signed integers)
■ chybná práce s pamětí
■ invalidní dereference (např. null dereference, use after free)
■ invalidní dealokace (např. double free)
■ memory leaking
■ nedefinované chování, nekonečné běhy programu, . ..
2/8
jak to děláme
typy použitých analýz
■ statické analýzy
■ analýza ukazatelů (pointer analysis)
■ analýza rozsahu proměnných (např. 1 < x < 36)
■ analýza vztahů mezi proměnnými (např. x < y + 5)
■ prořezávání programů (program slicing)
■ symbolické vykonání programu (symbolic execution)
■ dynamické analýzy a fuzzing
3/8
jak to děláme
typy použitých analýz
■ statické analýzy
■ analýza ukazatelů (pointer analysis)
■ analýza rozsahu proměnných (např. 1 < x < 36)
■ analýza vztahů mezi proměnnými (např. x < y + 5)
■ prořezávání programů (program slicing)
■ symbolické vykonání programu (symbolic execution)
■ dynamické analýzy a fuzzing
3/8
prořezávání programů (program slicing)
Které části programu neovlivňují platnost assertu?
z = z + 3; if (z > 0) {
x = z + 1;
z = 3 * x; } else {
y = z + 5;
x = x * x - z;
}
if (x > y)
z = x - 1; assert(x > 0);
4/8
prořezávání programů (program slicing)
Které části programu neovlivňují platnost assertu?
z = z + 3; if (z > 0) {
x = z + 1;
z = 3 * x; } else {
y = z + 5;
x = x * x - z;
}
assert(x > 0);
4/8
prořezávání programů (program slicing)
Které části programu neovlivňují platnost assertu?
z = z + 3; if (z > 0) {
x = z + 1;
z = 3 * x; } else {
x = x * x - z;
}
assert(x > 0);
4/8
prořezávání programů (program slicing)
Které části programu neovlivňují platnost assertu?
z = z + 3; if (z > 0) { x = z + 1;
} else {
x = x * x - z;
}
assert(x > 0);
4/8
prořezávání programů (program slicing)
Které části programu neovlivňují platnost assertu?
z = z + 3; if (z > 0) { x = z + 1;
} else {
x = x * x - z;
}
j '
assert(x > 0);
z = z + 3; if (z > 0)
x = z + 1 else
x = x * x - z assert(x > 0);
co vyvíjíme a v čem
Symbiotic
■ vyvíjený na Fl od roku 2012
■ kombinuje naše a externí nástroje a knihovny, např.
■ clang a LLVM framework
■ knihovna DG pro analýzu závislostí v programu
■ statický analyzátor paměti Predator
■ symbolický exekútor Klee
■ symbolický exekútor SlowBeast
■ naprogramováno v C++ a Pythonu
5/8
co vyvíjíme a v čem
Symbiotic
■ vyvíjený na Fl od roku 2012
■ kombinuje naše a externí nástroje a knihovny, např.
■ clang a LLVM framework
■ knihovna DG pro analýzu závislostí v programu
■ statický analyzátor paměti Predator
■ symbolický exekútor Klee
■ symbolický exekútor SlowBeast
■ naprogramováno v C++ a Pythonu
■ úspěchy v soutěžích Test-Comp a SV-COMP
■ 4 vítězství v kategorii věnované chybnám při práci s pamětí
■ 3 vítězství v kategorii věnované analýze reálných programů
■ celkové vítězství v SV-COMP 2022
■ celkem 15 medailí
5/8
SV-COMP 2022
zdroj: https://sv-comp.sosy-lab.org/2022/results/results-verified/
6/8
jak získat Symbiotic
aisa a nymfe(XY)
$ module add symbiotic-8.0.0
7/8
jak získat Symbiotic
aisa a nymfe(XY)
$ module add symbiotic-8.0.0
Fedora
# dnf install dnf-plugins-core // install copr support
# dnf copr enable -y Oaufover/symbiotic
# dnf install symbiotic
7/8
jak získat Symbiotic
aisa a nymfe(XY]
$ module add symbiotic-8.0.0
Fedora
# dnf install dnf-plugins-core // install copr support
# dnf copr enable -y @aufover/symbiotic
# dnf install symbiotic
ruční překlad
https: //github.com/staticafi/symbiotic
7/8
kdo jsme a jak se přidat
skupina Statica
■ součástí laboratoře Formela (C408)
■ skupina studentů pod vedením J. Strejčka a M. Trtíka
■ aktuálně 5 studentů
8/8
kdo jsme a jak se přidat
skupina Statica
■ součástí laboratoře Formela (C408)
■ skupina studentů pod vedením J. Strejčka a M. Trtíka
■ aktuálně 5 studentů
s námi získáš
■ možnost dělat velmi užitečný výzkum na mezinárodní úrovni
■ zajímavé téma pro bakalářku nebo diplomku
■ přístup do labu a do kuchyňky
■ možnost zapojit se do řešení grantů a získat stipendium
■ nové sociální vazby a zážitky (výlety, plavba lodí, ...)
8/8
kdo jsme a jak se přidat
skupina Statica
■ součástí laboratoře Formela (C408)
■ skupina studentů pod vedením J. Strejčka a M. Trtíka
■ aktuálně 5 studentů
s námi získáš
■ možnost dělat velmi užitečný výzkum na mezinárodní úrovni
■ zajímavé téma pro bakalářku nebo diplomku
■ přístup do labu a do kuchyňky
■ možnost zapojit se do řešení grantů a získat stipendium
■ nové sociální vazby a zážitky (výlety plavba lodí, ...)
... stačí napsat na strej cekOf i.muni.cz
8/8