Considerable research has been directed towards efficient test stimuli generation for Register Transfer Level (RTL) circuits. However, stimuli generation frameworks are still not capable of generating effective stimuli for all circuits. Some of the limiting factors are 1) It is hard to ascertain if a branch in the RTL code is reachable, and 2) Some hard-to-reach branches require intelligent algorithms to reach them. Since unreachable branches cannot be reached by any test sequence, we propose a method to deduce unreachability of a branch by looking for the possible values which a signal can take in an RTL code without explicit unrolling of the design. To the best of our knowledge, this method has been able to identify more unreachable branches than any method published in this domain, while being computationally less expensive. Moreover, some branches require very specific values on input signals in specific cycles to reach them. Conventional symbolic execution can generate those values but is computationally expensive. We propose a cycle-by-cycle restrictive symbolic execution that analyzes only a selected subset of program statements to reduce the computational cost. Our proposed method gathers information from an initial execution trace generated by any technique, to intelligently decide specific cycles where the application of this method will be helpful. This method can hybrid with simulation-based test stimuli generation methods to reduce the cost of formal verification. With this method, we were able to reach some previously unreached branches in ITC99 benchmark circuits. / Master of Science

Concurrent software has been widely utilizing in computer systems owing to the highly efficient computation. However, testing and verifying concurrent software remain challenging tasks. This matter is not only because of the non-deterministic thread interferences which are hard to reason about but also because of the large state space due to the simultaneous path and interleaving explosions. That is, the number of program paths in each thread may be exponential in the number of branch conditions, and also, the number of thread interleavings may be exponential in the number of concurrent operations. This dissertation presents a set of new methods, built upon symbolic execution, a program analysis technique that systematically explores program state space, for testing concurrent programs. By modeling both functional and non-functional properties of the programs as assertions, these new methods efficiently analyze the viable behaviors of the given concurrent programs. The first method is assertion guided symbolic execution, a state space reduction technique that identifies and eliminates redundant executions w.r.t the explored interleavings. The second method is incremental symbolic execution, which generates test inputs only for the influenced program behaviors by the small code changes between two program versions. The third method is SYMPLC, a technique with domain-specific reduction strategies for generating tests for the multitasking Programmable Logic Controller (PLC) programs written in languages specified by the IEC 61131-3 standard. The last method is adversarial symbolic execution, a technique for detecting concurrency related side-channel information leaks by analyzing the cache timing behaviors of a concurrent program in symbolic execution. This dissertation evaluates the proposed methods on a diverse set of both synthesized programs and real-world applications. The experimental results show that these techniques can significantly outperform state-of-the-art symbolic execution tools for concurrent software. / Doctor of Philosophy / Software testing is a technique that runs software as a black-box on computer hardware multiple times, with different inputs per run, to test if the software behavior conforms to the designed functionality by developers. Nowadays, programmers have been increasingly developing multithreaded and multitasking software, e.g., web browser and web server, to utilize the highly efficient multiprocessor hardware. This approach significantly improves the software performance since a large computing job can now decompose to a set of small jobs which can then distribute to concurrently running threads (tasks). However, testing multithreaded (multitask) software is extremely challenging. The most critical problem is the inherent non-determinism. Typically, executing sequential software with the same input data always results in the same output. However, running a multithreaded (multitask) software multiple times, even under the same input data, may yield different output in each run. The root reason is that concurrent threads (tasks) may interleave their running progress at any time; thus the internal software execution order may be altered unexpectedly, causing runtime errors. Meanwhile, finding such faults is difficult, since the number of all possible interleavings can be exponentially growing in the number of concurrent thread (task) operations. This dissertation proposes four methods to test multithreaded/multitask software efficiently. The first method summarizes the already-tested program behaviors to avoid future testing runs that cannot lead to new faults. The second method only tests program behaviors that are impacted by program changes. The third method tests multitask Programmable Logic Controller (PLC) programs by excluding infeasible testing runs w.r.t the PLC semantics. The last method tests non-functional program properties by systematic concurrency analysis. This dissertation evaluates these methods upon a diverse set of benchmarks. The experimental results show that the proposed methods significantly outperform state-of-the-art techniques for concurrent software analysis.

