|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
|
|
|
Static Behavioral Malware Detection over LLVM IR
Surovič, Marek ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this thesis we study methods for behavioral malware detection, which use techniques of formal verification. In particular we build on the works, which use inference of tree automata from syscall dependency graphs, obtained by static analysis of LLVM IR. We design and implement a prototype detector using the LLVM compiler framework. For experiments with the detector we use an obfuscating compiler capable of generating mutations of malware from C/C++ source code. We discuss preliminary experiments which show the capabilities of the detector and possible future extensions to the detector.
|
|
|
Předpověď nových chyb pomocí dolování dat v historii výsledků testů
Matys, Filip ; Vojnar, Tomáš (oponent) ; Šimková, Hana (vedoucí práce)
Softwarové projekty prochází jak obdobím údržby, tak v případě open source i náročným neřízeným vývojem. Obě tyto fáze jsou náchylné k regresím, tedy chybám vedoucím k degradaci již fungujících částí systému. Z tohoto důvodu je systém podrobován testováním v podobě testovacích sad, což je v mnoha případech časově velmi náročné. Z tohoto důvodu vznikají prediktory, které jsou schopny na základě změn kódu a historie testování odhadnout, kdy k takovým regresím může dojít, pomocí čehož pak lze testování soustředit na tato místa. Tyto prediktory jsou však často postaveny na metrikách kódu, které jsou čistě statické a neřeší sémantiku daného jazyka. Účelem této diplomové práce je vytvořit prediktor, který nebude spoléhat jen na tyto metriky, ale bude schopen analyzovat kód i ze sémantického pohledu.
|
|
|
Řídicí systém pro testování linuxových aplikací
Beneš, Eduard ; Vojnar, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Táto práca sa zaoberá problematikou riadiaceho systému pre testovanie linuxových aplikácií. Práca poukazuje na dôležitosť testovania software a jeho kvality pomocou automatizovaných softwarových nástrojov. Red Hat Test System (RHTS) je jedným z mnohých testovacích nástrojov. Predstavené sú rozdielne prístupy k ich klasifikácii a vyhodnocovaniu. Vybrané nástroje sú vyhodnotené a porovnané so systémom RHTS. V tejto práci je navrhnutý systém pre neinteraktívne testovanie linuxových aplikácií s podporou pre RHTS testy a s dôrazom na budúce rozšírenia. Implementovaný systém je následne otestovaný pomocou navrhnutých testov a popísaných je niekoľko príkladov použitia.
|
|
|
Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Kovalič, Peter ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se věnuje verifikaci ovládačů. Používají se při tom model checkery, hlavní z nich je Static Driver Verifier. Pomocí něj se kontroluje zvolený ovládač Ext2Fsd. Patří do skupiny ovládačů souborových systémů. Kontrola probíhá podle zadaných pravidel, které nesmí ovládač porušovat. Cílem práce bylo vybraný ovládač verifikovat pomocí zvoleného nástroje. Ve výsledcích bylo dosaženo stavu, kdy se ve verifikovaném ovládači objevili všechny tři dostupné možnosti výsledku ovládač splňoval některá pravidla, některá odhalily jeho chyby a jiné nebyly aplikovatelné. Na konci této práce se nachází ještě kapitola, věnována dalšímu model checkeru, s názvem Copper, která poskytuje základní poznatky o tomto nástroji.
|
|
|
Automated Verification in HW/SW Co-design
Charvát, Lukáš ; Kubátová, Hana (oponent) ; Řehák, Vojtěch (oponent) ; Vojnar, Tomáš (vedoucí práce)
The subject of the thesis is to design new hardware verification techniques optimized for a process of HW/SW co-design in which hardware and software are developed in parallel to speed up the development of new embedded systems. Currently, microprocessor co-design tools typically allow to verify designs by simulation and/or functional verification. However, even extensive functional verification can miss some non-trivial bugs. Therefore, formal verification has become more and more desirable in recent years. As opposed to testing and bug-hunting techniques that only aim at detecting flaws, the goal of formal verification is to rigorously prove that the system is indeed correct. Formal verification is, however, a very demanding task, and even though a lot of progress has been achieved in this area, formal verification is far from being able to fully automatically check all relevant properties of complex designs without a significant and costly human involvement in the verification process. The thesis deals with these challenges by focusing on verification techniques based on formal approaches, but possibly relaxing or limiting their precision and generality to achieve full automation. Further, the thesis also focuses on the efficiency of the proposed techniques and their ability to deliver continuous feedback about the verification process. Special attention is devoted to the development of formal methods for checking the equivalence of microprocessor designs on various levels of abstraction. Although these designs cannot be behaviorally equivalent, they are required to give mutually corresponding results when executing the same input program, which is a property difficult to achieve. As another considered topic, the thesis proposes methods for checking correctness of mechanisms preventing data and control hazards in single-pipelined implementations of microprocessors. The approaches described in this thesis has been implemented in the form of several tools which, after examining designs of multiple pipelined microprocessors, were able to deliver promising experimental results.
|
|
|
Testing of generated C compilers for processors in embedded systems
Dolíhal, Luděk ; Kubátová, Hana (oponent) ; Vojnar, Tomáš (oponent) ; Hruška, Tomáš (vedoucí práce)
The embedded systems have become essential for our everyday lives. They are usually highly specialized and optimized single purpose devices. The cores of this devices are usually composed of one or more application specific instruction-set processors. This dissertation thesis is focused on testing of tools for design of application specific instruction set processors (ASIP) and ASIPs itself. The aim is to create a system, that allows testing of the tools such as compiler, assembler, disassembler or debugger. Nevertheless, there is also need for more complex tests, for example integration tests, that ensure there is no incompatibility between the tools. Author created with support of continuous integration server an environment, that helps to reveal and fix errors during the design of the application specific processors and moreover this environment is automatized up to certain point.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
|
|
|
Správa paměti v Linuxu
Tuček, Jaroslav ; Kočí, Radek (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce popisuje správu paměti v jádře linuxu. První část je věnována stručnému shrnutí architektury operačních systémů a teorii správy paměti - jmenovitě virtuální paměti, stránkovacím tabulkám, algoritmům stránkování a jádrovým alokátorům. Druhá část se soustřeďuje na vlastní implementaci zmíněných principů ve skutečném operačním systému, linuxu. Součástí je též sada testů navržených pro zjištění chování paměťového správce a krátké zmínění současně existujících omezení včetně jejich navrhovaných řešení.
|
|
|
Použití statické analýzy pro detekci chyb v obsluze signálů
Kozovský, Daniel ; Vojnar, Tomáš (oponent) ; Peringer, Petr (vedoucí práce)
Táto práca sa zaoberá zásuvným modulom csigsafe pre prekladač GCC. Používa statickú analýzu programov na odhalenie chýb v obsluhe signálov podla normy POSIX. Tento nástroj analyzuje zdrojové súbory v jazyku C a C++. Tento analyzátor je vytvorený pre firmu Red Hat, ktorá ho používa na testovanie sRPM balíkov určených do ich Linuxových distribúcii. Nástroj bol testovaný na vzorku 37 projektoch s volne šíriteľnými zdrojmi. Z testovania sa ukázala užitočnosť nástroja pri vyhľadávaní chýb spojených s porušením pravidiel na správnu obsluhu signálov.
|
host ::
RSS.