|
|
Static Analysis of C Programs
Malík, Viktor ; Zuleger, Florian (oponent) ; Strejček, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis proposes several original contributions to the area of static analysis of software with focus on low-level systems code written in C. The contributions are split into two parts, each related to a different area of static analysis, namely formal verification of (low-level) C code and static analysis of semantic equivalence of different versions of the same software. The first part proposes new analyses suitable for verification engines that perform automatic invariant inference using an SMT solver. The proposed solution includes two abstract template domains that use logical formulae over bit-vectors to encode the shape of the program heap and the contents of the program arrays. The shape domain is based on computing a points-to relation between pointers and symbolic addresses of abstract memory objects. The array domain is based on splitting the arrays into several non-overlapping contiguous segments and computing a different invariant for each of them. Both domains can be combined with value domains in a straightforward manner, which particularly allows our approach to reason about shapes and contents of heap and array structures at the same time. The information obtained from the analyses can be used to prove memory safety and reachability properties, expressed by user assertions, of programs manipulating data structures. All of the proposed solutions have been implemented in the 2LS framework and compared against state-of-the-art tools that perform the best in the relevant categories of the well-known Software Verification Competition (SV-COMP). Results show that 2LS outperforms these tools on benchmarks requiring combined reasoning about unbounded data structures and their numerical contents. The second part of the thesis is motivated by existence of software projects that undergo regular refactorings and modifications and yet need to ensure semantic stability of some of their core parts. This part proposes a highly-scalable approach for automatically checking semantic equivalence of different versions of large, real-world C projects, with a particular focus on the Linux kernel. The proposed method uses a novel combination of pattern matching with light-weight static analysis and control-flow transformations. The method checks preservation of the semantics of functions forming the API of the project being analyzed as well as of the semantics of its global variables, which typically hold various control parameters. For the latter, a specialised slicing procedure is proposed to slice out code influenced by these variables and concentrate the further analysis on that code only. Although the method cannot prove equivalence on heavily refactored code, it can compare thousands of functions in the order of minutes while producing a low number of false non-equality verdicts as our experiments show. The method has been implemented over the LLVM infrastructure in a tool called DiffKemp. Our results show that DiffKemp, unlike other existing tools, gives practically useful results even on projects of the size of the Linux kernel.
|
|
|
Acceleration of DTLS Protocol in Linux Kernel
Krenželok, František ; Lichtner, Ondrej (oponent) ; Grégr, Matěj (vedoucí práce)
This thesis offers a overview of the DTLS1.3 protocol, focusing on critical features pertinent to both userspace applications and kernel-level integration. Key outcomes include the implementation of DTLS1.3 within GnuTLS and the extension of this protocol to the Linux kernel's TLS module. Additionally, the thesis evaluates the utility of this kernel module in conjunction with emerging technologies such as eBPF and projects like ktls-util.
|
|
|
Applying formal methods to analysis of semantic differences between versions of software
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an integration of formal methods into DiffKemp, a static analysis tool for analyzing semantic differences of large-scale C projects. The aim of this extension is to facilitate analysis of more complex code changes, which would typically be better handled by a tool based on formal methods, while also maintaining DiffKemp’s scalability to large projects. To achieve this, whenever a possible semantic change is found, the equivalence of the relevant instructions is encoded into an SMT problem instance and the difference is either confirmed or refuted using an SMT solver. The proposed solution has been implemented in DiffKemp and our experiments on a set of benchmarks called EqBench show that it extends the capabilities of DiffKemp, mainly with regards to sound analysis of refactorings of arithmetic expressions.
|
|
|
Automated Testing of OS Linux Protocol Stack Behaviour During Congestion
Tomašov, Adrián ; Grégr, Matěj (oponent) ; Lichtner, Ondrej (vedoucí práce)
This thesis is focused on observing and simulating network congestion in laboratory conditions, and on automated testing of the protocol stack in the Linux operating system during network congestion. We perform a set of experiments to find the impact of network congestion on the protocol stack. The simulation and emulation method of this network using physical device will be described. The outcome of this thesis are various configurations of devices and emulators for network congestion together with measurements and evaluation of results. These configurations will be used for automated testing of the kernel of the Linux operating system to catch development errors, network protocol stack errors and card driver error earlier.
|
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktické části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Práce je završena testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
|
|
Metody útoků na operační systém Linux
Procházka, Boris ; Malinka, Kamil (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato bakalářská práce se zaměřuje na bezpečnost Linuxového jádra z útočníkova pohledu. Snaží se identifikovat a zmapovat veškeré charakteristické rysy a metody používané dnešními počítačovými piráty. Jedním z cílů této práce je poskytnout komplexní pohled na danou problematiku. Ve výsledku tak může sloužit jako malá referenční příručka komukoliv, kdo má zájem o rozšíření znalostí z oblasti jaderné bezpečnosti. Práce se skládá ze čtyř částí. První opakuje a definuje nejzákladnější pojmy a členění z oblasti operačních systémů. Druhá a třetí část tvoří jádro práce. Zahrnují principy a metody používané pro skrytí procesů, souborů, spojení apod. Poslední kapitola je věnována doprovodným tématům. Přílohou k této bakalářské práci je skupina jaderným modulů, které demonstrují diskutované problémy, a tabulky, porovnávající současné rootkity.
|
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktická části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Konec práce je završený testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
|
|
Port Block Allocation for Network Address Translation
Odehnal, Tomáš ; Podermański, Tomáš (oponent) ; Grégr, Matěj (vedoucí práce)
This term project aims to study the issue of the Carrier-Grade NAT (CGN) technique, which has to create log messages with address translation for every new connection. Because the CGN is stationed between large networks, it may daily record hundreds of thousands of connections. This amount of records have high memory requirements and even more difficult is to search for a specific log record. These problems solve the port block allocation for address translation. The output of this work is the creation of a rule in the iptables that performs this port block allocation for address translation. It consists of a user part that processes the rules and a kernel module that implements the functionality of the rule.
|
|
|
Realizace internetové brány na Linuxu s pokročilým filtrováním
Matocha, Tomáš ; Pust, Radim (oponent) ; Jelínek, Mojmír (vedoucí práce)
Práce Realizace internetové brány na Linuxu s pokročilým filtrováním se soustřeďuje na~instalaci operačního systému Linux na~starší počítače, který plní funkci jako brána pro připojení klientů ve~vnitřní síti do internetu. V práci je uveden popis vytvoření pokročilého filtrování s~pomocí iptables. Ukazuje některé typy bezpečnosti proti útokům z Internetu. V~dalších kapitolách jsou probrány pokročilé mechanismy řízení provozu (jako tc a qdisc). Tento systém front se ukazuje jako velice přínosný všude tam, kde je potřeba hierarchicky dělit provoz mezi uživatele. Jsou popsány typy front a~sestavena konfigurace pro klienty ve vnitřní síti. Dále je uvedeno použití dns serveru typu caching-only a také aplikace denyhosts, která zvyšuje celkovou bezpecnost systému. Mít vlastní DNS server se osvědčuje, zejména pokud chceme snížit datový provoz. Poslední kapitola se zabývá radius serverem a jeho implementací s použitím apache a databáze mysql. Popsány jsou možnosti některých konfiguračních voleb jednotlivých služeb a také uvedeny příklady konfigurací. Nakonec je předveden systém pro autentizaci uživatelů skrze RADIUS server. Celá práce se snaží poskytnout komplexní pohled na problematiku bezpečnosti a~filtrování.
|
|
|
Systém pro ověření minimálních potřebných zdrojů pro běh aplikace
Žák, Jiří ; Doležal, Jan (oponent) ; Smrž, Pavel (vedoucí práce)
Cílem této bakalářské práce je vytvořit systém pro ověření minimálních potřebných zdrojů pro běh aplikace. Teoretická část se věnuje tématu vyhodnocovacích metrik počítačového výkonu a principu fungování operačního systému Linux. V praktické části je popsáno, jak byl vytvořen návrh a implementace celého systému, který využívá technologii BPF (Berkeley Packet Filter). Práce je završena testováním a vyhodnocením celé práce. Systém byl úspěšně nasazen v partnerské firmě BringAuto. Ukázalo se, že daný operační systém je dostatečně výkonný pro běh aplikací.
|
host ::
RSS.