Bakalářské práce
Symbolická exekuce pro R
Autor
Petr Šťastný
Rok
2024
Typ
Bakalářská práce
Vedoucí
Pierre Donat-Bouillud, Ph.D.
Oponenti
Sebastián Krynski, MSc.
Katedra
Anotace
Symbolic execution je technika, která umožňuje testovat programy a dokazovat jejich netriviální vlastnosti.
Vytvoření nového systému pro symbolic execution je náročné. Místo toho je použita technika, kdy je symbolicky spouštěn samotný interpret cílového jazyka, díky čemuž je jednodušší symbolicky spustit i programy v daném jazyce.
V této práci aplikuji tuto techniku na jazyk R. Výsledný program je možné použít například na otestování korektnosti knihoven nebo na generování typových anotací.
Diplomové práce
Vnořené smyčky a path explosion problém v symbolické exekuci
Autor
Vojtěch Rozhoň
Rok
2024
Typ
Diplomová práce
Vedoucí
Pierre Donat-Bouillud, Ph.D.
Oponenti
prof. Christoph Kirsch
Katedra
Anotace
Práce vyhodnocuje techniky pro řešení problému exploze cest v symbolické exekuci. Obzvláštní důraz je kladen na interakce jednotlivých technik se vnořenými cykly. Metody ořezávání cest, subsumpce cest, slučování stavů a shrnování cyklů jsou diskutovány na příkladech. Symbolická exekuce je spolu s těmito metodami implementována pro analýzu programů napsaných v edukačním programovacím jazyce microc, který je inspirován jazykem C. Práce představuje experimenty, které porovnávaly jednotlivé metody, obzvláště aby zjistili jak dobře se tyto metody vypořádávají s mnoha cykly a se vnořenými cykly. Generátor náhodných programů v jazyce microc byl implementován pro experimentování s implementovanou symbolickou exekucí.
Interpretace a diferenciální fuzzing jazyka Vyper
Autor
Miroslav Škrabal
Rok
2025
Typ
Diplomová práce
Vedoucí
Pierre Donat-Bouillud, Ph.D.
Oponenti
Ing. Josef Gattermayer, Ph.D.
Katedra
Anotace
Vyper je programovací jazyk pro psaní smart kontraktů pro EVM blockchainy. Smart kontrakty mohou držet až miliardy dolarů, a proto je jejich bezpečnost nejvyšší prioritou. V minulosti Vyper kompilátor obsahoval bugy, které ovlivňovaly produkční kontrakty a nakonec vedly k rozsáhlému hackerskému útoku. Tato práce se zabývá tématem testování kompilátorů se zaměřením na testování Vyper kompilátoru. Implementuje AST interpret pro Vyper a používá jej k diferenciálnímu fuzzování překladače. Přístup je testován pomocí experimentů proveditelnosti, kdy jsou dvě staré chyby Vyperu s vysokou a střední závažností přeneseny do aktuální verze a fuzzer je zaměřen na jejich nalezení. Experimenty ukázaly, že fuzzer je dokáže rychle odhalit, a lze jej tedy použít ke zlepšení správnosti překladače.