Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

When executing a security sensitive application, a developer has to trust many systems, from hardware to software, to ensure the integrity and security of the application. The Trusted Computing Base (TCB) of these systems comprises of complex hardware and many millions lines of code, the security of which cannot be assessed. In order to solve this problem, Intel developed the Software Guard eXtensions (SGX). These extensions give the developer a possibility of running programs inside an isolated space within the processor memory, secure from even the highest software privilege levels, reducing the complexity to a hardware TCB@. However, Intel SGX leaves memory management to the untrusted operating system and explicitly does not include side channels in the threat model. This opens the way for side channels as a means of extracting enclave secrets by monitoring enclave execution. Previous work shows that exploitation of vulnerabilities within enclaves is a well researched topic, but the detection and availability of vulnerabilities is needed to execute these attacks. This work researches a way to automatically detect bugs in Intel SGX Enclaves by a means of fuzzing. Fuzzing is an automated means of finding vulnerabilities by randomising input until interesting behaviour is encountered. Fuzzing Intel SGX enclaves differs from the normal white-box fuzzing, but does not completely fall into the black-box fuzzing category. A bug oracle is developed by combining two available side channels: a page fault side channel and a page table entry bits side channel using access and dirty bits. Memory accesses inside an enclave are monitored with a 4KB granularity. By controlling the accessible pages to the enclave and keeping the working set small, detailed memory footprints are recorded and refined using the page table entry bits. These memory footprints can then be used to detect possible vulnerabilities. The types of detectable vulnerabilities and their influence on the memory footprint graphs are discussed. To enhance input generation by the fuzzer, the input space of enclaves is investigated and smart input for each input channel is discussed, resulting in better vulnerability detection rates. Comparing enclave runs with a chosen difference metric allows the user to find interesting enclave inputs and executions for further research. Finally, an evaluation of the fuzzer and bug oracle is performed on enclave examples. The oracle is able to detect side channels with ease. Ultimately, the bug oracle is tested on a real world enclave, in which the tool was able to find a previously found bug in the edger8r tool from the Intel SGX SDK, showing the real world value of this tool.

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

