Projects

Projects running or completed in our research unit

COnFIDE

Cryptographic Foundations of Privacy in Distributed Ledgers

2020 – 2027 •  Vienna Science and Technology Fund (WWTF)  •  PI Georg Fuchsbauer
Abstract

We are observing a trend towards decentralization, reflected in technologies such as blockchains and distributed ledgers. These enable currencies without banks, community-based platforms without commercial actors, and many more. Central to all such systems is their transparency, allowing anyone to verify the system state, which makes trust in central parties obsolete. However, transparency conflicts with protection of user privacy (meanwhile even legally enforced by GDPR) and current systems cause huge environmental damage.

The goal of COnFIDE is to use cryptography to reconcile public verifiability with privacy in distributed ledgers, and to improve efficiency and sustainability of decentralized systems, avoiding wasting energy (as for mining Bitcoins) and storage (as for massive duplication of obsolete transaction data).

ForSmart

Effective Formal Methods for Smart-Contract Certification

2023 – 2027 •  Vienna Science and Technology Fund (WWTF)  •  PI Laura Kovacs  •  PI Matteo Maffei  •  PI Maria Christakis
Abstract

SCALE2

Scalable, Private, and Interoperable Layer 2

2023 – 2027 •  Vienna Science and Technology Fund (WWTF)  •  PI Georgia Avarikioti
Abstract

Partners
  • Institute of Science and Technology Austria, Klosterneuburg, Austria

W4MP

Fixing the Broken Bridge Between Mobile Apps and the Web

2023 – 2027 •  Vienna Science and Technology Fund (WWTF)  •  PI Martina Lindorfer
Abstract

The Web undertook a progressive conceptual switch from a mesh of interconnected documents to an application distribution platform. In parallel, smartphones and tablets changed the way people consume Web content. With Web apps being ubiquitous, mobile platforms are introducing new mechanisms to integrate Web content into the operating system: in addition to apps embedding browsers, cross-platform apps can be developed using Web frameworks with little to no app development experience. At the same time, powerful Web APIs are in development to close the gap between Web and native apps.

The security and privacy implications of this ongoing transformation have yet to be explored. In particular, the security analysis is hampered by the fast-changing nature of Web and mobile platforms and the contrasting evolution of functionalities across different OSes and browsers. Previous work mainly focused on security and privacy issues affecting either websites or mobile apps in isolation.

We propose to develop a unified framework that will enable us to rigorously evaluate the security implications of the intersection between Web and mobile platforms. We plan to shed light on new ways that Web and mobile apps can interact with each other and how these interactions could potentially lead to security and privacy issues. We will conduct large-scale measurements to confirm the impact of our findings, and we will propose remediation strategies for the emerging mechanisms analyzed.

SFB SPyCoDe

Semantic and Cryptographic Foundations of Security and Privacy by Compositional Design

2023 – 2026 •  Austrian Science Fund (FWF)  •  PI Laura Kovacs  •  PI Matteo Maffei
Abstract

Partners
  • Institute of Science and Technology Austria, Klosterneuburg, Austria
  • TU Graz, Graz, Austria
  • Universität Klagenfurt, Klagenfurt, Austria
  • Universität Wien, Wien
Publications
  • ALASCA: Reasoning in Quantified Linear Arithmetic
    Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., & Voronkov, A. (2023). ALASCA: Reasoning in Quantified Linear Arithmetic. In S. Sankaranarayanan & N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems (pp. 647–665). Springer.
    DOI: 10.1007/978-3-031-30823-9_33 Metadata
    Abstract
    Automated reasoning is routinely used in the rigorous construction and analysis of complex systems. Among different theories, arithmetic stands out as one of the most frequently used and at the same time one of the most challenging in the presence of quantifiers and uninterpreted function symbols. First-order theorem provers perform very well on quantified problems due to the efficient superposition calculus, but support for arithmetic reasoning is limited to heuristic axioms. In this paper, we introduce the ALASCA calculus that lifts superposition reasoning to the linear arithmetic domain. We show that ALASCA is both sound and complete with respect to an axiomatisation of linear arithmetic. We implemented and evaluated ALASCA using the Vampire theorem prover, solving many more challenging problems compared to state-of-the-art reasoners.
  • CheckMate: Automated Game-Theoretic Security Reasoning
    Brugger, L. S., Kovács, L., Petkovic Komel, A., Rain, S., & Rawson, M. (2023). CheckMate: Automated Game-Theoretic Security Reasoning. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 1407–1421). Association for Computing Machinery.
    DOI: 10.1145/3576915.3623183 Metadata
    Abstract
    We present the CheckMate framework for full automation of game-theoretic security analysis, with particular focus on blockchain technologies. CheckMate analyzes protocols modeled as games for their game-theoretic security - that is, for incentive compatibility and Byzantine fault-tolerance. The framework either proves the protocols secure by providing defense strategies or yields all possible attack vectors. For protocols that are not secure, CheckMate can also provide weakest preconditions under which the protocol becomes secure, if they exist. CheckMate implements a sound and complete encoding of game-theoretic security in first-order linear real arithmetic, thereby reducing security analysis to satisfiability solving. CheckMate further automates efficient handling of case splitting on arithmetic terms. Experiments show CheckMate scales, analyzing games with trillions of strategies that model phases of Bitcoin's Lightning Network.
  • Embedding the Connection Calculus in Satisfiability Modulo Theories
    Eisenhofer, C., Kovacs, L., & Rawson, M. (2024). Embedding the Connection Calculus in Satisfiability Modulo Theories. In Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) (pp. 54–63). CEUR-WS.org.
    DOI: 10.34726/5394 Metadata
    Abstract
    We investigate embedding a broad class of deduction systems in satisfiability solvers such as Z3. One such deduction system is the connection calculus. Using Z3’s support for user-propagation, proofs in a user-specified calculus can be found automatically via Z3’s internal satisfiability procedures. The approach places few constraints on the deduction system, yet allows for domain-specific optimisations if known. We discuss ramifications for proof search in the connection calculus.
  • Glimpse: On-Demand PoW Light Client with Constant-Size Storage for DeFi
    Scaffino, G., Aumayr, L., Avarikioti, G., & Maffei, M. (2023). Glimpse: On-Demand PoW Light Client with Constant-Size Storage for DeFi. In Proceedings of the 32nd USENIX Security Symposium (pp. 733–750).
    Metadata
    Abstract
    Cross-chain communication is instrumental in unleashing the full potential of blockchain technologies, as it allows users and developers to exploit the unique design features and the profit opportunities of different existing blockchains. The majority of interoperability solutions are provided by centralized exchanges and bridge protocols based on a trusted majority, both introducing undesirable trust assumptions compared to native blockchain assets. Hence, increasing attention has been given to decentralized solutions: Light and super-light clients paved the way for chain relays, which allow verifying on a blockchain the state of another blockchain by respectively verifying and storing a linear and logarithmic amount of data. Unfortunately, relays turn out to be inefficient in terms of computational costs, storage, or compatibility. We introduce Glimpse, an on-demand bridge that leverages a novel on-demand light client construction with only constant on-chain storage, cost, and computational overhead. Glimpse is expressive, enabling a plethora of DeFi and off-chain applications such as lending, pegs, proofs of oracle attestations, and betting hubs. Glimpse also remains compatible with blockchains featuring a limited scripting language such as the Liquid Network (a pegged sidechain of Bitcoin), for which we present a concrete instantiation. We prove Glimpse security in the Universal Composability (UC) framework and further conduct an economic analysis. We evaluate the cost of Glimpse for Bitcoin-like chains: verifying a simple transaction has at most 700 bytes of on-chain overhead, resulting in a one-time fee of $3, only twice as much as a standard Bitcoin transaction.
  • Non-Classical Logics in Satisfiability Modulo Theories
    Eisenhofer, C., Alassaf, R., Rawson, M., & Kovács, L. (2023). Non-Classical Logics in Satisfiability Modulo Theories. In D. R. S. Ramanayake & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 24–36). Springer.
    DOI: 10.1007/978-3-031-43513-3_2 Metadata
    Abstract
    We show that tableau methods for satisfiability in non-classical logics can be supported naturally in SMT solving via the framework of user-propagators. By way of demonstration, we implement the description logic $$\mathcal {ALC}$$ in the Z3 SMT solver and show that working with user-propagators allows us to significantly outperform encodings to first-order logic with relatively little effort. We promote user-propagators for creating solvers for non-classical logics based on tableau calculi.
  • Refining Unification with Abstraction
    Bhayat, A., Korovin, K., Kovacs, L., & Schoisswohl, J. (2023). Refining Unification with Abstraction. In R. Piskac & A. Voronkov (Eds.), Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 36–47). EasyChair EPiC.
    DOI: 10.29007/h65j Metadata
    Abstract
    Automated reasoning with theories and quantifiers is a common demand in formal methods. A major challenge that arises in this respect comes with rewriting/simplifying terms that are equal with respect to a background first-order theory T, as equality reasoning in this context requires unification moduloT. We introduce a refined algorithm for unification with abstraction inT, allowing for a fine-grained control of equality constraints and substitutions introduced by standard unification with abstraction approaches. We experimentally show the benefit of our approach within first-order linear rational arithmetic.
  • Reshaping Unplugged Computer Science Workshops for Primary School Education
    Martina Landman, Sophie Rain, Laura Kovács, & Gerald Futschek. (2023). Reshaping Unplugged Computer Science Workshops for Primary School Education. In J.-P. Pellet & G. Parriaux (Eds.), Informatics in Schools. Beyond Bits and Bytes: Nurturing Informatics Intelligence in Education : 16th International Conference on Informatics in Schools: Situation, Evolution, and Perspectives, ISSEP 2023, Lausanne, Switzerland, October 23–25, 2023, Proceedings (pp. 139–151). Springer.
    DOI: 10.1007/978-3-031-44900-0_11 Metadata
    Abstract
    Through meticulous analysis and adaptation, we reshaped unplugged computer science activities to align with the developmental needs and capabilities of primary school children. Our approach focuses on distilling the essence of computer science topics while tailoring their content and delivery methods to suit the younger audience. We describe our efforts and report on our experiences implementing our framework for eight primary school classes, turning our unplugged computer science workshops for secondary school classes into an educational playground for 192 primary school children. Our work contributes to the general societal mission of supporting more and more children to become interested in STEM, ensuring that our technological future is as diverse as possible.
  • Saturating Sorting without Sorts
    Georgiou, P., Hajdu, M., & Kovacs, L. (2024). Saturating Sorting without Sorts. arXiv.
    DOI: 10.34726/5861 Metadata
    Abstract
    We present a first-order theorem proving framework for establishing the correctness of functional programs implementing sorting algorithms with recursive data structures. We formalize the semantics of recursive programs in many-sorted first-order logic and integrate sortedness/permutation properties within our first-order formalization. Rather than focusing on sorting lists of elements of specific first-order theories, such as integer arithmetic, our list formalization relies on a sort parameter abstracting (arithmetic) theories and hence concrete sorts. We formalize the permutation property of lists in first-order logic so that we automatically prove verification conditions of such algorithms purely by superpositon-based first-order reasoning. Doing so, we adjust recent efforts for automating inducion in saturation. We advocate a compositional approach for automating proofs by induction required to verify functional programs implementing and preserving sorting and permutation properties over parameterized list structures. Our work turns saturation-based first-order theorem proving into an automated verification engine by (i) guiding automated inductive reasoning with manual proof splits and (ii) fully automating inductive reasoning in saturation. We showcase the applicability of our framework over recursive sorting algorithms, including Mergesort and Quicksort.
  • Superposition with Delayed Unification
    Bhayat, A., Schoisswohl, J., & Rawson, M. (2023). Superposition with Delayed Unification. In B. Pientka & C. Tinelli (Eds.), Automated Deduction – CADE 29  29th International Conference on Automated Deduction, Rome, Italy, July 1–4, 2023, Proceedings (pp. 23–40). Springer.
    DOI: 10.1007/978-3-031-38499-8_2 Metadata
    Abstract
    Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of the unification algorithm into inferences. For calculi that rely on unification procedures returning large or even infinite sets of unifiers, integrating unification into the calculus is an attractive method of dovetailing unification and inference. This applies, for example, to AC-superposition and higher-order superposition. We show that first-order superposition remains complete when moving unification rules to the calculus level. We discuss some of the benefits this has even for standard first-order superposition and provide an experimental evaluation.

CDL-BOT

Blockchain Technologies for the Internet of Things

2020 – 2025 •  Christian Doppler Research Association (CDG)  •  PI Matteo Maffei
Abstract

In recent years, Distributed Ledger Technologies (DLTs) like blockchains have gained much popularity both within industry and research. Today, DLTs are not only perceived as the underlying technology for cryptocurrencies like Bitcoin, but have also been identified as a potential disruptive technology in many different fields, e.g., supply chain tracking and healthcare. In a lot of these fields, blockchains are combined with Internet of Things (|oT) technologies in order to store data from real-world objects in a tamper-proof way, to process this data, and to share the results.

The widespread attention for DLTs has led to manifold research and development activities. These focus either on the application of blockchains in novel use cases, theenhancement of already existing technologies, or the development of completely new DLTs. As a result, today's DLT landscape is heavily fragmented, with different, incompatible technologies being available to potential users. Since interoperability between different blockchains is usually not foreseen in existing protocols and standards, functionalities like sending tokens from one participant to another, invoking and executing smart contracts, or guaranteeing validity of data stored in a blockchain can only be carried out within a single blockchain. This incompatibility contradicts the open nature of |oT- based systems, where heterogeneous technologies interact with each other, and therefore prevents the uptake of blockchains by the industry.

Therefore, the Christian Doppler Laboratory for Blockchain Technologies for the Internet of Things (CDL-BOT) will contribute to the foundations of blockchain interoperability by providing fundamental research results in the areas of cross-blockchain token transfers, cross-blockchain smart contract invocation and interaction, the integration of blockchains with further DLTs and other systems, and by providing client-side blockchain interoperability through developer support. In addition, research in the area of lightweight DLTs for the loT is conducted. While the focus of CDL-BOT is on the application of blockchain technologies in the |oT, other DLTs are also regarded. Furthermore, the research results from the laboratory are not only applicable to the |oT field, but also important for non-|oT-based systems where interoperability between different DLTs is necessary. By doing so, CDL-BOT stimulates a paradigm shift from todays closed blockchains to an open system where devices and users can interact with each other across the boundaries of DLTs.

Partners
  • IOTA Foundation, Berlin, Germany
  • Pantos GmbH, Wien, Austria