Differentielles Testen ist ein wichtiger Bestandteil der Qualitätssicherung von Software, mit dem Ziel Testeingaben zu generieren, die Unterschiede im Verhalten der Software deutlich machen. Solche Unterschiede können zwischen zwei Ausführungspfaden (1) in unterschiedlichen Programmversionen, aber auch (2) im selben Programm auftreten. In dem ersten Fall werden unterschiedliche Programmversionen mit der gleichen Eingabe untersucht, während bei dem zweiten Fall das gleiche Programm mit unterschiedlichen Eingaben analysiert wird. Die Regressionsanalyse, die Side-Channel Analyse, das Maximieren der Ausführungskosten eines Programms und die Robustheitsanalyse von Neuralen Netzwerken sind typische Beispiele für differentielle Softwareanalysen. Eine besondere Herausforderung liegt in der effizienten Analyse von mehreren Programmpfaden (auch über mehrere Programmvarianten hinweg). Die existierenden Ansätze sind dabei meist nicht (spezifisch) dafür konstruiert, unterschiedliches Verhalten präzise hervorzurufen oder sind auf einen Teil des Suchraums limitiert. Diese Arbeit führt das Konzept des hybriden differentiellen Software Testens (HyDiff) ein: eine hybride Analysetechnik für die Generierung von Eingaben zur Erkennung von semantischen Unterschieden in Software. HyDiff besteht aus zwei parallel laufenden Komponenten: (1) einem such-basierten Ansatz, der effizient Eingaben generiert und (2) einer systematischen Analyse, die auch komplexes Programmverhalten erreichen kann. Die such-basierte Komponente verwendet Fuzzing geleitet durch differentielle Heuristiken. Die systematische Analyse basiert auf Dynamic Symbolic Execution, das konkrete Eingaben bei der Analyse integrieren kann. HyDiff wird anhand mehrerer Experimente evaluiert, die in spezifischen Anwendungen im Bereich des differentiellen Testens ausgeführt werden. Die Resultate zeigen eine effektive Generierung von Testeingaben durch HyDiff, wobei es sich signifikant besser als die einzelnen Komponenten verhält. / Differential software testing is important for software quality assurance as it aims to automatically generate test inputs that reveal behavioral differences in software. The concrete analysis procedure depends on the targeted result: differential testing can reveal divergences between two execution paths (1) of different program versions or (2) within the same program. The first analysis type would execute different program versions with the same input, while the second type would execute the same program with different inputs. Therefore, detecting regression bugs in software evolution, analyzing side-channels in programs, maximizing the execution cost of a program over multiple executions, and evaluating the robustness of neural networks are instances of differential software analysis with the goal to generate diverging executions of program paths. The key challenge of differential software testing is to simultaneously reason about multiple program paths, often across program variants, in an efficient way. Existing work in differential testing is often not (specifically) directed to reveal a different behavior or is limited to a subset of the search space. This PhD thesis proposes the concept of Hybrid Differential Software Testing (HyDiff) as a hybrid analysis technique to generate difference revealing inputs. HyDiff consists of two components that operate in a parallel setup: (1) a search-based technique that inexpensively generates inputs and (2) a systematic exploration technique to also exercise deeper program behaviors. HyDiff’s search-based component uses differential fuzzing directed by differential heuristics. HyDiff’s systematic exploration component is based on differential dynamic symbolic execution that allows to incorporate concrete inputs in its analysis. HyDiff is evaluated experimentally with applications specific for differential testing. The results show that HyDiff is effective in all considered categories and outperforms its components in isolation.

