Alumni, Former Collaborators and Visitors
Former visitors of our research unit (sorted by leaving date, latest first):
Former postdocs in our research unit (sorted by leaving date, latest first):
Former Ph.D. students in our research unit (sorted by final date, latest first):
Former MSc/Diploma students supervised by our research unit (sorted by final date, latest first):
|2023-02 ‒ Supervisor: Matteo Maffei
A Systematic Investigation of Illicit Money Flows in the DeFi Ecosystem
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.
|2023-01 ‒ Supervisor: Matteo Maffei
Cross-Chain Traceability in Decentralized Finance
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 decentral- ized 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 individ- ual 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 analy- sis 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.
|Paul Theodor Hager
|2022-12 ‒ Supervisor: Martina Lindorfer
Curious Apps: Large-scale Detection of Apps Scanning Your Local Network
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.
|2022-09 ‒ Supervisor: Martina Lindorfer
Tracing Android Apps based on ART Ahead-Of-Time Compilation Profiles from Google Play
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.
|2022-06 ‒ Supervisor: Matteo Maffei
Sound Cross-Contract Reachability Analysis of Ethereum Smart Contracts
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.
|2021-12 ‒ Supervisor: Martina Lindorfer
Dynamic iOS Privacy Analysis: Verifying App Store Privacy Labels
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.
|2021-10 ‒ Supervisor: Matteo Maffei
Analysis of Decentralized Mixing Services in the Greater Bitcoin Ecosystem
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.
|2021-08 ‒ Supervisor: Matteo Maffei
Privacy Preserving Authenticated Key Exchange – Modelling, Constructions, Proofs and Veriﬁcation using Tamarin
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.
|2021-07 ‒ Supervisor: Matteo Maffei
Adaptor Signature Based Atomic Swaps Between Bitcoin and a Mimblewimble Based Cryptocurrency
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.
|2021-05 ‒ Supervisor: Martina Lindorfer
Large-scale Static Analysis of PII Leakage in IoT Companion Apps
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.
|2020-09 ‒ Supervisor: Martina Lindorfer
Detecting Neural Network Functions in Binaries Based on Syntactic Features
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.
|2020-06 ‒ Supervisor: Matteo Maffei
Payment Channel Network Analysis with Focus on Lightning Network
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.
|2020-01 ‒ Supervisor: Matteo Maffei
Static Analysis of eWASM Contracts
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.
|Jakob Felix Schneider
|2018-08 ‒ Supervisor: Matteo Maffei
Theoretical and Practical Smart Contracts Realization of an Investment Fund
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.
Please send corrections or updates to email@example.com.