Publications
  • A blockchain-based IoT data marketplace
    Sober, M., Scaffino, G., Schulte, S., & Kanhere, S. S. (2023). A blockchain-based IoT data marketplace. CLUSTER COMPUTING-THE JOURNAL OF NETWORKS SOFTWARE TOOLS AND APPLICATIONS, 26(6), 3523–3545.
    DOI: 10.1007/s10586-022-03745-6 Metadata
    Abstract
    The (IoT) is growing steadily, and so is the number of data that is generated by (IoT) devices. This makes it difficult to find and leverage relevant data (and data sources) without a data marketplace. Such a marketplace provides a platform to enable different parties, e.g., sensor operators and service providers, to trade their data. Today, most data marketplaces are based on centralized solutions, which may become a single point of failure and come with expensive infrastructure, trust problems, and privacy issues. Therefore, we propose the application of blockchain technology to implement a data marketplace for the IoT. Within the proposed marketplace, smart contracts are used to implement various functionalities and enforce the rules of the data exchange. The marketplace also includes a proxy, a broker, and (GUIs) to enable data trading. To show the applicability of the proposed data marketplace, we analyze the costs arising from the utilization of smart contracts.
  • Breaking and Fixing Virtual Channels: Domino Attack and Donner
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2023). Breaking and Fixing Virtual Channels: Domino Attack and Donner. In Proceedings Network and Distributed System Security Symposium 2023. 30th Annual Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    DOI: 10.14722/ndss.2023.24370 Metadata
    Abstract
    Payment channel networks (PCNs) mitigate the scalability issues of current decentralized cryptocurrencies. They allow for arbitrarily many payments between users connected through a path of intermediate payment channels, while requiring interacting with the blockchain only to open and close the channels. Unfortunately, PCNs are (i) tailored to payments, excluding more complex smart contract functionalities, such as the oracle-enabling Discreet Log Contracts and (ii) their need for active participation from intermediaries may make payments unreliable, slower, expensive, and privacy-invasive. Virtual channels are among the most promising techniques to mitigate these issues, allowing two endpoints of a path to create a direct channel over the intermediaries without any interaction with the blockchain. After such a virtual channel is constructed, (i) the endpoints can use this direct channel for applications other than payments and (ii) the intermediaries are no longer involved in updates. In this work, we first introduce the Domino attack, a new DoS/griefing style attack that leverages virtual channels to destruct the PCN itself and is inherent to the design adopted by the existing Bitcoin-compatible virtual channels. We then demonstrate its severity by a quantitative analysis on a snapshot of the Lightning Network (LN), the most widely deployed PCN at present. We finally discuss other serious drawbacks of existing virtual channel designs, such as the support for only a single intermediary, a latency and blockchain overhead linear in the path length, or a non-constant storage overhead per user. We then present Donner, the first virtual channel construction that overcomes the shortcomings above, by relying on a novel design paradigm. We formally define and prove security and privacy properties in the Universal Composability framework. Our evaluation shows that Donner is efficient, reduces the on-chain number of transactions for disputes from linear in the path length to a single one, which is the key to prevent Domino attacks, and reduces the storage overhead from logarithmic in the path length to constant. Donner is Bitcoin-compatible and can be easily integrated in the LN.
  • Breaking and Fixing Virtual Channels: Domino Attack and Donner
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2023, September 6). Breaking and Fixing Virtual Channels: Domino Attack and Donner [Presentation]. VISA Research - external research talks, Palo Alto, United States of America (the).
    Metadata
  • Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph
    Chatterjee, D., Banerjee, P., & Subhra Mazumdar. (2023). Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph. arXiv.
    DOI: 10.34726/5301 Metadata
    Abstract
    Hash-based Proof-of-Work (PoW) used in the Bitcoin Blockchain leads to high energy consumption and resource wastage. In this paper, we aim to re-purpose the energy by replacing the hash function with real-life problems having commercial utility. We propose Chrisimos, a useful Proof-of-Work where miners are required to find a minimal dominating set for real-life graph instances. A miner who is able to output the smallest dominating set for the given graph within the block interval time wins the mining game. We also propose a new chain selection rule that ensures the security of the scheme. Thus our protocol also realizes a decentralized minimal dominating set solver for any graph instance. We provide formal proof of correctness and show via experimental results that the block interval time is within feasible bounds of hash-based PoW.
  • Context-Aware Routing in Fog Computing Systems
    Karagiannis, V., Frangoudis, P., Dustdar, S., & Schulte, S. (2023). Context-Aware Routing in Fog Computing Systems. IEEE Transactions on Cloud Computing, 11(1), 532–549.
    DOI: 10.1109/TCC.2021.3102996 Metadata
    Abstract
    Fog computing enables the execution of IoT applications on compute nodes which reside both in the cloud and at the edge of the network. To achieve this, most fog computing systems route the IoT data on a path which starts at the data source, and goes through various edge and cloud nodes. Each node on this path may accept the data if there are available resources to process this data locally. Otherwise, the data is forwarded to the next node on path. Notably, when the data is forwarded (rather than accepted), the communication latency increases by the delay to reach the next node. To avoid this, we propose a routing mechanism which maintains a history of all nodes that have accepted data of each context in the past. By processing this history, our mechanism sends the data directly to the closest node that tends to accept data of the same context. This lowers the forwarding by nodes on path, and can reduce the communication latency. We evaluate this approach using both prototype- and simulation-based experiments which show reduced communication latency (by up to 23%) and lower number of hops traveled (by up to 73%), compared to a state-of-the-art method.
  • Foundations of Coin Mixing Services
    Glaeser, N., Maffei, M., Malavolta, G., Moreno-Sanchez, P., Tairi, E., & Thyagarajan, S. A. (2022). Foundations of Coin Mixing Services. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 1259–1273). Association for Computing Machinery.
    DOI: 10.34726/3601 Metadata
    Abstract
    Coin mixing services allow users to mix their cryptocurrency coins and thus enable unlinkable payments in a way that prevents tracking of honest users' coins by both the service provider and the users themselves. The easy bootstrapping of new users and backwards compatibility with cryptocurrencies (such as Bitcoin) with limited support for scripts are attractive features of this architecture, which has recently gained considerable attention in both academia and industry. A recent work of Tairi et al. [IEEE S&P 2021] formalizes the notion of a coin mixing service and proposes A2L, a new cryptographic protocol that simultaneously achieves high efficiency and interoperability. In this work, we identify a gap in their formal model and substantiate the issue by showing two concrete counterexamples: we show how to construct two encryption schemes that satisfy their definitions but lead to a completely insecure system. To amend this situation, we investigate secure constructions of coin mixing services. First, we develop the notion of blind conditional signatures (BCS), which acts as the cryptographic core for coin mixing services. We propose game-based security definitions for BCS and propose A2L+, a modified version of the protocol by Tairi et al. that satisfies our security definitions. Our analysis is in an idealized model (akin to the algebraic group model) and assumes the hardness of the one-more discrete logarithm problem. Finally, we propose A2L-UC, another construction of BCS that achieves the stronger notion of UC-security (in the standard model), albeit with a significant increase in computation cost. This suggests that constructing a coin mixing service protocol secure under composition requires more complex cryptographic machinery than initially thought.
  • Glimpse: On-Demand PoW Light Client with Constant-Size Storage for DeFi
    Scaffino, G., Aumayr, L., Avarikioti, G., & Maffei, M. (2023). Glimpse: On-Demand PoW Light Client with Constant-Size Storage for DeFi. In Proceedings of the 32nd USENIX Security Symposium (pp. 733–750).
    Metadata
    Abstract
    Cross-chain communication is instrumental in unleashing the full potential of blockchain technologies, as it allows users and developers to exploit the unique design features and the profit opportunities of different existing blockchains. The majority of interoperability solutions are provided by centralized exchanges and bridge protocols based on a trusted majority, both introducing undesirable trust assumptions compared to native blockchain assets. Hence, increasing attention has been given to decentralized solutions: Light and super-light clients paved the way for chain relays, which allow verifying on a blockchain the state of another blockchain by respectively verifying and storing a linear and logarithmic amount of data. Unfortunately, relays turn out to be inefficient in terms of computational costs, storage, or compatibility. We introduce Glimpse, an on-demand bridge that leverages a novel on-demand light client construction with only constant on-chain storage, cost, and computational overhead. Glimpse is expressive, enabling a plethora of DeFi and off-chain applications such as lending, pegs, proofs of oracle attestations, and betting hubs. Glimpse also remains compatible with blockchains featuring a limited scripting language such as the Liquid Network (a pegged sidechain of Bitcoin), for which we present a concrete instantiation. We prove Glimpse security in the Universal Composability (UC) framework and further conduct an economic analysis. We evaluate the cost of Glimpse for Bitcoin-like chains: verifying a simple transaction has at most 700 bytes of on-chain overhead, resulting in a one-time fee of $3, only twice as much as a standard Bitcoin transaction.
  • LightSwap: An Atomic Swap Does Not Require Timeouts at both Blockchains
    Hoenisch, P., Mazumdar, S., Moreno-Sanchez, P., & Ruj, S. (2023). LightSwap: An Atomic Swap Does Not Require Timeouts at both Blockchains. In J. Garcia-Alfaro, G. Navarro-Arribas, & N. Dragoni (Eds.), Data Privacy Management, Cryptocurrencies and Blockchain Technology (pp. 219–235). Springer Cham.
    DOI: 10.1007/978-3-031-25734-6_14 Metadata
    Abstract
    ecurity and privacy issues with centralized exchange services have motivated the design of atomic swap protocols for decentralized trading across currencies. These protocols follow a standard blueprint similar to the 2-phase commit in databases: (i) both users first lock their coins under a certain (cryptographic) condition and a timeout; (ii-a) the coins are swapped if the condition is fulfilled; or (ii-b) coins are released after the timeout. The quest for these protocols is to minimize the requirements from the scripting language supported by the swapped coins, thereby supporting a larger range of cryptocurrencies. The recently proposed universal atomic swap protocol [IEEE S&P’22] demonstrates how to swap coins whose scripting language only supports the verification of a digital signature on a transaction. However, the timeout functionality is cryptographically simulated with verifiable timelock puzzles, a computationally expensive primitive that hinders its use in battery-constrained devices such as mobile phones. In this state of affairs, we question whether the 2-phase commit paradigm is necessary for atomic swaps in the first place. In other words, is it possible to design a secure atomic swap protocol where the timeout is not used by (at least one of the two) users? In this work, we present LightSwap, the first secure atomic swap protocol that does not require the timeout functionality (not even in the form of a cryptographic puzzle) by one of the two users. LightSwap is thus better suited for scenarios where a user, running an instance of LightSwap on her mobile phone, wants to exchange coins with an online exchange service running an instance of LightSwap on a computer. We show how LightSwap can be used to swap Bitcoin and Monero, an interesting use case since Monero does not provide any scripting functionality support other than linkable ring signature verification.
  • LightSwap: An Atomic Swap Does Not Require Timeouts At Both Blockchains
    Hoenisch, P., Mazumdar, S., Moreno-Sanchez, P., & Ruj, S. (2022). LightSwap: An Atomic Swap Does Not Require Timeouts At Both Blockchains. Cryptology ePrint Archive.
    DOI: 10.34726/3662 Metadata
    Abstract
    Security and privacy issues with centralized exchange services have motivated the design of atomic swap protocols for decentralized trading across currencies. These protocols follow a standard blueprint similar to the 2-phase commit in databases: (i) both users first lock their coins under a certain (cryptographic) condition and a timeout; (ii-a) the coins are swapped if the condition is fulfilled; or (ii-b) coins are released after the timeout. The quest for these protocols is to minimize the requirements from the scripting language supported by the swapped coins, thereby supporting a larger range of cryptocurrencies. The recently proposed universal atomic swap protocol [IEEE S&P’22] demonstrates how to swap coins whose scripting language only supports the verification of a digital signature on a transaction. However, the timeout functionality is cryptographically simulated with verifiable timelock puzzles, a computationally expensive primitive that hinders its use in battery-constrained devices such as mobile phones. In this state of affairs, we question whether the 2-phase commit paradigm is necessary for atomic swaps in the first place. In other words, is it possible to design a secure atomic swap protocol where the timeout is not used by (at least one of the two) users? In this work, we present LightSwap, the first secure atomic swap protocol that does not require the timeout functionality (not even in the form of a cryptographic puzzle) by one of the two users. LightSwap is thus better suited for scenarios where a user, running an instance of LightSwap on her mobile phone, wants to exchange coins with an online exchange service running an instance of LightSwap on a computer. We show how LightSwap can be used to swap Bitcoin and Monero, an interesting use case since Monero does not provide any scripting functionality support other than linkable ring signature verification.
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Thyagarajan, S. A., Malavolta, G., Moreno-Sanchez, P., & Maffei, M. (2022). Sleepy Channels: Bi-directional Payment Channels without Watchtowers. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 179–192). Association for Computing Machinery.
    DOI: 10.1145/3548606.3559370 Metadata
    Abstract
    Payment channels (PC) are a promising solution to the scalability issue of cryptocurrencies, allowing users to perform the bulk of the transactions off-chain without needing to post everything on the blockchain. Many PC proposals however, suffer from a severe limitation: Both parties need to constantly monitor the blockchain to ensure that the other party did not post an outdated transaction. If this event happens, the honest party needs to react promptly and engage in a punishment procedure. This means that prolonged absence periods (e.g., a power outage) may be exploited by malicious users. As a mitigation, the community has introduced watchtowers, a third-party monitoring the blockchain on behalf of off-line users. Unfortunately, watchtowers are either trusted, which is critical from a security perspective, or they have to lock a certain amount of coins, called collateral, for each monitored PC in order to be held accountable, which is financially infeasible for a large network. We present Sleepy Channels, the first bi-directional PC protocol without watchtowers (or any other third party) that supports an unbounded number of payments and does not require parties to be persistently online. The key idea is to confine the period in which PC updates can be validated on-chain to a short, pre-determined time window, which is when the PC parties have to be online. This behavior is incentivized by letting the parties lock a collateral in the PC, which can be adjusted depending on their mutual trust and which they get back much sooner if they are online during this time window. Our protocol is compatible with any blockchain that is capable of verifying digital signatures (e.g., Bitcoin), as shown by our proof of concept. Moreover, our experimental results show that Sleepy Channels impose a communication and computation overhead similar to state-of-the-art PC protocols while removing watchtower's collateral and fees for the monitoring service.
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2022, October 31). Sleepy Channels: Bi-directional Payment Channels without Watchtowers [Poster Presentation]. Crypto Economics Security Conference, Berkeley, United States of America (the).
    Metadata
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2023, February 28). Sleepy Channels: Bi-directional Payment Channels without Watchtowers [Poster Presentation]. Network and Distributed System Security Symposium (NDSS) 2023, United States of America (the).
    Metadata
  • Sleepy Channels: Bitcoin-Compatible Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2023, August 30). Sleepy Channels: Bitcoin-Compatible Bi-directional Payment Channels without Watchtowers [Conference Presentation]. The Science of Blockchain Conference 2023, Stanford, United States of America (the).
    Metadata
  • Strategic Analysis of Griefing Attack in Lightning Network
    Mazumdar, S., Banerjee, P., Sinha, A., Ruj, S., & Roy, B. (2022). Strategic Analysis of Griefing Attack in Lightning Network. IEEE Transactions on Network and Service Management.
    DOI: 10.34726/3581 Metadata
    Abstract
    Hashed Timelock Contract (HTLC) in Lightning Network is susceptible to a griefing attack. An attacker can block several channels and stall payments by mounting this attack. A state-of-the-art countermeasure, Hashed Timelock Contract with Griefing-Penalty (HTLC-GP) is found to work under the classical assumption of participants being either honest or malicious but fails for rational participants. To address the gap, we introduce a game-theoretic model for analyzing griefing attacks in HTLC. We use this model to analyze griefing attacks in HTLC-GP and conjecture that it is impossible to design an efficient protocol that will penalize a malicious participant with the current Bitcoin scripting system. We study the impact of the penalty on the cost of mounting the attack and observe that HTLC-GP is weakly effective in disincentivizing the attacker in certain conditions. To further increase the cost of attack, we introduce the concept of guaranteed minimum compensation, denoted as ζ, and modify HTLC-GP into HTLC-GPζ. By experimenting on several instances of Lightning Network, we observe that the total coins locked in the network drops to 28% for HTLC-GPζ, unlike in HTLC-GP where total coins locked does not drop below 40%. These results justify that HTLC-GPζ is better than HTLC-GP to counter griefing attacks.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2022). Thora: Atomic and Privacy-Preserving Multi-Channel Updates. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 165–178). Association for Computing Machinery.
    DOI: 10.1145/3548606.3560556 Metadata
    Abstract
    Most blockchain-based cryptocurrencies suffer from a heavily limited transaction throughput, which is a barrier to their growing adoption. Payment channel networks (PCNs) are one of the promising solutions to this problem. PCNs reduce the on-chain load of transactions and increase the throughput by processing many payments off-chain. In fact, any two users connected via a path of payment channels (i.e., joint addresses between the two channel end-points) can perform payments, and the underlying blockchain is used only when there is a dispute between users. Unfortunately, payments in PCNs can only be conducted securely along a path, which prevents the design of many interesting applications. Moreover, the most widely used implementation, the Lightning Network in Bitcoin, suffers from a collateral lock time linear in the path length, it is affected by security issues, and it relies on specific scripting features called Hash Timelock Contracts that hinders the applicability of the underlying protocol in other blockchains. In this work, we present Thora, the first Bitcoin-compatible off-chain protocol that enables the atomic update of arbitrary channels (i.e., not necessarily forming a path). This enables the design of a number of new off-chain applications, such as payments across different PCNs sharing the same blockchain, secure and trustless crowdfunding, and channel rebalancing. Our construction requires no specific scripting functionalities other than digital signatures and timelocks, thereby being applicable to a wider range of blockchains. We formally define security and privacy in the Universal Composability framework and show that our cryptographic protocol is a realization thereof. In our performance evaluation, we show that our construction requires only constant collateral, independently from the number of channels, and has only a moderate off-chain communication as well as computation overhead.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2023, February 28). Thora: Atomic and Privacy-Preserving Multi-Channel Updates [Poster Presentation]. Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    Metadata
    Abstract
    Most blockchain-based cryptocurrencies suffer from a heavily limited transaction throughput, which is a barrier to their growing adoption. Payment channel networks (PCNs) are one of the promising solutions to this problem. PCNs reduce the on-chain load of transactions and increase the throughput by processing many payments off-chain. In fact, any two users connected via a path of payment channels (i.e., joint addresses between the two channel end-points) can perform payments, and the underlying blockchain is used only when there is a dispute between users. Unfortunately, payments in PCNs can only be conducted securely along a path, which prevents the design of many interesting applications. Moreover, the most widely used implementation, the Lightning Network in Bitcoin, suffers from a collateral lock time linear in the path length, it is affected by security issues, and it relies on specific scripting features called Hash Timelock Contracts that hinders the applicability of the underlying protocol in other blockchains. In this work, we present Thora, the first Bitcoin-compatible off-chain protocol that enables the atomic update of arbitrary channels (i.e., not necessarily forming a path). This enables the design of a number of new off-chain applications, such as payments across different PCNs sharing the same blockchain, secure and trustless crowdfunding, and channel rebalancing. Our construction requires no specific scripting functionalities other than digital signatures and timelocks, thereby being applicable to a wider range of blockchains. We formally define security and privacy in the Universal Composability framework and show that our cryptographic protocol is a realization thereof. In our performance evaluation, we show that our construction requires only constant collateral, independently from the number of channels, and has only a moderate off-chain communication as well as computation overhead.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2023, August 30). Thora: Atomic and Privacy-Preserving Multi-Channel Updates [Conference Presentation]. The Science of Blockchain Conference 2023 (SBC’23), Stanford University, United States of America (the).
    Metadata
  • Thora: Atomic And Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Kasra Abbaszadeh, & Maffei, M. (2022, October 31). Thora: Atomic And Privacy-Preserving Multi-Channel Updates [Poster Presentation]. Crypto Economics Security Conference, Berkeley, United States of America (the).
    Metadata
  • Towards a Game-Theoretic Security Analysis of Off-Chain Protocols
    Rain, S., Avarikioti, G., Kovacs, L., & Maffei, M. (2023). Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 107–122). IEEE.
    DOI: 10.1109/CSF57540.2023.00003 Metadata
    Abstract
    Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. In this work we take a first step towards a principled game-theoretic security analysis of off-chain protocols by introducing the first game-theoretic model that is expressive enough to reason about their security. We advocate the use of Extensive Form Games (EFGs) and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize parties to upload old channel states on-chain. Moreover, we model the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network.
  • Towards faster settlement in HTLC-based Cross-Chain Atomic Swaps
    Mazumdar, S. (2022). Towards faster settlement in HTLC-based Cross-Chain Atomic Swaps. arXiv.
    DOI: 10.34726/3805 Metadata
    Abstract
    Hashed Timelock (HTLC)-based atomic swap protocols enable the exchange of coins between two or more parties without relying on a trusted entity. This protocol is like the American call option without premium. It allows the finalization of a deal within a certain period. This puts the swap initiator at liberty to delay before deciding to proceed with the deal. If she finds the deal unprofitable, she just waits for the time-period of the contract to elapse. However, the counterparty is at a loss since his assets remain locked in the contract. The best he can do is to predict the initiator's behavior based on the asset's price fluctuation in the future. But it is difficult to predict as cryptocurrencies are quite volatile, and their price fluctuates abruptly. We perform a game theoretic analysis of HTLC-based atomic cross-chain swap to predict whether a swap will succeed or not. From the strategic behavior of the players, we infer that this model lacks fairness. We propose Quick Swap, a two-party protocol based on hashlock and timelock that fosters faster settlement of the swap. The parties are required to lock griefing-premium along with the principal amount. If the party griefs, he ends up paying the griefing-premium. If a party finds a deal unfavorable, he has the provision to cancel the swap. We prove that Quick Swap is more participant-friendly than HTLC-based atomic swap. Our work is the first to propose a protocol to ensure fairness of atomic-swap in a cyclic multi-party setting.