Thesis (MSc)--Stellenbosch University, 2013. / ENGLISH ABSTRACT: Probabilistic symbolic execution is a new approach that extends the normal symbolic execution with probability calculations. This approach combines symbolic execution and model counting to estimate the number of input values that would satisfy a given path condition, and thus is able to calculate the execution probability of a path. The focus has been on programs that manipulate primitive types such as linear integer arithmetic in object-oriented programming languages such as Java. In this thesis, we extend probabilistic symbolic execution to handle data structures, thus allowing support for reference types. Two techniques are proposed to calculate the probability of an execution when the programs have structures as inputs: an approximate approach that assumes probabilities for certain choices stay fixed during the execution and an accurate technique based on counting valid structures. We evaluate these approaches on an example of a Binary Search Tree and compare it to the classic approach which only take symbolic values as input. / AFRIKAANSE OPSOMMING: Probabilistiese simboliese uitvoering is ’n nuwe benadering wat die normale simboliese uitvoering uitbrei deur waarksynlikheidsberekeninge by te voeg. Hierdie benadering kombineer simboliese uitvoering en modeltellings om die aantal invoerwaardes wat ’n gegewe padvoorwaarde sal bevredig, te beraam en is dus in staat om die uitvoeringswaarskynlikheid van ’n pad te bereken. Tot dus vêr was die fokus op programme wat primitiewe datatipes manipuleer, byvoorbeeld lineêre heelgetalrekenkunde in objek-geörienteerde tale soos Java. In hierdie tesis brei ons probabilistiese simboliese uitvoering uit om datastrukture, en dus verwysingstipes, te dek. Twee tegnieke word voorgestel om die uitvoeringswaarskynlikheid van ’n program met datastrukture as invoer te bereken. Eerstens is daar die benaderingstegniek wat aanneem dat waarskynlikhede vir sekere keuses onveranderd sal bly tydens die uitvoering van die program. Tweedens is daar die akkurate tegniek wat gebaseer is op die telling van geldige datastrukture. Ons evalueer hierdie benaderings op ’n voorbeeld van ’n binêre soekboom en vergelyk dit met die klassieke tegniek wat slegs simboliese waardes as invoer neem.

L’analyse de codes malveillants est un domaine de recherche en pleine expansion de par la criticité des infrastructures touchées et les coûts impliqués de plus en plus élevés. Ces logiciels utilisent fréquemment différentes techniques d’évasion visant à limiter la détection et ralentir les analyses. Parmi celles-ci, l’obfuscation permet de cacher le comportement réel d’un programme. Cette thèse étudie l’utilité de l’Exécution Symbolique Dynamique (DSE) pour la rétro-ingénierie. Tout d’abord, nous proposons deux variantes du DSE plus adaptées aux codes protégés. La première est une redéfinition générique de la phase de calcul de prédicat de chemin basée sur une manipulation flexible des concrétisations et symbolisations tandis que la deuxième se base sur un algorithme d’exécution symbolique arrière borné. Ensuite, nous proposons différentes combinaisons avec d’autres techniques d’analyse statique afin de tirer le meilleur profit de ces algorithmes. Enfin tous ces algorithmes ont été implémentés dans différents outils, Binsec/se, Pinsec et Idasec, puis testés sur différents codes malveillants et packers. Ils ont permis de détecter et contourner avec succès les obfuscations ciblées dans des cas d’utilisations réels tel que X-Tunnel du groupe APT28/Sednit. / Malware analysis is a growing research field due to the criticity and variety of assets targeted as well as the increasing implied costs. These softwares frequently use evasion tricks aiming at hindering detection and analysis techniques. Among these, obfuscation intent to hide the program behavior. This thesis studies the potential of Dynamic Symbolic Execution (DSE) for reverse-engineering. First, we propose two variants of DSE algorithms adapted and designed to fit on protected codes. The first is a flexible definition of the DSE path predicate computation based on concretization and symbolization. The second is based on the definition of a backward-bounded symbolic execution algorithm. Then, we show how to combine these techniques with static analysis in order to get the best of them. Finally, these algorithms have been implemented in different tools Binsec/se, Pinsec and Idasec interacting alltogether and tested on several malicious codes and commercial packers. Especially, they have been successfully used to circumvent and remove the obfuscation targeted in real-world malwares like X-Tunnel from the famous APT28/Sednit group.

