Cyberattacks happen constantly. One tool of attackers to maintain covert persistence on systems are rootkits, tools that can hide the adversaries files and processes from the legitimate administrators. Rootkits that sit in the kernel are hard to detect, because there is no higher authority on the system. A number of methods have been proposed to detect rootkits, but the topic is under constant evolution as new rootkitting methods are developed and better detection approaches are proposed. In this thesis we look at the existing methods of rootkit detection and discuss behaviour-based anomaly detection in more detail. First we look at what types of rootkits exist and compare several of them, where we find similarities in kernel rootkits on how they manipulate the kernel. Then we argue why there are only few points in the kernel where a rootkit could intervene to achieve rootkit functionality. Next, we dissect the getdents system call, which is the target of most kernel rootkits, as it is the one and only interface through which the kernel lists files and processes to userspace. The main idea of the work conducted in this thesis is to develop an algorithm that catches the rootkits actions by measuring the runtime of certain pieces of kernel code. We demonstrate the time measurement with a proof-of-concept implementation using eBPF [5] technology and the BCC toolchain [87]. Furthermore, to evaluate this on recent (6.5+) kernels, we implement our own rootkit since there are no rootkits publicly available that work on recent kernels. Our experiments show that when measured at the correct place, a rootkit creates evident time-delay artefacts, that could facilitate automatic rootkit detection.
reposiTUm entry (with fulltext)

Falcon has been selected for standardization by NIST as a post-quantum digital signature scheme. Although there have been several published attacks against Falcon that target vulnerabilities on the implementation side, the physical security of the scheme has not been thoroughly studied yet. We present a broad analysis of the physical security of the Falcon signature scheme that includes attacks from prior publications as well as novel vulnerabilities and takes into account the mathematical foundations of the scheme, such as the Fast Fourier Transform, discrete Gaussian distributions and a tower of fields. Additionally, we closely investigate one of the new attack vectors, NarrowSampling. We simulate a fault injection attack based on a parallelepiped learning technique applied to a signature distribution with lowered standard deviation. Each individual phase of the attack is analyzed and the influence of the most important attack parameters is measured and evaluated. For Falcon parameter sets with reduced security we are able to fully recover the secret key.
reposiTUm entry (with fulltext)

Browsers are implemented based on specifications written by disjoint groups of people. Specifications for different components of the browser can end up being contradictory in a way that introduces security bugs because of the complexity of the software. One way to reduce the likelihood of such specification bugs is to build a formal model of the browser that can be mechanically checked for clashes instead of relying on people to examine informal written descriptions for potential problems. We propose a new browser specification model that uses refinement types to check that all provided API functions maintain our defined security invariant. The model is a transition system in which the state is the browser internals and trace of events and the state transitions are the API functions. If all API functions are safe, then any script which only interacts with the browser using those functions cannot violate the invariant. Theinvariant is a conjunction of existing component security invariants from the literature, which we refer to as subinvariants. This approach allows us to prove that scripts are safe without modeling the contents ofthe scripts themselves. We are also able to model unbound traces without the exponential blow up of more traditional state space exploration approach. In addition, we were able to prioritize extensibility by using Coq’s module system and minimizing proof rewrites as new components are introduced. As presented in our main findings, we were able to mostly automate proof search using the Hammer library for a given component’s functions with regards to proofs of other components’ subinvariants.
reposiTUm entry (with fulltext)

The number of blockchain applications has grown immensely over the last decade, creating many new research areas dedicated to advancing and analyzing this technology. One of the most well-known implementations is the Bitcoin network, which established a decentralized payment facility, based on a publicly accessible blockchain ledger. Despite its promising features, the growth in its popularity has also led to uncovering many issues and limitations of the original design. One specific problem Bitcoin encounters as it seeks to establish itself in the Decentralized Finance sector is its ability to scale as the transaction throughput grows. Off-chain solutions, such as the Lightning Network, aim to shift the load away from the blockchain (hence off-chain) and create direct Payment Channels between principals. In this way, the parties can publish on-chain only the transaction that establishes a new channel and the one that closes the communication, while all the intermediate exchanges are handled off-chain. Through a consensus protocol, participants exchange valid on-chain transactions to update their common financial state at their discretion. Once completed, the final result is recorded on the blockchain. Such implementations often rely on timeout periods, which are enforced through the Bitcoin network and its scripting language, and the disclosure of secret data to either revoke outdated states or as proof for successful payments. As the complexity of such protocols increases, relying solely on manual reasoning for their correctness is insufficient, as it can be extremely time-consuming and error-prone. Hence, within this work, we provide the basis for a semi-automated off-chain protocol verification in Bitcoin using the proof-oriented programming language F*. We extend the symbolic verification framework DY* with a blockchain model supporting reasoning over time and introduce important modifications in the type system, allowing us to annotate secret values that will be intentionally disclosed without violating existing secrecy guarantees. To verify the correctness of the blockchain system, a set of lemmas expressing properties of a valid blockchain are proven correct. Additionally, two simple protocol implementations are provided to introduce the usage of newly added functionalities.
reposiTUm entry (with fulltext)