IoTIO

IoTIO: Analyzing and Understanding the Internet of Insecure Things

2020 – 2025 •  Vienna Science and Technology Fund (WWTF)  •  PI Martina Lindorfer
Abstract

Consumer devices, from door locks to light bulbs, are becoming increasingly smart. They are linked with other devices as part of smart homes and offices, usually Internet-connected, and may be publicly accessible through misconfiguration or IPv6.

The corresponding security and privacy implications have yet to be explored in depth, and their analysis is complicated by device type and architecture diversity. Prior work focused on case studies of specific device types, or analyzed devices' firmware in isolation, requiring substantial manual effort. In contrast, the automatic analysis of devices' interaction with their environment and other devices could uncover new vulnerability types and privacy violations.

In this project, we will propose scalable techniques to analyze smart devices for potential vulnerabilities based on how they are collecting, processing, and sharing data by interacting with their mobile companion app or smart hubs. We will provide a proof-of-concept tool to show our research's practicality.

The basis of our project are novel software and network analyses of companion apps and hub integration to synthesize protocols, discover commands to exercise device functionality, and identify information flows ‒ without requiring access to the smart devices themselves.

The project is a multi-disciplinary research effort enabling security and privacy analyses. It has also societal impact by enabling informed decision making by manufactures, lawmakers, and users.

Partners
  • Ruhr-Universität Bochum, Bochum, Germany