The overall goal of this research is to reduce the cost of software development and improve the quality of software. Symbolic execution is a program-analysis technique that is used to address several problems that arise in developing high-quality software. Despite the fact that the symbolic execution technique is well understood, and performing symbolic execution on simple programs is straightforward, it is still not possible to apply the technique to the general class of large, real-world software. A symbolic-execution system can be effectively applied to large, real-world software if it has at least the two features: efficiency and automation. However, efficient and automatic symbolic execution of real-world programs is a lofty goal because of both theoretical and practical reasons. Theoretically, achieving this goal requires solving an intractable problem (i.e., solving constraints). Practically, achieving this goal requires overwhelming effort to implement a symbolic-execution system that can precisely and automatically symbolically execute real-world programs. This research makes three major contributions. 1. Three new techniques that address three important problems of symbolic execution. Compared to existing techniques, the new techniques * reduce the manual effort that may be required to symbolically execute those programs that either generate complex constraints or parts of which cannot be symbolically executed due to limitations of a symbolic-execution system. * improve the usefulness of symbolic execution (e.g., expose more bugs in a program) by enabling discovery of more feasible paths within a given time budget. 2. A novel approach that uses symbolic execution to generate test inputs for Apps that run on modern mobile devices such as smartphones and tablets. 3. Implementations of the above techniques and empirical results obtained from applying those techniques to real-world programs that demonstrate their effectiveness.

Šiame dokumente aprašytas darbas susideda iš trijų pagrindinių dalių. Pirmojoje (analizės) dalyje yra apžvelgiamos programinės įrangos kokybės užtikrinimo veiklos – konkrečiai testavimo procesas. Didžiausias dėmesys yra skiriamas automatizuotam testų generavimui. Antrojoje (projektinėje) dalyje aprašomas simboliniu vykdymu grindžiamas mutacinis testų generavimo metodas. Taip pat detalizuojamas jo realizavimas kuriamoje sistemoje – aprašomi statiniai ir dinaminiai vaizdai. Trečiojoje dalyje (tyrimo ir eksperimentinėje) yra analizuojamas sukurtas metodas, vertinamos įvairiausios jo charakteristikos, metrikos ir realizuojami patobulinimai. Šie sistemos priežiūros darbai leido sumažinti ciklomatinį metodų sudėtingumą ir pagreitinti realizuoto testų generavimo metodo veikimą. Aprašytas metodas pasižymi tuo, jog jo pagalba galima sugeneruoti testus aptinkančius programinio kodo mutacijas, o testų generavimui yra naudojamas simbolinis vykdymas, o ne atsitiktinių skaičių generatorius. / This work consists of three major parts. The first (analytical) part is the review of software quality assurance activities - specifically the testing process. The main focus is on automated test generation. The second (design) part describes the mutation testing based on symbolic execution test generation method. It also specifies the implementation details of the systems under development - described in the static and dynamic perspectives. The third part (research and experimental) is devoted for analysis of developed method. Here wide range of characteristics and metrics are analyzed. Also, some improvements are implemented. This helped to reduce system’s methods cyclomatic complexity and greatly increased speeds at witch tests generation are performed. The method described is characterized by the fact that it can help generate tests that detect mutations in the software code and symbolic execution is used for test generation, rather than a random number generator.