Bots are increasingly relevant agents on the Ethereum blockchain that enable high degrees of automation and efficiency. On the other hand, they can pose adversarial danger to users and protocols. Therefore, it is crucial to detect bots and investigate their behavior in order to inform policy and human users of the associated risks. To better understand the bot landscape on Ethereum, we propose a categorization of bots integrating existing research with findings of new bot classes documented by code or on-chain data. This categorization consists of 7 main categories and 26 subcategories of bots. Existing bot detection systems are predominantly based on predefined rules and highly specific to certain types of bots, making them inflexible and unable to detect unanticipated changes in bot behavior. In order to explore a more data-driven approach, we investigate to what extent bots on Ethereum can be detected using supervised and unsupervised machine learning. As a benchmark, we use rule-based heuristic methods to distinguish bots from humans. Our findings suggest that bots can be successfully distinguished using supervised learning and unsupervised methods can find clusters exhibiting a high purity of bots. Supervised methods using only a small dataset showed better results than clustering using much more data, while both methods beat the rule-based heuristic benchmark models by a large margin. Finally, we define five time frames on the Ethereum blockchain and use our best-performing classifier to detect bots in each of them. Comparing the time windows, we observe that bots are more prevalent in hype phases of Ethereum.
reposiTUm entry (with fulltext)

Frameworks play a pivotal role in expediting the development of mobile applications, enhancing efficiency of the development process. Notably, Cross-Platform Development Frameworks (CPDFs) have garnered significant attention for their capability to facilitate the creation of applications across various platforms through a unified codebase. Despite the widespread adoption of these frameworks, there exists little research focused on detecting their usage in applications, with no comprehensive comparisons among available detectors. This thesis addresses this research gap by presenting a list of current framework detectors, delving into their operational mechanisms, and conducting a comparative analysis. Leveraging a dataset comprising 524 Android applications developed using known, diverse frameworks, we employ various obfuscation techniques to assess their impact on the performance of different detectors. Notably, our investigation reveals that conventional detectors can be thwarted by simple renaming techniques, such as class, file, directory, and library renaming, applied using simple bash scripts. Motivated by these findings, we introduce a novel framework detector that relies on binary code similarity metrics comparing function features extracted from the applications’ binary Of Ahead Time (OAT) representation. The results of our analysis underscore the potential of utilizing function features derived from binary OAT representations for framework detection, highlighting a promising avenue for further research in this domain.
reposiTUm entry (with fulltext)

Equivalence class signatures (EQS) are digital signatures which provide the additional functionality that lets users adapt a given signature to a related message without knowledge of the secret key. They have been used to instantiate numerous cryptographic primitives and increased their efficiency.Unforgeability of the original EQS construction is proven in the generic group model, a theoretical model that treats the underlying group as "ideal". There exist constructions from standard assumptions but those only achieve weak security notions.In this work we strive to answer the question whether EQS schemes which satisfy the original model can be proved secure under standard assumptions with standard techniques. We answer in the negative. There cannot be an efficient security reduction which runs an adversary breaking unforgeability to then break a non-interactive computational assumption. This will be shown by construction of efficient meta-reductions that either break the security of the scheme or said computational problem directly.
reposiTUm entry (with fulltext)