Publications
  • A Comparative Analysis of Certificate Pinning in Android & iOS
    Pradeep, A., Paracha, M. T., Bhowmick, P., Davanian, A., Razaghpanah, A., Chung, T., Lindorfer, M., Vallina-Rodriguez, N., Levin, D., & Choffnes, D. (2022). A Comparative Analysis of Certificate Pinning in Android & iOS. In Proceedings of the 22nd ACM Internet Measurement Conference (pp. 605–618). ACM.
    DOI: 10.34726/3505 Metadata
    Abstract
    TLS certificate pinning is a security mechanism used by applications (apps) to protect their network traffic against malicious certificate authorities (CAs), in-path monitoring, and other methods of TLS tampering. Pinning can provide enhanced security to defend against malicious third-party access to sensitive data in transit (e.g., to protect sensitive banking and health care information), but can also hide an app’s personal data collection from users and auditors. Prior studies found pinning was rarely used in the Android ecosystem, except in high-profile, security-sensitive apps; and, little is known about its usage on iOS and across mobile platforms. In this paper, we thoroughly investigate the use of certificate pinning on Android and iOS. We collect 5,079 unique apps from the two official app stores: 575 common apps, 1,000 popular apps each, and 1,000 randomly selected apps each. We develop novel, cross-platform, static and dynamic analysis techniques to detect the usage of certificate pinning. Thus, our study offers a more comprehensive understanding of certificate pinning than previous studies. We find certificate pinning as much as 4 times more widely adopted than reported in recent studies. More specifically, we find that 0.9% to 8% of Android apps and 2.5% to 11% of iOS apps use certificate pinning at run time (depending on the aforementioned sets of apps). We then investigate which categories of apps most frequently use pinning (e.g., apps in the “finance” category), which destinations are typically pinned (e.g., first-party destinations vs those used by third-party libraries), which certificates are pinned and how these are pinned (e.g., CA vs leaf certificates), and the connection security for pinned connections vs unpinned ones (e.g., the use of weak ciphers or improper certificate validation). Lastly, we investigate how many pinned connections are amenable to binary instrumentation to reveal the contents of their connections; for those that are, we analyze the data sent over pinned connections to understand what is protected by pinning.
  • ART-assisted App Diffing: Defeating Dalvik Bytecode Shrinking, Obfuscation, and Optimization with Android's OAT Compiler
    Bleier, J., & Lindorfer, M. (2022, May 23). ART-assisted App Diffing: Defeating Dalvik Bytecode Shrinking, Obfuscation, and Optimization with Android’s OAT Compiler [Poster Presentation]. 43rd IEEE Symposium on Security and Privacy, San Francisco, United States of America (the).
    Metadata
    Abstract
    Android aims to provide a secure and feature-rich, yet resource-saving platform for its applications (apps). To achieve these goals, the compilation to distributable packages shrinks, obfuscates, and optimizes the code by default. As an additional optimization, the Android Runtime (ART) nowadays compiles the app’s bytecode to native code on the device instead of executing it in the Dalvik VM. We study the effects of these changes in the Android build and runtime environment on the problem of calculating app similarity. We compare existing bytecode-based tools to our novel approach of using the recompiled (and optimized) binary form. We propose OATMEAL, an extensible framework to generate reliable ground truth for evaluating app similarity approaches and provide a benchmark dataset to the community. We built this dataset from open-source apps available on F-Droid in various configurations that optimize and obfuscate the bytecode. Using this dataset, we show the limitations of existing Android-specific bytecode analysis approaches when faced with the new optimizing R8 bytecode compiler. We further demonstrate how well BinDiff, a state-of-the-art binary-based alternative, works in scoring the similarity of apps. With OATMEAL, we provide the foundation for integrating and benchmarking further approaches, both for calculating the similarity between apps (based on bytecode or binary code), and for evaluating their robustness to evolving optimization and obfuscation techniques.
  • Comparing User Perceptions of Anti-Stalkerware Apps with the Technical Reality
    Fassl, M., Anell, S., Houy, S., Lindorfer, M., & Krombholz, K. (2022). Comparing User Perceptions of Anti-Stalkerware Apps with the Technical Reality. In Proceedings of the Eighteenth Symposium on Usable Privacy and Security (SOUPS 2022) (pp. 135–154). USENIX Association.
    DOI: 10.34726/3902 Metadata
    Abstract
    Every year an increasing number of users face stalkerware on their phones. Many of them are victims of intimate partner surveillance (IPS) who are unsure how to identify or remove stalkerware from their phones. An intuitive approach would be to choose anti-stalkerware from the app store. However, a mismatch between user expectations and the technical capabilities can produce an illusion of security and risk compensation behavior (i.e., the Peltzmann effect). We compare users’ perceptions of anti-stalkerware with the technical reality. First, we applied thematic analysis to app reviews to analyze user perceptions. Then, we performed a cognitive walkthrough of two prominent anti-stalkerware apps available on the Google Play Store and reverse-engineered them to understand their detection features. Our results suggest that users base their trust on the look and feel of the app, the number and type of alerts, and the apps’ affordances. We also found that app capabilities do not correspond to the users’ perceptions and expectations, impacting their practical effectiveness. We discuss different stakeholders’ options to remedy these challenges and better align user perceptions with the technical reality.
  • Connecting the .dotfiles: Checked-In Secret Exposure with Extra (Lateral Movement) Steps
    Jungwirth, G., Saha, A., Schröder, M., Fiebig, T., Lindorfer, M., & Cito, J. (2023). Connecting the .dotfiles: Checked-In Secret Exposure with Extra (Lateral Movement) Steps. In IEEE/ACM 20th International Conference on Mining Software Repositories (MSR) (pp. 322–333).
    DOI: 10.1109/MSR59073.2023.00051 Metadata
    Abstract
    Personal software configurations, known as dotfiles, are increasingly being shared in public repositories. To understand the security and privacy implications of this phenomenon, we conducted a large-scale analysis of dotfiles repositories on GitHub. Furthermore, we surveyed repository owners to understand their motivations for sharing dotfiles, and their awareness of the security implications. Our mixed-method approach consisted of two parts: (1) We mined 124,230 public dotfiles repositories and inductively searched them for security and privacy flaws. (2) We then conducted a survey of repository owners (n=1,650) to disclose our findings and learn more about the problems and implications. We found that 73.6 % of repositories leak potentially sensitive information, most commonly email addresses (of which we found 1.2 million), but also RSA private keys, API keys, installed software versions, browsing history, and even mail client inboxes. In addition, we found that sharing is mainly ideological (an end in itself) and to show off ("ricing"), in addition to easing machine setup. Most users are confident about the contents of their files and claim to understand the security implications. In response to our disclosures, a small minority (2.2%) will make their repositories private or delete them, but the majority of respondents will continue sharing their dotfiles after taking appropriate actions. Dotfiles repositories are a great tool for developers to share knowledge and communicate - if done correctly. We provide recommendations for users and platforms to make them more secure. Specifically, tools should be used to manage dotfiles. In addition, platforms should work on more sophisticated tests, to find weaknesses automatically and inform the users or control the damage.
  • I Still Know What You Watched Last Sunday: Privacy of the HbbTV Protocol in the European Smart TV Landscape
    Tagliaro, C., Hahn, F., Sepe, R., Aceti, A., & Lindorfer, M. (2023). I Still Know What You Watched Last Sunday: Privacy of the HbbTV Protocol in the European Smart TV Landscape. In Proceedings Network and Distributed System Security (NDSS) Symposium 2023. 30th Annual Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    DOI: 10.14722/ndss.2023.24102 Metadata
    Abstract
    The ever-increasing popularity of Smart TVs and support for the Hybrid Broadcast Broadband TV (HbbTV) standard allow broadcasters to enrich content offered to users via the standard broadcast signal with Internet-delivered apps, e.g., ranging from quizzes during a TV show to targeted advertisement. HbbTV works using standard web technologies as transparent overlays over a TV channel. Despite the number of HbbTV-enabled devices rapidly growing, studies on the protocol’s security and privacy aspects are scarce, and no standard protective measure is in place. We fill this gap by investigating the current state of HbbTV in the European landscape and assessing its implications for users’ privacy. We shift the focus from the Smart TV’s firmware and app security, already studied in-depth in related work, to the content transmission protocol itself. Contrary to traditional “linear TV” signals, HbbTV allows for bi-directional communication: in addition to receiving TV content, it also allows for transmitting data back to the broadcaster. We describe techniques broadcasters use to measure users’ (viewing) preferences and show how the protocol’s implementation can cause severe privacy risks by studying its deployment by 36 TV channels in five European countries (Italy, Germany, France, Austria, and Finland). We also survey users’ awareness of Smart TV and HbbTV-related risks. Our results show little understanding of the possible threats users are exposed to. Finally, we present a denylist-based mechanism to ensure a safe experience for users when watching TV and to reduce the privacy issues that HbbTV may pose.
  • IoTFlow: Inferring IoT Device Behavior at Scale through Static Mobile Companion App Analysis
    Schmidt, D., Tagliaro, C., Borgolte, K., & Lindorfer, M. (2023). IoTFlow: Inferring IoT Device Behavior at Scale through Static Mobile Companion App Analysis. In CCS ’23: Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (pp. 681–695). Association for Computing Machinery.
    DOI: 10.1145/3576915.3623211 Metadata
    Abstract
    The number of “smart” devices, that is, devices making up the Internet of Things (IoT), is steadily growing. They suffer from vulnerabilities just as other software and hardware. Automated analysis techniques can detect and address weaknesses before attackers can misuse them. Applying existing techniques or developing new approaches that are sufficiently general is challenging though. Contrary to other platforms, the IoT ecosystem features various software and hardware architectures. We introduce IoTFlow, a new static analysis approach for IoT devices that leverages their mobile companion apps to address the diversity and scalability challenges. IoTFlow combines Value Set Analysis (VSA) with more general data-flow analysis to automatically reconstruct and derive how companion apps communicate with IoT devices and remote cloud-based backends, what data they receive or send, and with whom they share it. To foster future work and reproducibility, our IoTFlow implementation is open source. We analyze 9,889 manually verified companion apps with IoTFlow to understand and characterize the current state of security and privacy in the IoT ecosystem, which also demonstrates the utility of IoTFlow. We compare how these IoT apps differ from 947 popular general-purpose apps in their local network commu- nication, the protocols they use, and who they communicate with. Moreover, we investigate how the results of IoTFlow compare to dynamic analysis, with manual and automated interaction, of 13 IoT devices when paired and used with their companion apps. Overall, utilizing IoTFlow, we discover various IoT security and privacy issues, such as abandoned domains, hard-coded credentials, expired certificates, and sensitive personal information being shared.
  • Mixed Signals: Analyzing Software Attribution Challenges in the Android Ecosystem
    Hageman, K., Feal, A., Gamba, J., Girish, A., Bleier, J., Lindorfer, M., Tapiador, J., & Vallina-Rodriguez, N. (2023). Mixed Signals: Analyzing Software Attribution Challenges in the Android Ecosystem. IEEE Transactions on Software Engineering, 49(4), 2964–2979.
    DOI: 10.34726/5296 Metadata
    Abstract
    The ability to identify the author responsible for a given software object is critical for many research studies and for enhancing software transparency and accountability. However, as opposed to other application markets like Apple's iOS App Store, attribution in the Android ecosystem is known to be hard. Prior research has leveraged market metadata and signing certificates to identify software authors without questioning the validity and accuracy of these attribution signals. However, Android application (app) authors can, either intentionally or by mistake, hide their true identity due to: (1) the lack of policy enforcement by markets to ensure the accuracy and correctness of the information disclosed by developers in their market profiles during the app release process, and (2) the use of self-signed certificates for signing apps instead of certificates issued by trusted CAs. In this paper, we perform the first empirical analysis of the availability, volatility and overall aptness of publicly available market and app metadata for author attribution in Android markets. To that end, we analyze a dataset of over 2.5 million market entries and apps extracted from five Android markets for over two years. Our results show that widely used attribution signals are often missing from market profiles and that they change over time. We also invalidate the general belief about the validity of signing certificates for author attribution. For instance, we find that apps from different authors share signing certificates due to the proliferation of app building frameworks and software factories. Finally, we introduce the concept of an attribution graph and we apply it to evaluate the validity of existing attribution signals on the Google Play Store. Our results confirm that the lack of control over publicly available signals can confuse automatic attribution processes.
  • No Spring Chicken: Quantifying the Lifespan of Exploits in IoT Malware Using Static and Dynamic Analysis
    Al Alsadi, A. A., Sameshima, K., Bleier, J., Yoshioka, K., Lindorfer, M., van Eeten, M., & Hernández Gañán, C. (2022). No Spring Chicken: Quantifying the Lifespan of Exploits in IoT Malware Using Static and Dynamic Analysis. In Yuji Suga, Kouichi Sakurai, Xuhua Ding, & Kazue Sako (Eds.), ASIA CCS ’22: Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security (pp. 309–321). Association for Computing Machinery.
    DOI: 10.1145/3488932.3517408 Metadata
    Abstract
    The Internet of things (IoT) is composed by a wide variety of software and hardware components that inherently contain vulnerabilities. Previous research has shown that it takes only a few minutes from the moment an IoT device is connected to the Internet to the first infection attempts. Still, we know little about the evolution of exploit vectors: Which vulnerabilities are being targeted in the wild, how has the functionality changed over time, and for how long are vulnerabilities being targeted? Understanding these questions can help in the secure development, and deployment of IoT networks. We present the first longitudinal study of IoT malware exploits by analyzing 17,720 samples collected from three different sources from 2015 to 2020. Leveraging static and dynamic analysis, we extract exploits from these binaries to then analyze them along the following four dimensions: (1) evolution of infection vectors over the years, (2) exploit lifespan, vulnerability age, and the time-to-exploit of vulnerabilities, (3) functionality of exploits, and (4) targeted IoT devices and manufacturers. Our descriptive analysis uncovers several patterns: IoT malware keeps evolving, shifting from simply leveraging brute force attacks to including dozens of device-specific exploits. Once exploits are developed, they are rarely abandoned. The most recent binaries still target (very) old vulnerabilities. In some cases, new exploits are developed for a vulnerability that has been known for years. We find that the mean time-to-exploit after vulnerability disclosure is around 29 months, much longer than for malware targeting other environments.
  • Not that Simple: Email Delivery in the 21st Century
    Holzbauer, F., Ullrich, J., Lindorfer, M., & Fiebig, T. (2022). Not that Simple: Email Delivery in the 21st Century. In Proceedings of the 2022 USENIX Annual Technical Conference (pp. 295–308). USENIX Association.
    DOI: 10.34726/4024 Metadata
    Abstract
    Over the past two decades, the number of RFCs related to email and its security has exploded from below 100 to nearly 500. This embedded the Simple Mail Transfer Protocol (SMTP) into a tree of interdependent and delivery-relevant standards. In this paper, we investigate how far real-world deployments keep up with this increasing complexity of delivery- and security options. To gain an in-depth picture of email delivery apart from the giants in the ecosystem (Gmail, Outlook, etc.), we engage people to send emails to eleven differently configured target domains. Our measurements allow us to evaluate core aspects of email delivery, including security features, DNS configuration, and IP version support on the sending side across different types of providers. We find that novel technologies are often insufficiently supported, even by large providers. For example, while 65.4% of email providers can resolve hosts via IPv6, only 44.3% can also deliver emails via IPv6. Concerning security features, we observe that less than half (41.5%) of all providers rely on DNSSEC validating resolvers, and encryption is mostly opportunistic, with 89.7% of providers accepting invalid certificates. TLSA, as a DNS-based certificate verification method, is only used by 31.7% of the providers in our study. Finally, we turned our eye to the impact modern standards have on unsolicited bulk email (SPAM). We found that greylisting is effective, reducing the SPAM volume by roughly half while not impacting regular delivery. However, and interestingly, SPAM delivery currently seems to focus on plaintext IPv4 connections, making IPv6-only, TLS-enforcing inbound email servers a more effective anti-SPAM measure—even though it also means rejecting a major portion of legitimate emails.
  • Not Your Average App: A Large-scale Privacy Analysis of Android Browsers
    Pradeep, A., Feal, Á., Gamba, J., Rao, A., Lindorfer, M., Vallina-Rodriguez, N., & Choffnes, D. (2023). Not Your Average App: A Large-scale Privacy Analysis of Android Browsers. In M. L. Mazurek & M. Sherr (Eds.), Proceedings on Privacy Enhancing Technologies Symposium 2023 (pp. 29–46).
    DOI: 10.56553/popets-2023-0003 Metadata
    Abstract
    The privacy-related behavior of mobile browsers has remained widely unexplored by the research community. In fact, as opposed to regular Android apps, mobile browsers may present contradicting privacy behaviors. On the one hand, they can have access to (and can expose) a unique combination of sensitive user data, from users’ browsing history to permission-protected personally identifiable information (PII) such as unique identifiers and geolocation. On the other hand, they are in a unique position to protect users’ privacy by limiting data sharing with other parties by implementing ad- blocking features. In this paper, we perform a comparative and empirical analysis on how hundreds of Android web browsers protect or expose user data during browsing sessions. To this end, we collect the largest dataset of Android browsers to date, from the Google Play Store and four Chinese app stores. Then, we develop a novel analysis pipeline that combines static and dynamic analysis methods to find a wide range of privacy-enhancing (e.g., ad-blocking) and privacy-harming behaviors (e.g., sending browsing histories to third parties, not validating TLS certificates, and exposing PII—including non-resettable identifiers—to third parties) across browsers. We find that various popular apps on both Google Play and Chinese stores have these privacy-harming behaviors, including apps that claim to be privacy-enhancing in their descriptions. Overall, our study not only provides new insights into important yet overlooked considerations for browsers’ adoption and transparency, but also that automatic app analysis systems (e.g., sandboxes) need context-specific analysis to reveal such privacy behaviors.
  • Of Ahead Time: Evaluating Disassembly of Android Apps Compiled to Binary OATs Through the ART
    Bleier, J., & Lindorfer, M. (2023). Of Ahead Time: Evaluating Disassembly of Android Apps Compiled to Binary OATs Through the ART. In J. Polakis & E. van der Kouwe (Eds.), EUROSEC ’23: Proceedings of the 16th European Workshop on System Security (pp. 21–29).
    DOI: 10.1145/3578357.3591219 Metadata
    Abstract
    The Android operating system has evolved significantly since its initial release in 2008. Most importantly, in a continuing effort to increase the run-time performance of mobile applications (apps) and to reduce resource requirements, the way code is executed has transformed from being bytecode-based to a binary-based approach: Apps are still mainly distributed as Dalvik bytecode, but the Android Runtime (ART) uses an optimizing compiler to create binary code ahead-of-time (AOT), just-in-time (JIT), or as a combination of both. These changes in the build pipeline, including increasing obfuscation and optimization of the Dalvik bytecode, invalidate assumptions of bytecode-based static code analysis approaches through identifier renaming and code shrinking. Furthermore, customized apps can be distributed pre-compiled with devices’ firmware, sidestepping the bytecode altogether. Finally, Android apps have always relied on native binary code libraries for performance-critical tasks. We propose to narrow the gap between bytecode and binary code by leveraging the ART compiler’s capability to create well-formed ELF binaries, called OATs, as the basis for further static code analysis. To this end, we created a pipeline to automatically and efficiently compile APKs to OATs into a benchmark dataset of 1,339 apps. We then evaluate five popular disassemblers based on how well they can analyze these OATs based on how well they can detect function boundaries. Our results, in particular, compared to the success rate of two bytecode-based analyzers, demonstrate that our OAT-based approach can help to bring a wider set of code analysis tools and techniques to the area of Android app analysis.
  • Tarnhelm: Isolated, Transparent & Confidential Execution of Arbitrary Code in ARM's TrustZone
    Quarta, D., Ianni, M., Machiry, A., Fratantonio, Y., Gustafson, E., Balzarotti, D., Lindorfer, M., Vigna, G., & Kruegel, C. (2021). Tarnhelm: Isolated, Transparent & Confidential Execution of Arbitrary Code in ARM’s TrustZone. In Proceedings of the 2021 Research on offensive and defensive techniques in the Context of Man At The End (MATE) Attacks. ACM, Austria. ACM.
    DOI: 10.1145/3465413.3488571 Metadata ⯈Fulltext (preprint)
    Abstract
    Protecting the confidentiality of applications on commodity operating systems, both on desktop and mobile devices, is challenging: attackers have unrestricted control over an application´s processes and thus direct access to any of the application´s assets. However, the application´s code itself can be of great commercial value, for example in the case of proprietary code or additional functionality obtained as downloadable content and via in-app purchases, which are widely used to monetize free applications through premium content. Developers still rely heavily on obfuscation to protect their own code from unauthorized tampering or copying, providing an obstacle for an attacker, but not preventing compromise. In this paper, we present Tarnhelm, an approach to offer a practical and transparent primitive to implement code confidentiality by extending ARM´s TrustZone, a TEE that so far provides limited functionality to application developers. Tarnhelm allows develop- ers to easily designate part of their code as confidential through source code annotations. At compile time, Tarnhelm automatically partitions the application into regular application code, executed in the "normal world," and the invisible code, transparently executed in the "secure world." Tarnhelm tightly couples and secures the execution in both worlds without exposing any additional attack surface by combining a number of different techniques, such as secure code loading, system call forwarding, transparent world switching, and the enforcement of inter-world control-flow integrity. We implemented a proof of concept of Tarnhelm and demonstrate its feasibility in a mobile computing setting.