<div>Fuzzing is a simple yet effect approach to discover bugs by repeatedly testing the target system using randomly generated inputs. In this thesis, we identify several limitations in state-of-the-art fuzzing techniques: (1) the coverage wall issue , fuzzer-generated inputs cannot bypass complex sanity checks in the target programs and are unable to cover code paths protected by such checks; (2) inability to adapt to interfaces to inject fuzzer-generated inputs, one important example of such interface is the software/hardware interface between drivers and their devices; (3) dependency on code coverage feedback, this dependency makes it hard to apply fuzzing to targets where code coverage collection is challenging (due to proprietary components or special software design).</div><div><br></div><div><div>To address the coverage wall issue, we propose T-Fuzz, a novel approach to overcome the issue from a different angle: by removing sanity checks in the target program. T-Fuzz leverages a coverage-guided fuzzer to generate inputs. Whenever the coverage wall is reached, a light-weight, dynamic tracing based technique detects the input checks that the fuzzer-generated inputs fail. These checks are then removed from the target program. Fuzzing then continues on the transformed program, allowing the code protected by the removed checks to be triggered and potential bugs discovered. Fuzzing transformed programs to find bugs poses two challenges: (1) removal of checks leads to over-approximation and false positives, and (2) even for true bugs, the crashing input on the transformed program may not trigger the bug in the original program. As an auxiliary post-processing step, T-Fuzz leverages a symbolic execution-based approach to filter out false positives and reproduce true bugs in the original program.</div></div><div><br></div><div><div>By transforming the program as well as mutating the input, T-Fuzz covers more code and finds more true bugs than any existing technique. We have evaluated T-Fuzz on the DARPA Cyber Grand Challenge dataset, LAVA-M dataset and 4 real-world programs (pngfix, tiffinfo, magick and pdftohtml). For the CGC dataset, T-Fuzz finds bugs in 166 binaries, Driller in 121, and AFL in 105. In addition, we found 4 new bugs in previously-fuzzed programs and libraries.</div></div><div><br></div><div><div>To address the inability to adapt to inferfaces, we propose USBFuzz. We target the USB interface, fuzzing the software/hardware barrier. USBFuzz uses device emulation</div><div>to inject fuzzer-generated input to drivers under test, and applies coverage-guided fuzzing to device drivers if code coverage collection is supported from the kernel. In its core, USBFuzz emulates an special USB device that provides data to the device driver (when it performs IO operations). This allows us to fuzz the input space of drivers from the device’s perspective, an angle that is difficult to achieve with real hardware. USBFuzz discovered 53 bugs in Linux (out of which 37 are new, and 36 are memory bugs of high security impact, potentially allowing arbitrary read or write in the kernel address space), one bug in FreeBSD, four bugs (resulting in Blue Screens of Death) in Windows and three bugs (two causing an unplanned restart, one freezing the system) in MacOS.</div></div><div><br></div><div><div>To break the dependency on code coverage feedback, we propose WebGLFuzzer. To fuzz the WebGL interface (a set of JavaScript APIs in browsers allowing high performance graphics rendering taking advantage of GPU acceleration on the device), where code coverage collection is challenging, we introduce WebGLFuzzer, which internally uses a log guided fuzzing technique. WebGLFuzzer is not dependent on code coverage feedback, but instead, makes use of the log messages emitted by browsers to guide its input mutation. Compared with coverage guided fuzzing, our log guided fuzzing technique is able to perform more meaningful mutation under the guidance of the log message. To this end, WebGLFuzzer uses static analysis to identify which argument to mutate or which API call to insert to the current program to fix the internal WebGL program state given a log message emitted by the browser. WebGLFuzzer is under evaluation and so far, it has found 6 bugs, one of which is able to freeze the X-Server.</div></div>