Given the recent advancements in quantum computing and Shor's algorithm, this project aims at bringing Post-Quantum cryptography for e-mail and file encryption as well as software distribution to the OpenPGP protocol. 14 new algorithm identifiers are added to the protocol, implementing different security levels of CRYSTALS-Dilithium and CRYSTALS-Kyber hybrid with elliptic curves, and two standalone variants of SPHINCS+. An extensive discussion is provided on the algorithm choice and construction, considering security factors, user experience, and the interest of various stakeholders. The project also develops an implementation in Golang expanding the existing go-crypto library, to ensure that the proposed standard can be cleanly implemented, and to measure the actual performance on real desktop and mobile devices. The performance data is then carefully analyzed to provide insights on the expected differences in user experience and the necessary changes to the OpenPGP applications.
reposiTUm entry (with fulltext)

WebViews play a critical role in integrating web content into mobile apps. However, balancing their smooth integration with security has been a challenge. More recently, modern cross-platform mobile frameworks (XMFs) such as React Native and Flutter have emerged as popular tools for streamlining cross-platform development. Despite their growing adoption, the security implications of WebViews in these frameworks remain largely unexplored. This thesis fills this gap by systematically investigating the integration and vulnerabilities of WebViews within XMFs.Throughout this thesis, we describe five vulnerabilities associated with using WebViews that pose threats ranging from information leakage to phishing attacks. These vulnerabilities include (a) surreptitious access to methods injected via the JavaScript interface, (b) lack of effective navigation restrictions, (c) insecure HTTP authentication, (d) unauthorized navigation within iframes, and (e) insecure defaults. Our analysis of 3,411 apps shows that many XMF-based apps are likely to be affected due to their use of features found to be vulnerable. While determining the exact number of vulnerable apps is challenging due to the novelty of modern XMFs and the corresponding lack of advanced analysis tools, these findings highlight the urgent need for improved security auditing and provide valuable insights for developers, security analysts, and the broader mobile app industry.
reposiTUm entry (with fulltext)

Zero-knowledge proofs enable proving a statement without revealing any information beyond its truth. This paradoxical notion has evolved over the last few decades from a theoretical concept to the wide adoption of highly efficient zero-knowledge proof systems in practice. At the forefront of this development are proof systems called zk-SNARKs, which stands for zero-knowledge succinct non-interactive argument of knowledge. Not only do they avoid multiple rounds of interaction, but zk-SNARKs also offer succinct proofs whose length is much shorter than the size of the proved statement, with some constructions even achieving constant-size proofs. Among the most recent state-of-the-art constructions is the zk-SNARK "PLONK" by Gabizon, Williamson, and Ciobotaru from 2019. It has constant-size proofs of only half a kilobyte and sublinear proof verification time. Furthermore, it only requires a single trusted setup of its public parameters to support proofs of any statement up to a certain size bound, making PLONK a universal and fully succinct zk-SNARK. Although highly influential and implemented in several real-world applications, there is no formal security proof of its zero knowledge property. In this thesis, we disclose a vulnerability found in PLONK's implementation of zero knowledge and propose how to fix it. As a result, the PLONK protocol has been patched accordingly. Our primary contribution is a formal security proof establishing that the resulting version of PLONK achieves statistical zero knowledge. Towards this goal, we show how to simulate proofs up to an exponentially small difference without relying on any secret information used by the prover. Following the standard definition of zero knowledge, this implies that PLONK proofs reveal (statistically) zero information beyond the truth of the statement. Moreover, we conduct a rigorous security analysis of the entire PLONK protocol, proving the security of all its underlying components. This allows us to show a precise upper bound on PLONK's knowledge soundness error in the algebraic group model. Since the original proof given by the authors of PLONK relies on the same idealized model, our results help towards a better understanding of the security guarantees of PLONK in general.
reposiTUm entry (with fulltext)