CoRaF

A Composable Rational Framework for Blockchain Systems

2022 – 2025 •  Austrian Science Fund (FWF)  •  PI Georgia Avarikioti
Abstract

Bitcoin marked the beginning of a new era in digital finance; the data structure known as the blockchain enabled financial transactions to be executed in a secure decentralized manner, therefore revolutionizing the financial landscape. Blockchains naturally form environments where the participants act for profit (i.e., participants are rational). Nevertheless, current works typically analyze the security of blockchain protocols in the traditional setting where some of the participants are malicious and the rest are honest as there is no general framework to analyze blockchains from a rational perspective. Furthermore, blockchain systems are complex and consist of several components that handle different performance aspects, such as the network layer or Layer 0, the consensus layer or Layer 1, and the off-chain network or Layer 2. All these layers interact with each other and the security of each layer depends on the security of its substrate layer and vice versa. Therefore, the composition of protocols in the blockchain setting is vital for the security guarantees and the correct operation of cryptocurrencies. The goal of this project is to introduce a composable framework for the security analysis of blockchain protocols under a hybrid model of both rational and malicious participants. This is a significant yet currently missing tool with impact across multiple disciplines such as computer science and economics.

Browsec

Foundations and Tools for Client-Side Web Security

2018 – 2024 •  European Research Council (ERC)  •  PI Matteo Maffei
Abstract

The constantly increasing number of attacks on web applications shows how their rapid development has not been accompanied by adequate security foundations and demonstrates the lack of solid security enforcement tools. Indeed, web applications expose a gigantic attack surface, which hinders a rigorous understanding and enforcement of security properties. Hence, despite the worthwhile efforts to design secure web applications, users for a while will be confronted with vulnerable, or maliciously crafted, code. Unfortunately, end users have no way at present to reliably protect themselves from malicious applications. BROWSEC will develop a holistic approach to client-side web security, laying its theoretical foundations and developing innovative security enforcement technologies. In particular, BROWSEC will deliver the first client-side tool to secure web applications that is practical, in that it is implemented as an efficient and easily deployable browser extension, and also provably sound, i.e., backed up by machine-checked proofs that the tool provides end users with the required security guarantees. At the core of the proposal lies a novel monitoring technique, which treats the browser as a blackbox and intercepts its inputs and outputs in order to prevent dangerous information flows. With this lightweight monitoring approach, we aim at enforcing strong security properties without requiring any expensive and, given the dynamic nature of web applications, statically infeasible program analysis.

BROWSEC is thus a multidisciplinary research effort, promising practical impact and delivering breakthrough advancements in various disciplines, such as web security, JavaScript semantics, software engineering, and program verification.

Partners
  • Wolfgang Pauli Institute, Wien, Austria
Publications
  • Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2022, August 31). Blitz: Secure Multi-Hop Payments Without Two-Phase Commits [Conference Presentation]. The Science of Blockchain Conference 2022, Stanford, United States of America (the).
    Metadata
  • Breaking and Fixing Virtual Channels: Domino Attack and Donner
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2023). Breaking and Fixing Virtual Channels: Domino Attack and Donner. In Proceedings Network and Distributed System Security Symposium 2023. 30th Annual Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    DOI: 10.14722/ndss.2023.24370 Metadata
    Abstract
    Payment channel networks (PCNs) mitigate the scalability issues of current decentralized cryptocurrencies. They allow for arbitrarily many payments between users connected through a path of intermediate payment channels, while requiring interacting with the blockchain only to open and close the channels. Unfortunately, PCNs are (i) tailored to payments, excluding more complex smart contract functionalities, such as the oracle-enabling Discreet Log Contracts and (ii) their need for active participation from intermediaries may make payments unreliable, slower, expensive, and privacy-invasive. Virtual channels are among the most promising techniques to mitigate these issues, allowing two endpoints of a path to create a direct channel over the intermediaries without any interaction with the blockchain. After such a virtual channel is constructed, (i) the endpoints can use this direct channel for applications other than payments and (ii) the intermediaries are no longer involved in updates. In this work, we first introduce the Domino attack, a new DoS/griefing style attack that leverages virtual channels to destruct the PCN itself and is inherent to the design adopted by the existing Bitcoin-compatible virtual channels. We then demonstrate its severity by a quantitative analysis on a snapshot of the Lightning Network (LN), the most widely deployed PCN at present. We finally discuss other serious drawbacks of existing virtual channel designs, such as the support for only a single intermediary, a latency and blockchain overhead linear in the path length, or a non-constant storage overhead per user. We then present Donner, the first virtual channel construction that overcomes the shortcomings above, by relying on a novel design paradigm. We formally define and prove security and privacy properties in the Universal Composability framework. Our evaluation shows that Donner is efficient, reduces the on-chain number of transactions for disputes from linear in the path length to a single one, which is the key to prevent Domino attacks, and reduces the storage overhead from logarithmic in the path length to constant. Donner is Bitcoin-compatible and can be easily integrated in the LN.
  • Breaking and Fixing Virtual Channels: Domino Attack and Donner
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2023, September 6). Breaking and Fixing Virtual Channels: Domino Attack and Donner [Presentation]. VISA Research - external research talks, Palo Alto, United States of America (the).
    Metadata
  • Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph
    Chatterjee, D., Banerjee, P., & Subhra Mazumdar. (2023). Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph. arXiv.
    DOI: 10.34726/5301 Metadata
    Abstract
    Hash-based Proof-of-Work (PoW) used in the Bitcoin Blockchain leads to high energy consumption and resource wastage. In this paper, we aim to re-purpose the energy by replacing the hash function with real-life problems having commercial utility. We propose Chrisimos, a useful Proof-of-Work where miners are required to find a minimal dominating set for real-life graph instances. A miner who is able to output the smallest dominating set for the given graph within the block interval time wins the mining game. We also propose a new chain selection rule that ensures the security of the scheme. Thus our protocol also realizes a decentralized minimal dominating set solver for any graph instance. We provide formal proof of correctness and show via experimental results that the block interval time is within feasible bounds of hash-based PoW.
  • Cookie Crumbles: Breaking and Fixing Web Session Integrity
    Marco Squarcina, Adão, P., Lorenzo Veronese, & Matteo Maffei. (2023). Cookie Crumbles: Breaking and Fixing Web Session Integrity. In J. Calandrino & C. Troncoso (Eds.), SEC ’23: Proceedings of the 32nd USENIX Conference on Security Symposium (pp. 5539–5556). USENIX Association.
    DOI: 10.34726/5329 Metadata
    Abstract
    Cookies have a long history of vulnerabilities targeting their confidentiality and integrity. To address these issues, new mechanisms have been proposed and implemented in browsers and server-side applications. Notably, improvements to the Secure attribute and cookie prefixes aim to strengthen cookie integrity against network and same-site attackers, whereas SameSite cookies have been touted as the solution to CSRF. On the server, token-based protections are considered an effective defense for CSRF in the synchronizer token pattern variant. In this paper, we question the effectiveness of these protections and study the real-world security implications of cookie integrity issues, showing how security mechanisms previously considered robust can be bypassed, exposing Web applications to session integrity attacks such as session fixation and cross-origin request forgery (CORF). These flaws are not only implementation-specific bugs but are also caused by compositionality issues of security mechanisms or vulnerabilities in the standard. Our research contributed to 12 CVEs, 27 vulnerability disclosures, and updates to the cookie standard. It comprises (i) a thorough cross-browser evaluation of cookie integrity issues, that results in new attacks originating from implementation or specification inconsistencies, and (ii) a security analysis of the top 13 Web frameworks, exposing session integrity vulnerabilities in 9 of them. We discuss our responsible disclosure and propose practical mitigations.
  • Foundations of Coin Mixing Services
    Glaeser, N., Maffei, M., Malavolta, G., Moreno-Sanchez, P., Tairi, E., & Thyagarajan, S. A. (2022). Foundations of Coin Mixing Services. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 1259–1273). Association for Computing Machinery.
    DOI: 10.34726/3601 Metadata
    Abstract
    Coin mixing services allow users to mix their cryptocurrency coins and thus enable unlinkable payments in a way that prevents tracking of honest users' coins by both the service provider and the users themselves. The easy bootstrapping of new users and backwards compatibility with cryptocurrencies (such as Bitcoin) with limited support for scripts are attractive features of this architecture, which has recently gained considerable attention in both academia and industry. A recent work of Tairi et al. [IEEE S&P 2021] formalizes the notion of a coin mixing service and proposes A2L, a new cryptographic protocol that simultaneously achieves high efficiency and interoperability. In this work, we identify a gap in their formal model and substantiate the issue by showing two concrete counterexamples: we show how to construct two encryption schemes that satisfy their definitions but lead to a completely insecure system. To amend this situation, we investigate secure constructions of coin mixing services. First, we develop the notion of blind conditional signatures (BCS), which acts as the cryptographic core for coin mixing services. We propose game-based security definitions for BCS and propose A2L+, a modified version of the protocol by Tairi et al. that satisfies our security definitions. Our analysis is in an idealized model (akin to the algebraic group model) and assumes the hardness of the one-more discrete logarithm problem. Finally, we propose A2L-UC, another construction of BCS that achieves the stronger notion of UC-security (in the standard model), albeit with a significant increase in computation cost. This suggests that constructing a coin mixing service protocol secure under composition requires more complex cryptographic machinery than initially thought.
  • Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures
    Aumayr, L., Oguzhan Ersoy, Erwig, A., Faust, S., Hostáková, K., Maffei, M., Moreno-Sanchez, P., & Riahi, S. (2022, August 30). Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures [Conference Presentation]. The Science of Blockchain Conference 2022, Stanford, United States of America (the).
    Metadata
  • Glimpse: On-Demand PoW Light Client with Constant-Size Storage for DeFi
    Scaffino, G., Aumayr, L., Avarikioti, G., & Maffei, M. (2023). Glimpse: On-Demand PoW Light Client with Constant-Size Storage for DeFi. In Proceedings of the 32nd USENIX Security Symposium (pp. 733–750).
    Metadata
    Abstract
    Cross-chain communication is instrumental in unleashing the full potential of blockchain technologies, as it allows users and developers to exploit the unique design features and the profit opportunities of different existing blockchains. The majority of interoperability solutions are provided by centralized exchanges and bridge protocols based on a trusted majority, both introducing undesirable trust assumptions compared to native blockchain assets. Hence, increasing attention has been given to decentralized solutions: Light and super-light clients paved the way for chain relays, which allow verifying on a blockchain the state of another blockchain by respectively verifying and storing a linear and logarithmic amount of data. Unfortunately, relays turn out to be inefficient in terms of computational costs, storage, or compatibility. We introduce Glimpse, an on-demand bridge that leverages a novel on-demand light client construction with only constant on-chain storage, cost, and computational overhead. Glimpse is expressive, enabling a plethora of DeFi and off-chain applications such as lending, pegs, proofs of oracle attestations, and betting hubs. Glimpse also remains compatible with blockchains featuring a limited scripting language such as the Liquid Network (a pegged sidechain of Bitcoin), for which we present a concrete instantiation. We prove Glimpse security in the Universal Composability (UC) framework and further conduct an economic analysis. We evaluate the cost of Glimpse for Bitcoin-like chains: verifying a simple transaction has at most 700 bytes of on-chain overhead, resulting in a one-time fee of $3, only twice as much as a standard Bitcoin transaction.
  • LightSwap: An Atomic Swap Does Not Require Timeouts At Both Blockchains
    Hoenisch, P., Mazumdar, S., Moreno-Sanchez, P., & Ruj, S. (2022). LightSwap: An Atomic Swap Does Not Require Timeouts At Both Blockchains. Cryptology ePrint Archive.
    DOI: 10.34726/3662 Metadata
    Abstract
    Security and privacy issues with centralized exchange services have motivated the design of atomic swap protocols for decentralized trading across currencies. These protocols follow a standard blueprint similar to the 2-phase commit in databases: (i) both users first lock their coins under a certain (cryptographic) condition and a timeout; (ii-a) the coins are swapped if the condition is fulfilled; or (ii-b) coins are released after the timeout. The quest for these protocols is to minimize the requirements from the scripting language supported by the swapped coins, thereby supporting a larger range of cryptocurrencies. The recently proposed universal atomic swap protocol [IEEE S&P’22] demonstrates how to swap coins whose scripting language only supports the verification of a digital signature on a transaction. However, the timeout functionality is cryptographically simulated with verifiable timelock puzzles, a computationally expensive primitive that hinders its use in battery-constrained devices such as mobile phones. In this state of affairs, we question whether the 2-phase commit paradigm is necessary for atomic swaps in the first place. In other words, is it possible to design a secure atomic swap protocol where the timeout is not used by (at least one of the two) users? In this work, we present LightSwap, the first secure atomic swap protocol that does not require the timeout functionality (not even in the form of a cryptographic puzzle) by one of the two users. LightSwap is thus better suited for scenarios where a user, running an instance of LightSwap on her mobile phone, wants to exchange coins with an online exchange service running an instance of LightSwap on a computer. We show how LightSwap can be used to swap Bitcoin and Monero, an interesting use case since Monero does not provide any scripting functionality support other than linkable ring signature verification.
  • Rigorous Methods for Smart Contracts
    Bjørner, N., Christakis, M., Maffei, M., & Rosu, G. (Eds.). (2022). Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing.
    DOI: 10.4230/DagRep.11.9.80 Metadata
    Abstract
    This report documents the program and the outcomes of Dagstuhl Seminar 21431 “Rigorous Methods for Smart Contracts”. Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a “once in a lifetime” opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management. Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.
  • SecWasm: Information Flow Control for WebAssembly
    Bastys, I., Algehed, M., Sjösten, A., & Sabelfeld, A. (2022). SecWasm: Information Flow Control for WebAssembly. In Static Analysis (pp. 74–103). Springer Nature Switzerland AG.
    DOI: 10.1007/978-3-031-22308-2_5 Metadata
    Abstract
    We introduce SecWasm, the first general purpose information-flow control system for WebAssembly (Wasm), thus extending the safety guarantees offered by Wasm with guarantees that applications manipulate sensitive data in a secure way. SecWasm is a hybrid system enforcing termination-insensitive noninterference which overcomes the challenges posed by the uncommon characteristics for machine languages of Wasm in an elegant and thorough way.
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Thyagarajan, S. A., Malavolta, G., Moreno-Sanchez, P., & Maffei, M. (2022). Sleepy Channels: Bi-directional Payment Channels without Watchtowers. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 179–192). Association for Computing Machinery.
    DOI: 10.1145/3548606.3559370 Metadata
    Abstract
    Payment channels (PC) are a promising solution to the scalability issue of cryptocurrencies, allowing users to perform the bulk of the transactions off-chain without needing to post everything on the blockchain. Many PC proposals however, suffer from a severe limitation: Both parties need to constantly monitor the blockchain to ensure that the other party did not post an outdated transaction. If this event happens, the honest party needs to react promptly and engage in a punishment procedure. This means that prolonged absence periods (e.g., a power outage) may be exploited by malicious users. As a mitigation, the community has introduced watchtowers, a third-party monitoring the blockchain on behalf of off-line users. Unfortunately, watchtowers are either trusted, which is critical from a security perspective, or they have to lock a certain amount of coins, called collateral, for each monitored PC in order to be held accountable, which is financially infeasible for a large network. We present Sleepy Channels, the first bi-directional PC protocol without watchtowers (or any other third party) that supports an unbounded number of payments and does not require parties to be persistently online. The key idea is to confine the period in which PC updates can be validated on-chain to a short, pre-determined time window, which is when the PC parties have to be online. This behavior is incentivized by letting the parties lock a collateral in the PC, which can be adjusted depending on their mutual trust and which they get back much sooner if they are online during this time window. Our protocol is compatible with any blockchain that is capable of verifying digital signatures (e.g., Bitcoin), as shown by our proof of concept. Moreover, our experimental results show that Sleepy Channels impose a communication and computation overhead similar to state-of-the-art PC protocols while removing watchtower's collateral and fees for the monitoring service.
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2022, October 31). Sleepy Channels: Bi-directional Payment Channels without Watchtowers [Poster Presentation]. Crypto Economics Security Conference, Berkeley, United States of America (the).
    Metadata
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2023, February 28). Sleepy Channels: Bi-directional Payment Channels without Watchtowers [Poster Presentation]. Network and Distributed System Security Symposium (NDSS) 2023, United States of America (the).
    Metadata
  • Sleepy Channels: Bitcoin-Compatible Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2023, August 30). Sleepy Channels: Bitcoin-Compatible Bi-directional Payment Channels without Watchtowers [Conference Presentation]. The Science of Blockchain Conference 2023, Stanford, United States of America (the).
    Metadata
  • Strategic Analysis of Griefing Attack in Lightning Network
    Mazumdar, S., Banerjee, P., Sinha, A., Ruj, S., & Roy, B. (2022). Strategic Analysis of Griefing Attack in Lightning Network. IEEE Transactions on Network and Service Management.
    DOI: 10.34726/3581 Metadata
    Abstract
    Hashed Timelock Contract (HTLC) in Lightning Network is susceptible to a griefing attack. An attacker can block several channels and stall payments by mounting this attack. A state-of-the-art countermeasure, Hashed Timelock Contract with Griefing-Penalty (HTLC-GP) is found to work under the classical assumption of participants being either honest or malicious but fails for rational participants. To address the gap, we introduce a game-theoretic model for analyzing griefing attacks in HTLC. We use this model to analyze griefing attacks in HTLC-GP and conjecture that it is impossible to design an efficient protocol that will penalize a malicious participant with the current Bitcoin scripting system. We study the impact of the penalty on the cost of mounting the attack and observe that HTLC-GP is weakly effective in disincentivizing the attacker in certain conditions. To further increase the cost of attack, we introduce the concept of guaranteed minimum compensation, denoted as ζ, and modify HTLC-GP into HTLC-GPζ. By experimenting on several instances of Lightning Network, we observe that the total coins locked in the network drops to 28% for HTLC-GPζ, unlike in HTLC-GP where total coins locked does not drop below 40%. These results justify that HTLC-GPζ is better than HTLC-GP to counter griefing attacks.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2022). Thora: Atomic and Privacy-Preserving Multi-Channel Updates. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 165–178). Association for Computing Machinery.
    DOI: 10.1145/3548606.3560556 Metadata
    Abstract
    Most blockchain-based cryptocurrencies suffer from a heavily limited transaction throughput, which is a barrier to their growing adoption. Payment channel networks (PCNs) are one of the promising solutions to this problem. PCNs reduce the on-chain load of transactions and increase the throughput by processing many payments off-chain. In fact, any two users connected via a path of payment channels (i.e., joint addresses between the two channel end-points) can perform payments, and the underlying blockchain is used only when there is a dispute between users. Unfortunately, payments in PCNs can only be conducted securely along a path, which prevents the design of many interesting applications. Moreover, the most widely used implementation, the Lightning Network in Bitcoin, suffers from a collateral lock time linear in the path length, it is affected by security issues, and it relies on specific scripting features called Hash Timelock Contracts that hinders the applicability of the underlying protocol in other blockchains. In this work, we present Thora, the first Bitcoin-compatible off-chain protocol that enables the atomic update of arbitrary channels (i.e., not necessarily forming a path). This enables the design of a number of new off-chain applications, such as payments across different PCNs sharing the same blockchain, secure and trustless crowdfunding, and channel rebalancing. Our construction requires no specific scripting functionalities other than digital signatures and timelocks, thereby being applicable to a wider range of blockchains. We formally define security and privacy in the Universal Composability framework and show that our cryptographic protocol is a realization thereof. In our performance evaluation, we show that our construction requires only constant collateral, independently from the number of channels, and has only a moderate off-chain communication as well as computation overhead.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2023, February 28). Thora: Atomic and Privacy-Preserving Multi-Channel Updates [Poster Presentation]. Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    Metadata
    Abstract
    Most blockchain-based cryptocurrencies suffer from a heavily limited transaction throughput, which is a barrier to their growing adoption. Payment channel networks (PCNs) are one of the promising solutions to this problem. PCNs reduce the on-chain load of transactions and increase the throughput by processing many payments off-chain. In fact, any two users connected via a path of payment channels (i.e., joint addresses between the two channel end-points) can perform payments, and the underlying blockchain is used only when there is a dispute between users. Unfortunately, payments in PCNs can only be conducted securely along a path, which prevents the design of many interesting applications. Moreover, the most widely used implementation, the Lightning Network in Bitcoin, suffers from a collateral lock time linear in the path length, it is affected by security issues, and it relies on specific scripting features called Hash Timelock Contracts that hinders the applicability of the underlying protocol in other blockchains. In this work, we present Thora, the first Bitcoin-compatible off-chain protocol that enables the atomic update of arbitrary channels (i.e., not necessarily forming a path). This enables the design of a number of new off-chain applications, such as payments across different PCNs sharing the same blockchain, secure and trustless crowdfunding, and channel rebalancing. Our construction requires no specific scripting functionalities other than digital signatures and timelocks, thereby being applicable to a wider range of blockchains. We formally define security and privacy in the Universal Composability framework and show that our cryptographic protocol is a realization thereof. In our performance evaluation, we show that our construction requires only constant collateral, independently from the number of channels, and has only a moderate off-chain communication as well as computation overhead.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2023, August 30). Thora: Atomic and Privacy-Preserving Multi-Channel Updates [Conference Presentation]. The Science of Blockchain Conference 2023 (SBC’23), Stanford University, United States of America (the).
    Metadata
  • Thora: Atomic And Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Kasra Abbaszadeh, & Maffei, M. (2022, October 31). Thora: Atomic And Privacy-Preserving Multi-Channel Updates [Poster Presentation]. Crypto Economics Security Conference, Berkeley, United States of America (the).
    Metadata
  • Towards a Game-Theoretic Security Analysis of Off-Chain Protocols
    Rain, S., Avarikioti, G., Kovacs, L., & Maffei, M. (2023). Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 107–122). IEEE.
    DOI: 10.1109/CSF57540.2023.00003 Metadata
    Abstract
    Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. In this work we take a first step towards a principled game-theoretic security analysis of off-chain protocols by introducing the first game-theoretic model that is expressive enough to reason about their security. We advocate the use of Extensive Form Games (EFGs) and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize parties to upload old channel states on-chain. Moreover, we model the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network.
  • Towards faster settlement in HTLC-based Cross-Chain Atomic Swaps
    Mazumdar, S. (2022). Towards faster settlement in HTLC-based Cross-Chain Atomic Swaps. arXiv.
    DOI: 10.34726/3805 Metadata
    Abstract
    Hashed Timelock (HTLC)-based atomic swap protocols enable the exchange of coins between two or more parties without relying on a trusted entity. This protocol is like the American call option without premium. It allows the finalization of a deal within a certain period. This puts the swap initiator at liberty to delay before deciding to proceed with the deal. If she finds the deal unprofitable, she just waits for the time-period of the contract to elapse. However, the counterparty is at a loss since his assets remain locked in the contract. The best he can do is to predict the initiator's behavior based on the asset's price fluctuation in the future. But it is difficult to predict as cryptocurrencies are quite volatile, and their price fluctuates abruptly. We perform a game theoretic analysis of HTLC-based atomic cross-chain swap to predict whether a swap will succeed or not. From the strategic behavior of the players, we infer that this model lacks fairness. We propose Quick Swap, a two-party protocol based on hashlock and timelock that fosters faster settlement of the swap. The parties are required to lock griefing-premium along with the principal amount. If the party griefs, he ends up paying the griefing-premium. If a party finds a deal unfavorable, he has the provision to cancel the swap. We prove that Quick Swap is more participant-friendly than HTLC-based atomic swap. Our work is the first to propose a protocol to ensure fairness of atomic-swap in a cyclic multi-party setting.
  • WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms
    Veronese, L., Farinier, B., Bernardo, P., Tempesta, M., Squarcina, M., & Maffei, M. (2023). WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms. In 2023 IEEE Symposium on Security and Privacy (SP) (pp. 2761–2779). IEEE.
    DOI: 10.1109/SP46215.2023.10179465 Metadata
    Abstract
    The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a toolchain turning the Coq model and the Web invariants into SMT-lib formulas to enable model checking with the Z3 theorem prover. If a violation is found, the toolchain automatically generates executable tests corresponding to the discovered attack trace, which is validated across major browsers.We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.