Le test boîte blanche basé sur les chemins est largement utilisé pour la validation de programmes. A partir du graphe de flot de contrôle (CFG) du programme sous test, les cas de test sont générés en sélectionnant des chemins d'intérêt, puis en essayant de fournir, pour chaque chemin, des valeurs d'entrées concrètes qui déclencheront l'exécution du programme le long de ce chemin.Il existe de nombreuses manières de définir les chemins d'intérêt: les méthodes de test structurel sélectionnent des chemins remplissant un critère de couverture concernant les éléments du graphe; dans l'approche aléatoire, les chemins sont tirés selon une distribution de probabilité sur ces éléments. Ces méthodes aléatoires ont l'avantage de fournir un moyen d'évaluer la qualité d'un jeu de test à travers la probabilité minimale de couvrir un élément du critère.Fournir des valeurs concrètes d'entrées nécessite de construire le prédicat de cheminement chaque chemin, i.e. la conjonction des contraintes sur les entrées devant être vérifiée pour que le système s'exécute le long de ce chemin. Cette construction se fait par exécution symbolique. Les données de test sont ensuite déterminées par résolution de contraintes. Si le prédicat d'un chemin est insatisfiable, le chemin est dit infaisable. Il est très courant qu'un programme présente de tels chemins, leur nombre surpassent généralement de loin celui des faisables. Les chemins infaisables sélectionnés lors la première étape ne contribuent pas au jeu de test final, et doivent être tirés à nouveau. La présence de ces chemins pose un sérieux problème aux méthodes structurelles et à toutes les méthodes d'analyse statique, la qualité des approximations qu'elles fournissent étant réduite par les données calculées le long de chemins infaisables.De nombreuses méthodes ont été proposées pour résoudre ce problème, telles que le test concolique ou le test aléatoire basé sur les domaines d'entrée. Nous présentons un algorithme qui construit de meilleures approximations du comportement d'un programme que son CFG, produisant un nouveau CFG qui sur-approxime l'ensemble des chemins faisables mais présentant moins de chemins infaisables. C'est dans ce nouveau graphe que sont tirés les chemins.Nous avons modélisé notre approche et prouvé formellement, à l'aide de l'assistant de preuve interactif Isabelle/HOL, les propriétés principales établissant sa correction.Notre algorithme se base sur l'exécution symbolique et la résolution de contraintes, permettant de détecter si certains chemins sont infaisables ou non. Nos programmes peuvent contenir des boucles, et leurs graphes des cycles. Afin d'éviter de suivre infiniment les chemins cycliques, nous étendons l'exécution symbolique avec la détection de subsomptions. Une subsomption peut être vue comme le fait qu'un certain point atteint durant l'analyse est un cas particulier d'un autre atteint précédemment: il n'est pas nécessaire d'explorer les successeurs d'un point subsumé, ils sont subsumés par les successeurs du subsumeur. Notre algorithme a été implémenté par un prototype, dont la conception suit fidèlement la formalisation, offrant un haut niveau de confiance dans sa correction.Dans cette thèse, nous présentons les concepts théoriques sur lesquels notre approche se base, sa formalisation à l'aide d'Isabelle/HOL, les algorithmes implémentés par notre prototype et les diverses expériences menées et résultats obtenus à l'aide de ce prototype. / White-box, path-based, testing is largely used for the validation of programs. Given the control-flow graph (CFG) of the program under test, a test suit is generated by selecting a collection of paths of interest, then trying to provide, for each path, some concrete input values that will make the program follow that path during a run.For the first step, there are various ways to define paths of interest: structural testing methods select some set of paths that fulfills coverage criteria related to elements of the graph; in random-based techniques, paths are selected according to a given distribution of probability over these elements (for instance, uniform probability over all paths of length less than a given bound). Both approaches can be combined as in structural statistical testing. The random-based methods above have the advantage of providing a way to assess the quality of a test set as the minimal probability of covering an element of a criterion.The second step requires to produce for each path its path predicate, i.e. the conjunction of the constraints over the input parameters that must hold for the system to run along that path. This is done using symbolic execution. Then, constraint-solving is used to compute test data. If there is no input values such that the path predicate evaluates to true, the path is infeasible. It is very common for a program to have infeasible paths and such paths can largely outnumber feasible paths. Infeasible paths selected during the first step will not contribute to the final test suite, and there is no better choice than to select another path, hoping for its feasibility. Handling infeasible paths is the serious limitation of structural methods since most of the time is spent selecting useless paths. It is also a major challenge for all techniques in static analysis of programs, since the quality of the approximations they provide is lowered by data computed for paths that do not correspond to actual program runs.To overcome this problem, different methods have been proposed, like concolic testing or random testing based on the input domain. In path-biased random testing, paths are drawn according to a given distribution and their feasibility is checked in a second step. We present an algorithm that builds better approximations of the behavior of a program than its CFG, providing a transformed CFG, which still over-approximates the set of feasible paths but with fewer infeasible paths. This transformed graph is used for drawing paths at random.We modeled our graph transformations and formally proved, using the interactive theorem proving environment Isabelle/HOL, the key properties that establish the correctness of our approach.Our algorithm uses symbolic execution and constraint solving, which allows to detect whether some paths are infeasible. Since programs can contain loops, their graphs can contain cycles. In order to avoid to follow infinitely a cyclic path, we enrich symbolic execution with the detection of subsumptions. A subsumption can be interpreted as the fact that some node met during the analysis is a particular case of another node met previously: there is no need to explore the successors of the subsumed node: they are subsumed by the successors of the subsumer. Our algorithm has been implemented by a prototype, whose design closely follows said formalization, giving a good level of confidence in its correctness.In this thesis, we introduce the theoretical concepts on which our approach relies, its formalization in Isabelle/HOL, the algorithms our prototype implements and the various experiments done and results obtained using it.