With the increasingly popular blockchain technology and its areas of application, illicit activities have repeatedly shown to be a problem in recent years. The lack of regula- tion, combined with the fact that pseudo-anonymity is intrinsically provided by most blockchains and their applications, makes them popular platforms to launder money coming from illegal activities like scams, exploits and hacks. The relative novelty of decentralized transaction systems and their far-reaching possibilities additionally add to this phenomenon. Decentralised protocols in the form of Smart Contracts (SCs) - computer programs that run on the blockchain - are one of the many innovative building blocks of new financial systems. This new paradigm of decentralisation, better known as Decentralized Finance (DeFi), has become one of the fastest-growing segments in the crypto industry in recent years. A variety of DeFi platforms that enable investing, lending and managing assets have emerged on different blockchains. Ethereum is one of these blockchains. It provides a robust infrastructure for SCs, has a big user base and is home to a variety of protocols. The fact that DeFi protocols also enable financial transactions without identification requirements makes them attractive for the transfer of illicit funds originating from fraudulent activities. The aim of this work is to provide a better insight into how fraudulent transaction activities on the Ethereum blockchain are related to DeFi protocols, through quantitative methods. In a web search, we collect a dataset of Ethereum addresses related to fraudulent activities. The found addresses and a dataset of DeFi protocols are used to enrich transaction data of the Ethereum network. We examine the resulting network in a graph database and highlight transaction flows and their relation to DeFi protocols. In a transaction analysis we compare different fraudulent activities and their connection to DeFi protocols.w Our analysis shows that Decentralized Exchanges (DEXs) are common receivers of fraudulent funds. Uniswap (an open-source protocol for providing liquidity and trading Ethereum Request for Comments (ERC-20) tokens is particularly affected. In a more detailed analysis, we therefore also show how tokens are exchanged within the Uniswap protocol, and which ERC-20 tokens are preferentially used by fraudulent addresses. By examining message traces, we gain insight into how fraudulent addresses take advantage of decentralised protocols and how transactions within the protocol take place.
reposiTUm entry (with fulltext)

Cross-chain interoperability is becoming more critical as additional blockchains are added to the Internet of Blockchains. Assets are no longer bound to a specific blockchain but flow across different blockchains, often by making use of decentralized exchange services. However, the interoperability of blockchains also poses a system risk, as failures or issues in one blockchain can have ripple effects on other blockchains as well. In decentralized finance and cross-chain interoperability, the Terra Network is a blockchain that has received significant attention from both institutional and individual investors. The Terra Network’s ability to communicate with other blockchains via a number of protocols and cross-chain bridges was a key selling point. This thesis investigates the Terra network in depth, both before and during its col- lapse, looking at its on-chain activity between smart contracts and user accounts and its cross-chain transactions using some of the most popular cross-chain technologies. The first research question was about which assets were used in cross-chain asset transfers between Terra and other blockchains connected through the decentralized exchange Thorchain. The main asset was BUSD on the Binance blockchain, followed by BTC and ETH. The second research question was about the flow of assets between accounts and smart contracts within Terra before and during the collapse. The analysis shows that Nexus and Anchor Protocol were the dominant smart contracts with a severe outflow during the collapse. The last research question was about analysing how decentralized Terra, Thorchain and the inter-blockchain communication between Terra and the Cosmos Ecosystem are. It was shown that several centralization issues are present, especially amongst computation services, validator locations and IBC relayers. The implications of the thesis are, that asset flow through the analysed cross-chain technologies is visible and can be tracked, as one would expect from on-chain data as well. Centralization is an issue on various levels of analysis with most analysed blockchains and technologies. Validators are heavily centralized by location and computation services used.
reposiTUm entry (with fulltext)

Privacy leaks and shady fingerprinting techniques are becoming more and more relevant in our connected world: Not only on websites but also smartphones.All kinds of different data points are used to create user profiles for fingerprinting and advertisement. These data points often contain sensitive information and, if not carefully used and stored, may be leaked. In our work we search for Android applications(apps) which are scanning the local area network (LAN) and potentially are using these datapoints for fingerprinting or advertisement.We summarize how LAN scanning in Android apps can be done technique-wise (what kind of LAN scanning techniques exist?) and implementation-wise (how can these LAN scanning techniques be implemented?). Based on this research, we developed over 40 handcrafted Yara rules to match Android apps with LAN scanning capabilities. We use this Yara ruleset in our hybrid analysis framework to find apps that are LAN scanning without user interaction. Our proposed framework consists of three parts: First, we use our Yara ruleset to pre-filter Android apps which contain data/functions related to LAN scanning. Next, we dynamically run the pre-filtered Android apps on a real Android smartphone and capture the network traffic. In the last step, we analyze the network dumps for LAN scanning activities. We run our hybrid analysis framework with 3 different Android app datasets (Top 1,000 General Purpose, 1,259 IoT/companion apps, 117 malware apps), totaling over 2,300 different Android apps. We found 8 Android apps ARP scanning the LAN and 29 Android apps sending SSDP search requests without user interaction. Based on our findings we conduct case studies to research why the found Android apps are doing this. We found at least one Android app where we feel certain the LAN scanning happens for fingerprinting reasons.
reposiTUm entry (with fulltext)

Android is widely used as an operating system for smartphones.Because Android apps have access to personal and privacy-sensitive data, they pose an important research target for privacy analysis.Data leaks, where personal information is disclosed to third parties, are often introduced by app developers intentionally for different reasons like monetization.Especially dynamic analysis, where the behavior of an app is examined during its run time, is able to discover such leaks.Dynamic analysis, however, requires the app to execute the functionalities that cause the data leak.Hence, such analysis approaches strive to achieve a high execution coverage, meaning that as much code of the app as possible gets executed.This necessitates to generate the correct inputs for the app to trigger all target functionalities. Automated tools that are used for this task do not have information about the functionalities of the app.Therefore, the generation of the needed inputs is typically infeasible in acceptable time.Because data leaks primarily occur in code paths that are executed frequently (hot code), we develop a method in this thesis that assists to focus dynamic analysis to those code paths.When an app is installed from the Google Play Store, a list of hot code is downloaded and used for performance optimizations.Our approach utilizes these lists to determine, which parts of the apps are hot.As the Play Store API is not publicly documented, we perform reverse engineering to obtain information on how these so-called ahead-of-time (AOT) compilation profiles are downloaded.Based on the gathered information, we then develop a proof of concept that is capable of downloading these AOT profiles systematically.Furthermore, we implement DEX-Tracer, a proof-of-concept tool that utilizes an AOT profile to monitor which of the contained hot code paths actually get executed during run time of the target app.This information can be viewed after DEX-Tracer exits.When used in conjunction with dynamic analysis, this technique works as a metric to determine the progress of the analysis.We empirically demonstrate that our approach to use AOT profiles for this purpose is feasible.The results of this work therefore allow to increase the efficiency of dynamic analysis of Android apps.
reposiTUm entry (with fulltext)

The Ethereum blockchain is the most prominent platform that enables the execution of smart contracts as part of transactions. A smart contract is a program which describes how the state maintained by the blockchain should be updated. As part of its execution, a smart contract may also call or create other contracts. Bugs in the implementation of a smart contract can lead to an inconsistent or unexpected contract state, which may have catastrophic financial consequences. We hence present multeThor, a static analysis tool which is able to answer queries regarding the reachability of certain execution states of smart contracts. In order to deal with statically unknown information, we use techniques from abstract interpretation. The implementation of the analysis then uses an abstract variant of the bytecode semantics of Ethereum smart contracts, which can automatically be executed through Horn clause resolution. During a preanalysis, the tool aims to concretely determine other contracts that may be called. Thereafter, the bytecode of such call targets is automatically downloaded and ultimately incorporated in later stages of the analysis. This allows to more precisely determine the effects of calls to known contracts and especially enables a reasonable analysis of contracts with library calls. One key property of multeThor is its soundness, which means that the tool always derives an abstraction of a reachable execution state. Therefore, multeThor can be used to prove the absence of problematic execution states. We provide a proof sketch to formally show the soundness of multeThor. Through an experimental evaluation on a dataset consisting of contracts obtained from the Ethereum blockchain, we demonstrate that multeThor can be used to verify the generic security property single-entrancy. We also compare the results with those of the previous tool eThor, whose analysis is solely based on the bytecode of the single analyzed contract. In particular, we observe that multeThor can successfully prove the single-entrancy property for a higher number of instances, which empirically shows that its analysis is more precise than that of eThor. Finally, by means of an example, we demonstrate the ability of multeThor to verify functional correctness properties of contracts with library calls.
reposiTUm entry (with fulltext)

Bridge the Gap is a trend that aims to allow web browsers to start smartphone apps on a mobile device. This is achieved by so-called Deep Links, which enable direct linking to specific in-app resources. However, the resulting fusion of the web and native apps also introduces new attack vectors. There are numerous studies on security and privacy concerns of Deep Links on the open-source operating system Android, showing that these are prone to threats such as hijacking. The proprietary operating system iOS has a similar implementation of deep linking mechanisms to Android. However, there are not many publications on this matter, possibly due to the unavailability of iOS’ source code. In this thesis, we investigate the security of mobile Deep Links. First, we present known attack scenarios for Android with regards to Custom Schemes and App Links. Then, we consider the applicability of these attack vectors to deep linking mechanisms on iOS. Therefore, we develop vulnerable apps implementing discussed security issues, analyze whether an attacker could abuse them, and what security and privacy implications this has. Next, we compare our results to the corresponding mechanisms and security concerns of Android. Finally, to gain an insight into the actual security implications of the presented attack vectors, we analyze the distribution of Deep Links in the wild, based on a dataset containing over 11,000 iOS apps from the official Apple App Store.
reposiTUm entry (with fulltext)

Smartphones bundle large amounts of our personal data, like photos, contact information, and location data, in a single place. Users can grant applications (“apps”) access to this data, but they can hardly control or verify how the data is used afterwards. In an attempt to make the collection of privacy-sensitive data more transparent to the user, Apple has recently introduced so-called App Privacy Details (“privacy labels”) on the App Store. They require iOS apps to disclose which kinds of data types they or their third-party partners collect and how they store and use it. One major shortcoming of the system is that these declarations are not verified or audited by Apple, opening the possibility for potential misuse.The aim of this thesis was to evaluate how dynamic mobile analysis methods can be used to investigate an app’s privacy-related behavior at run time in an automated manner, and how they could be used to verify declared privacy labels.Using Dynamic Instrumentation with API Method Call Interception as well as Network Analysis, we created an analysis platform capable of conducting such an analysis on a larger number of apps in an automated manner with minimal interaction by the researcher.To evaluate the real-world performance of the platform, we used it to analyze the privacy behavior of 120 apps in three different case studies. Specifically, we focused on identifying misuse of the “Device ID” label, which apps need to declare if they collect the device’s Advertising Identifier, a valuable data point that allows tracking services to cross-reference user data across apps. Our results show that our platform could successfully verify a declared privacy label for the Advertising Identifier in 70% of cases. Furthermore, we also discovered that among 50 apps who declared not to collect any data, 24% of them still did.We conclude that privacy labels are an important step towards making the use of sensitive data more transparent to the user, but more work needs to be done to ensure that users do not lose their trust in them caused by inaccurate and unvalidated declarations.
reposiTUm entry (with fulltext)

With the rising popularity of Bitcoin, the desire for effective privacy preserving techniques rises as well. Wasabi Wallet and Samourai Wallet are two often recommended wallet services based on decentralized CoinJoins which promise robust and secure mixing of bitcoins. This thesis investigates the role of both wallet services in the greater Bitcoin ecosystem, how it has evolved over time, and whether it is possible to de-anonymize participants. In order to analyze the role of both wallet services, heuristics are developed which detect CoinJoin transactions by both services. The discovered transactions are subsequently analyzed, showing that the number of transactions and the amount of mixed coins is steadily increasing, indicating a growing user base. Furthermore, addresses of entities which are connected to various criminal activities, such as service hacks and ransomware, have been observed within two hops of CoinJoin transactions conducted by both Wasabi Wallet and Samourai Wallet. Finally, the underlying framework used by both wallet services is analyzed in regards to the dangers of coin theft, denial-of-service, and de-anonymization. We show that while an adversarial coordinator could potentially de-anonymize users, such actions would likely lead to retroactive suspicions as they would need to be conducted in an overt fashion. Furthermore, both wallet services are robust against coin theft from any party, and feature measures against denial-of-service attacks.
reposiTUm entry (with fulltext)

Privacy preserving authenticated key exchange (PPAKE) protocols are authenticated key exchange (AKE) protocols that aim to hide the identities of the communicating parties from third parties. Hence the security models of AKE are extended with additional properties. PPAKE protocols have been studied previously. Our aim is to strengthen the existing privacy properties of such protocols. Most notably we additionally consider attacks in which the adversary does not complete the protocol run (e.g. due to the inability to authenticate itself). These attacks are relevant because since some adversaries might not even care if the protocol run is aborted after they deanonymize their target. Furthermore we introduce a formal model that incorporates these properties and several protocols that fulfill different levels of privacy. One of the protocols is a generic construction from generic cryptographic building blocks and hence allows for a post-quantum secure instantiation. Additonally we present formal proofs of all protocols in our model. The second part of this thesis deals with the automated verification of the privacy properties of the main protocol of the first part. Automated verification is used to either find an attack or conclude that the specified properties indeed hold. This gives additional confidence in the correctness of the security proofs contained in this work. First we evaluated the protocol using the Tamarin Prover, which however is unable to finish its proof or find a contradiction with the given resources (approx. 60 GB memory). Then we utilized the verification software ProVerif and were able to prove the security of the protocol. We will present both the Tamarin Prover encoding as well as the ProVerif encoding.
reposiTUm entry (with fulltext)

Since the inception of Bitcoin in 2008, we have witnessed continuous growth in the Bitcoin and blockchain space. As the number of individual cryptocurrencies rises, interoperability between them becomes a critical topic, for instance, to allow for decentralized coin exchange. By utilizing smart contracts or script constructs available on most blockchain systems, connecting two cryptocurrencies is possible via so-called Atomic Swaps. However, for the currencies focusing on privacy enhancements, no such capabilities exist. This thesis explores the Mimblewimble protocol, a construction of an exceptionally efficient privacy-enhancing cryptocurrency. By building on other authors' previous work, we formalize different kinds of Mimblewimble transactions that allow for shared coin ownership and simple contracts and prove their security and correctness. We improve on the protocol's security model by identifying and resolving a weakness in prior formalizations. Utilizing our advanced transaction protocols, we manage to design an Atomic Swap protocol for Mimblewimble-based systems built solely with cryptographic primitives. We further formalize an Atomic Swap protocol between Bitcoin and Grin, a Mimblewimble-based cryptocurrency. We then implement a proof of concept in the programming language Rust, which we successfully deploy and evaluate on the Bitcoin and Grin testnets.
reposiTUm entry (with fulltext)

Security and privacy problems of smart devices are often reported in the news. One possibility to improve the current situation are large-scale analyzes. Researchers and manufacturers can use such analysis to detect weaknesses, report them, and fix them before they get misused. However, to be able to perform a large-scale analysis, two difficulties need to be overcome. First, the diversity regarding software and hardware of smart devices makes a general approach difficult. Second, analyzes are often associated with high costs if physical devices are needed for the selected approach. We developed a static analysis approach for Internet of Things (IoT) companion applications (apps) to circumvent those difficulties. Companion apps are mobile apps, allowing their users to interact with smart devices. We focused on two aspects of companion apps that distinguish them from other applications: the communication over the local network and the used protocols. For this thesis, we use two analysis techniques to collect further information about the devices: taint analysis and value set analysis. We have chosen the latter for reconstructing URLs called by the applications and thereby detecting local communication. In this thesis, we analyzed in total 124 companion apps with our approach. We show the information obtained by the reconstructed endpoints. Furthermore, we present the flows found in two companion apps in detail, which contain threats to user's security and privacy. Overall, we make one step towards large-scale analysis of personally identifiable information (PII) leakage in IoT companion apps.
reposiTUm entry (with fulltext)

Deep learning (DL) is emerging on mobile devices. Cat ear photo filters, OCR credit card recognizers, and auto-correct software already often have a neural network (NN) processor as their core in common. With on-device NN comes the need to also deploy the models to the device. These models are part of the intellectual property of the app’s vendor and thus carry value. Stolen models could cost the owner market share or render attacks on its apps possible. We present an approach to detect deep learning implementing libraries in Android apps by looking for the presence of commonly used mathematical functions such as the general matrix-matrix multiplication. We use reference implementations of these functions and compute fuzzy hashes of basic blocks belonging to loops using a sliding window. We compare these hashes with the hashes generated in a similar fashion for a library under investigation. This provides us with the possibility to automatically determine if a library is implementing DL which enables analysts to quickly separate non-NN binaries from NN binaries. Furthermore, it enables analysts to determine early on if a suspicious app is running NN inference in the cloud. Currently, only one other NN detection approach exists, presented by Xu et al., which searches binaries for strings typically found in NN libraries. While comparing our work with this approach, we found that our approach is able to detect significantly more NN libraries.
reposiTUm entry (with fulltext)

During the financial crisis in 2008, a digital, distributed and decentralised crypto currency arose. Bitcoin was intended to overcome control and censorship by governmental authorities and to enable its users to be under full control of their assets at any time. With ongoing adoption and an increasing amount of transactions, limitations like scalability and weak privacy came to light. To hurdle these limitations, second layer networks were developed among other solutions. Those networks are operating on top of the blockchain. Instead of storing every single transaction on the blockchain, they only store results of several transactions on it. This allows a higher scalability and a better privacy to the users. In this thesis, we show that there are still some privacy issues within the Lightning Network, a second layer network for Bitcoin. Therefore we collected data from the Lightning Network over a certain period and performed several analyses on it. We also linked data collected from the Lightning Network to extracted data from the Bitcoin blockchain to increase the knowledge about the interacting participants. In a final step, we used a cryptoasset analytics tool to enrich our data by information gained from the user behaviour of Bitcoin. With this approach, we were able to link data from the Bitcoin blockchain, the Lightning Network and a cryptoasset analytics tool. In detail, we mapped one of the biggest nodes from the Lightning Network, a very popular wallet service, to the respective cluster known to the cryptoasset analytics tool based on a heuristic. This allowed us a broad insight into the participants that we will present in this paper. Even if the Lightning Network was intended to strengthen the privacy of Bitcoin users, the privacy can nevertheless be reduced by combining data from the Lightning Network, the Bitcoin blockchain and information from a cryptoasset analytics tool.
reposiTUm entry (with fulltext)

In todays society, cryptocurrencies are widely used in diverse fields. Besides the classical direction of cryptocurrencies like Bitcoin with the focus on direct coin exchanges, other cryptocurrencies provide the additional ability of executing complex programs. Ethereum is such a cryptocurrency platform, which supports the execution of programs, called smart contracts, on its blockchain. Currently, smart contracts in Ethereum are executed inside the Ethereum Virtual Machine. This however is planned to change in the next major Ethereum update with eWASM as the successor. While there are many research projects available for EVM contract security, in eWASM this field is virtually unexplored. Due to the substantial amount of differences between the two execution engines, it is vital to explore security properties of eWASM contracts. During this work a static analysis of eWASM contracts was created which is capable of finding reentrancy security vulnerabilities. Since eWASM is still under development, no complete definition of its behavior is available. As a result, the first step was to research several resources in order to gain an insight into the behavior of eWASM. Based on the research, a complete and formal semantic definition of eWASM contract execution was formalized. With the help of this semantics, an abstract formalization was developed in the intermediate language HoRSt which is executed with the SMT solver Z3. Together with the development of a contract parsing mechanism, the definition of reachability queries allows for checking reentrancy possibilities. In order for the abstraction of the formalization to give reliable guarantees, soundness of the abstraction has to be shown. A proof sketch was created, which provides a convincing argument that the abstraction is indeed sound. Besides the successful static analysis of smaller eWASM contracts, the work also represents a stepping stone for future work in this area. Emphasis was placed on highlighting all encountered pitfalls together with contemplated and chosen solutions. In future or continuing projects these directions and respective impacts can be revisited conveniently.
reposiTUm entry (with fulltext)

In the last years, the blockchain technology has been adopted by many traditional fields (such as the financial sector) for reinventing existing applications and giving rise to new use cases. However, during this period of rapid progress the spotlight remained on fast product development, which has led to many security issues throughout the last years resulting in hundreds of millions of USD stolen or lost. Nearly all current public blockchains offer no formal semantics or formal frameworks for verifying smart contract code. This thesis presents a novel semantics for smart contract interactions and a state-of-the-art implementation of a smart-contract-based investment fund for the Ethereum blockchain. The focus lies on connecting a formal semantics for smart contracts to the actual business use case of an investment fund. Specifically, the semantics introduced provides a novel approach by targeting smart contract interactions rather than single smart contract executions. The blockchain is represented by a global state on which complex transaction can be modelled using a big-step semantics. The fully-fledged investment fund ERCFund implemented in the course of this thesis makes it possible to invest in an actively managed portfolio of ERC20-Tokens and Ether by introducing an on-demand minted and burned token as the medium for shares in the fund. Moreover, the software supports many advanced features, such as cold-wallet support and multi-signature protection with off-chain signing. We show that the novel semantics introduced is applicable in a real business setting by adapting and proving an integral security feature for a building block of our investment fund.
reposiTUm entry (with fulltext)