SPFBT

Security and Privacy Foundations of Blockchain Technologies

2020 – 2024 •  SBA Research gemeinnützige GmbH  •  PI Matteo Maffei
Abstract

Blockchains are emerging as a disruptive technology for securing transactions and computations across mutually distrustful peers. The security and privacy of blockchains, however, depends on a complicated combination of cryptography, programming languages, game theory, distributed systems, and network concepts, which is not well understood. The goal of this project is to lay sound foundations for blockchain technologies, devising techniques for their provable analysis and design.

DLDaI

Distributed Ledger Development and Implementation

2022 – 2024 •  ABC Research GmbH  •  PI Matteo Maffei
Abstract

PROFET

Cryptographic Foundations for Future-proof Internet Security

2019 – 2023 •  Austrian Science Fund (FWF)  •  PI Matteo Maffei
Abstract

Today, much of our personal freedom and the power to guarantee and maintain a free society depends on cryptographic primitives (e.g., digital signatures and encryption) incorporated in the security protocols of today's Internet used for securing many daily tasks such as messaging, online banking or sending e-mails. While anticipated regulations like the upcoming EU General Data Protection Regulation (GDPR) promote the usage of cryptography to protect sensitive data, revelations about activities of governmental agencies have revealed worryingly information. Examples include subverting cryptographic software products, subverting certification authorities, backdooring cryptographic schemes, or influencing and weakening cryptographic standardization processes. Besides providing governmental institutions means to spy on citizens, such practices are highly vulnerable to also be exploited by non-governmental attackers.

Many of the public-key cryptographic schemes used to secure today's Internet were not designed with the functionality and the security requirements in mind that come along with tomorrow's envisioned use-cases on the Internet. This requires novel and typically more advanced cryptographic schemes that consider aspects that were not known or of interest in the early days of the Internet. Cryptography for a future-proof Internet needs to consider a potentially huge number of devices to which data is communicated simultaneously and shared selectively and needs to be flexible enough to work on both ends of the spectrum, i.e., resource constrained IoT devices as well as cloud-powered services. What is more, new security aspects such as readiness for a post-quantum era as well as the increasing importance of cryptographic schemes which are resilient against threats due to subversion as well as surveillance (as mentioned before) are of high relevance.

PROFET targets at designing public-key cryptography capable to secure tomorrow's Internet which will encompass paradigms such as cloud computing, the IoT and distributed ledgers as essential ingredients. We thereby want to specifically put our focus on two highly important issues for the future: (1) designing security models and cryptographic schemes that are surveillance and subversion resilient by design, e.g., provide strong notions such as forward security and post-compromise security, and (2) designing cryptographic schemes that remain secure in the presence of powerful quantum computers, i.e., schemes that provide post-quantum security. We will on the one hand work on foundational aspects, but also investigate the application of our techniques to certain problems encountered in the IoT and cloud application scenarios.

ViSP

Vienna Cybersecurity and Privacy Research Center

2019 – 2023 •  Vienna Business Agency (WAW)  •  PI Matteo Maffei
Abstract

The aim of ViSP is to break down the silos and boost the existing research synergies among the partner institutions, to establish a graduate educational program in cybersecurity and privacy, and to create all together an internationally leading research and educational brand for cybersecurity and privacy in Vienna.

While the primary goals are research excellence and education, ViSP will have a significant impact on industry and regional development. Cybersecurity and privacy expertise is extremely required by enterprises, which open branches and labs in close proximity to research centers and universities leading in this field, due to the availability of the required know-how, possibilities of technology transfer, and access to specialized students. Cybersecurity and privacy are also a flourishing field worldwide for startups created by students during or at the end of their studies, which will be promoted and mentored in the incubation phase by ViSP.

The ultimate goal is to establish Vienna as the place to be for cybersecurity and privacy research in Europe. Besides the central location and the excellent quality of life, the unique selling point of the Viennese landscape in the cybersecurity and privacy domain is the unmatchable concentration of research excellence (as witnessed, e.g., by the 6 ERC grants in this field, all joining ViSP, which has no equal in Europe) and the number of universities and research centers active in this field, which however requires a consolidation effort to emerge internationally as a leading location.

Partners
  • Ruhr-Universität Bochum, Bochum, Germany