As the number of Internet of Things devices is increasing rapidly, it is of utmost significance that the implementations of protocols for constrained devices are bug-free. In general implementations of network protocols are error-prone due to their complex nature and ambiguities in the protocol specification. Implementations of network protocols often contain critical errors which could be exploited. To avoid bugs and vulnerabilities, the implementation of network protocols has to adhere to their specifications. The objective of this thesis is to use symbolic execution to test one implementation of the Ephemeral Diffie-Hellman Over COSE (EDHOC) protocol and one implementation of the Constrained Application Protocol (CoAP) against their specifications. The goal is to identify bugs such as crashes, non-conformances, memory errors, and security vulnerabilities that may occur if the implementations are not adhering to their specifications. The methodology to do this consists of three steps: 1) extracting requirements from the protocols Request For Comments and expressing them as formulas, 2) preparing the system under test for symbolic execution and applying the formulas during symbolic execution to detect any paths that violate a requirement, 3) for every path which violates a requirement, the concrete value that the symbolic execution engine provided is used in the unmodified implementation to validate the bug. In total seven non-conformances were found which have been reported to developers. One non-conformance was found in the EDHOC implementation and six were found in the CoAP implementation. / Eftersom antalet Internet of Things enheter ökar snabbt är det av yttersta vikt att imple-menteringarna av nätverksprotokoll för Internet of Things enheter är korrekta. Generellt sett är implementeringar av nätverksprotokoll felbenägna på grund av deras komplexa natur och oklarheter i protokollspecifikationen. Implementeringar av nätverksprotokoll innehåller ofta kritiska buggar som kan utnyttjas. För att undvika buggar och sårbarheter måste implementeringar av nätverksprotokoll följa sina specifikationer. Målet med detta examensarbete är att använda symbolisk exekvering för att testa en implementation av protokollet Ephemeral Diffie-Hellman Over COSE ( EDHOC ) och en implementation av protokollet Constrained Application Protocol (CoAP) mot deras specifikationer. Syftet är att identifiera buggar såsom krascher, icke-konformiteter, minnesfel och säker-hetssårbarheter som kan uppstå om implementeringarna inte följer sina specifikationer. Metodiken för att uppnå detta består av tre steg: 1) extrahera krav från protokollensspecifikationer och uttrycka dem som formler, 2) förbereda systemet som ska testas försymbolisk exekvering och tillämpa formlerna under symbolisk exekvering för att upp-täcka eventuella vägar som bryter mot ett krav, 3) för varje väg som bryter mot ett krav används det konkreta värde som den symboliska exekveringsmotorn tillhandahåller i den oförändrade implementationen för att validera buggen. Totalt sett hittades sju icke-konformiteter. En icke-konformitet hittades i EDHOC implementeringen och sex hittades i CoAP implementeringen.