This thesis discusses the formal verification of applications built on top of FreeRTOS, a free, real-time operating system that has been specifically designed for microprocessors with limited hardware. The main focus of these verifications will be on providing strong guarantees with respect to correct resource management and the absence of data races, both important aspects for applications that handle many resources concurrently. This is often the case in an IoT setting for which FreeRTOS specifically forms a steady basis. These guarantees will be obtained using the VeriFast program verifier, a formal verification tool currently in development at the KU Leuven that is based on a descendant of Hoare logic called separation logic. The result of this thesis is twofold: first, a real world application that has been provided by SmartNodes, a company active in the smart lighting sector, will be verified for data race and deadlock freedom in the form of a case study. This will most importantly show the applicability of VeriFast as a formal verification tool for FreeRTOS based applications. Secondly, the specifications used to perform this verification will be extracted and generalized for use in other verifications of similar applications, contributing these generalizations to the field of formal verification. While all verifications were successful, some assumptions had to be made to keep the scope manageable. Additionally, difficulties were encountered due to the limitations of VeriFast in terms of low-level code support and special data type support. As a result, FreeRTOS services that were written on an assembly level could not be verified, and certain data types such as unions had to be replaced for the verification to succeed. Finally, a relevant paper by Chandrasekaran et al. is discussed that describes a FreeRTOS version with support for multi-core processors and deals with a comparable problem of proving data race and deadlock freedom for this extension, this time using a different formal verification tool named SPIN.

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Recent advancements in the automotive industry have extended vehicles with elaborate systems for entertainment and navigation, that are connected to wide-range networks like the internet. With the onboard embedded devices that enable those novelties therefore becoming remotely accessible, internal vehicle networks are exposed with them, and by extension all components they connect. Controller Area Networks (CAN) are in widespread use for governing communication within vehicle boundaries, and inherently offer little resistance against the security threats that come with remote, possibly malicious, parties gaining access to them. Considering the safety-critical application domain of CAN, remote attackers could however cause great harm when unrestricted in their actions. Several existing security mechanisms are effective in hardening CAN nodes, and embedded devices in general, against such increased malicious activity. For instance, cryptographic protocols have been put in place to establish the authenticity of CAN traffic. However, such communication-specific security measures come at the cost of bandwidth, computational resources, and real-time guarantees. Their repercussions on performance and timeliness go against the very nature of automotive applications, thus implying their own effects on vehicle safety. Taking those considerations into account, recent research proposes to implement CAN communication security measures using covert channels, which in essence are collateral transmission forms that do not increase network load, to enable strong security guarantees without harming safety as much as existing solutions. This master's thesis further explores that approach, in three main areas. First, an overview of covert, and covert-like, bandwidth sources applicable to CAN is constructed, which extends the set of covert channels considered in existing work. Second, a timing based covert channel is selected from that overview, and assessed in different practical implementations, each designed to yield stronger guarantees of performance and reliability than its precedent. Third, an extension to an existing security framework for CAN applications is proposed, which hardens its message authentication mechanism against packet loss through that same timing channel. The security implications of that approach are analysed, and found not to harm that framework's original security guarantees. This master's thesis investigates and assesses covert bandwidth opportunities in CAN, and migrates their use to the practical context of enhancing an existing security framework's approach to CAN message authentication.

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Het bouwen van veilige software is de dag van vandaag belangrijker dan ooit. Heel veel belangrijke toepassingen steunen op een correcte werking van software. Foutloze software afleveren is echter niet eenvoudig. Er kruipt zeer veel tijd in het schrijven van testen en manueel de geschreven code nakijken. Fuzzers kunnen een zeer interessante meerwaarde zijn bij het testen van het programma op softwarefouten. Dit zijn tools die op een geautomatiseerde manier op zoek gaan naar fouten in een programma. Dit doen ze door het programma op zoveel mogelijk verschillende manieren te doen lopen op basis van verschillende invoer. Twee verschillende types van zo’n tools komen aan bod. Enerzijds een mutatiege- baseerde fuzzer, AFL, en anderzijds een fuzzer die gebruik maakt van symbolische executie, KLEE. Beide zijn ze bedoeld om zoveel mogelijk fouten op te sporen, en zoveel mogelijk code te testen. Deze tools hebben hetzelfde doel, maar intern werken ze op een heel verschillende manier. Deze masterproef doet een vergelijkende studie naar de performantie en de bruikbaar- heid tussen deze twee verschillende manieren om aan fuzzing te doen. Deze studie gebruikt hiervoor een testomgeving, om objectief deze tools te kunnen vergelijken. Deze testomgeving bevat enkele van de meest voorkomende en gevaarlijkste fouten. Verder komen beide fuzzers aan bod in een casestudy op het archiveerprogramma 7-zip. Deze casestudy gaat dieper in op het gebruik van de fuzzers op een echte applicatie. Uit deze experimenten vloeien enkele resultaten die meer inzichten verschaffen in het gebruik van beide types van fuzzers. Deze inzichten omvatten eventuele aanpassingen aan de te testen software om de performantie van de fuzzers te verhogen.

Choose an application

• Reference Manager
• EndNote
• RefWorks (Direct export to RefWorks)

Smartphone devices are used more and more for tasks that rely on sensitive data, online banking, e-health and so on. While this is a natural evolution with respect to functionality, the security features of a smartphone are not as extensive as those of a personal computer. Many smartphone devices have an ARM System on Chip, equipped with ARM TrustZone by which the manufacturer attempts to increase the security of these devices. ARM TrustZone is a hardware security solution which provides a Trusted Execution Environment. With this capability, features like secure memory, trusted Input and Output, and process execution isolation are available. Smartphone manufacturers like Samsung utilize this ARM TrustZone framework to build up a security solution like Samsung KNOX. The downside of these solutions is that the manufacturer stays in control of the smartphone even after it has been sold. They decide which software is allowed to run on the device and which is not. To return the control and ownership to the users, the PinePhone has been introduced, an open smartphone with ARM TrustZone features. To access these Trusted Execution Environment functionalities a kernel is required. For this, there are also open source solutions like OP-TEE. The tools to obtain a secure open smartphone device exist, but they need to be put together along with security implementations to become a complete product. In this work, a crucial part of Remote Attestation has been looked at, namely measuring the integrity of applications running in the Normal World of the ARM TrustZone framework. Lots of research has been done to isolate applications in the Secure World from the rich Operating System. Also securing the data storage or the Input and Output channels related to these applications are common practice and well understood. Of course, the security of these applications is of utmost importance but this Secure World could also increase the security guarantees for the Normal World. One way of doing this is by allowing the Secure World to attest processes in the Normal World.