Publications
  • Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2022, August 31). Blitz: Secure Multi-Hop Payments Without Two-Phase Commits [Conference Presentation]. The Science of Blockchain Conference 2022, Stanford, United States of America (the).
    Metadata
  • Breaking and Fixing Virtual Channels: Domino Attack and Donner
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2023). Breaking and Fixing Virtual Channels: Domino Attack and Donner. In Proceedings Network and Distributed System Security Symposium 2023. 30th Annual Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    DOI: 10.14722/ndss.2023.24370 Metadata
    Abstract
    Payment channel networks (PCNs) mitigate the scalability issues of current decentralized cryptocurrencies. They allow for arbitrarily many payments between users connected through a path of intermediate payment channels, while requiring interacting with the blockchain only to open and close the channels. Unfortunately, PCNs are (i) tailored to payments, excluding more complex smart contract functionalities, such as the oracle-enabling Discreet Log Contracts and (ii) their need for active participation from intermediaries may make payments unreliable, slower, expensive, and privacy-invasive. Virtual channels are among the most promising techniques to mitigate these issues, allowing two endpoints of a path to create a direct channel over the intermediaries without any interaction with the blockchain. After such a virtual channel is constructed, (i) the endpoints can use this direct channel for applications other than payments and (ii) the intermediaries are no longer involved in updates. In this work, we first introduce the Domino attack, a new DoS/griefing style attack that leverages virtual channels to destruct the PCN itself and is inherent to the design adopted by the existing Bitcoin-compatible virtual channels. We then demonstrate its severity by a quantitative analysis on a snapshot of the Lightning Network (LN), the most widely deployed PCN at present. We finally discuss other serious drawbacks of existing virtual channel designs, such as the support for only a single intermediary, a latency and blockchain overhead linear in the path length, or a non-constant storage overhead per user. We then present Donner, the first virtual channel construction that overcomes the shortcomings above, by relying on a novel design paradigm. We formally define and prove security and privacy properties in the Universal Composability framework. Our evaluation shows that Donner is efficient, reduces the on-chain number of transactions for disputes from linear in the path length to a single one, which is the key to prevent Domino attacks, and reduces the storage overhead from logarithmic in the path length to constant. Donner is Bitcoin-compatible and can be easily integrated in the LN.
  • Breaking and Fixing Virtual Channels: Domino Attack and Donner
    Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2023, September 6). Breaking and Fixing Virtual Channels: Domino Attack and Donner [Presentation]. VISA Research - external research talks, Palo Alto, United States of America (the).
    Metadata
  • Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph
    Chatterjee, D., Banerjee, P., & Subhra Mazumdar. (2023). Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph. arXiv.
    DOI: 10.34726/5301 Metadata
    Abstract
    Hash-based Proof-of-Work (PoW) used in the Bitcoin Blockchain leads to high energy consumption and resource wastage. In this paper, we aim to re-purpose the energy by replacing the hash function with real-life problems having commercial utility. We propose Chrisimos, a useful Proof-of-Work where miners are required to find a minimal dominating set for real-life graph instances. A miner who is able to output the smallest dominating set for the given graph within the block interval time wins the mining game. We also propose a new chain selection rule that ensures the security of the scheme. Thus our protocol also realizes a decentralized minimal dominating set solver for any graph instance. We provide formal proof of correctness and show via experimental results that the block interval time is within feasible bounds of hash-based PoW.
  • Cookie Crumbles: Breaking and Fixing Web Session Integrity
    Marco Squarcina, Adão, P., Lorenzo Veronese, & Matteo Maffei. (2023). Cookie Crumbles: Breaking and Fixing Web Session Integrity. In J. Calandrino & C. Troncoso (Eds.), SEC ’23: Proceedings of the 32nd USENIX Conference on Security Symposium (pp. 5539–5556). USENIX Association.
    DOI: 10.34726/5329 Metadata
    Abstract
    Cookies have a long history of vulnerabilities targeting their confidentiality and integrity. To address these issues, new mechanisms have been proposed and implemented in browsers and server-side applications. Notably, improvements to the Secure attribute and cookie prefixes aim to strengthen cookie integrity against network and same-site attackers, whereas SameSite cookies have been touted as the solution to CSRF. On the server, token-based protections are considered an effective defense for CSRF in the synchronizer token pattern variant. In this paper, we question the effectiveness of these protections and study the real-world security implications of cookie integrity issues, showing how security mechanisms previously considered robust can be bypassed, exposing Web applications to session integrity attacks such as session fixation and cross-origin request forgery (CORF). These flaws are not only implementation-specific bugs but are also caused by compositionality issues of security mechanisms or vulnerabilities in the standard. Our research contributed to 12 CVEs, 27 vulnerability disclosures, and updates to the cookie standard. It comprises (i) a thorough cross-browser evaluation of cookie integrity issues, that results in new attacks originating from implementation or specification inconsistencies, and (ii) a security analysis of the top 13 Web frameworks, exposing session integrity vulnerabilities in 9 of them. We discuss our responsible disclosure and propose practical mitigations.
  • Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures
    Aumayr, L., Oguzhan Ersoy, Erwig, A., Faust, S., Hostáková, K., Maffei, M., Moreno-Sanchez, P., & Riahi, S. (2022, August 30). Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures [Conference Presentation]. The Science of Blockchain Conference 2022, Stanford, United States of America (the).
    Metadata
  • Hide & Seek: Privacy-Preserving Rebalancing on Payment Channel Networks
    Avarikioti, G., Pietrzak, K., Salem, I., Schmid, S., Tiwari, S., & Yeo, M. (2022). Hide & Seek: Privacy-Preserving Rebalancing on Payment Channel Networks. In I. Eyal & J. Garay (Eds.), Financial Cryptography and Data Security (pp. 358–373). Springer-Verlag.
    DOI: 10.1007/978-3-031-18283-9_17 Metadata
    Abstract
    Payment channels effectively move the transaction load off-chain thereby successfully addressing the inherent scalability problem most cryptocurrencies face. A major drawback of payment channels is the need to “top up” funds on-chain when a channel is depleted. Rebalancing was proposed to alleviate this issue, where parties with depleting channels move their funds along a cycle to replenish their channels off-chain. Protocols for rebalancing so far either introduce local solutions or compromise privacy. In this work, we present an opt-in rebalancing protocol that is both private and globally optimal, meaning our protocol maximizes the total amount of rebalanced funds. We study rebalancing from the framework of linear programming. To obtain full privacy guarantees, we leverage multi-party computation in solving the linear program, which is executed by selected participants to maintain efficiency. Finally, we efficiently decompose the rebalancing solution into incentive-compatible cycles which conserve user balances when executed atomically.
  • LightSwap: An Atomic Swap Does Not Require Timeouts At Both Blockchains
    Hoenisch, P., Mazumdar, S., Moreno-Sanchez, P., & Ruj, S. (2022). LightSwap: An Atomic Swap Does Not Require Timeouts At Both Blockchains. Cryptology ePrint Archive.
    DOI: 10.34726/3662 Metadata
    Abstract
    Security and privacy issues with centralized exchange services have motivated the design of atomic swap protocols for decentralized trading across currencies. These protocols follow a standard blueprint similar to the 2-phase commit in databases: (i) both users first lock their coins under a certain (cryptographic) condition and a timeout; (ii-a) the coins are swapped if the condition is fulfilled; or (ii-b) coins are released after the timeout. The quest for these protocols is to minimize the requirements from the scripting language supported by the swapped coins, thereby supporting a larger range of cryptocurrencies. The recently proposed universal atomic swap protocol [IEEE S&P’22] demonstrates how to swap coins whose scripting language only supports the verification of a digital signature on a transaction. However, the timeout functionality is cryptographically simulated with verifiable timelock puzzles, a computationally expensive primitive that hinders its use in battery-constrained devices such as mobile phones. In this state of affairs, we question whether the 2-phase commit paradigm is necessary for atomic swaps in the first place. In other words, is it possible to design a secure atomic swap protocol where the timeout is not used by (at least one of the two) users? In this work, we present LightSwap, the first secure atomic swap protocol that does not require the timeout functionality (not even in the form of a cryptographic puzzle) by one of the two users. LightSwap is thus better suited for scenarios where a user, running an instance of LightSwap on her mobile phone, wants to exchange coins with an online exchange service running an instance of LightSwap on a computer. We show how LightSwap can be used to swap Bitcoin and Monero, an interesting use case since Monero does not provide any scripting functionality support other than linkable ring signature verification.
  • SecWasm: Information Flow Control for WebAssembly
    Bastys, I., Algehed, M., Sjösten, A., & Sabelfeld, A. (2022). SecWasm: Information Flow Control for WebAssembly. In Static Analysis (pp. 74–103). Springer Nature Switzerland AG.
    DOI: 10.1007/978-3-031-22308-2_5 Metadata
    Abstract
    We introduce SecWasm, the first general purpose information-flow control system for WebAssembly (Wasm), thus extending the safety guarantees offered by Wasm with guarantees that applications manipulate sensitive data in a secure way. SecWasm is a hybrid system enforcing termination-insensitive noninterference which overcomes the challenges posed by the uncommon characteristics for machine languages of Wasm in an elegant and thorough way.
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Thyagarajan, S. A., Malavolta, G., Moreno-Sanchez, P., & Maffei, M. (2022). Sleepy Channels: Bi-directional Payment Channels without Watchtowers. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 179–192). Association for Computing Machinery.
    DOI: 10.1145/3548606.3559370 Metadata
    Abstract
    Payment channels (PC) are a promising solution to the scalability issue of cryptocurrencies, allowing users to perform the bulk of the transactions off-chain without needing to post everything on the blockchain. Many PC proposals however, suffer from a severe limitation: Both parties need to constantly monitor the blockchain to ensure that the other party did not post an outdated transaction. If this event happens, the honest party needs to react promptly and engage in a punishment procedure. This means that prolonged absence periods (e.g., a power outage) may be exploited by malicious users. As a mitigation, the community has introduced watchtowers, a third-party monitoring the blockchain on behalf of off-line users. Unfortunately, watchtowers are either trusted, which is critical from a security perspective, or they have to lock a certain amount of coins, called collateral, for each monitored PC in order to be held accountable, which is financially infeasible for a large network. We present Sleepy Channels, the first bi-directional PC protocol without watchtowers (or any other third party) that supports an unbounded number of payments and does not require parties to be persistently online. The key idea is to confine the period in which PC updates can be validated on-chain to a short, pre-determined time window, which is when the PC parties have to be online. This behavior is incentivized by letting the parties lock a collateral in the PC, which can be adjusted depending on their mutual trust and which they get back much sooner if they are online during this time window. Our protocol is compatible with any blockchain that is capable of verifying digital signatures (e.g., Bitcoin), as shown by our proof of concept. Moreover, our experimental results show that Sleepy Channels impose a communication and computation overhead similar to state-of-the-art PC protocols while removing watchtower's collateral and fees for the monitoring service.
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2022, October 31). Sleepy Channels: Bi-directional Payment Channels without Watchtowers [Poster Presentation]. Crypto Economics Security Conference, Berkeley, United States of America (the).
    Metadata
  • Sleepy Channels: Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2023, February 28). Sleepy Channels: Bi-directional Payment Channels without Watchtowers [Poster Presentation]. Network and Distributed System Security Symposium (NDSS) 2023, United States of America (the).
    Metadata
  • Sleepy Channels: Bitcoin-Compatible Bi-directional Payment Channels without Watchtowers
    Aumayr, L., Sri AravindaKrishnan Thyagarajan, Giulio Malavolta, Moreno-Sanchez, P., & Maffei, M. (2023, August 30). Sleepy Channels: Bitcoin-Compatible Bi-directional Payment Channels without Watchtowers [Conference Presentation]. The Science of Blockchain Conference 2023, Stanford, United States of America (the).
    Metadata
  • Strategic Analysis of Griefing Attack in Lightning Network
    Mazumdar, S., Banerjee, P., Sinha, A., Ruj, S., & Roy, B. (2022). Strategic Analysis of Griefing Attack in Lightning Network. IEEE Transactions on Network and Service Management.
    DOI: 10.34726/3581 Metadata
    Abstract
    Hashed Timelock Contract (HTLC) in Lightning Network is susceptible to a griefing attack. An attacker can block several channels and stall payments by mounting this attack. A state-of-the-art countermeasure, Hashed Timelock Contract with Griefing-Penalty (HTLC-GP) is found to work under the classical assumption of participants being either honest or malicious but fails for rational participants. To address the gap, we introduce a game-theoretic model for analyzing griefing attacks in HTLC. We use this model to analyze griefing attacks in HTLC-GP and conjecture that it is impossible to design an efficient protocol that will penalize a malicious participant with the current Bitcoin scripting system. We study the impact of the penalty on the cost of mounting the attack and observe that HTLC-GP is weakly effective in disincentivizing the attacker in certain conditions. To further increase the cost of attack, we introduce the concept of guaranteed minimum compensation, denoted as ζ, and modify HTLC-GP into HTLC-GPζ. By experimenting on several instances of Lightning Network, we observe that the total coins locked in the network drops to 28% for HTLC-GPζ, unlike in HTLC-GP where total coins locked does not drop below 40%. These results justify that HTLC-GPζ is better than HTLC-GP to counter griefing attacks.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2022). Thora: Atomic and Privacy-Preserving Multi-Channel Updates. In CCS ’22: Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (pp. 165–178). Association for Computing Machinery.
    DOI: 10.1145/3548606.3560556 Metadata
    Abstract
    Most blockchain-based cryptocurrencies suffer from a heavily limited transaction throughput, which is a barrier to their growing adoption. Payment channel networks (PCNs) are one of the promising solutions to this problem. PCNs reduce the on-chain load of transactions and increase the throughput by processing many payments off-chain. In fact, any two users connected via a path of payment channels (i.e., joint addresses between the two channel end-points) can perform payments, and the underlying blockchain is used only when there is a dispute between users. Unfortunately, payments in PCNs can only be conducted securely along a path, which prevents the design of many interesting applications. Moreover, the most widely used implementation, the Lightning Network in Bitcoin, suffers from a collateral lock time linear in the path length, it is affected by security issues, and it relies on specific scripting features called Hash Timelock Contracts that hinders the applicability of the underlying protocol in other blockchains. In this work, we present Thora, the first Bitcoin-compatible off-chain protocol that enables the atomic update of arbitrary channels (i.e., not necessarily forming a path). This enables the design of a number of new off-chain applications, such as payments across different PCNs sharing the same blockchain, secure and trustless crowdfunding, and channel rebalancing. Our construction requires no specific scripting functionalities other than digital signatures and timelocks, thereby being applicable to a wider range of blockchains. We formally define security and privacy in the Universal Composability framework and show that our cryptographic protocol is a realization thereof. In our performance evaluation, we show that our construction requires only constant collateral, independently from the number of channels, and has only a moderate off-chain communication as well as computation overhead.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2023, February 28). Thora: Atomic and Privacy-Preserving Multi-Channel Updates [Poster Presentation]. Network and Distributed System Security Symposium (NDSS) 2023, San Diego, United States of America (the).
    Metadata
    Abstract
    Most blockchain-based cryptocurrencies suffer from a heavily limited transaction throughput, which is a barrier to their growing adoption. Payment channel networks (PCNs) are one of the promising solutions to this problem. PCNs reduce the on-chain load of transactions and increase the throughput by processing many payments off-chain. In fact, any two users connected via a path of payment channels (i.e., joint addresses between the two channel end-points) can perform payments, and the underlying blockchain is used only when there is a dispute between users. Unfortunately, payments in PCNs can only be conducted securely along a path, which prevents the design of many interesting applications. Moreover, the most widely used implementation, the Lightning Network in Bitcoin, suffers from a collateral lock time linear in the path length, it is affected by security issues, and it relies on specific scripting features called Hash Timelock Contracts that hinders the applicability of the underlying protocol in other blockchains. In this work, we present Thora, the first Bitcoin-compatible off-chain protocol that enables the atomic update of arbitrary channels (i.e., not necessarily forming a path). This enables the design of a number of new off-chain applications, such as payments across different PCNs sharing the same blockchain, secure and trustless crowdfunding, and channel rebalancing. Our construction requires no specific scripting functionalities other than digital signatures and timelocks, thereby being applicable to a wider range of blockchains. We formally define security and privacy in the Universal Composability framework and show that our cryptographic protocol is a realization thereof. In our performance evaluation, we show that our construction requires only constant collateral, independently from the number of channels, and has only a moderate off-chain communication as well as computation overhead.
  • Thora: Atomic and Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Abbaszadeh, K., & Maffei, M. (2023, August 30). Thora: Atomic and Privacy-Preserving Multi-Channel Updates [Conference Presentation]. The Science of Blockchain Conference 2023 (SBC’23), Stanford University, United States of America (the).
    Metadata
  • Thora: Atomic And Privacy-Preserving Multi-Channel Updates
    Aumayr, L., Kasra Abbaszadeh, & Maffei, M. (2022, October 31). Thora: Atomic And Privacy-Preserving Multi-Channel Updates [Poster Presentation]. Crypto Economics Security Conference, Berkeley, United States of America (the).
    Metadata
  • Towards a Game-Theoretic Security Analysis of Off-Chain Protocols
    Rain, S., Avarikioti, G., Kovacs, L., & Maffei, M. (2023). Towards a Game-Theoretic Security Analysis of Off-Chain Protocols. In 2023 IEEE 36th Computer Security Foundations Symposium (CSF) (pp. 107–122). IEEE.
    DOI: 10.1109/CSF57540.2023.00003 Metadata
    Abstract
    Off-chain protocols constitute one of the most promising approaches to solve the inherent scalability issue of blockchain technologies. The core idea is to let parties transact on-chain only once to establish a channel between them, leveraging later on the resulting channel paths to perform arbitrarily many peer-to-peer transactions off-chain. While significant progress has been made in terms of proof techniques for off-chain protocols, existing approaches do not capture the game-theoretic incentives at the core of their design, which led to overlooking significant attack vectors like the Wormhole attack in the past. In this work we take a first step towards a principled game-theoretic security analysis of off-chain protocols by introducing the first game-theoretic model that is expressive enough to reason about their security. We advocate the use of Extensive Form Games (EFGs) and introduce two instances of EFGs to capture security properties of the closing and the routing of the Lightning Network. Specifically, we model the closing protocol, which relies on punishment mechanisms to disincentivize parties to upload old channel states on-chain. Moreover, we model the routing protocol, thereby formally characterizing the Wormhole attack, a vulnerability that undermines the fee-based incentive mechanism underlying the Lightning Network.
  • Towards faster settlement in HTLC-based Cross-Chain Atomic Swaps
    Mazumdar, S. (2022). Towards faster settlement in HTLC-based Cross-Chain Atomic Swaps. arXiv.
    DOI: 10.34726/3805 Metadata
    Abstract
    Hashed Timelock (HTLC)-based atomic swap protocols enable the exchange of coins between two or more parties without relying on a trusted entity. This protocol is like the American call option without premium. It allows the finalization of a deal within a certain period. This puts the swap initiator at liberty to delay before deciding to proceed with the deal. If she finds the deal unprofitable, she just waits for the time-period of the contract to elapse. However, the counterparty is at a loss since his assets remain locked in the contract. The best he can do is to predict the initiator's behavior based on the asset's price fluctuation in the future. But it is difficult to predict as cryptocurrencies are quite volatile, and their price fluctuates abruptly. We perform a game theoretic analysis of HTLC-based atomic cross-chain swap to predict whether a swap will succeed or not. From the strategic behavior of the players, we infer that this model lacks fairness. We propose Quick Swap, a two-party protocol based on hashlock and timelock that fosters faster settlement of the swap. The parties are required to lock griefing-premium along with the principal amount. If the party griefs, he ends up paying the griefing-premium. If a party finds a deal unfavorable, he has the provision to cancel the swap. We prove that Quick Swap is more participant-friendly than HTLC-based atomic swap. Our work is the first to propose a protocol to ensure fairness of atomic-swap in a cyclic multi-party setting.
  • WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms
    Veronese, L., Farinier, B., Bernardo, P., Tempesta, M., Squarcina, M., & Maffei, M. (2023). WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms. In 2023 IEEE Symposium on Security and Privacy (SP) (pp. 2761–2779). IEEE.
    DOI: 10.1109/SP46215.2023.10179465 Metadata
    Abstract
    The complexity of browsers has steadily increased over the years, driven by the continuous introduction and update of Web platform components, such as novel Web APIs and security mechanisms. Their specifications are manually reviewed by experts to identify potential security issues. However, this process has proved to be error-prone due to the extensiveness of modern browser specifications and the interplay between new and existing Web platform components. To tackle this problem, we developed WebSpec, the first formal security framework for the analysis of browser security mechanisms, which enables both the automatic discovery of logical flaws and the development of machine-checked security proofs. WebSpec, in particular, includes a comprehensive semantic model of the browser in the Coq proof assistant, a formalization in this model of ten Web security invariants, and a toolchain turning the Coq model and the Web invariants into SMT-lib formulas to enable model checking with the Z3 theorem prover. If a violation is found, the toolchain automatically generates executable tests corresponding to the discovered attack trace, which is validated across major browsers.We showcase the effectiveness of WebSpec by discovering two new logical flaws caused by the interaction of different browser mechanisms and by identifying three previously discovered logical flaws in the current Web platform, as well as five in old versions. Finally, we show how WebSpec can aid the verification of our proposed changes to amend the reported inconsistencies affecting the current Web platform.
  • Wiser: Increasing Throughput in Payment Channel Networks with Transaction Aggregation
    Tiwari, S., Yeo, M., Avarikioti, G., Salem, I., Pietrzak, K., & Schmid, S. (2022). Wiser: Increasing Throughput in Payment Channel Networks with Transaction Aggregation. In AFT ’22: Proceedings of the 4th ACM Conference on Advances in Financial Technologies (pp. 217–231). Association for Computing Machinery.
    DOI: 10.1145/3558535.3559775 Metadata
    Abstract
    Payment channel networks (PCNs) are one of the most prominent solutions to the limited transaction throughput of blockchains. Nevertheless, PCNs suffer themselves from a throughput limitation due to the capital constraints of their channels. A similar dependence on high capital is also found in inter-bank payment settlements, where the so-called netting technique is used to mitigate liquidity demands. In this work, we alleviate this limitation by introducing the notion of transaction aggregation: instead of executing transactions sequentially through a PCN, we enable senders to aggregate multiple transactions and execute them simultaneously to benefit from several amounts that may "cancel out". Two direct advantages of our proposal is the decrease in intermediary fees paid by senders as well as the obfuscation of the transaction data from the intermediaries. We formulate the transaction aggregation as a computational problem, a generalization of the Bank Clearing Problem. We present a generic framework for the transaction aggregation execution, and thereafter we propose Wiser as an implementation of this framework in a specific hub-based setting. To overcome the NP-hardness of the transaction aggregation problem, in Wiser we propose a fixed-parameter linear algorithm for a special case of transaction aggregation as well as the Bank Clearing Problem. Wiser can also be seen as a modern variant of the Hawala money transfer system, as well as a decentralized implementation of the overseas remittance service of Wise.

