Programanalízis szimbolikus végrehajtás alkalmazásával

OData támogatás
Konzulens:
Izsó Tamás
Hálózati Rendszerek és Szolgáltatások Tanszék

A program analízis módszereit már évtizedek óta használják a szoftverfejlesztés különböző fázisaiban. A jelentős példák közé tartoznak az optimalizáló fordítók és a szoftver validációs eszközök. Bár a szimbolikus végrehajtás először egy 1976-os publikációban bukkant fel, csak nemrég, az SMT solverek fejlődése, a számítási kapacitás növekedése és a bináris analízis keretrendszerek megjelenése tette a gyakorlatban is pratktikussá nemtriviális programokon.

A szimbolikus végrehajtás jelentős alkalmazási területévé vált a szoftverek biztonsági tesztelése és a lefordított programok visszafejtésének segítése. Több ilyen célú rendszer is megjelent, az egyik legismertebb a Microsoft SAGE white-box fuzzere, amelynek alkalmazásával jelentős számú biztonsági hibát találtak a Windows 7 operációs rendszerben.

A dolgozatban a szimbolikus végrehajtás alkalmazhatóságát próbálom felmérni a szoftverek biztonsági tesztelésében és a binárisok visszafejtésében. Ennek érdekében módosítok egy létező white-box fuzzing rendszert, alkalmassá téve a hálózati forgalom alapú tesztelésre, bemutatom a rendszer architektúráját, értékelem a kapott eredményeket, illetve a lehetséges fejlesztési irányokat.

Letölthető fájlok

A témához tartozó fájlokat csak bejelentkezett felhasználók tölthetik le.