PR4DLT

Privacy-Preserving Regulatory Technologies for Distributed Ledger Technologies

2018 – 2021 •  Austrian Research Promotion Agency (FFG)  •  PI Matteo Maffei
Abstract

The rise of cryptocurrencies and their underlying distributed ledger technologies (DLT), commonly referred to as blockchains, has captured the interest of diverse communities, science and market alike. Decentralized cryptocurrencies, such as Bitcoin, are increasingly perceived as viable alternatives to classical payment methods. In March 2017, the monetary value of a "bitcoin" surpassed the value of an ounce of gold for the first time 1. Different countries all over the world are currently experimenting with incorporating cryptocurrencies into their regulatory framework. The classification and regulatory requirements when engaging with Bitcoin still varies by country or territory 2. In May 2016, the muncipality of Zug (Switzerland) started to accept Bitcoin payments for government services 3. In April 2017, Japan became the first country in the world to recognize Bitcoin as a legal method of payment 4. Australia is planning to follow soon 5. Such developments introduce new regulatory compliance requirements for financial institutions, businesses, individuals and the public sector. For instance, legally recognizing digital assets secured by a DLT as a payment method implies that compliance rules against money laundering also need to come into effect. This new state of affairs generates a conflict between decentralized, cross-national, and potentially anonymous transactions facilitated by DLT on the one side, and the need for their regulation and taxation at national-level jurisdictions on the other side. The underlying technologies themselves may currently render it difficult, if not infeasible, to implement certain regulatory requirements 6. Regulatory Technology or RegTech is a subclass of FinTech (i.e., Financial Technologies) and refers to the use of information technology in the context of regulatory monitoring, reporting, and compliance from which the finance industry benefits. How can RegTech cope efficiently with DLT-based assets and their underlying technologies? This project, PR4DLT, aims to address this question by performing basic research in the area of privacy-preserving regulatory technologies in the context of distributed ledgers to derive the appropriate theoretical and technical foundations for their practical application. Thereby, basic building blocks for future regulatory technologies are created that can serve as a starting point as well as a construction kit for implementing different compliance requirements in a secure and privacy-preserving way. PR4DLT addresses the question of how Blockchain- and Distributed Ledger Technologies can comply with potential future regulations from a technical viewpoint, while at the same time maintaining decentralization and privacy characteristics as far as possible.

SP-PCN

Security and Privacy for Payment-Channel Networks

2019 – 2020 •  Austrian Science Fund (FWF)
Abstract

Bitcoin sparked the blockchain ecosystem and has been followed by a plethora of blockchain approaches. Their growing expectations and usage is at odds with their scalability. Bitcoin today supports tens of transaction per second, a rate far from satisfactory to cater the current demand. Unfortunately, this is not an isolated symptom from Bitcoin but an epidemic problem with blockchain today. The most promising scalability solution today are payment channels: Two users leverage a single on-chain transaction to establish a shared deposit of coins. Subsequent payments are performed off-chain by agreeing on an updated deposits balance. Finally, only one additional on-chain transaction is required to close the deposit in the blockchain. Leveraging paths of payment channels, a payment-channel network allow any two users to pay each other. Unfortunately, current payment-channel networks at are their infancy and more work is required to bring them to minimum standards for mass adoption with proper security and privacy guarantees. In this state of affairs, the focus of this project is two-fold: (WP1) studying the theoretical possibilities and limits of payment-channel networks for mass adoption with sufficient security and privacy guarantees; (WP2) laying the foundations for payment-channel networks applications in order to release all their potential. WP1 is divided in three tasks: (a) set the foundations of security and privacy for payment channels. Simplified transaction formats augment the probability of success at providing security and privacy guarantees while reducing the amount of information to be stored at the blockchain. This is definitely a mandatory requirement given the current scalability issues; (b) set the foundations for offline users in payment-channel networks. Current approaches require that all users are always online, a requirement that clearly hinders their deployment in practice as users come and go as they please; (c) set the foundations of interoperable payment channels. Current isolated blockchains clearly restrict their potential. By providing interoperable protocols, we plan to release the whole potential of payment-channel networks. WP2 is also divided in three tasks: (a) build payment-channels secure against stronger adversaries such as quantum attackers; (b) build payment-channel networks over privacy-preserving cryptocurrencies such as Monero or Zcash, an open problem today that however would pave the way for better privacy guarantees; (c) build currency exchange protocols to support seamless exchanges of not only coins but any other good that can be represented in the blockchain, a main use case hindered today due to the isolation of different blockchains. Therefore, this project will provide the missing foundations and constructions to bring payment-channel networks into a solid state that can get mass adoption as scalability solution.

SLN

Scalability for Lightning Networks

2018 – 2020 •  Chaincode Labs Inc  •  PI Matteo Maffei
Abstract

The Bitcoin blockchain provides a transaction rate of tens of transactions per second, far below what is needed to cater the growing number of transactions in the Bitcoin ecosystem. This constitutes a systematic scalability issue that is not unique to Bitcoin, as it is applicable to other blockchains as well. In this state of affairs, off-chain contracts have emerged as the most widely adopted scalability solution. Current deployments such as the Lightning Network have demonstrated that off-chain contracts (e.g., payment channels) can interact with each other to enable off-chain applications such as decentralized off-chain payments. Despite the indisputable advantages provided by off-chain contracts, they still present several challenges that are understudied and yet are crucial to successfully support off-chain applications. In this project, we plan to lay the foundations for off-chain contracts and study the possibilities and theoretical limits with this technology.

Ethertrust

Ethertrust - Trustworthy smart contracts

2018 – 2019 •  netidee.at  •  PI Matteo Maffei
Abstract

(German) Die Kryptowährung Ethereum erlaubt Nutzern neben der Tätigung von Finanztransaktionen auch die Ausführung beliebiger Programme so genannter smart contracts (ESC). Da ESC Finanzflüsse steuern, können Programmfehler schnell zu hohen Verlusten führen. Für den Nutzer sind solche Fehler oder sogar absichtlich implementierte schädliche Verhaltensweisen aus dem Code des Vertrages jedoch kaum ersichtlich. In unserer aktuellen Forschung entwickeln wir eine statische Analyse-Methode, die es erlaubt automatisch zu beweisen, dass ein ESC bestimmte schädliche Eigenschaften nicht besitzt. Aus dieser Methode entwickeln wir einen Online-Service, der es Nutzern von Ethereum ermöglicht ihre eigenen Verträge oder solche, mit denen sie interagieren wollen, automatisch zu analysieren. Unser Ziel ist ein intuitiv bedienbares Online-Tool, bei dem die Nutzer die betreffenden Verträge hochladen, aus einem Pool Eigenschaften wählen können und anschließend verständliche Analyseresultate erhalten.