2024

• (Inner-product) functional encryption with updatable ciphertexts
  Cini, V., Ramacher, S., Slamanig, D., Striecks, C., & Tairi, E. (2024). (Inner-product) functional encryption with updatable ciphertexts. Journal of Cryptology, 37, Article 8.
  DOI: 10.1007/s00145-023-09486-y Metadata
  

  Abstract

  We propose a novel variant of functional encryption which supports ciphertext updates, dubbed ciphertext-updatable functional encryption. Such a feature further broadens the practical applicability of the functional encryption paradigm and allows for fine-grained access control even after a ciphertext is generated. Updating ciphertexts is carried out via so-called update tokens which a dedicated party can use to convert ciphertexts. However, allowing update tokens requires some care for the security definition. Our contribution is threefold: (a) We define our new primitive with a security notion in the indistinguishability setting. Within CUFE, functional decryption keys and ciphertexts are labeled with tags such that only if the tags of the decryption key and the ciphertext match, then decryption succeeds. Furthermore, we allow ciphertexts to switch their tags to any other tag via update tokens. Such tokens are generated by the holder of the main secret key and can only be used in the desired direction. (b) We present a generic construction of CUFE for any functionality as well as predicates different from equality testing on tags which relies on the existence of indistinguishability obfuscation (iO). (c) We present a practical construction of CUFE for the inner-product functionality from standard assumptions (i.e., LWE) in the random-oracle model. On the technical level, we build on the recent functional encryption schemes with fine-grained access control and linear operations on encrypted data (Abdalla et al., AC’20) and introduce an additional ciphertext updatability feature. Proving security for such a construction turned out to be non-trivial, particularly when revealing keys for the updated challenge ciphertext is allowed. Overall, such construction enriches the set of known inner-product functional encryption schemes with the additional updatability feature of ciphertexts.
• 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.
• 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.

2023

• Non-interactive Mimblewimble transactions, revisited
  Fuchsbauer, G., & Orrù, M. (2023). Non-interactive Mimblewimble transactions, revisited. In Advances in Cryptology - ASIACRYPT 2022 (pp. 713–744). Springer.
  DOI: 10.1007/978-3-031-22963-3_24 Metadata
• SNACKs: Leveraging Proofs of Sequential Work for Blockchain Light Clients
  Abusalah, H., Fuchsbauer, G., Gazi, P., & Klein, K. (2023). SNACKs: Leveraging Proofs of Sequential Work for Blockchain Light Clients. In Advances in Cryptology - ASIACRYPT 2022 (pp. 806–836). Springer.
  DOI: 10.1007/978-3-031-22963-3_27 Metadata
• 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.
• 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.
• 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.
• Distributed Key Generation with Smart Contracts using zk-SNARKs
  Sober, M., Max Kobelt, Scaffino, G., Kaaser, D., & Schulte, S. (2023). Distributed Key Generation with Smart Contracts using zk-SNARKs. In SAC ’23: Proceedings of the 38th ACM/SIGAPP Symposium on Applied Computing (pp. 231–240). Association for Computing Machinery.
  DOI: 10.34726/4523 Metadata
  

  Abstract

  Distributed Key Generation (DKG) is an extensively researched topic as it is fundamental to threshold cryptosystems. Emerging technologies such as blockchains benefit massively from applying threshold cryptography in consensus protocols, randomness beacons, and threshold signatures. However, blockchains and smart contracts also enable further improvements of DKG protocols by providing a decentralized computation and communication platform. For that reason, we propose a DKG protocol that uses smart contracts to ensure the correct execution of the protocol, allow dynamic participation, and provide crypto-economic incentives to encourage honest behavior. The DKG protocol uses a dispute and key derivation mechanism based on Zero-Knowledge Succinct Non-interactive Arguments of Knowledge (zk-SNARKs) to reduce the costs of applying smart contracts by moving the computations off-chain, where the smart contract only verifies the correctness of the computation.
• How to simulate PLONK: A formal security analysis of a zk-SNARK
  Sefranek, M. (2023). How to simulate PLONK: A formal security analysis of a zk-SNARK [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2023.111120 Metadata
  

  Abstract

  Zero-knowledge proofs enable proving a statement without revealing any information beyond its truth. This paradoxical notion has evolved over the last few decades from a theoretical concept to the wide adoption of highly efficient zero-knowledge proof systems in practice. At the forefront of this development are proof systems called zk-SNARKs, which stands for zero-knowledge succinct non-interactive argument of knowledge. Not only do they avoid multiple rounds of interaction, but zk-SNARKs also offer succinct proofs whose length is much shorter than the size of the proved statement, with some constructions even achieving constant-size proofs. Among the most recent state-of-the-art constructions is the zk-SNARK "PLONK" by Gabizon, Williamson, and Ciobotaru from 2019. It has constant-size proofs of only half a kilobyte and sublinear proof verification time. Furthermore, it only requires a single trusted setup of its public parameters to support proofs of any statement up to a certain size bound, making PLONK a universal and fully succinct zk-SNARK. Although highly influential and implemented in several real-world applications, there is no formal security proof of its zero knowledge property. In this thesis, we disclose a vulnerability found in PLONK's implementation of zero knowledge and propose how to fix it. As a result, the PLONK protocol has been patched accordingly. Our primary contribution is a formal security proof establishing that the resulting version of PLONK achieves statistical zero knowledge. Towards this goal, we show how to simulate proofs up to an exponentially small difference without relying on any secret information used by the prover. Following the standard definition of zero knowledge, this implies that PLONK proofs reveal (statistically) zero information beyond the truth of the statement. Moreover, we conduct a rigorous security analysis of the entire PLONK protocol, proving the security of all its underlying components. This allows us to show a precise upper bound on PLONK's knowledge soundness error in the algebraic group model. Since the original proof given by the authors of PLONK relies on the same idealized model, our results help towards a better understanding of the security guarantees of PLONK in general.
• 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.
• 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.
• 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
• Back-to-the-Future Whois: An IP Address Attribution Service for Working with Historic Datasets
  Streibelt, F., Lindorfer, M., Gürses, S., Hernández Gañán, C., & Fiebig, T. (2023). Back-to-the-Future Whois: An IP Address Attribution Service for Working with Historic Datasets. In Passive and Active Measurement : 24th International Conference, PAM 2023, Virtual Event, March 21–23, 2023, Proceedings (pp. 209–226). Springer.
  DOI: 10.1007/978-3-031-28486-1_10 Metadata
  

  Abstract

  Researchers and practitioners often face the issue of having to attribute an IP address to an organization. For current data this is comparably easy, using services like whois or other databases. Similarly, for historic data, several entities like the RIPE NCC provide websites that provide access to historic records. For large-scale network measurement work, though, researchers often have to attribute millions of addresses. For current data, Team Cymru provides a bulk whois service which allows bulk address attribution. However, at the time of writing, there is no service available that allows historic bulk attribution of IP addresses. Hence, in this paper, we introduce and evaluate our ‘Back-to-the-Future whois’ service, allowing historic bulk attribution of IP addresses on a daily granularity based on CAIDA Routeviews aggregates. We provide this service to the community for free, and also share our implementation so researchers can run instances themselves.
• 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
• Virtual Payment Channel Networks in Cryptocurrencies
  Aumayr, L. (2023, October 12). Virtual Payment Channel Networks in Cryptocurrencies [Presentation]. Lunchtime Seminar, Universität Innsbruck, Austria.
  Metadata
  

  Abstract

  Permissionless cryptocurrencies like Bitcoin are revolutionary but come with limitations - notably, they can handle only an extremely limited number of transactions per second. Enter Payment Channel Networks (PCNs), which let two users exchange numerous transactions with a minimal blockchain footprint. Imagine it as setting up a temporary tab with a friend, recording the final result instead of each tiny transaction. But PCNs are not perfect. They often require the use of intermediaries for routing payments, which means added fees and potential privacy concerns. Furthermore, their design primarily supports payments, leaving out numerous other fascinating blockchain applications. In this talk, we will dive into these challenges and introduce virtual channels (VCs) - a novel approach designed to address these limitations. VCs allow users to bypass intermediaries with temporary, off-chain channels and can host a wider range of applications, thus providing a cheap and generic solution for having scalable applications on Bitcoin and other cryptocurrencies
• On the impossbility of proving security of equivalence class signatures from computational assumptions
  Regen, F. (2023). On the impossbility of proving security of equivalence class signatures from computational assumptions [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2023.116107 Metadata
  

  Abstract

  Equivalence class signatures (EQS) are digital signatures which provide the additional functionality that lets users adapt a given signature to a related message without knowledge of the secret key. They have been used to instantiate numerous cryptographic primitives and increased their efficiency.Unforgeability of the original EQS construction is proven in the generic group model, a theoretical model that treats the underlying group as "ideal". There exist constructions from standard assumptions but those only achieve weak security notions.In this work we strive to answer the question whether EQS schemes which satisfy the original model can be proved secure under standard assumptions with standard techniques. We answer in the negative. There cannot be an efficient security reduction which runs an adversary breaking unforgeability to then break a non-interactive computational assumption. This will be shown by construction of efficient meta-reductions that either break the security of the scheme or said computational problem directly.
• 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.
• 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.
• 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
• Divide & Scale: Formalization and Roadmap to Robust Sharding
  Avarikioti, G., Desjardins, A., Kokoris-Kogias, L., & Wattenhofer, R. (2023). Divide & Scale: Formalization and Roadmap to Robust Sharding. In S. Rajsbaum, A. Balliu, J. Daymude, & D. Olivetti (Eds.), Structural Information and Communication Complexity : 30th International Colloquium, SIROCCO 2023, Alcalá de Henares, Spain, June 6–9, 2023, Proceedings (pp. 199–245). Springer.
  DOI: 10.1007/978-3-031-32733-9_10 Metadata
  

  Abstract

  Sharding distributed ledgers is a promising on-chain solution for scaling blockchains but lacks formal grounds, nurturing skepticism on whether such complex systems can scale blockchains securely. We fill this gap by introducing the first formal framework as well as a roadmap to robust sharding. In particular, we first define the properties sharded distributed ledgers should fulfill. We build upon and extend the Bitcoin backbone protocol by defining consistency and scalability. Consistency encompasses the need for atomic execution of cross-shard transactions to preserve safety, whereas scalability encapsulates the speedup a sharded system can gain in comparison to a non-sharded system. Using our model, we explore the limitations of sharding. We show that a sharded ledger with n participants cannot scale under a fully adaptive adversary, but it can scale up to m shards where $$n=c'm\log m$$, under an epoch-adaptive adversary; the constant $$c'$$ encompasses the trade-off between security and scalability. This is possible only if the sharded ledgers create succinct proofs of the valid state updates at every epoch. We leverage our results to identify the sufficient components for robust sharding, which we incorporate in a protocol abstraction termed Divide & Scale. To demonstrate the power of our framework, we analyze the most prominent sharded blockchains (Elastico, Monoxide, OmniLedger, RapidChain) and pinpoint where they fail to meet the desired properties.
• FnF-BFT: A BFT Protocol with Provable Performance Under Attack
  Avarikioti, G., Heimbach, L., Schmid, R., Vanbever, L., Wattenhofer, R., & Wintermeyer, P. (2023). FnF-BFT: A BFT Protocol with Provable Performance Under Attack. In S. Rajsbaum, A. Balliu, J. Dymude, & D. Olivetti (Eds.), Structural Information and Communication Complexity : 30th International Colloquium, SIROCCO 2023, Alcalá de Henares, Spain, June 6–9, 2023, Proceedings (pp. 165–198). Springer.
  DOI: 10.1007/978-3-031-32733-9_9 Metadata
  

  Abstract

  We introduce FnF-BFT, the first partially synchronous BFT protocol with performance guarantees under truly byzantine attacks during stable networking conditions. At its core, FnF-BFT parallelizes the execution of requests by allowing all replicas to act as leaders independently. Leader parallelization distributes the load over all replicas. Consequently, FnF-BFT fully utilizes all correct replicas’ processing power and increases throughput by overcoming the single-leader bottleneck. We prove lower bounds on FnF-BFT ’s efficiency and performance in synchrony: the amortized communication complexity is linear in the number of replicas and thus competitive with state-of-the-art protocols; FnF-BFT ’s amortized throughput with less than $$\frac{1}{3}$$ byzantine replicas is at least $$\frac{16}{27}$$ th of its best-case throughput. We also provide a proof-of-concept implementation and preliminary evaluation of FnF-BFT.
• 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.
• 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.
• 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.
• 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.
• 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.
• Lightning Creation Games
  Avarikioti, G., Lizurej, T., Michalak, T., & Yeo, M. (2023). Lightning Creation Games. In E. Bertino, B. Li, O. Frieder, & X. Jia (Eds.), 2023 IEEE 43rd International Conference on Distributed Computing Systems (ICDCS 2023) (pp. 603–613). IEEE.
  DOI: 10.1109/ICDCS57875.2023.00037 Metadata
  

  Abstract

  Payment channel networks (PCNs) are a promising solution to the scalability problem of cryptocurrencies. Any two users connected by a payment channel in the network can theoretically send an unbounded number of instant, costless transactions between them. Users who are not directly connected can also transact with each other in a multi-hop fashion. In this work, we study the incentive structure behind the creation of payment channel networks, particularly from the point of view of a single user that wants to join the network. We define a utility function for a new user in terms of expected revenue, expected fees, and the cost of creating channels, and then provide constant factor approximation algorithms that optimise the utility function given a certain budget. Additionally, we take a step back from a single user to the whole network and examine the parameter spaces under which simple graph topologies form a Nash equilibrium.
• 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.
• Quantum cryptanalysis of Farfalle and (generalised) key-alternating Feistel networks
  Hodžić, S., Roy, A., & Andreeva, E. (2023). Quantum cryptanalysis of Farfalle and (generalised) key-alternating Feistel networks. Designs, Codes and Cryptography.
  DOI: 10.1007/s10623-023-01305-6 Metadata
  

  Abstract

  Farfalle is a permutation-based construction for building a pseudorandom function which has been proposed by Bertoni et al. in 2017. In this work, we show that by observing suitable inputs to Farfalle, one can derive various constructions of a periodic function with a period that involves a secret key. As this admits the application of Simon’s algorithm in the so-called Q2 attack model, we further show that in the case when internal rolling function is linear, then the secret key can be extracted under feasible assumptions. Furthermore, using the provided constructions of periodic functions for Farfalle, we show that one can mount forgery attacks on the session-supporting mode for authenticated encryption (Farfalle-SAE) and the synthetic initial value AE mode (Farfalle-SIV). In addition, as the wide block cipher mode Farfalle-WBC is a 4-round Feistel scheme, a quantum distinguisher is constructed in the case when input branches are containing at last two blocks, where length of one block corresponds to the size of a permutation employed in Farfalle (a similar attack can be mounted to Farfalle-WBC-AE). And finally, we consider the problem of extracting a secret round key out of different periods obtained from a (Generalized) Feistel scheme (GFN), which has not been addressed in any of the previous works which consider the application of Simon’s (or Simon-Grover) algorithm to round reduced versions of GFNs. In this part, we assume that the key is added to an input of an inner function utilized in the round function of a given GFN. By applying two different interpolation formulas, we show that one can extract the round key by utilizing amount of different periods which is closely related to the polynomial/algebraic degree of underlying inner function. Our methods can be seen as an extension of existing quantum attacks on key-alternating GFNs based on Simon’s or Simon-Grover algorithms.
• Heads in the Clouds? Measuring Universities’ Migration to Public Clouds: Implications for Privacy & Academic Freedom
  Fiebig, T., Gürses, S., Hernández Gañán, C., Kotkamp, E., Kuipers, F., Lindorfer, M., Prisse, M., & Sari, T. (2023). Heads in the Clouds? Measuring Universities’ Migration to Public Clouds: Implications for Privacy & Academic Freedom. In M. L. Mazurek & M. Sherr (Eds.), Proceedings on Privacy Enhancing Technologies (pp. 117–150). De Gruyter Open / Sciendo.
  DOI: 10.56553/popets-2023-0044 Metadata
  

  Abstract

  With the emergence of remote education and work in universities due to COVID-19, the 'zoomification' of higher education, i.e., the migration of universities to the clouds, reached the public discourse. Ongoing discussions reason about how this shift will take control over students' data away from universities, and may ultimately harm the privacy of researchers and students alike. However, there has been no comprehensive measurement of universities' use of public clouds and reliance on Software-as-a-Service offerings to assess how far this migration has already progressed. We perform a longitudinal study of the migration to public clouds among universities in the U.S. and Europe, as well as institutions listed in the Times Higher Education (THE) Top100 between January 2015 and October 2022. We find that cloud adoption differs between countries, with one cluster (Germany, France, Austria, Switzerland) showing a limited move to clouds, while the other (U.S., U.K., the Netherlands, THE Top100) frequently outsources universities' core functions and services---starting long before the COVID-19 pandemic. We attribute this clustering to several socio-economic factors in the respective countries, including the general culture of higher education and the administrative paradigm taken towards running universities. We then analyze and interpret our results, finding that the implications reach beyond individuals' privacy towards questions of academic independence and integrity.
• 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.
• CryptoMaze: Privacy-Preserving Splitting of Off-Chain Payments
  Mazumdar, S., & Ruj, S. (2023). CryptoMaze: Privacy-Preserving Splitting of Off-Chain Payments. IEEE Transactions on Dependable and Secure Computing, 20(2), 1060–1073.
  DOI: 10.1109/TDSC.2022.3148476 Metadata
  

  Abstract

  Payment Channel Networks or PCNs solve the problem of scalability in Blockchain by executing payments off-chain. Due to a lack of sufficient capacity in the network, high-valued payments are split and routed via multiple paths. Existing multi-path payment protocols either fail to achieve atomicity or are susceptible to wormhole attack. We propose a secure and privacy-preserving atomic multi-path payment protocol CryptoMaze. Our protocol avoids the formation of multiple off-chain contracts on edges shared by the paths routing partial payments. It also guarantees unlinkability between partial payments. We provide a formal definition of the protocol in the Universal Composability framework and analyze the security. We implement CryptoMaze on several instances of Lightning Network and simulated networks. Our protocol requires 11s for routing a payment of 0.04 BTC on a network instance comprising 25600 nodes. The communication cost is less than 1MB in the worst-case. On comparing the performance of CryptoMaze with several state-of-the-art payment protocols, we observed that our protocol outperforms the rest in terms of computational cost and has a feasible communication overhead.
• Describing and Organizing Semantic Web and Machine Learning Systems in the SWeMLS-KG
  Ekaputra, F. J., Llugiqi, M., Sabou, M., Ekelhart, A., Paulheim, H., Breit, A., Revenko, A., Waltersdorfer, L., Farfar, K. E., & Auer, S. (2023). Describing and Organizing Semantic Web and Machine Learning Systems in the SWeMLS-KG. In C. Pesquita, E. Jimenez-Ruiz, J. McCusker, D. Faria, M. Dragoni, A. Dimou, R. Troncy, & S. Hertling (Eds.), The Semantic Web : 20th International Conference, ESWC 2023, Hersonissos, Crete, Greece, May 28–June 1, 2023, Proceedings (pp. 372–389). Springer Cham.
  DOI: 10.1007/978-3-031-33455-9_22 Metadata
  

  Abstract

  The overall AI trend of creating neuro-symbolic systems is reflected in the Semantic Web community with an increased interest in the development of systems that rely on both Semantic Web resources and Machine Learning components (SWeMLS, for short). However, understanding trends and best practices in this rapidly growing field is hampered by a lack of standardized descriptions of these systems and an annotated corpus of such systems. To address these gaps, we leverage the results of a large-scale systematic mapping study collecting information about 470 SWeMLS papers and formalize these into one resource containing: (i) the SWeMLS ontology, (ii) the SWeMLS pattern library containing machine-actionable descriptions of 45 frequently occurring SWeMLS workflows, and (iii) SWEMLS-KG, a knowledge graph including machine-actionable metadata of the papers in terms of the SWeMLS ontology. This resource provides the first framework for semantically describing and organizing SWeMLS thus making a key impact in (1) understanding the status quo of the field based on the published paper corpus and (2) enticing the uptake of machine-processable system documentation in the SWeMLS area.
• Let's Go Eevee! A Friendly and Suitable Family of AEAD Modes for IoT-to-Cloud Secure Computation
  Bhati, A. S., Pohle, E., Abidin, A., Andreeva, E., & Preneel, B. (2023). Let’s Go Eevee! A Friendly and Suitable Family of AEAD Modes for IoT-to-Cloud Secure Computation. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 2546–2560). Association for Computing Machinery.
  DOI: 10.1145/3576915.3623091 Metadata
  

  Abstract

  IoT devices collect privacy-sensitive data, e.g., in smart grids or in medical devices, and send this data to cloud servers for further processing. In order to ensure confidentiality as well as authenticity of the sensor data in the untrusted cloud environment, we consider a transciphering scenario between embedded IoT devices and multiple cloud servers that perform secure multi-party computation (MPC). Concretely, the IoT devices encrypt their data with a lightweight symmetric cipher and send the ciphertext to the cloud servers. To obtain the secret shares of the cleartext message for further processing, the cloud servers engage in an MPC protocol to decrypt the ciphertext in a distributed manner. This way, the plaintext is never exposed to the individual servers. As an important building block in this scenario, we propose a new, provably secure family of lightweight modes for authenticated encryption with associated data (AEAD), called Eevee. The Eevee family has fully parallel decryption, making it suitable for MPC protocols for which the round complexity depends on the complexity of the function they compute. Further, our modes use the lightweight forkcipher primitive that offers fixed-length output expansion and a compact yet parallelizable internal structure. All Eevee members improve substantially over the few available state-of-the-art (SotA) MPC-friendly modes and other standard solutions. We benchmark the Eevee family on a microcontroller and in MPC. Our proposed mode Jolteon (when instantiated with ForkSkinny) provides 1.85x to 3.64x speedup in IoT-encryption time and 3x to 4.5x speedup in both MPC-decryption time and data for very short queries of 8 bytes and, 1.55x to 3.04x and 1.23x to 2.43x speedup, respectively, in MPC-decryption time and data for queries up to 500 bytes when compared against SotA MPC-friendly modes instantiated with SKINNY. We also provide two advanced modes, Umbreon and Espeon, that show a favorable performance-security trade-off with stronger security guarantees such as nonce-misuse security. Additionally, all Eevee members have full n-bit security (where n is the block size of the underlying primitive), use a single primitive and require smaller state and HW area when compared with the SotA modes under their original security settings.
• 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
• 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.
• 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.
• 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.
• LedgerLocks: A Security Framework for Blockchain Protocols Based on Adaptor Signatures
  Tairi, E., Moreno-Sanchez, P., & Schneidewind, C. (2023). LedgerLocks: A Security Framework for Blockchain Protocols Based on Adaptor Signatures. In CCS ’23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 859–873). Association for Computing Machinery.
  DOI: 10.1145/3576915.3623149 Metadata
  

  Abstract

  The scalability and interoperability challenges in current cryptocurrencies have motivated the design of cryptographic protocols that enable efficient applications on top and across widely used cryptocurrencies such as Bitcoin or Ethereum. Examples of such protocols include (virtual) payment channels, atomic swaps, oracle-based contracts, deterministic wallets, and coin mixing services. Many of these protocols are built upon minimal core functionalities supported by a wide range of cryptocurrencies. Most prominently, adaptor signatures (AS) have emerged as a powerful tool for constructing blockchain protocols that are (mostly) agnostic to the specific logic of the underlying cryptocurrency. Even though AS-based protocols are built upon the same cryptographic principles, there exists no modular and faithful way for reasoning about their security. Instead, all the works analyzing such protocols focus on reproving how adaptor signatures are used to cryptographically link transactions while considering highly simplified blockchain models that do not capture security-relevant aspects of transaction execution in blockchain-based consensus. To help this, we present LedgerLocks, a framework for the secure design of AS-based blockchain applications in the presence of a realistic blockchain. LedgerLocks defines the concept of AS-locked transactions, transactions whose publication is bound to the knowledge of a cryptographic secret. We argue that AS-locked transactions are the common building block of AS-based blockchain protocols and we define GLedgerLocks a realistic ledger model in the Universal Composability framework with built-in support for AS-locked transactions. As LedgerLocks abstracts from the cryptographic realization of AS-locked transactions, it allows protocol designers to focus on the blockchain-specific security considerations instead.
• Optimizing 0-RTT Key Exchange with Full Forward Security
  Göth, C., Ramacher, S., Slamanig, D., Striecks, C., Tairi, E., & Zikulnig, A. (2023). Optimizing 0-RTT Key Exchange with Full Forward Security. In CCSW ’23: Proceedings of the 2023 on Cloud Computing Security Workshop (pp. 55–68). Association for Computing Machinery (ACM).
  DOI: 10.1145/3605763.3625246 Metadata
  

  Abstract

  Secure communication protocols such as TLS 1.3 or QUIC are doing the heavy lifting in terms of security of today's Internet. These modern protocols provide modes that do not need an interactive handshake, but allow to send cryptographically protected data with the first client message in zero round-trip time (0-RTT). While this helps to reduce communication latency, the security of such protocols in terms of forward security is rather weak. In recent years, the academic community investigated ways of mitigating this problem and achieving full forward security and replay resilience for such 0-RTT protocols. In particular, this can be achieved via a so-called Puncturable Key Encapsulation Mechanism (PKEM). While the first such schemes were too expensive to be used in practice, Derler et al. (EUROCRYPT 2018) proposed a variant of PKEMs called Bloom Filter Key Encapsulation Mechanism (BFKEM). Unfortunately, these primitives have only be investigated asymptotically and no real benchmarks were conducted. Dallmeier et al. (CANS 2020) were the first to study their practical application within the QUIC protocol. They build upon a specific BFKEM instantiation and conclude that while it comes with significant computational overhead, its practical use is feasible, especially in applications where the increased CPU and memory load can be tolerated. In this paper, we revisit their choice of the concrete BFKEM instantiation and show that by relying on the concept of Time-based BFKEMs (TB-BFKEMs), also introduced by Derler et al. (EUROCRYPT 2018), one can combine the advantages of having computational efficiency and smaller key sizes. We thereby investigate algorithmic as well as conceptual optimizations with various trade-offs and conclude that our approach seems favorable for many practical settings. Overall, this extends the applicability of 0-RTT protocols with strong security in practice.
• 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.
• A Forkcipher-Based Pseudo-Random Number Generator
  Andreeva, E., & Weninger, A. (2023). A Forkcipher-Based Pseudo-Random Number Generator. In M. Tibouchi & X. Wang (Eds.), Applied Cryptography and Network Security (pp. 3–31).
  DOI: 10.1007/978-3-031-33491-7_1 Metadata
  

  Abstract

  Good randomness is needed for most cryptographic applications. In practice pseudo-random number generators (PRNGs) are employed. CTR_DRBG is a popular choice and among the recommended PRNGs by NIST. It is defined for use with primitives like AES or TDEA, which are not always suited for lightweight applications. In this work we propose FCRNG, a new PRNG, similar to CTR_DRBG, that is optimized for the lightweight setting (e.g. the Internet of Things). Our FCRNG construction utilizes the expanding and tweakable forkcipher primitive instantiated with ForkSkinny, which was introduced by Andreeva et al. at ASIACRYPT 2019. FCRNG employs internally a forkcipher-based counter-style mode FCTR. We propose two FCTR variants: FCTR-c for optimized speed and FCTR-T for optimized security. We then show that FCRNG with ForkSkinny can be 33% faster than CTR_DRBG when instantiated with the AES blockcipher. FCRNG achieves also a better security bound in the robustness security game - first introduced by Dodis et al. at CCS’13 and now the standard security goal for PRNGs. Contrary to the CRYPTO 2020 security bound by Hoang and Shen established for CTR_DRBG, the security of our construction with FCTR-T does not degrade with the length of the random inputs, nor the amount of requested output pseudorandom bits. FCRNG passes all tests of the NIST test suite for pseudorandom number generators.
• 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.

2022

• Double-authentication-preventing signatures in the standard model
  Catalano, D., Fuchsbauer, G., & Soleimanian, A. (2022). Double-authentication-preventing signatures in the standard model. Journal of Computer Security, 30(1), 3–38.
  DOI: 10.3233/JCS-200117 Metadata
  

  Abstract

  A double-authentication preventing signature (DAPS) scheme is a digital signature scheme equipped with a self-enforcement mechanism. Messages consist of an address and a payload component, and a signer is penalized if she signs two messages with the same addresses but different payloads. The penalty is the disclosure of the signer's signing key. Most of the existing DAPS schemes are proved secure in the random oracle model (ROM), while the efficient ones in the standard model only support address spaces of polynomial size. We present DAPS schemes that are efficient, secure in the standard model under standard assumptions and support large address spaces. Our main construction builds on vector commitments (VC) and double-trapdoor chameleon hash functions (DCH). We also provide a DAPS realization from Groth-Sahai (GS) proofs that builds on a generic construction by Derler et al., which they instantiate in the ROM. The GS-based construction, while less efficient than our main one, shows that a general yet efficient instantiation of DAPS in the standard model is possible. An interesting feature of our main construction is that it can be easily modified to guarantee security even in the most challenging setting where no trusted setup is provided. To the best of our knowledge, ours seems to be the first construction achieving this in the standard model.
• 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.
• 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.
• Position Paper: Escaping Academic Cloudification to Preserve Academic Freedom
  Fiebig, T., Gürses, S., & Lindorfer, M. (2022). Position Paper: Escaping Academic Cloudification to Preserve Academic Freedom. Privacy Studies Journal, 51–68.
  DOI: 10.7146/psj.vi.132713 Metadata
  

  Abstract

  Especially since the onset of the COVID-19 pandemic, the use of cloud-based tools and solutions - lead by the ‘Zoomification’ of education, has picked up attention in the EdTech and privacy communities. In this paper, we take a look at the progressing use of cloud-based educational tools, often controlled by only a handful of major corporations. We analyse how this ‘cloudification’ impacts academics’ and students’ privacy and how it influences the handling of privacy by universities and higher education institutions. Furthermore, we take a critical perspective on how this cloudification may not only threaten users’ privacy, but ultimately may also compromise core values like academic freedom: the dependency relationships between universities and corporations could impact curricula, while also threatening what research can be conducted. Finally, we take a perspective on universities’ cloudification in different western regions to identify policy mechanisms and recommendations that can enable universities to preserve their academic independence, without compromising on digitalization and functionality.
• Credential Transparency System
  Chase, M., Fuchsbauer, G., Ghosh, E., & Plouviez, A. (2022). Credential Transparency System. In Security and Cryptography for Networks (pp. 313–335).
  DOI: 10.1007/978-3-031-14791-3_14 Metadata
  

  Abstract

  A major component of the entire digital identity ecosystem are verifiable credentials. However, for users to have complete control and privacy of their digital credentials, they need to be able to store and manage these credentials and associated cryptographic key material on their devices. This approach has severe usability challenges including portability across devises. A more practical solution is for the users to trust a more reliable and available service to manage credentials on their behalf, such as in the case of Single Sign-On (SSO) systems and identity hubs. But the obvious downside of this design is the immense trust that the users need to place on these service providers. In this work, we introduce and formalize a credential transparency system (CTS) framework that adds strong transparency guarantees to a credential management system while preserving privacy and usability features of the system. CTS ensures that if a service provider presents any credential to an honest verifier on behalf of a user, and the user’s device tries to audit all the shows presented on the user’s behalf, the service provider will not be able to drop or modify any show information without getting caught. We define CTS to be a general framework that is compatible with a wide range of credential management systems including SSO and anonymous credential systems. We also provide a CTS instantiation and prove its security formally.
• Approximate Distance-Comparison-Preserving Symmetric Encryption
  Fuchsbauer, G., Ghosal, R., Hauke, N., & O’Neill, A. (2022). Approximate Distance-Comparison-Preserving Symmetric Encryption. In Security and Cryptography for Networks (pp. 117–144).
  DOI: 10.1007/978-3-031-14791-3_6 Metadata
  

  Abstract

  We introduce distance-comparison-preserving symmetric encryption (DCPE), a new type of property-preserving encryption that preserves relative distance between plaintext vectors. DCPE is naturally suited for nearest-neighbor search on encrypted data. To boost security, we divert from prior work on Property Preserving Encryption (PPE) and ask for approximate comparison, which is natural given the prevalence of approximate nearest neighbor (ANN) search. We study what security approximate DCPE can provide and how to construct it. Based on a relation we prove between approximate DCP and approximate distance-preserving functions, we design our core approximate DCPE scheme for Euclidean distance we call Scale-And-Perturb (SAP ). The encryption algorithm of our core scheme processes plaintexts on-the-fly. To further enhance security, we also introduce two preprocessing techniques: (1) normalizing the plaintext distribution, and (2) shuffling, wherein the component-wise encrypted dataset is randomly permuted. We prove that SAP achieves a suitable indistinguishability-based security notion we call real-or-replaced indistinguishability (RoR ). In particular, our RoR result implies that our scheme prevents a form of membership inference attack. Moreover, we show for i.i.d. multivariate normal plaintexts, we get security against approximate frequency-finding attacks, the main line of attacks against property-preserving encryption. This follows from a one-wayness (OW) analysis. Finally, carefully combining our OW and RoR results, we are able characterize bit-security of SAP. Overall, we find that our DCPE scheme not only has superior bit-security to Order Preserving Encryption (OPE) but resists relevant attacks that even ideal order-revealing encryption (Boneh et al., EUROCRYPT 2015) does not.
• 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.
• 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.
• 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.
• 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
• 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
• 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
• 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
• 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.
• The security of Mimblewimble
  Fuchsbauer, G. (2022, June 27). The security of Mimblewimble [Keynote Presentation]. 22nd Central European Conference on Cryptography, Smolenice, Slovakia.
  Metadata
  

  Abstract

  Mimblewimble is a payment protocol that underlies several cryptocurrencies and is now also supported by Litecoin. Besides offering privacy by design, it improves on scalability: while in Bitcoin every transaction must be stored forever, in Mimblewimble only the "unspent transaction outputs", which represent the current state of the system, must be kept. In joint work with Michele Orrù and Yannick Seurin, we have formally shown the security of Mimblewimble (EUROCRYPT'19), as well as that of a recent extension (ia.cr/2022/265).
• Evolution of Payment Channels
  Aumayr, L. (2022, July 27). Evolution of Payment Channels [Presentation]. DFINITY Foundation - research talks, Austria.
  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.
• 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.
• 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.
• 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.
• 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.
• Suborn Channels: Incentives Against Timelock Bribes
  Avarikioti, G., & Thyfronitis Litos, O. S. (2022). Suborn Channels: Incentives Against Timelock Bribes. In Financial Cryptography and Data Security (pp. 488–511). Springer Nature Switzerland AG.
  DOI: 10.34726/3904 Metadata
  

  Abstract

  As the Bitcoin mining landscape becomes more competitive, analyzing potential attacks under the assumption of rational miners becomes increasingly relevant. In the rational setting, blockchain users can bribe miners to reap an unfair benefit. Established protocols such as Duplex Micropayment Channels and Lightning Channels are susceptible to bribery, which upends their financial guarantees. Indeed, we prove that in a two-party contract in which the honest party can spend an output right away, whereas the malicious can only spend the same output after a timelock, the latter party can promise a high fee to the miners, who then intentionally ignore the transaction of the honest party in anticipation of the higher fee. This effectively prevents a valid transaction from ever entering the blockchain, resulting in potentially severe financial losses for the honest and considerable gains for the malicious party. We expand previous results on timelock bribes to more realistic blockchains, proving that a general class of contracts are susceptible. We then apply our results to Duplex Micropayment Channels and Lightning Channels, providing exact bounds on their safe operating region. Furthermore, we enhance the Bitcoin Script of Duplex Micropayment Channels so that the coins of a party that attempts to bribe are given to the miners as fees, therefore effectively disincentivizing bribes. Our solution, named Suborn channels, is implemented as a proof-of-concept. We also propose a small change to Lightning Channels that achieves a similar effect. Moreover, we formally express the exact circumstances under which our two proposals ensure alignment of miner incentives with the prescribed protocol outcome.
• 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.
• 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.
• DCSO: towards an ontology for machine-actionable data management plans
  Cardoso, J., Castro, L. J., Ekaputra, F. J., Jacquemot-Perbal, M.-C., Suchánek, M., Miksa, T., & Borbinha, J. (2022). DCSO: towards an ontology for machine-actionable data management plans. Journal of Biomedical Semantics, 13, Article 21.
  DOI: 10.1186/s13326-022-00274-4 Metadata
  

  Abstract

  The concept of Data Management Plan (DMP) has emerged as a fundamental tool to help researchers through the systematical management of data. The Research Data Alliance DMP Common Standard (DCS) working group developed a set of universal concepts characterising a DMP so it can be represented as a machine-actionable artefact, i.e., machine-actionable Data Management Plan (maDMP). The technology-agnostic approach of the current maDMP specification: (i) does not explicitly link to related data models or ontologies, (ii) has no standardised way to describe controlled vocabularies, and (iii) is extensible but has no clear mechanism to distinguish between the core specification and its extensions.This paper reports on a community effort to create the DMP Common Standard Ontology (DCSO) as a serialisation of the DCS core concepts, with a particular focus on a detailed description of the components of the ontology. Our initial result shows that the proposed DCSO can become a suitable candidate for a reference serialisation of the DMP Common Standard.
• Non-Linear reasoning in the superposition calculus
  Lackner, A. (2022). Non-Linear reasoning in the superposition calculus [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2022.90765 Metadata
  

  Abstract

  Proving arithmetic properties has many applications, ranging from classical use cases of computer algebra and functional analysis to more applied case studies from software analysis and verification. For example, program loops over numeric data structures naturally implement addition, multiplication and exponentiation operations. While automating reasoning about such arithmetic properties has already made significant progress in the domain of linear algebra, non-linear reasoning in the context of satisfiability and validity checking is sill at its infancy. Although this subfield of automated reasoning is still quite unexplored, there do exist SMT-solvers (satisfiability modulo theory) which are able to reason about such non-linear arithmetic properties. Whenever new proving techniques or improvements are discovered, a typical approach to evaluate their performance is to test them on challenges of varying difficulty and compare different metrics like runtime or quality of the result (e.g. length of the proof) with those of other solvers. For non-linear arithmetic over reals and over integers, a large dataset of such challenges already exists (e.g. SMT-Lib benchmarks). Although these benchmarks are well suited for performance tests, they are often complex and only theoretically readable by humans. Therefore, it usually becomes difficult to get to the real problem when a benchmark is not solved. In this thesis, we describe various ways to generate benchmarks where the complexitycan be adjusted in different ways. The benchmarks are not created from scratch but are based on challenges originally designed for loop invariant generators. For a wide range of loops, these invariants can be represented by polynomials over the variables occurring in the program, which makes them a perfect fit for our benchmarks. The benchmarks formulate a correctness claim for polynomial loop invariants in first-order logic. All the methods described in this thesis for generating such benchmarks are proven to be sound. That is, we show that the correctness claim is a valid formula if and only if the corresponding polynomial invariant is indeed an invariant of the considered loop. The already mentioned variation of the benchmark is then achieved by exploiting properties of polynomial invariants. Experiments on the generated benchmarks were then conducted, using the two state-of-the-art solvers Vampire and Z3. Based on the resultsof the experiments, we have investigated the impact of varying the complexity of the benchmarks. Additionally, we suggest further approaches and adaptions to the solver in an attempt to improve their performance
• Android vs. iOS: : security of mobile Deep Links
  Steinböck, M. (2022). Android vs. iOS: : security of mobile Deep Links [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2022.93327 Metadata
  

  Abstract

  Bridge the Gap is a trend that aims to allow web browsers to start smartphone apps on a mobile device. This is achieved by so-called Deep Links, which enable direct linking to specific in-app resources. However, the resulting fusion of the web and native apps also introduces new attack vectors. There are numerous studies on security and privacy concerns of Deep Links on the open-source operating system Android, showing that these are prone to threats such as hijacking. The proprietary operating system iOS has a similar implementation of deep linking mechanisms to Android. However, there are not many publications on this matter, possibly due to the unavailability of iOS’ source code. In this thesis, we investigate the security of mobile Deep Links. First, we present known attack scenarios for Android with regards to Custom Schemes and App Links. Then, we consider the applicability of these attack vectors to deep linking mechanisms on iOS. Therefore, we develop vulnerable apps implementing discussed security issues, analyze whether an attacker could abuse them, and what security and privacy implications this has. Next, we compare our results to the corresponding mechanisms and security concerns of Android. Finally, to gain an insight into the actual security implications of the presented attack vectors, we analyze the distribution of Deep Links in the wild, based on a dataset containing over 11,000 iOS apps from the official Apple App Store.
• Systematic Analysis of Programming Languages and Their Execution Environments for Spectre Attacks
  Naseredini, A., Gast, S., Schwarzl, M., Sousa Bernardo, P. M., Smajic, A., Canella, C., Berger, M., & Gruss, D. (2022). Systematic Analysis of Programming Languages and Their Execution Environments for Spectre Attacks. In P. Mori, G. Lenzini, & S. Furnell (Eds.), Proceedings of the 8th International Conference on Information Systems Security and Privacy (pp. 48–59). SciTePress.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  In this paper, we analyze the security of programming languages and their execution environments (compilers and interpreters) with respect to Spectre attacks. The analysis shows that only 16 out of 42 execution environments have mitigations against at least one Spectre variant, i.e., 26 have no mitigations against any Spectre variant. Using our novel tool Speconnector, we develop Spectre proof-of-concept attacks in 8 programming languages and on code generated by 11 execution environments that were previously not known to be affected. Our results highlight some programming languages that are used to implement security-critical code, but remain entirely unprotected, even three years after the discovery of Spectre.
• 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.
• 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.

2021

• FWS: Analyzing, Maintaining and Transcompiling Firewalls
  Bodei, C., Ceragioli, L., Degano, P., Focardi, R., Galletta, L., Luccio, F., Tempesta, M., & Veronese, L. (2021). FWS: Analyzing, Maintaining and Transcompiling Firewalls. Journal of Computer Security, 29(1), 77–134.
  DOI: 10.3233/jcs-200017 Metadata
  

  Abstract

  Firewalls are essential for managing and protecting computer networks. They permit specifying which packets are allowed to enter a network, and also how these packets are modified by IP address translation and port redirection. Configuring a firewall is notoriously hard, and one of the reasons is that it requires using low level, hard to interpret, configuration languages. Equally difficult are policy maintenance and refactoring, as well as porting a configuration from one firewall system to another. To address these issues we introduce a pipeline that assists system administrators in checking if: (i) the intended security policy is actually implemented by a configuration; (ii) two configurations are equivalent; (iii) updates have the desired effect on the firewall behavior; (iv) there are useless or redundant rules; additionally, an administrator can (5) transcompile a configuration into an equivalent one in a different language; and (vi) maintain a configuration using a generic, declarative language that can be compiled into different target languages. The pipeline is based on IFCL, an intermediate firewall language equipped with a formal semantics, and it is implemented in an open source tool called FWS. In particular, the first stage decompiles real firewall configurations for iptables, ipfw, pf and (a subset of) Cisco IOS into IFCL. The second one transforms an IFCL configuration into a logical predicate and uses the Z3 solver to synthesize an abstract specification that succinctly represents the firewall behavior. System administrators can use FWS to analyze the firewall by posing SQL-like queries, and update the configuration to meet the desired security requirements. Finally, the last stage allows for maintaining a configuration by acting directly on its abstract specification and then compiling it to the chosen target language. Tests on real firewall configurations show that FWS can be fruitfully used in real-world scenarios.
• Donner: UTXO-Based Virtual Channels Across Multiple Hops
  Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2021, September 7). Donner: UTXO-Based Virtual Channels Across Multiple Hops [Presentation]. Bitcoin Sydney Socratic Seminar, Australia.
  Metadata
• Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
  Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2021, April 27). Blitz: Secure Multi-Hop Payments Without Two-Phase Commits [Presentation]. Bitcoin Sydney Socratic Seminar, Australia.
  Metadata
• Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
  Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2021, February 24). Blitz: Secure Multi-Hop Payments Without Two-Phase Commits [Presentation]. Decrypto Seminar, Unknown.
  Metadata
• Designing Secure Payment Channel Schemes
  Aumayr, L. (2021, November 16). Designing Secure Payment Channel Schemes [Presentation]. Singapore Management University - Online Topic, Singapore.
  Metadata
• Beyond Payments in Payment Channel Networks
  Aumayr, L. (2021, November 16). Beyond Payments in Payment Channel Networks [Presentation]. Software Seminar Series (S3), Spain.
  Metadata
• Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
  Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2021, May 26). Blitz: Secure Multi-Hop Payments Without Two-Phase Commits [Conference Presentation]. Theory and Practice of Blockchains, Unknown.
  Metadata
• Off-chain Scaling of Cryptocurrencies
  Aumayr, L. (2021, December 9). Off-chain Scaling of Cryptocurrencies [Presentation]. VISP blockchain research meetup, Austria.
  Metadata
• 1, 2, 3, Fork: Counter Mode Variants based on a Generalized Forkcipher
  Andreeva, E., Bhati, A. S., Preneel, B., & Vizár, D. (2021). 1, 2, 3, Fork: Counter Mode Variants based on a Generalized Forkcipher. IACR Transactions on Symmetric Cryptology, 2021(3).
  DOI: 10.46586/tosc.v2021.i3.1-35 Metadata
  

  Abstract

  A multi-forkcipher (MFC) is a generalization of the forkcipher (FC) primitive introduced by Andreeva et al. at ASIACRYPT’19. An MFC is a tweakable cipher that computes s output blocks for a single input block, with s arbitrary but fixed. We define the MFC security in the ind-prtmfp notion as indistinguishability from s tweaked permutations. Generalizing tweakable block ciphers (TBCs, s = 1), as well as forkciphers (s = 2), MFC lends itself well to building simple-to-analyze modes of operation that support any number of cipher output blocks. Our main contribution is the generic CTR encryption mode GCTR that makes parallel calls to an MFC to encrypt a message M. We analyze the set of all 36 “simple and natural” GCTR variants under the nivE security notion by Peyrin and Seurin from CRYPTO’16. Our proof method makes use of an intermediate abstraction called tweakable CTR (TCTR) that captures the core security properties of GCTR common to all variants, making their analyses easier. Our results show that many of the schemes achieve from well beyond birthday bound (BBB) to full n-bit security under nonce respecting adversaries and some even BBB and close to full n-bit security in the face of realistic nonce misuse conditions. We finally present an efficiency comparison of GCTR using ForkSkinny (an MFC with s = 2) with the traditional CTR and the more recent CTRT modes, both are instantiated with the SKINNY TBC. Our estimations show that any GCTR variant with ForkSkinny can achieve an efficiency advantage of over 20% for moderately long messages, illustrating that the use of an efficient MFC with s ≥ 2 brings a clear speed-up.
• Large-scale Static Analysis of PII Leakage in IoT Companion Apps
  Schmidt, D. (2021). Large-scale Static Analysis of PII Leakage in IoT Companion Apps [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2021.86548 Metadata
  

  Abstract

  Security and privacy problems of smart devices are often reported in the news. One possibility to improve the current situation are large-scale analyzes. Researchers and manufacturers can use such analysis to detect weaknesses, report them, and fix them before they get misused. However, to be able to perform a large-scale analysis, two difficulties need to be overcome. First, the diversity regarding software and hardware of smart devices makes a general approach difficult. Second, analyzes are often associated with high costs if physical devices are needed for the selected approach. We developed a static analysis approach for Internet of Things (IoT) companion applications (apps) to circumvent those difficulties. Companion apps are mobile apps, allowing their users to interact with smart devices. We focused on two aspects of companion apps that distinguish them from other applications: the communication over the local network and the used protocols. For this thesis, we use two analysis techniques to collect further information about the devices: taint analysis and value set analysis. We have chosen the latter for reconstructing URLs called by the applications and thereby detecting local communication. In this thesis, we analyzed in total 124 companion apps with our approach. We show the information obtained by the reconstructed endpoints. Furthermore, we present the flows found in two companion apps in detail, which contain threats to user's security and privacy. Overall, we make one step towards large-scale analysis of personally identifiable information (PII) leakage in IoT companion apps.
• Formal Methods for the Security Analysis of Smart Contracts
  Maffei, M. (2021). Formal Methods for the Security Analysis of Smart Contracts. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 8–8). TU Wien Academic Press.
  DOI: 10.34727/2021/isbn.978-3-85448-046-4_3 Metadata
• Blitz: Secure Multi-Hop Payments Without Two-Phase Commits
  Aumayr, L., Moreno-Sanchez, P., Kate, A., & Maffei, M. (2021). Blitz: Secure Multi-Hop Payments Without Two-Phase Commits. In 30th USENIX Security Symposium (pp. 4043–4060). USENIX: The Advanced Computing Systems Association.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Payment-channel networks (PCN) are the most prominent approach to tackle the scalability issues of current permissionless blockchains. A PCN reduces the load on-chain by allowing arbitrarily many off-chain multi-hop payments (MHPs) between any two users connected through a path of payment channels. Unfortunately, current MHP protocols are far from satisfactory. One-round MHPs (e.g., Interledger) are insecure as a malicious intermediary can steal the payment funds. Two-round MHPs (e.g., Lightning Network (LN)) follow the 2-phase-commit paradigm as in databases to overcome this issue. However, when tied with economical incentives, 2-phase-commit brings other security threats (i.e., wormhole attacks), staggered collateral (i.e., funds are locked for a time proportional to the payment path length) and dependency on specific scripting language functionality (e.g., Hash Time-Lock Contracts) that hinders a wider deployment in practice. We present Blitz, a novel MHP protocol that demonstrates for the first time that we can achieve the best of the two worlds: a single round MHP where no malicious intermediary can steal coins. Moreover, Blitz provides the same privacy for sender and receiver as current MHP protocols do, is not prone to the wormhole attack and requires only constant collateral. Additionally, we construct MHPs using only digital signatures and a timelock functionality, both available at the core of virtually every cryptocurrency today. We provide the cryptographic details of Blitz and we formally prove its security. Furthermore, our experimental evaluation on a LN snapshot shows that (i) staggered collateral in LN leads to in between 4x and 33x more unsuccessful payments than the constant collateral in Blitz; (ii) Blitz reduces the size of the payment contract by 26%; and (iii) Blitz prevents up to 0.3 BTC (3397 USD in October 2020) in fees being stolen over a three day period as it avoids wormhole attacks by design.
• Interpolation Cryptanalysis of Unbalanced Feistel Networks with Low Degree Round Functions
  Andreeva, E., Roy, A., & Sauer, J. F. (2021). Interpolation Cryptanalysis of Unbalanced Feistel Networks with Low Degree Round Functions. In Selected Areas in Cryptography (pp. 273–300). Springer LNCS.
  DOI: 10.1007/978-3-030-81652-0_11 Metadata ⯈Fulltext (preprint)
  

  Abstract

  In recent years a new type of block ciphers and hash functions over a (large) field, such as MiMC and GMiMC, have been designed. Their security, particularly over a prime field, is mainly determined by algebraic cryptanalysis techniques, such as Gröbner basis and interpolation attacks. In SAC 2019, Li and Preneel presented low memory interpolation attack against the MiMC and Feistel-MiMC designs. In this work we answer the open question posed in their work and show that low memory interpolation attacks can be extended to unbalanced Feistel networks (UFN) with low degree functions, and in particular to the GMiMC design. Our attack applies to UFNs with expanding and contracting round functions keyed either via identical (univariate) or distinct round keys (multivariate). Since interpolation attacks do not necessarily yield the best possible attacks over a binary extension field, we focus our analysis on prime fields Fp . Our next contribution is to develop an improved technique for a more efficient key recovery against UFNs with expanding round function. We show that the final key recovery step can be reduced not only to the gcd but also to the root finding problem. Despite its higher theoretical complexity, we show that our approach has a particularly interesting application on Sponge hash functions based on UFNs, such as GMiMCHash. We illustrate for the first time how our root finding technique can be used to find collision, second preimage and preimage attacks on (reduced round) members of the GMiMCHash family. In addition, we support our theoretical analysis with small-scale experimental results.
• Bitcoin-Compatible Virtual Channels
  Aumayr, L., Ersoy, O., Erwig, A., Faust, S., Hostáková, K., Maffei, M., Moreno-Sanchez, P., & Riahi, S. (2021). Bitcoin-Compatible Virtual Channels. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE Symposium on Security and Privacy 2021, Oakland, United States of America (the). IEEE Computer Society.
  DOI: 10.1109/sp40001.2021.00097 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Current permissionless cryptocurrencies such as Bitcoin suffer from a limited transaction rate and slow confirmation time, which hinders their large scale adoption. Payment channels are one of the most promising solutions to address these problems, as they allow two end-points of the channel to perform arbitrarily many payments in a peer-to-peer fashion while uploading only two transactions on the blockchain. This concept has been generalized into payment-channel networks where a path of payment channels is used to settle the payment between two users that might not share a channel between them. However, this approach requires the active involvement of each user in the path, making the system less reliable (they might be offline), more expensive (they charge fees per payment) and slower (intermediaries need to be actively involved in the payment). To mitigate this issue, recent work has introduced the concept of virtual channels, which involve intermediaries only in the initial creation of a bridge between payer and payee, who can later on independently perform arbitrarily many off-chain transactions. Unfortunately, existing constructions are only available for Ethereum, as they rely on its account model and Turing-complete scripting language. The realization of virtual channels in other blockchain technologies with limited scripting capabilities, like Bitcoin, was considered so far an open challenge. In this work, we present the first virtual channel protocols that are built on the UTXO-model and require a script language supporting only a digital signature scheme and a timelock functionality, being thus backwards compatible with virtually every cryptocurrency, including Bitcoin. We formalize the security properties of virtual channels as an ideal functionality in the Universal Composability framework, and prove that our protocol constitutes a secure realization thereof. We have prototyped and evaluated our protocol on the Bitcoin blockchain, demonstrating its efficiency: for n sequential payments, they require an off-chain exchange of 11+2⋅(n−1) transactions or a total of 4219+695⋅(n−1) bytes, with no on-chain footprint in the optimistic case.
• Post-Quantum Adaptor Signature for Privacy-Preserving Off-Chain Payments
  Tairi, E., Moreno-Sanchez, P., & Maffei, M. (2021). Post-Quantum Adaptor Signature for Privacy-Preserving Off-Chain Payments. In Financial Cryptography and Data Security (pp. 131–150).
  DOI: 10.1007/978-3-662-64331-0_7 Metadata
  

  Abstract

  Adaptor signatures (AS) are an extension of digital signatures that enable the encoding of a cryptographic hard problem (e.g., discrete logarithm) within the signature itself. An AS scheme ensures that (i) the signature can be created only by the user knowing the solution to the cryptographic problem; (ii) the signature reveals the solution itself; (iii) the signature can be verified with the standard verification algorithm. These properties have made AS a salient building block for many blockchain applications, in particular, off-chain payment systems such as payment-channel networks, payment-channel hubs, atomic swaps or discrete log contracts. Current AS constructions, however, are not secure against adversaries with access to a quantum computer. In this work, we present IAS, a construction for adaptor signatures that relies on standard cryptographic assumptions for isogenies, and builds upon the isogeny-based signature scheme CSI-FiSh. We formally prove the security of IAS against a quantum adversary. We have implemented IAS and our evaluation shows that IAS can be incorporated into current blockchains while requiring ∼1500 bytes of storage size on-chain and ∼140 milliseconds for digital signature verification. We also show how IAS can be seamlessly leveraged to build post-quantum off-chain payment applications without harming their security and privacy.
• A²L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs
  Tairi, E., Moreno-Sanchez, P., & Maffei, M. (2021). A²L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs. In 2021 IEEE Symposium on Security and Privacy (SP). IEEE Symposium on Security and Privacy 2021, United States of America (the).
  DOI: 10.1109/sp40001.2021.00111 Metadata
  

  Abstract

  Payment channel hubs (PCHs) constitute a promising solution to the inherent scalability problems of blockchain technologies, allowing for off-chain payments between sender and receiver through an intermediary, called the tumbler. While state-of-the-art PCHs provide security and privacy guarantees against a malicious tumbler, they do so by relying on the scripting-based functionality available only at few cryptocurrencies, and they thus fall short of fundamental properties such as backwards compatibility and efficiency. In this work, we present Trilero, the first PCH protocol to achieve all aforementioned properties. Trilero builds upon A2L, a novel cryptographic primitive that realizes a three-party protocol for conditional transactions, where the tumbler pays the receiver only if the latter solves a cryptographic challenge with the help of the sender, which implies the sender has paid the tumbler. We prove the security and privacy guarantees of A2L (which carry over to Trilero) in the Universal Composability framework and present a provably secure instantiation based on adaptor signatures. We implemented A2L and compared it to TumbleBit, the state-of-the-art Bitcoin-compatible PCH. Asymptotically, A2L has a communication complexity that is constant, as opposed to linear in the security parameter like in TumbleBit. In practice, A2L requires ∼33x less bandwidth than TumleBit, while retaining the computational cost (or providing 2x speedup with a preprocessing technique). This demonstrates that A2L (and thus Trilero) is ready to be deployed today. In theory, we demonstrate for the first time that it is possible to design a secure and privacy-preserving PCH while requiring only digital signatures and timelock functionality from the underlying scripting language. In practice, this result makes Trilero backwards compatible with virtually all cryptocurrencies available today, even those offering a highly restricted form of scripting language such as Ripple or Stellar. The practical appealing of Trilero has resulted in a proof-of-concept implementation in the COMIT Network, a blockchain technology focused on cross-currency payments.
• Updatable Signatures and Message Authentication Codes
  Cini, V., Ramacher, S., Slamanig, D., Striecks, C., & Tairi, E. (2021). Updatable Signatures and Message Authentication Codes. In Public-Key Cryptography – PKC 2021 (pp. 691–723). Springer, Cham.
  DOI: 10.1007/978-3-030-75245-3_25 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Cryptographic objects with updating capabilities have been proposed by Bellare, Goldreich and Goldwasser (CRYPTO'94) under the umbrella of incremental cryptography. They have recently seen increased interest, motivated by theoretical questions (Ananth et al., EC'17) as well as concrete practical motivations (Lehmann et al., EC'18; Groth et al. CRYPTO'18; Kloo{\ss} et al., EC'19). In this work, the form of updatability we are particularly interested in is that primitives are key-updatable \textit{and} allow to update ``old" cryptographic objects, e.g., signatures or message authentication codes, from the ``old" key to the updated key at the same time without requiring full access to the new key (i.e., only via a so-called update token). Inspired by the rigorous study of updatable encryption by Lehmann and Tackmann (EC'18) and Boyd et al. (CRYPTO'20), we introduce a definitional framework for updatable signatures (USs) and message authentication codes (UMACs). We discuss several applications demonstrating that such primitives can be useful in practical applications, especially around key rotation in various domains, as well as serve as building blocks in other cryptographic schemes. We then turn to constructions and our focus there is on ones that are secure and practically efficient. In particular, we provide generic constructions from key-homomorphic primitives (signatures and PRFs) as well as direct constructions. This allows us to instantiate these primitives from various assumptions such as DDH or CDH (latter in bilinear groups), or the (R)LWE and the SIS assumptions. As an example, we obtain highly practical US schemes from BLS signatures or UMAC schemes from the Naor-Pinkas-Reingold PRF.
• Can I Take Your Subdomain? Exploring Same-Site Attacks in the Modern Web
  Squarcina, M., Tempesta, M., Veronese, L., Calzavara, S., & Maffei, M. (2021). Can I Take Your Subdomain? Exploring Same-Site Attacks in the Modern Web. In 30th USENIX Security Symposium (pp. 2917–2934). 30th USENIX Security Symposium, USENIX Security 2021, August 11-13, 2021.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Related-domain attackers control a sibling domain of their target web application, e.g., as the result of a subdomain takeover. Despite their additional power over traditional web attackers, related-domain attackers received only limited attention by the research community. In this paper we define and quantify for the first time the threats that related-domain attackers pose to web application security. In particular, we first clarify the capabilities that related-domain attackers can acquire through different attack vectors, showing that different instances of the related-domain attacker concept are worth attention. We then study how these capabilities can be abused to compromise web application security by focusing on different angles, including: cookies, CSP, CORS, postMessage and domain relaxation. By building on this framework, we report on a large-scale security measurement on the top 50k domains from the Tranco list that led to the discovery of vulnerabilities in 887, sites, where we quantified the threats posed by related-domain attackers to popular web applications.
• Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference
  Girol, G., Farinier, B., & Bardin, S. (2021). Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference. In Computer Aided Verification (pp. 669–693). Springer LNCS.
  DOI: 10.1007/978-3-030-81685-8_32 Metadata
  

  Abstract

  This paper introduces a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 4 existing vulnerabilities, and compare it with standard symbolic execution.
• EssentialFP: Exposing the Essence of Browser Fingerprinting
  Sjösten, A., Hedin, D., & Sabelfeld, A. (2021). EssentialFP: Exposing the Essence of Browser Fingerprinting. In 2021 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW). EuroS&P 2021 SecWeb Workshop, Vienna, Austria.
  DOI: 10.1109/eurospw54576.2021.00011 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Web pages aggressively track users for a variety of purposes from targeted advertisements to enhanced authentication. As browsers move to restrict traditional cookie-based tracking, web pages increasingly move to tracking based on browser fingerprinting. Unfortunately, the state-of-the-art to detect fingerprinting in browsers is often error-prone, resorting to imprecise heuristics and crowd-sourced filter lists. This paper presents EssentialFP, a principled approach to detecting fingerprinting on the web. We argue that the pattern of (i) gathering information from a wide browser API surface (multiple browser-specific sources) and (ii) communicating the information to the network (network sink) captures the essence of fingerprinting. This pattern enables us to clearly distinguish fingerprinting from similar types of scripts like analytics and polyfills. We demonstrate that information flow tracking is an excellent fit for exposing this pattern. To implement EssentialFP we leverage, extend, and deploy JSFlow, a state-of-the-art information flow tracker for JavaScript, in a browser. We illustrate the effectiveness of EssentialFP to spot fingerprinting on the web by evaluating it on two categories of web pages: one where the web pages perform analytics, use polyfills, and show ads, and one where the web pages perform authentication, bot detection, and fingerprinting-enhanced Alexa top pages.
• The Remote on the Local: Exacerbating Web Attacks Via Service Workers Caches
  Squarcina, M., Calzavara, S., & Maffei, M. (2021). The Remote on the Local: Exacerbating Web Attacks Via Service Workers Caches. In 2021 IEEE Security and Privacy Workshops (SPW). 15th IEEE Workshop on Offensive Technologies, San Francisco, CA, United States of America (the).
  DOI: 10.1109/spw53761.2021.00062 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Service workers boost the user experience of modern web applications by taking advantage of the Cache API to improve responsiveness and support offline usage. In this paper, we present the first security analysis of the threats posed by this programming practice, identifying an attack with major security implications. In particular, we show how a traditional XSS attack can abuse the Cache API to escalate into a person-in-the-middle attack against cached content, thus compromising its confidentiality and integrity. Remarkably, this attack enables new threats which are beyond the scope of traditional XSS. After defining the attack, we study its prevalence in the wild, finding that the large majority of the sites which register service workers using the Cache API are vulnerable as long as a single webpage in the same origin of the service worker is affected by an XSS. Finally, we propose a browser-side countermeasure against this attack, and we analyze its effectiveness and practicality in terms of security benefits and backward compatibility with existing web applications.
• Transferable E-Cash: A Cleaner Model and the First Practical Instantiation
  Bauer, B., Fuchsbauer, G., & Qian, C. (2021). Transferable E-Cash: A Cleaner Model and the First Practical Instantiation. In Public-Key Cryptography – PKC 2021 (pp. 559–590). Springer.
  DOI: 10.1007/978-3-030-75248-4_20 Metadata ⯈Fulltext (preprint)
• The One-More Discrete Logarithm Assumption in the Generic Group Model
  Bauer, B., Fuchsbauer, G., & Plouviez, A. (2021). The One-More Discrete Logarithm Assumption in the Generic Group Model. In Lecture Notes in Computer Science (pp. 587–617). Springer.
  DOI: 10.1007/978-3-030-92068-5_20 Metadata ⯈Fulltext (preprint)
  

  Abstract

  The one more-discrete logarithm assumption (OMDL) underlies the security analysis of identification protocols, blind signature and multi-signature schemes, such as blind Schnorr signatures and the recent MuSig2 multi-signatures. As these schemes produce standard Schnorr signatures, they are compatible with existing systems, e.g. in the context of blockchains. OMDL is moreover assumed for many results on the impossibility of certain security reductions. Despite its wide use, surprisingly, OMDL is lacking any rigorous analysis; there is not even a proof that it holds in the generic group model (GGM). (We show that a claimed proof is flawed.) In this work we give a formal proof of OMDL in the GGM. We also prove a related assumption, the one-more computational Diffie-Hellman assumption, in the GGM. Our proofs deviate from prior GGM proofs and replace the use of the Schwartz-Zippel Lemma by a new argument.
• Compactness of Hashing Modes and Efficiency Beyond Merkle Tree
  Andreeva, E., Bhattacharyya, R., & Roy, A. (2021). Compactness of Hashing Modes and Efficiency Beyond Merkle Tree. In Lecture Notes in Computer Science (pp. 92–123). Springer.
  DOI: 10.1007/978-3-030-77886-6_4 Metadata ⯈Fulltext (preprint)
  

  Abstract

  We revisit the classical problem of designing optimally efficient cryptographically secure hash functions. Hash functions are traditionally designed via applying modes of operation on primitives with smaller domains. The results of Shrimpton and Stam (ICALP 2008), Rogaway and Steinberger (CRYPTO 2008), and Mennink and Preneel (CRYPTO 2012) show how to achieve optimally efficient designs of 2n-to-n-bit compression functions from non-compressing primitives with asymptotically optimal 2n/2−ϵ -query collision resistance. Designing optimally efficient and secure hash functions for larger domains ( >2n bits) is still an open problem. To enable efficiency analysis and comparison across hash functions built from primitives of different domain sizes, in this work we propose the new compactness efficiency notion. It allows us to focus on asymptotically optimally collision resistant hash function and normalize their parameters based on Stam´s bound from CRYPTO 2008 to obtain maximal efficiency. We then present two tree-based modes of operation as a design principle for compact, large domain, fixed-input-length hash functions. 1. Our first construction is an Augmented Binary Tree (ABR) mode. The design is a (2ℓ+2ℓ−1−1)n -to-n-bit hash function making a total of (2ℓ−1) calls to 2n-to-n-bit compression functions for any ℓ≥2 . Our construction is optimally compact with asymptotically (optimal) 2n/2−ϵ -query collision resistance in the ideal model. For a tree of height ℓ , in comparison with Merkle tree, the ABR mode processes additional (2ℓ−1−1) data blocks making the same number of internal compression function calls. 2. With our second design we focus our attention on the indifferentiability security notion. While the ABR mode achieves collision resistance, it fails to achieve indifferentiability from a random oracle within 2n/3 queries. ABR+ compresses only 1 less data block than ABR with the same number of compression calls and achieves in addition indifferentiability up to 2n/2−ϵ queries. Both of our designs are closely related to the ubiquitous Merkle Trees and have the potential for real-world applicability where the speed of hashing is of primary interest.
• Optimized Software Implementations for the Lightweight Encryption Scheme ForkAE
  Andreeva, E., Deprez, A., Bermudo Mera, J. M., Karmakar, A., & Purnal, A. (2021). Optimized Software Implementations for the Lightweight Encryption Scheme ForkAE. In Smart Card Research and Advanced Applications (pp. 68–83). Springer.
  DOI: 10.1007/978-3-030-68487-7_5 Metadata ⯈Fulltext (preprint)
  

  Abstract

  In this work we develop optimized software implementations for ForkAE, a second round candidate in the ongoing NIST lightweight cryptography standardization process. Moreover, we analyze the performance and efficiency of different ForkAE implementations on two embedded platforms: ARM Cortex-A9 and ARM Cortex-M0. First, we study portable ForkAE implementations. We apply a decryption optimization technique which allows us to accelerate decryption by up to 35%. Second, we go on to explore platform-specific software optimizations. In platforms where cache-timing attacks are not a risk, we present a novel table-based approach to compute the SKINNY round function. Compared to the existing portable implementations, this technique speeds up encryption and decryption by 20% and 25%, respectively. Additionally, we propose a set of platform-specific optimizations for processors with parallel hardware extensions such as ARM NEON. Without relying on parallelism provided by long messages (cf. bit-sliced implementations), we focus on the primitive-level ForkSkinny parallelism provided by ForkAE to reduce encryption and decryption latency by up to 30%. We benchmark the performance of our implementations on the ARM Cortex-M0 and ARM Cortex-A9 processors and give a comparison with the other SKINNY-based schemes in the NIST lightweight competition - SKINNY-AEAD and Romulus.
• Nonce-Misuse Security of the SAEF Authenticated Encryption Mode
  Andreeva, E., Bhati, A. S., & Vizár, D. (2021). Nonce-Misuse Security of the SAEF Authenticated Encryption Mode. In Selected Areas in Cryptography (pp. 512–534). Springer LNCS.
  DOI: 10.1007/978-3-030-81652-0_20 Metadata ⯈Fulltext (preprint)
  

  Abstract

  ForkAE is a NIST lightweight cryptography candidate that uses the forkcipher primitive in two modes of operation - SAEF and PAEF - optimized for authenticated encryption of the shortest messages. SAEF is a sequential and online AEAD that minimizes the memory footprint compared to its alternative parallel mode PAEF, catering to the most constrained devices. SAEF was proven AE secure against nonce-respecting adversaries. Due to their more acute and direct exposure to device misuse and mishandling, in most use cases of lightweight cryptography, nonce reuse presents a very realistic attack vector. Furthermore, many lightweight applications mandate security for their online AEAD schemes against block-wise adversaries. Surprisingly, a very few NIST lightweight AEAD candidates come with provable guarantees against these security threats. In this work we investigate the provable security guarantees of SAEF when nonces are repeated under a refined version of the notion of online authenticated encryption OAE given by Fleischmann et al. in 2012. Using the coefficient H technique we show that, with no modifications, SAEF is OAE secure up to the birthday security bound, i.e., up to 2n/2 processed blocks of data, where n is the block size of the forkcipher. The implications of our work is that SAEF is safe to use in a block-wise fashion, and that if nonces get repeated, this has no impact on ciphertext integrity and confidentiality only degrades by a limited extent up to repetitions of common message prefixes.
• Cross-Layer Deanonymization Methods in the Lightning Protocol
  Romiti, M., Victor, F., Moreno-Sanchez, P., Nordholt, P. S., Haslhofer, B., & Maffei, M. (2021). Cross-Layer Deanonymization Methods in the Lightning Protocol. In Lecture Notes in Computer Science. Springer Verlag, Austria. Springer LNCS.
  DOI: 10.1007/978-3-662-64322-8 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Bitcoin (BTC) pseudonyms (layer 1) can effectively be deanonymized using heuristic clustering techniques. However, while performing transactions off-chain (layer 2) in the Lightning Network (LN) seems to enhance privacy, a systematic analysis of the anonymity and pri-vacy leakages due to the interaction between the two layers is missing. We present clustering heuristics that group BTC addresses, based on their in-teraction with the LN, as well as LN nodes, based on shared naming and hosting information. We also present linking heuristics that link 45.97% of all LN nodes to 29.61% BTC addresses interacting with the LN. These links allow us to attribute information (e.g., aliases, IP addresses) to 21.19% of the BTC addresses contributing to their deanonymization. Further, these deanonymization results suggest that the security and privacy of LN payments are weaker than commonly believed, with LN users being at the mercy of as few as five actors that control 36 nodes and over 33% of the total capacity. Overall, this is the first paper to present a method for linking LN nodes with BTC addresses across layers and to discuss privacy and security implications.
• 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.
• Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures
  Aumayr, L., Ersoy, O., Erwig, A., Faust, S., Hostáková, K., Maffei, M., Moreno-Sanchez, P., & Riahi, S. (2021). Generalized Channels from Limited Blockchain Scripts and Adaptor Signatures. In Lecture Notes in Computer Science (pp. 635–664). Springer.
  DOI: 10.1007/978-3-030-92075-3_22 Metadata
  

  Abstract

  Decentralized and permissionless ledgers offer an inherently low transaction rate, as a result of their consensus protocol demanding the storage of each transaction on-chain. A prominent proposal to tackle this scalability issue is to utilize off-chain protocols, where parties only need to post a limited number of transactions on-chain. Existing solutions can roughly be categorized into: (i) application-specific channels (e.g., payment channels), offering strictly weaker functionality than the underlying blockchain; and (ii) state channels, supporting arbitrary smart contracts at the cost of being compatible only with the few blockchains having Turing-complete scripting languages (e.g., Ethereum). In this work, we introduce and formalize the notion of generalized channels allowing users to perform any operation supported by the underlying blockchain in an off-chain manner. Generalized channels thus extend the functionality of payment channels and relax the definition of state channels. We present a concrete construction compatible with any blockchain supporting transaction authorization, time-locks and constant number of Boolean ∧ and ∨ operations -- requirements fulfilled by many (non-Turing-complete) blockchains including the popular Bitcoin. To this end, we leverage adaptor signatures -- a cryptographic primitive already used in the cryptocurrency literature but formalized as a standalone primitive in this work for the first time. We formally prove the security of our generalized channel construction in the Universal Composability framework. As an important practical contribution, our generalized channel construction outperforms the state-of-the-art payment channel construction, the Lightning Network, in efficiency. Concretely, it halves the off-chain communication complexity and reduces the on-chain footprint in case of disputes from linear to constant in the number of off-chain applications funded by the channel. Finally, we evaluate the practicality of our construction via a prototype implementation and discuss various applications including financially secured fair two-party computation.

2020

• Privacy preserving authenticated Kkey exchange : Modelling, constructions, proofs and formal verification : Modellierung, Konstruktionen, Beweise und Verification
  Weninger, A. J. (2020). Privacy preserving authenticated Kkey exchange : Modelling, constructions, proofs and formal verification :  Modellierung, Konstruktionen, Beweise und Verification [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2021.87263 Metadata
  

  Abstract

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

  Abstract

  The widespread adoption of decentralized cryptocurrencies, such as Bitcoin or Ethereum, is currently hindered by their inherently limited transaction rate. One of the most prominent proposals to tackle this scalability issue are payment channels which allow mutually distrusted parties to exchange an arbitrary number of payments in the form of off-chain authenticated messages while posting only a limited number of transactions onto the blockchain. Specifically, two transactions suffice, unless a dispute between these parties occurs, in which case more on-chain transactions are required to restore the correct balance. Unfortunately, popular constructions, such as the Lightning network for Bitcoin, suffer from heavy communication complexity both off-chain and on-chain in case of dispute. Concretely, the communication overhead grows exponentially and linearly, respectively, in the number of applications that run in the channel. In this work, we introduce and formalize the notion of generalized channels for Bitcoin-like cryptocurrencies. Generalized channels significantly extend the concept of payment channels so as to perform off-chain any operation supported by the underlying blockchain. Besides the gain in expressiveness, generalized channels outperform state-of-the-art payment channel constructions in efficiency, reducing the communication complexity and the on-chain footprint in case of disputes to linear and constant, respectively. We provide a cryptographic instantiation of generalized channels that is compatible with Bitcoin, leveraging adaptor signatures -- a cryptographic primitive already used in the cryptocurrency literature but formalized as a standalone primitive in this work for the first time. We formally prove the security of our construction in the Universal Composability framework. Furthermore, we conduct an experimental evaluation, demonstrating the expressiveness and performance of generalized channels when used as building blocks for popular off-chain applications, such as channel splitting and payment-channel networks.
• Simpler Constructions of Asymmetric Primitives from Obfuscation
  Farshim, P., Fuchsbauer, G., & Passelègue, A. (2020). Simpler Constructions of Asymmetric Primitives from Obfuscation. In Progress in Cryptology – INDOCRYPT 2020 (pp. 715–738). Springer.
  DOI: 10.1007/978-3-030-65277-7_32 Metadata
• Language-Based Web Session Integrity
  Calzavara, S., Focardi, R., Grimm, N., Maffei, M., & Tempesta, M. (2020). Language-Based Web Session Integrity. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). IEEE Computer Security Foundations Symposium, Santa Barbara, USA, Non-EU. IEEE Computer Society.
  DOI: 10.1109/csf49147.2020.00016 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Session management is a fundamental component of web applications: despite the apparent simplicity, correctly implementing web sessions is extremely tricky, as witnessed by the large number of existing attacks. This motivated the design of formal methods to rigorously reason about web session security which, however, are not supported at present by suitable automated verification techniques. In this paper we introduce the first security type system that enforces session security on a core model of web applications, focusing in particular on server-side code. We showcase the expressiveness of our type system by analyzing the session management logic of HotCRP, Moodle, and phpMyAdmin, unveiling novel security flaws that have been acknowledged by software developers.
• eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts
  Schneidewind, C., Grishchenko, I., Scherer, M., & Maffei, M. (2020). eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security. ACM Conference on Computer and Communications Security (CCS), Washington, USA, Non-EU. Association for Computing Machinery ACM.
  DOI: 10.1145/3372297.3417250 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Ethereum has emerged as the most popular smart contract platform, with hundreds of thousands of contracts stored on the blockchain and covering diverse application scenarios, such as auctions, trading platforms, or elections. Given the financial nature of smart contracts, security vulnerabilities may lead to catastrophic consequences and, even worse, can hardly be fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging. This is as e.g., Ethereum's transaction-oriented programming mechanisms feature a subtle semantics, and since the blockchain data at execution time, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode, and a large-scale experimental evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 94% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.
• The Good, The Bad and The Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts
  Schneidewind, C., Scherer, M., & Maffei, M. (2020). The Good, The Bad and The Ugly: Pitfalls and Best Practices in Automated Sound Static Analysis of Ethereum Smart Contracts. In Lecture Notes in Computer Science (pp. 212–231). Springer.
  DOI: 10.1007/978-3-030-61467-6_14 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Ethereum smart contracts are distributed programs running on top of the Ethereum blockchain. Since program flaws can cause significant monetary losses and can hardly be fixed due to the immutable nature of the blockchain, there is a strong need of automated analysis tools which provide formal security guarantees. Designing such analyzers, however, proved to be challenging and error-prone. We review the existing approaches to automated, sound, static analysis of Ethereum smart contracts and highlight prevalent issues in the state of the art. Finally, we overview eThor, a recent static analysis tool that we developed following a principled design and implementation approach based on rigorous semantic foundations to overcome the problems of past works
• A Quantitative Analysis of Security, Anonymity and Scalability for the Lightning Network
  Tikhomirov, S., Moreno-Sanchez, P., & Maffei, M. (2020). A Quantitative Analysis of Security, Anonymity and Scalability for the Lightning Network. In 2020 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW). IEEE Security & Privacy On The Blockchain, Genova, EU. IEEE.
  DOI: 10.1109/eurospw51379.2020.00059 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Payment channel networks have been introduced to mitigate the scalability issues inherent to permissionless decentralized cryptocurrencies such as Bitcoin. Launched in 2018, the Lightning Network (LN) has been gaining popularity and consists today of more than 5000 nodes and 35000 payment channels that jointly hold 965 bitcoins (9.2M USD as of June 2020). This adoption has motivated research from both academia and industryPayment channels suffer from security vulnerabilities, such as the wormhole attack [39], anonymity issues [38], and scalability limitations related to the upper bound on the number of concurrent payments per channel [28], which have been pointed out by the scientific community but never quantitatively analyzedIn this work, we first analyze the proneness of the LN to the wormhole attack and attacks against anonymity. We observe that an adversary needs to control only 2% of nodes to learn sensitive payment information (e.g., sender, receiver, and amount) or to carry out the wormhole attack. Second, we study the management of concurrent payments in the LN and quantify its negative effect on scalability. We observe that for micropayments, the forwarding capability of up to 50% of channels is restricted to a value smaller than the channel capacity. This phenomenon hinders scalability and opens the door for denial-of-service attacks: we estimate that a network-wide DoS attack costs within 1.6M USD, while isolating the biggest community costs only 238k USDOur findings should prompt the LN community to consider the issues studied in this work when educating users about path selection algorithms, as well as to adopt multi-hop payment protocols that provide stronger security, privacy and scalability guarantees.
• Blind Schnorr Signatures and Signed ElGamal Encryption in the Algebraic Group Model
  Fuchsbauer, G., Plouviez, A., & Seurin, Y. (2020). Blind Schnorr Signatures and Signed ElGamal Encryption in the Algebraic Group Model. In Advances in Cryptology – EUROCRYPT 2020 (pp. 63–95). Springer.
  DOI: 10.1007/978-3-030-45724-2_3 Metadata
• Efficient Signatures on Randomizable Ciphertexts
  Bauer, B., & Fuchsbauer, G. (2020). Efficient Signatures on Randomizable Ciphertexts. In Lecture Notes in Computer Science (pp. 359–381). Springer.
  DOI: 10.1007/978-3-030-57990-6_18 Metadata
• Double-Authentication-Preventing Signatures in the Standard Model
  Catalano, D., Fuchsbauer, G., & Soleimanian, A. (2020). Double-Authentication-Preventing Signatures in the Standard Model. In Lecture Notes in Computer Science (pp. 338–358). Springer.
  DOI: 10.1007/978-3-030-57990-6_17 Metadata
• Bulwark: Holistic and Verified Security Monitoring of Web Protocols
  Veronese, L., Calzavara, S., & Compagna, L. (2020). Bulwark: Holistic and Verified Security Monitoring of Web Protocols. In Computer Security – ESORICS 2020 (pp. 23–41). Springer.
  DOI: 10.1007/978-3-030-58951-6_2 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Modern web applications often rely on third-party services to provide their functionality to users. The secure integration of these services is a non-trivial task, as shown by the large number of attacks against Single Sign On and Cashier-as-a-Service protocols. In this paper we present Bulwark, a new automatic tool which generates formally verified security monitors from applied pi-calculus specifications of web protocols. The security monitors generated by Bulwark offer holistic protection, since they can be readily deployed both at the client side and at the server side, thus ensuring full visibility of the attack surface against web protocols. We evaluate the effectiveness of Bulwark by testing it against a pool of vulnerable web applications that use the OAuth 2.0 protocol or integrate the PayPal payment system.
• Formalizing Graph Trail Properties in Isabelle/HOL
  Kovács, L., Lachnitt, H., & Szeider, S. (2020). Formalizing Graph Trail Properties in Isabelle/HOL. In Lecture Notes in Computer Science (pp. 190–205). LNCS.
  DOI: 10.1007/978-3-030-53518-6_12 Metadata ⯈Fulltext (preprint)
  

  Abstract

  We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weights over edges, and prove lower bounds over the length of trails in weighted graphs. We do so by extending the graph theory library of Isabelle/HOL with an algorithm computing the length of a longest strictly decreasing graph trail starting from a vertex for a given weight distribution, and prove that any decreasing trail is also an increasing one.
• When Malware is Packin' Heat; Limits of Machine Learning Classifiers Based on Static Analysis Features
  Aghakhani, H., Gritti, F., Mecca, F., Lindorfer, M., Ortolani, S., Balzarotti, D., Vigna, G., & Krügel, C. (2020). When Malware is Packin’ Heat; Limits of Machine Learning Classifiers Based on Static Analysis Features. In Network and Distributed System Security Symposium (NDSS). Internet Society.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Machine learning techniques are widely used in addition to signatures and heuristics to increase the detection rate of anti-malware software, as they automate the creation of detection models, making it possible to handle an ever-increasing number of new malware samples. In order to foil the analysis of anti-malware systems and evade detection, malware uses packing and other forms of obfuscation. However, few realize that benign applications use packing and obfuscation as well, to protect intellectual property and prevent license abuse. In this paper, we study how machine learning based on static analysis features operates on packed samples. Malware researchers have often assumed that packing would prevent machine learning techniques from building effective classifiers. However, both industry and academia have published results that show that machine-learning-based classifiers can achieve good detection rates, leading many experts to think that classifiers are simply detecting the fact that a sample is packed, as packing is more prevalent in malicious samples. We show that, different from what is commonly assumed, packers do preserve some information when packing programs that is "useful" for malware classification. However, this information does not necessarily capture the sample´s behavior. We demonstrate that the signals extracted from packed executables are not rich enough for machine-learning-based models to (1) generalize their knowl- edge to operate on unseen packers, and (2) be robust against adversarial examples. We also show that a na ̈ıve application of machine learning techniques results in a substantial number of false positives, which, in turn, might have resulted in incorrect labeling of ground-truth data used in past work.
• FlowPrint: Semi-Supervised Mobile-App Fingerprinting on Encrypted Network Traffic
  van Ede, T., Bortolameotti, R., Continella, A., Ren, J., Dubois, D., Lindorfer, M., Choffnes, D., van Steen, M., & Peter, A. (2020). FlowPrint: Semi-Supervised Mobile-App Fingerprinting on Encrypted Network Traffic. In Network and Distributed System Security Symposium (NDSS). Internet Society.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Mobile-application fingerprinting of network traffic is valuable for many security solutions as it provides insights into the apps active on a network. Unfortunately, existing techniques require prior knowledge of apps to be able to recognize them. However, mobile environments are constantly evolving, i.e., apps are regularly installed, updated, and uninstalled. Therefore, it is infeasible for existing fingerprinting approaches to cover all apps that may appear on a network. Moreover, most mobile traffic is encrypted, shows similarities with other apps, e.g., due to common libraries or the use of content delivery networks, and depends on user input, further complicating the fingerprinting process. As a solution, we propose FLOWPRINT, a semi-supervised approach for fingerprinting mobile apps from (encrypted) net- work traffic. We automatically find temporal correlations among destination-related features of network traffic and use these correlations to generate app fingerprints. Our approach is able to fingerprint previously unseen apps, something that existing techniques fail to achieve. We evaluate our approach for both Android and iOS in the setting of app recognition, where we achieve an accuracy of 89.2%, significantly outperforming state- of-the-art solutions. In addition, we show that our approach can detect previously unseen apps with a precision of 93.5%, detecting 72.3% of apps within the first five minutes of communication.
• TXTing 101: Finding Security Issues in the Long Tail of DNS TXT Records
  der Toorn, O. van, van Rijswijk-Deij, R., Fiebig, T., Lindorfer, M., & Sperotto, A. (2020). TXTing 101: Finding Security Issues in the Long Tail of DNS TXT Records. In 2020 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW). IEEE.
  DOI: 10.1109/eurospw51379.2020.00080 Metadata ⯈Fulltext (preprint)
  

  Abstract

  The DNS TXT resource record is the one with the most flexibility for its contents, as it is a largely unstructured. Although it might be the ideal basis for storing any form of text-based information, it also poses a security threat, as TXT records can also be used for malicious and unintended practices. Yet, TXT records are often overlooked in security research. In this paper, we present the first structured study of the uses of TXT records, with a specific focus on security implications. We are able to classify over 99.54% of all TXT records in our dataset, finding security issues including accidentally published private keys and exploit delivery attempts. We also report on our lessons learned during our large-scale, systematic analysis of TXT records.
• A Classification of Computational Assumptions in the Algebraic Group Model
  Bauer, B., Fuchsbauer, G., & Loss, J. (2020). A Classification of Computational Assumptions in the Algebraic Group Model. In Advances in Cryptology – CRYPTO 2020 (pp. 121–151). Springer.
  DOI: 10.1007/978-3-030-56880-1_5 Metadata
• Filter List Generation for Underserved Regions
  Sjösten, A., Snyder, P., Pastor, A., Papadopoulos, P., & Livshits, B. (2020). Filter List Generation for Underserved Regions. In Proceedings of The Web Conference 2020. ACM/IW3C2.
  DOI: 10.1145/3366423.3380239 Metadata
  

  Abstract

  Filter lists play a large and growing role in protecting and assisting web users. The vast majority of popular filter lists are crowd-sourced, where a large number of people manually label resources related to undesirable web resources (e.g. ads, trackers, paywall libraries), so that they can be blocked by browsers and extensions. Because only a small percentage of web users participate in the generation of filter lists, a crowd-sourcing strategy works well for blocking either uncommon resources that appear on "popular" websites, or resources that appear on a large number of "unpopular" websites. A crowd-sourcing strategy will perform poorly for parts of the web with small "crowds", such as regions of the web serving languages with (relatively) few speakers. This work addresses this problem through the combination of two novel techniques: (i) deep browser instrumentation that allows for the accurate generation of request chains, in a way that is robust in situations that confuse existing measurement techniques, and (ii) an ad classifier that uniquely combines perceptual and page-context features to remain accurate across multiple languages. We apply our unique two-step filter list generation pipeline to three regions of the web that currently have poorly maintained filter lists: Sri Lanka, Hungary, and Albania. We generate new filter lists that complement existing filter lists. Our complementary lists block an additional 3,349 of ad and ad-related resources (1,771 unique) when applied to 6,475 pages targeting these three regions. We hope that this work can be part of an increased effort at ensuring that the security, privacy, and performance benefits of web resource blocking can be shared with all users, and not only those in dominant linguistic or economic regions.
• A Voting-Based Blockchain Interoperability Oracle
  Scaffino, G., Schulte, S., Sober, M., & Spanring, C. (2020). A Voting-Based Blockchain Interoperability Oracle. In 2021 IEEE International Conference on Blockchain (Blockchain). IEEE.
  DOI: 10.1109/blockchain53845.2021.00030 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Today´s blockchain landscape is severely fragmented as more and more heterogeneous blockchain platforms have been developed in recent years. These blockchain platforms are not able to interact with each other or with the outside world since only little emphasis is placed on the interoperability between them. Already proposed solutions for blockchain interoperability such as naive relay or oracle solutions are usually not broadly applicable since they are either too expensive to operate or very resource-intensive. For that reason, we propose a blockchain interoperability oracle that follows a voting-based approach based on threshold signatures. The oracle nodes generate a distributed private key to execute an off-chain aggregation mechanism to collectively respond to requests. Compared to state-of-the-art relay schemes, our approach does not incur any ongoing costs and since the on-chain component only needs to verify a single signature, we can achieve remarkable cost savings compared to conventional oracle solutions
• Secrets in Source Code: Reducing False Positives using Machine Learning
  Saha, A., Denning, T., Srikumar, V., & Kasera, S. K. (2020). Secrets in Source Code: Reducing False Positives using Machine Learning. In 2020 International Conference on COMmunication Systems & NETworkS (COMSNETS). IEEE Xplore Digital Library.
  DOI: 10.1109/comsnets48256.2020.9027350 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Private and public git repositories often contain unintentional sensitive information in the source code. Many tools have been developed to scan repositories looking for potential secrets and credentials committed in the code base, inadvertently or intentionally, for taking corrective action once these secrets and credentials are found. However, most of these existing works either target a specific type of secret or generate a large number of false positives. Our research aims to create a generalized framework to detect all kinds of secrets - which includes API keys, asymmetric private keys, client secrets, generic passwords - using an extensive regular expression list. We then apply machine learning models to intelligently distinguish between a real secret from a false positive. The combination of regular expression based approach and machine learning allows for the identification of different types of secrets, specifically generic passwords which are ignored by existing works, and subsequent reduction of possible false positives. We also evaluate our machine learning model using a precision-recall curve that can be used by an operator to find the optimal trade-off between the number of false positives and false negatives depending on their specific application. Using a Voting Classifier (combination of Logistic Regression, Naïve Bayes and SVM) we are able to reduce the number of false positives considerably.
• The Remote on the Local: Exacerbating Web Attacks Via Service Workers Caches in Progressive Web Applications
  Somé, D. F., Squarcina, M., Calzavara, S., & Maffei, M. (2020). The Remote on the Local: Exacerbating Web Attacks Via Service Workers Caches in Progressive Web Applications. EuroS&P 2020 SecWeb Workshop, Genova, IT, EU.
  Metadata
  

  Abstract

  Progressive Web Applications (PWAs) are the new trend in web development, promising several features and similar advantages as native applications. They heavily rely on modern web APIs to offer an engaging user experience. Service Workers are one of the core technologies employed by PWAs. They work as a proxy server for websites, allowing requests and responses to be modified, cached and served to the browser even when the user is offline. In this work we showcase a number of flaws in the Cache API that allow an attacker to void the security policies put in place by web developers, posing serious security and privacy threats. Given that these attacks are enabled by the presence of Service Workers, we demonstrate the impact of our findings by performing a large-scale analysis on the top 110K websites. Finally, we propose a redesign of the Cache API that prevents all the attacks discussed in the paper.

2019

• Group ORAM for Privacy and AccessControl in Outsourced Personal Records
  Maffei, M., Malavolta, G., Reinert, M., & Schröder, D. (2019). Group ORAM for Privacy and AccessControl in Outsourced Personal Records. Journal of Computer Security, 27(1), 1–47.
  DOI: 10.3233/jcs-171030 Metadata
  

  Abstract

  Cloud storage has rapidly become a cornerstone of many IT infrastructures, constituting a seamless solution for the backup, synchronization, and sharing of large amounts of data. Putting user data in the direct control of cloud service providers, however, raises security and privacy concerns related to the integrity of outsourced data, the accidental or intentional leakage of sensitive information, the profiling of user activities and so on. Furthermore, even if the cloud provider is trusted, users having access to outsourced files might be malicious and misbehave. These concerns are particularly serious in sensitive applications like personal health records and credit score systems. To tackle this problem, we present ΠGORAM, a definitional framework for Group Oblivious RAM, in which we formalize several security and privacy properties such as secrecy, integrity, anonymity, and obliviousness. ΠGORAM allows per entry access control, as selected by the data owner. ΠGORAM is the first framework to define such a wide range of security and privacy properties for outsourced storage. Regarding obliviousness, we tackle two different attacker models: our first definition protects against an honest-but-curious server while our second definition protects against such a server colluding with malicious clients. In the latter model, we prove a server-side computational lower bound of Ω(n) where n is the number of entries in the database, i.e., every operations requires to process a constant fraction of the database. Furthermore, we present two constructions: a pure cryptographic instantiation, which achieves an O(n) amortized communication and computation complexity and a construction based on a trusted proxy with logarithmic communication and server-side computational complexity. The second construction bypasses the previously established lower bound leveraging a trusted party. Both schemes achieve secrecy, integrity, and obliviousness with respect to a server colluding with malicious clients, but not anonymity due to the deployed access control mechanism. In the former model, we present a cryptographic system that achieves secrecy, integrity, obliviousness, and anonymity. In the process of designing an efficient construction, we developed three new, generally applicable cryptographic schemes, namely, batched zero-knowledge proof of shuffle correctness, the hash-and-proof paradigm, which even improves upon the former, and an accountability technique based on chameleon signatures, which we consider of independent interest. We implemented our constructions in Amazon Elastic Compute Cloud (EC2) and ran a performance evaluation demonstrating the scalability and efficiency of our construction.
• Gathering of robots in a ring with mobile faults
  Das, S., Focardi, R., Luccio, F. L., Markou, E., & Squarcina, M. (2019). Gathering of robots in a ring with mobile faults. Theoretical Computer Science, 764, 42–60.
  DOI: 10.1016/j.tcs.2018.05.002 Metadata ⯈Fulltext (preprint)
  

  Abstract

  This paper studies the well-known problem of gathering multiple mobile agents moving in a graph, but unlike previous results, we consider the problem in the presence of an adversarial mobile entity which we call the malicious agent. The malicious entity can occupy any empty node and prevent honest mobile agents from entering this node. This new adversarial model is interesting as it models transient mobile faults that can appear anywhere in a network. Moreover, our model lies between the less powerful delay-fault model, where the adversary can block an agent for only a finite time, and the more powerful but static fault model of black holes that can even destroy the agents. We study the problem for ring networks and we provide a complete characterization of the solvability of gathering, depending on the size n of the ring and the number of agents k. We consider both oriented or unoriented rings with either synchronous or asynchronous agents. We prove that in an unoriented ring network with asynchronous agents the problem is not solvable when k is even, while for synchronous agents the problem is unsolvable when both n is odd and k is even. We then present algorithms that solve gathering for all the remaining cases, thus completely solving the problem. Finally, we provide a proof-of-concept implementation of the synchronous algorithms using programmable Lego Mindstorms EV3 robots.
• Atomic Multi-Channel Updates with Constant Collateral in Bitcoin-Compatible Payment-Channel Networks
  Egger, C., Maffei, M., & Moreno-Sanchez, P. (2019). Atomic Multi-Channel Updates with Constant Collateral in Bitcoin-Compatible Payment-Channel Networks. In ACM (Ed.), Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. ACM.
  DOI: 10.1145/3319535.3345666 Metadata
• Automatisierte Prognose der Entwicklung von Kryptowährungspreisen
  Aumayr, L. (2019). Automatisierte Prognose der Entwicklung von Kryptowährungspreisen [Diploma Thesis, Technische Universität Wien]. reposiTUm.
  DOI: 10.34726/hss.2019.55455 Metadata
  

  Abstract

  Since the introduction of Bitcoin, cryptocurrencies have become very attractive as an alternative digital payment method and a highly speculative investment. With the rise in computational power and the growth of available data, the artificial intelligence concept of deep neural networks had a surge of popularity over the last years as well. With the introduction of the long short-term memory (LSTM) architecture, neural networks became more efficient in understanding long-term dependencies in data such as time series. In this thesis, we combine these two topics, by using neural networks to make a prognosis of cryptocurrency prices. In particular, we test if LSTM based neural networks can produce profitable trading signals for the cryptocurrency Ethereum. We experiment with different preprocessing techniques and different targets, both for price regression and trading signal classification. We evaluate two LSTM based networks and one convolutional neural network (CNN) LSTM hybrid. As data for training we use historical Ethereum price data in one-minute intervals from August 2017 to December 2018. We measure the performance of the models via backtesting, where we simulate trading on historic data not used for training based on the models predictions. We analyze that performance and compare it with the buy and hold strategy. The simulation is carried out on bullish, bearish and stagnating time periods. In the evaluation, we find the best performing target and pinpoint two preprocessing combinations that are most suitable for this task. We conclude that the CNN LSTM hybrid is capable of profitably forecasting trading signals for Ethereum, outperforming the buy and hold strategy by roughly 30%, while the performance of the other two models was disappointing.
• Latex Gloves: Protecting Browser Extensions from Probing and Revelation Attacks
  Sjösten, A., Van Acker, S., Picazo-Sanchez, P., & Sabelfeld, A. (2019). Latex Gloves: Protecting Browser Extensions from Probing and Revelation Attacks. In Proceedings 2019 Network and Distributed System Security Symposium. The Internet Society.
  DOI: 10.14722/ndss.2019.23309 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Browser extensions enable rich experience for the users of today's web. Being deployed with elevated privileges, extensions are given the power to overrule web pages. As a result, web pages often seek to detect the installed extensions, sometimes for benign adoption of their behavior but sometimes as part of privacy-violating user fingerprinting. Researchers have studied a class of attacks that allow detecting extensions by probing for Web Accessible Resources (WARs) via URLs that include public extension IDs. Realizing privacy risks associated with WARs, Firefox has recently moved to randomize a browser extension's ID, prompting the Chrome team to plan for following the same path. However, rather than mitigating the issue, the randomized IDs can in fact exacerbate the extension detection problem, enabling attackers to use a randomized ID as a reliable fingerprint of a user. We study a class of extension revelation attacks, where extensions reveal themselves by injecting their code on web pages. We demonstrate how a combination of revelation and probing can uniquely identify 90% out of all extensions injecting content, in spite of a randomization scheme. We perform a series of large-scale studies to estimate possible implications of both classes of attacks. As a countermeasure, we propose a browser-based mechanism that enables control over which extensions are loaded on which web pages and present a proof of concept implementation which blocks both classes of attacks.
• Forkcipher: A New Primitive for Authenticated Encryption of Very Short Messages
  Andreeva, E., Lallemand, V., Purnal, A., Reyhanitabar, R., Roy, A., & Vizár, D. (2019). Forkcipher: A New Primitive for Authenticated Encryption of Very Short Messages. In Lecture Notes in Computer Science (pp. 153–182). Springer LNCS.
  DOI: 10.1007/978-3-030-34621-8_6 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Highly efficient encryption and authentication of short messages is an essential requirement for enabling security in constrained scenarios such as the CAN FD in automotive systems (max. message size 64 bytes), massive IoT, critical communication domains of 5G, and Narrowband IoT, to mention a few. In addition, one of the NIST lightweight cryptography project requirements is that AEAD schemes shall be "optimized to be efficient for short messages (e.g., as short as 8 bytes)". In this work we introduce and formalize a novel primitive in symmetric cryptography called forkcipher. A forkcipher is a keyed primitive expanding a fixed-lenght input to a fixed-length output. We define its security as indistinguishability under a chosen ciphertext attack (for n-bit inputs to 2n-bit outputs). We give a generic construction validation via the new iterate-fork-iterate design paradigm. We then propose ForkSkinny as a concrete forkcipher instance with a public tweak and based on SKINNY: a tweakable lightweight cipher following the TWEAKEY framework. We conduct extensive cryptanalysis of ForkSkinny against classical and structure-specific attacks. We demonstrate the applicability of forkciphers by designing three new provably-secure nonce-based AEAD modes which offer performance and security tradeoffs and are optimized for efficiency of very short messages. Considering a reference block size of 16 bytes, and ignoring possible hardware optimizations, our new AEAD schemes beat the best SKINNY-based AEAD modes. More generally, we show forkciphers are suited for lightweight applications dealing with predominantly short messages, while at the same time allowing handling arbitrary messages sizes. Furthermore, our hardware implementation results show that when we exploit the inherent parallelism of ForkSkinny we achieve the best performance when directly compared with the most efficient mode instantiated with SKINNY.
• Reversible Proofs of Sequential Work
  Pietrzak, K., Walter, M., Klein, K., Kamath, C., & Abusalah, H. (2019). Reversible Proofs of Sequential Work. In Advances in Cryptology – EUROCRYPT 2019 (pp. 277–291). Springer LNCS.
  DOI: 10.1007/978-3-030-17656-3_10 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Proofs of sequential work (PoSW) are proof systems where a prover, upon receiving a statement χ and a time parameter T computes a proof ϕ(χ,T) which is efficiently and publicly verifiable. The proof can be computed in T sequential steps, but not much less, even by a malicious party having large parallelism. A PoSW thus serves as a proof that T units of time have passed since χ was received. PoSW were introduced by Mahmoody, Moran and Vadhan [MMV11], a simple and practical construction was only recently proposed by Cohen and Pietrzak [CP18]. In this work we construct a new simple PoSW in the random permutation model which is almost as simple and efficient as [CP18] but conceptually very different. Whereas the structure underlying [CP18] is a hash tree, our construction is based on skip lists and has the interesting property that computing the PoSW is a reversible computation. The fact that the construction is reversible can potentially be used for new applications like constructing proofs of replication. We also show how to "embed" the sloth function of Lenstra and Weselowski [LW17] into our PoSW to get a PoSW where one additionally can verify correctness of the output much more efficiently than recomputing it (though recent constructions of "verifiable delay functions" subsume most of the applications this construction was aiming at).
• Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability
  Malavolta, G., Moreno-Sanchez, P., Schneidewind, C., Kate, A., & Maffei, M. (2019). Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability. In Proceedings 2019 Network and Distributed System Security Symposium. Network and Distributed System Security Symposium (NDSS), USA, Non-EU.
  DOI: 10.14722/ndss.2019.23330 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Tremendous growth in cryptocurrency usage is exposing the inherent scalability issues with permis- sionless blockchain technology. Payment-channel networks (PCNs) have emerged as the most widely deployed solution to mitigate the scalability issues, allowing the bulk of payments between two users to be carried out off-chain. Unfortunately, as reported in the literature and further demonstrated in this paper, current PCNs do not provide meaningful security and privacy guarantees [30], [40]. In this work, we study and design secure and privacy- preserving PCNs. We start with a security analysis of exist- ing PCNs, reporting a new attack that applies to all major PCNs, including the Lightning Network, and allows an attacker to steal the fees from honest intermediaries in the same payment path. We then formally define anonymous multi-hop locks (AMHLs), a novel cryptographic primitive that serves as a cornerstone for the design of secure and privacy-preserving PCNs. We present several provably secure cryptographic instantiations that make AMHLs compatible with the vast majority of cryptocurrencies. In particular, we show that (linear) homomorphic one-way functions suffice to construct AMHLs for PCNs supporting a script language (e.g., Ethereum). We also propose a construction based on ECDSA signatures that does not require scripts, thus solving a prominent open problem in the field. AMHLs constitute a generic primitive whose useful- ness goes beyond multi-hop payments in a single PCN and we show how to realize atomic swaps and interoper- able PCNs from this primitive. Finally, our performance evaluation on a commodity machine finds that AMHL operations can be performed in less than 100 millisec- onds and require less than 500 bytes of communication overhead, even in the worst case. In fact, after acknowl- edging our attack, the Lightning Network developers have implemented our ECDSA-based AMHLs into their PCN. This demonstrates the practicality of our approach and its impact on the security, privacy, interoperability, and scalability of today´s cryptocurrencies.
• Atomic Multi-Channel Updates with Constant Collateral in Bitcoin-Compatible Payment-Channel Networks
  Egger, C., Moreno-Sanchez, P., & Maffei, M. (2019). Atomic Multi-Channel Updates with Constant Collateral in Bitcoin-Compatible Payment-Channel Networks [Conference Presentation]. Scaling Bitcoin 2019, Tel Aviv, Israel.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Current cryptocurrencies provide a heavily limited transaction throughput that is clearly insufficient to cater their growing adop- tion. Payment-channel networks (PCNs) have emerged as an inter- esting solution to the scalability issue and are currently deployed by popular cryptocurrencies such as Bitcoin and Ethereum. While PCNs do increase the transaction throughput by processing pay- ments off-chain and using the blockchain only as a dispute arbitra- tor, they unfortunately require high collateral (i.e., they lock coins for a non-constant time along the payment path) and are restricted to payments in a path from sender to receiver. These issues have severe consequences in practice. The high collateral enables denial- of-service attacks that hamper the throughput and utility of the PCN. Moreover, the limited functionality hinders the applicability of current PCNs in many important application scenarios. Unfortu- nately, current proposals do not solve either of these issues, or they require Turing-complete language support, which severely limit their applicability. In this work, we present AMCU, the first protocol for atomic multi-channel updates and reduced collateral that is compatible with Bitcoin (and other cryptocurrencies with reduced scripting ca- pabilities). We provide a formal model in the Universal Composabil- ity framework and show that AMCU realizes it, thus demonstrating that AMCU achieves atomicity and value privacy. Moreover, the reduced collateral mitigates the consequences of griefing attacks in PCNs while the (multi-payment) atomicity achieved by AMCU opens the door to new applications such as credit rebalancing and crowdfunding that are not possible otherwise. Moreover, our eval- uation results demonstrate that AMCU has a performance in line with that of the Lightning Network (the most widely deployed PCN) and thus is ready to be deployed in practice.
• Verifying Relational Properties using Trace Logic
  Barthe, G., Eilers, R., Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Verifying Relational Properties using Trace Logic. In B. Clark & J. Yang (Eds.), 2019 Formal Methods in Computer Aided Design (FMCAD). IEEE.
  DOI: 10.23919/fmcad.2019.8894277 Metadata
• Reducing Automotive Counterfeiting usingBlockchain: Benefits and Challenges
  Lu, D., Moreno-Sanchez, P., Zeryihun, A., Bajpayi, S., Yin, S., Feldman, K., Kosofsky, J., Mitra, P., & Kate, A. (2019). Reducing Automotive Counterfeiting usingBlockchain: Benefits and Challenges. In 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON) (pp. 39–48). IEEE Computer Society.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Counterfeiting constitutes a major challenge incurrent supply chains leading to millions of dollars of lostrevenue for the involved parties every year. Hardware-based au-thentication solutions built upon physically unclonable functions(PUF) and RFID tags prevent counterfeiting in a multipartysupply chain context. Unfortunately, these solutions cannotprevent counterfeiting and duplication attacks by supply chainparties themselves, as they can simply equivocate by duplicatingproducts in their local and unique activity ledger.In this work, we study the benefits and challenges of usingdistributed ledger technology (or blockchain) to prevent coun-terfeiting even in the presence of malicious supply chain parties.In particular, we show that the provision of a distributed andappend-only ledger jointly governed by supply chain partiesthemselves, by means of a distributed consensus algorithm,makes permissioned blockchains such as Hyperledger Fabric apromising approach towards mitigating counterfeiting. At thesame time, the distributed nature of the ledger also possessesa privacy challenge as competing supply chain parties strive toprotect their businesses from the prying eyes of competitors.Additionally, we show our efforts to build a blockchain-basedcounterfeiting prevention system for automotive supply chains,albeit the lessons learned are seamlessly applied to other supplychains. From our experience, we highlight two lessons: (i)the requirement of adding identities other than supply chainentities themselves to facilitate the tracking of goods; and (ii)the challenges derived from privacy enforcement in such apermissioned scenario. We thus finalize this work with a set ofchallenges that need to be overcome to achieve the best of bothworlds: a solution to the counterfeiting problem using distributedledger technology while providing the privacy notions of interestfor supply chain parties.Index Terms-Blockchain, supply chain, privacy, access con-trol, Hyperledger Fabric
• From Firewalls to Functions and Back
  Ceragioli, L., Galletta, L., & Tempesta, M. (2019). From Firewalls to Functions and Back. In Proceedings of the Third Italian Conference on Cyber Security (p. 13). CEUR-Proceedings.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Designing and maintaining firewall configurations is hardalso for expert system administrators. Indeed, policies are made of alarge number of rules and are written in low-level configuration languagesthat are specific to the firewall system in use. To simplify the work ofsystem administrators, some authors of the present paper proposed inprevious work a transcompilation pipeline and a tool that(i)extractsthe meaning of a real configuration by representing it into a tabular form;(ii)refactorsa configuration by removing redundant rules;(iii)portsthepolicy from a firewall system to another. Here, we extend this pipelineby proposing a new characterization that models rulesets and firewallsas functions from packets to transformations. Transformations specifywhich packets are accepted by the firewall and how they are translated.Using this functional characterization we propose two new algorithmsthat simplify the treatment of the pipeline
• Postcards from the Post-HTTP World: Amplification of HTTPS Vulnerabilities in the Web Ecosystem
  Calzavara, S., Focardi, R., Nemec, M., Rabitti, A., & Squarcina, M. (2019). Postcards from the Post-HTTP World: Amplification of HTTPS Vulnerabilities in the Web Ecosystem. In 2019 IEEE Symposium on Security and Privacy (SP). IEEE, Austria. IEEE.
  DOI: 10.1109/sp.2019.00053 Metadata ⯈Fulltext (preprint)
  

  Abstract

  HTTPS aims at securing communication over theWeb by providing a cryptographic protection layer that ensuresthe confidentiality and integrity of communication and enablesclient/server authentication. However, HTTPS is based on theSSL/TLS protocol suites that have been shown to be vulnerableto various attacks in the years. This has required fixes andmitigations both in the servers and in the browsers, producing acomplicated mixture of protocol versions and implementations inthe wild, which makes it unclear which attacks are still effectiveon the modern Web and what is their import on web applicationsecurity. In this paper, we present the first systematic quantitativeevaluation of web application insecurity due to cryptographicvulnerabilities. We specify attack conditions against TLS usingattack trees and we crawl the Alexa Top 10k to assess the importof these issues onpage integrity,authentication credentialsandweb tracking. Our results show that the security of a consistentnumber of websites is severely harmed by cryptographic weak-nesses that, in many cases, are due to external or related-domainhosts. This empirically, yet systematically demonstrates how arelatively limited number of exploitable HTTPS vulnerabilitiesare amplified by the complexity of the web ecosystem.
• Trace Reasoning for Formal Verification using the First-Order Superposition Calculus
  Georgiou, P., Gleiss, B., Kovacs, L., & Maffei, M. (2019). Trace Reasoning for Formal Verification using the First-Order Superposition Calculus. FMCAD 2019 Student Forum, San Jose, US, Non-EU.
  Metadata
• Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability
  Malavolta, G., Moreno-Sanchez, P., Schneidewind, C., Kate, A., & Maffei, M. (2019). Anonymous Multi-Hop Locks for Blockchain Scalability and Interoperability. ACM Advances in Financial Technologies AFT 2019, Zurich, Switzerland, Non-EU.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Tremendous growth in cryptocurrency usage is exposing the inherent scalability issues with permis- sionless blockchain technology. Payment-channel networks (PCNs) have emerged as the most widely deployed solution to mitigate the scalability issues, allowing the bulk of payments between two users to be carried out off-chain. Unfortunately, as reported in the literature and further demonstrated in this paper, current PCNs do not provide meaningful security and privacy guarantees [30], [40]. In this work, we study and design secure and privacy- preserving PCNs. We start with a security analysis of exist- ing PCNs, reporting a new attack that applies to all major PCNs, including the Lightning Network, and allows an attacker to steal the fees from honest intermediaries in the same payment path. We then formally define anonymous multi-hop locks (AMHLs), a novel cryptographic primitive that serves as a cornerstone for the design of secure and privacy-preserving PCNs. We present several provably secure cryptographic instantiations that make AMHLs compatible with the vast majority of cryptocurrencies. In particular, we show that (linear) homomorphic one-way functions suffice to construct AMHLs for PCNs supporting a script language (e.g., Ethereum). We also propose a construction based on ECDSA signatures that does not require scripts, thus solving a prominent open problem in the field. AMHLs constitute a generic primitive whose useful- ness goes beyond multi-hop payments in a single PCN and we show how to realize atomic swaps and interoper- able PCNs from this primitive. Finally, our performance evaluation on a commodity machine finds that AMHL operations can be performed in less than 100 millisec- onds and require less than 500 bytes of communication overhead, even in the worst case. In fact, after acknowl- edging our attack, the Lightning Network developers have implemented our ECDSA-based AMHLs into their PCN. This demonstrates the practicality of our approach and its impact on the security, privacy, interoperability, and scalability of today's cryptocurrencies.

2018

• ClearChart: Ensuring integrity of consumer ratings in online marketplaces
  Moreno-Sanchez, P., Mahmood, U., & Kate, A. (2018). ClearChart: Ensuring integrity of consumer ratings in online marketplaces. Computers and Security, 78, 90–102.
  DOI: 10.1016/j.cose.2018.04.014 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Popular online marketplaces make an extensive use of ratings to inform their prospective buyers about best-rated products in their service. Given a strong inclination among online buyers towards buying the best-rated products, there is a clear monetary incentive to sellers, and in turn to service providers, to unfairly push their favored products at the top of the ratings lists. Due to the centralized nature of these systems, the problem is particularly hard to solve against undetectable attacks by service providers. In this paper, we propose ClearChart, a transparency-enhancing mechanism to discourage this misbehavior in today's centralized marketplaces. Our protocol employs a novel distributed version of homomorphic MAC along with cryptographic accumulators and digital signatures to protect integrity of the ratings and improves verifiability of the ratings list. ClearChart introduces only a minimal storage overhead to the buyers and sellers, and can also tolerate collusion among sellers, the service provider and a subset of buyers. We have implemented ClearChart and demonstrated its practicality with an empirical evaluation.
• A Semantic Framework for the Security Analysis of Ethereum Smart Contracts
  Grishchenko, I., Schneidewind, C., & Maffei, M. (2018). A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In Lecture Notes in Computer Science (pp. 243–269). Springer Open.
  DOI: 10.1007/978-3-319-89722-6_10 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed. In this paper, we present the first complete small-step semantics of EVM bytecode, which we formalize in the F* proof assistant, obtaining executable code that we successfully validate against the official Ethereum test suite. Furthermore, we formally define for the first time a number of central security properties for smart contracts, such as call integrity, atomicity, and independence from miner controlled parameters. This formalization relies on a combination of hyper- and safety properties. Along this work, we identified various mistakes and imprecisions in existing semantics and verification tools for Ethereum smart contracts, thereby demonstrating once more the importance of rigorous semantic foundations for the design of security verification techniques.
• Settling Payments Fast and Private: Efficient Decentralized Routing for Path-Based Transactions
  Roos, S., Moreno-Sanchez, P., Kate, A., & Goldberg, I. (2018). Settling Payments Fast and Private: Efficient Decentralized Routing for Path-Based Transactions. In Proceedings 2018 Network and Distributed System Security Symposium. Network and Distributed System Security Symposium (NDSS), USA, Non-EU.
  DOI: 10.14722/ndss.2018.23254 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Decentralized path-based transaction (PBT) net- works maintain local payment channels between participants. Pairs of users leverage these channels to settle payments via a path of intermediaries without the need to record all transactions in a global blockchain. PBT networks such as Bitcoin´s Lightning Network and Ethereum´s Raiden Network are the most prominent examples of this emergent area of research. Both networks overcome scalability issues of widely used cryptocurrencies by replacing expensive and slow on-chain blockchain operations with inexpensive and fast off-chain transfers. At the core of a decentralized PBT network is a routing algorithm that discovers transaction paths between sender and receiver. In recent years, a number of routing algorithms have been proposed, including landmark routing, utilized in the decentralized IOU credit network SilentWhispers, and Flare, a link state algorithm for the Lightning Network. However, the existing efforts lack either efficiency or privacy, as well as the comprehensive analysis that is indispensable to ensure the success of PBT networks in practice. In this work, we first identify several efficiency concerns in existing routing algorithms for decentralized PBT networks. Armed with this knowledge, we design and evaluate SpeedyMurmurs, a novel routing algorithm for decentralized PBT networks using efficient and flexible embedding-based path discovery and on-demand efficient stabi- lization to handle the dynamics of a PBT network. Our simulation study, based on real-world data from the currently deployed Ripple credit network, indicates that SpeedyMurmurs reduces the overhead of stabilization by up to two orders of magnitude and the overhead of routing a transaction by more than a factor of two. Furthermore, using SpeedyMurmurs maintains at least the same success ratio as decentralized landmark routing, while providing lower delays. Finally, SpeedyMurmurs achieves key privacy goals for routing in decentralized PBT networks.
• Subset Predicate Encryption and Its Applications
  Katz, J., Maffei, M., Malavolta, G., & Schröder, D. (2018). Subset Predicate Encryption and Its Applications. In Cryptology and Network Security (pp. 115–134). Springer International Publishing.
  DOI: 10.1007/978-3-030-02641-7_6 Metadata ⯈Fulltext (preprint)
  

  Abstract

  In this work we introduce the notion of Subset Predicate Encryption, a form of attribute-based encryption (ABE) in which a message is encrypted with respect to a set s′ and the resulting ciphertext can be decrypted by a key that is associated with a set s if and only if s⊆s′. We formally define our primitive and identify several applications. We also propose two new constructions based on standard assumptions in bilinear groups; the constructions have very efficient decryption algorithms (consisting of one and two pairing computations, respectively) and small keys: in both our schemes, private keys contain only two group elements. We prove selective security of our constructions without random oracles. We demonstrate the usefulness of Subset Predicate Encryption by describing several black-box transformations to more complex primitives, such as identity-based encryption with wildcards and ciphertext-policy ABE for DNF formulas over a small universe of attributes. All of the resulting schemes are as efficient as the base Subset Predicate Encryption scheme in terms of decryption and key generation.
• UniTraX: Protecting Data Privacy with Discoverable Biases
  Munz, R., Eigner, F., Maffei, M., Francis, P., & Garg, D. (2018). UniTraX: Protecting Data Privacy with Discoverable Biases. In L. Bauer & R. Küsters (Eds.), Principles of Security and Trust (pp. 278–299). Springer, Lecture Notes in Computer Science.
  DOI: 10.1007/978-3-319-89722-6_12 Metadata ⯈Fulltext (preprint)
  

  Abstract

  An ongoing challenge with differentially private database systems is that of maximizing system utility while staying within a certain privacy budget. One approach is to maintain per-user budgets instead of a single global budget, and to silently drop users whose budget is depleted. This, however, can lead to very misleading analyses because the system cannot provide the analyst any information about which users have been dropped. This paper presents UniTraX, the first differentially private system that allows per-user budgets while providing the analyst information about the budget state. The key insight behind UniTraX is that it tracks budget not only for actual records in the system, but at all points in the domain of the database, including points that could exist but do not. UniTraX can safely report the budget state because the analyst does not know if the state refers to actual records or not. We prove that UniTraX is differentially private. UniTraX is compatible with existing differentially private analyses and our implementation on top of PINQ shows only moderate runtime overheads on a realistic workload.
• Equivalence Properties by Typing in Cryptographic Branching Protocols
  Cortier, V., Grimm, N., Lallemand, J., & Maffei, M. (2018). Equivalence Properties by Typing in Cryptographic Branching Protocols. In L. Bauer & R. Küsters (Eds.), Principles of Security and Trust (pp. 160–187). Springer LNCS.
  DOI: 10.1007/978-3-319-89722-6_7 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Recently, many tools have been proposed for automatically analysing, in symbolic models, equivalence of security protocols. Equivalence is a property needed to state privacy properties or game-based properties like strong secrecy. Tools for a bounded number of sessions can decide equivalence but typically suffer from efficiency issues. Tools for an unbounded number of sessions like Tamarin or ProVerif prove a stronger notion of equivalence (diff-equivalence) that does not properly handle protocols with else branches. Building upon a recent approach, we propose a type system for reasoning about branching protocols and dynamic keys. We prove our type system to entail equivalence, for all the standard primitives. Our type system has been implemented and shows a significant speedup compared to the tools for a bounded number of sessions, and compares similarly to ProVerif for an unbounded number of sessions. Moreover, we can also prove security of protocols that require a mix of bounded and unbounded number of sessions, which ProVerif cannot properly handle.
• A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
  Grimm, N., Maillard, K., Fournet, C., Hritcu, C., Maffei, M., Protzenko, J., Ramananandro, T., Swamy, N., & Zanella-Béguelin, S. (2018). A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. ACM Digital Library.
  DOI: 10.1145/3167090 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Relational properties describe multiple runs of one or more programs. They characterize many useful notions of security, program refinement, and equivalence for programs with diverse computational effects, and they have received much attention in the recent literature. Rather than developing separate tools for special classes of effects and relational properties, we advocate using a general purpose proof assistant as a unifying framework for the relational verification of effectful programs. The essence of our approach is to model effectful computations using monads and to prove relational properties on their monadic representations, making the most of existing support for reasoning about pure programs. We apply this method in F* and evaluate it by encoding a variety of relational program analyses, including information flow control, program equivalence and refinement at higher order, correctness of program optimizations and game-based cryptographic security. By relying on SMT-based automation, unary weakest preconditions, user-defined effects, and monadic reification, we show that, compared to unary properties, verifying relational properties requires little additional effort from the F* programmer.
• Functional Credentials
  Deuber, D., Maffei, M., Malavolta, G., Rabkin, M., Schröder, D., & Simkin, M. (2018). Functional Credentials. In Proceedings on Privacy Enhancing Technologies (pp. 64–84). Walter de Gruyter GmbH.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  A functional credential allows a user to anonymously prove possession of a set of attributes that fulfills a certain policy. The policies are arbitrary polynomially computable predicates that are evaluated over arbitrary attributes. The key feature of this primitive is the delegation of verification to third parties, called designated verifiers. The delegation protects the privacy of the policy : A designated verifier can verify that a user satisfies a certain policy without learning anything about the policy itself. We illustrate the usefulness of this property in different applications, including outsourced databases with access control. We present a new framework to construct functional credentials that does not require (non-interactive) zero-knowledge proofs. This is important in settings where the statements are complex and thus the resulting zero-knowledge proofs are not efficient. Our construction is based on any predicate encryption scheme and the security relies on standard assumptions. A complexity analysis and an experimental evaluation confirm the practicality of our approach.
• Simple Password Hardened Encryption Services
  Maffei, M., Reinert, M., Lai, R., Egger, C., Chow, S. S. M., & Schröder, D. (2018). Simple Password Hardened Encryption Services. In Proceedings of the 27th USENIX Security Symposium (pp. 1405–1421). USENIX.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Passwords and access control remain the popular choice for protecting sensitive data stored online, despite their well-known vulnerability to brute-force attacks. A natural solution is to use encryption. Although standard practices of using encryption somewhat alleviate the problem, decryption is often needed for utility, and keeping the decryption key within reach is obviously dangerous. To address this seemingly unavoidable problem in data security, we propose password-hardened encryption (PHE). With the help of an external crypto server, a service provider can recover the user data encrypted by PHE only when an end user supplied a correct password. PHE inherits the security features of passwordhardening (Usenix Security ´15), adding protection for the user data. In particular, the crypto server does not learn any information about any user data. More importantly, both the crypto server and the service provider can rotate their secret keys, a proactive security mechanism mandated by the Payment Card Industry Data Security Standard (PCI DSS). We build an extremely simple password-hardened encryption scheme. Compared with the state-of-the-art password-hardening scheme (Usenix Security ´17), our scheme only uses minimal number-theoretic operations and is, therefore, 30% - 50% more efficient. In fact, our extensive experimental evaluation demonstrates that our scheme can handle more than 525 encryption and (successful) decryption requests per second per core, which shows that it is lightweight and readily deployable in large-scale systems. Regarding security, our scheme also achieves a stronger soundness property, which puts less trust on the good behavior of the crypto server.
• WPSE: Fortifying Web Protocols via Browser-Side Security Monitoring
  Calzavara, S., Maffei, M., Schneidewind, C., Tempesta, M., & Squarcina, M. (2018). WPSE: Fortifying Web Protocols via Browser-Side Security Monitoring. In Proceedings of the 27th USENIX Security Symposium (pp. 1493–1510). USENIX.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  We present WPSE, a browser-side security monitor for web protocols designed to ensure compliance with the intended protocol flow, as well as confidentiality and integrity properties of messages. We formally prove that WPSE is expressive enough to protect web applications from a wide range of protocol implementation bugs and web attacks. We discuss concrete examples of attacks which can be prevented by WPSE on OAuth 2.0 and SAML 2.0, including a novel attack on the Google implementation of SAML 2.0 which we discovered by formalizing the protocol specification in WPSE. Moreover, we use WPSE to carry out an extensive experimental evaluation of OAuth 2.0 in the wild. Out of 90 tested websites, we identify security flaws in 55 websites (61.1%), including new critical vulnerabilities introduced by tracking libraries such as Facebook Pixel, all of which fixable by WPSE. Finally, we show that WPSE works flawlessly on 83 websites (92.2%), with the 7 compatibility issues being caused by custom implementations deviating from the OAuth 2.0 specification, one of which introducing a critical vulnerability.
• Foundations and Tools for the Static Analysis of Ethereum Smart Contracts
  Gishchenko, I., Maffei, M., & Schneidewind, C. (2018). Foundations and Tools for the Static Analysis of Ethereum Smart Contracts. In G. Weissenbacher & H. Chockler (Eds.), Computer Aided Verification (pp. 51–78). Springer Open.
  DOI: 10.1007/978-3-319-96145-3_4 Metadata ⯈Fulltext (preprint)
  

  Abstract

  The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics. This work will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust [1], a framework for the static analysis of Ethereum smart contracts which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first static analysis for EVM bytecode that comes with a proof of soundness.
• MineSweeper: An In-depth Look into Drive-by Cryptocurrency Mining and Its Defense
  Konoth, R. K., Vineti, E., Moonsamy, V., Lindorfer, M., Kruegel, C., Bos, H., & Vigna, G. (2018). MineSweeper: An In-depth Look into Drive-by Cryptocurrency Mining and Its Defense. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. ACM.
  DOI: 10.1145/3243734.3243858 Metadata ⯈Fulltext (preprint)
  

  Abstract

  A wave of alternative coins that can be effectively mined without specialized hardware, and a surge in cryptocurrencies´ market value has led to the development of cryptocurrency mining (cryptomining) services, such as Coinhive, which can be easily integrated into websites to monetize the computational power of their visitors. While legitimate website operators are exploring these services as an alternative to advertisements, they have also drawn the attention of cybercriminals: drive-by mining (also known as cryptojacking) is a new web-based attack, in which an infected website secretly executes JavaScript code and/or a WebAssembly module in the user´s browser to mine cryptocurrencies without her consent. In this paper, we perform a comprehensive analysis on Alexa´s Top 1 Million websites to shed light on the prevalence and profitabil- ity of this attack. We study the websites affected by drive-by mining to understand the techniques being used to evade detection, and the latest web technologies being exploited to efficiently mine cryptocurrency. As a result of our study, which covers 28 Coinhive-like services that are widely being used by drive-by mining websites, we identified 20 active cryptomining campaigns. Motivated by our findings, we investigate possible countermeasures against this type of attack. We discuss how current blacklisting approaches and heuristics based on CPU usage are insufficient, and present MineSweeper, a novel detection technique that is based on the intrinsic characteristics of cryptomining code, and, thus, is resilient to obfuscation. Our approach could be integrated into browsers to warn users about silent cryptomining when visiting websites that do not ask for their consent.
• Panoptispy: Characterizing Audio and Video Exfiltration from Android Applications
  Pan, E., Ren, J., Lindorfer, M., Wilson, C., & Choffnes, D. (2018). Panoptispy: Characterizing Audio and Video Exfiltration from Android Applications. In Proceedings on Privacy Enhancing Technologies (pp. 33–50). DeGruyter.
  DOI: 10.1515/popets-2018-0030 Metadata ⯈Fulltext (preprint)
  

  Abstract

  The high-fidelity sensors and ubiquitous internet connectivity offered by mobile devices have facilitated an explosion in mobile apps that rely on multi-media features. However, these sensors can also be used in ways that may violate user´s expectations and personal privacy. For example, apps have been caught taking pictures without the user´s knowledge and passively listened for inaudible, ultrasonic audio beacons. The developers of mobile device operating systems recognize that sensor data is sensitive, but unfortunately existing permission models only mitigate some of the privacy concerns surrounding multimedia data. In this work, we present the first large-scale empirical study of media permissions and leaks from Android apps, covering 17,260 apps from Google Play, AppChina, Mi.com, and Anzhi. We study the behavior of these apps using a combination of static and dynamic analysis techniques. Our study reveals several alarming privacy risks in the Android app ecosystem, including apps that over-provision their media permissions and apps that share image and video data with other parties in unexpected ways, without user knowledge or consent. We also identify a previously unreported privacy risk that arises from third-party libraries that record and upload screenshots and videos of the screen without informing the user and without requiring any permissions.
• GuardION: Practical Mitigation of DMA-Based Rowhammer Attacks on ARM
  van der Veen, V., Lindorfer, M., Fratantonio, Y., Padmanabha Pillai, H., Vigna, G., Kruegel, C., Bos, H., & Razavi, K. (2018). GuardION: Practical Mitigation of DMA-Based Rowhammer Attacks on ARM. In Detection of Intrusions and Malware, and Vulnerability Assessment (pp. 92–113). Springer.
  DOI: 10.1007/978-3-319-93411-2_5 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Over the last two years, the Rowhammer bug transformed from a hard-to-exploit DRAM disturbance error into a fully weaponized attack vector. Researchers demonstrated exploits not only against desktop computers, but also used single bit flips to compromise the cloud and mobile devices, all without relying on any software vulnerability. Since hardware-level mitigations cannot be backported, a search for software defenses is pressing. Proposals made by both academia and industry, however, are either impractical to deploy, or insufficient in stopping all attacks: we present rampage, a set of DMA-based Rowhammer attacks against the latest Android OS, consisting of (1) a root exploit, and (2) a series of app-to-app exploit scenarios that bypass all defenses. To mitigate Rowhammer exploitation on ARM, we propose guardion, a lightweight defense that prevents DMA-based attacks-the main attack vector on mobile devices-by isolating DMA buffers with guard rows. We evaluate guardion on 22 benchmark apps and show that it has a negligible memory overhead (2.2 MB on average). We further show that we can improve system performance by re-enabling higher order allocations after Google disabled these as a reaction to previous attacks.
• Bug Fixes, Improvements, ... and Privacy Leaks - A Longitudinal Study of PII Leaks Across Android App Versions
  Ren, J., Lindorfer, M., Dubois, D. J., Rao, A., Choffnes, D., & Vallina-Rodriguez, N. (2018). Bug Fixes, Improvements, ... and Privacy Leaks - A Longitudinal Study of PII Leaks Across Android App Versions. In Proceedings 2018 Network and Distributed System Security Symposium. Internet Society.
  DOI: 10.14722/ndss.2018.23143 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Is mobile privacy getting better or worse over time? In this paper, we address this question by studying privacy leaks from historical and current versions of 512 popular Android apps, covering 7,665 app releases over 8 years of app version history. Through automated and scripted interaction with apps and analysis of the network traffic they generate on real mobile devices, we identify how privacy changes over time for individual apps and in aggregate. We find several trends that include increased collection of personally identifiable information (PII) across app versions, slow adoption of HTTPS to secure the information sent to other parties, and a large number of third parties being able to link user activity and locations across apps. Interestingly, while privacy is getting worse in aggregate, we find that the privacy risk of individual apps varies greatly over time, and a substantial fraction of apps see little change or even improvement in privacy. Given these trends, we propose metrics for quantifying privacy risk and for providing this risk assessment proactively to help users balance the risks and benefits of installing new versions of apps.
• Firewall Management With FireWall Synthesizer
  Tempesta, M., Bodei, C., Degano, P., Forcardi, R., Galletta, L., & Veronese, L. (2018). Firewall Management With FireWall Synthesizer. In keiner (p. 1). ITASEC.
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Firewalls are notoriously hard to configure and maintain. Policies are written in low-level, system-specific languages where rules are inspected and enforced along non-trivialcontrol flow paths. Moreover, firewalls are tightly related to Network Address Translation(NAT) since filters need to be specified taking into account the possible translations ofpacket addresses, further complicating the task of network administrators. To simplifythis job, we proposeFireWall Synthesizer(FWS), a tool that decompiles real firewallconfigurations from different systems into an abstract specification. This representationhighlights the meaning of a configuration, i.e., the allowed connections with possible addresstranslations. We show the usage of FWS in analyzing and maintaining a configuration ona simple (yet realistic) scenario and we discuss how the tool scales on real-world policies
• Mind Your Keys? A Security Evaluation of Java Keystores
  Focardi, R., Squarcina, M., Steel, G., Palmarini, M., & Tempesta, M. (2018). Mind Your Keys? A Security Evaluation of Java Keystores. In Proceedings of 2019 Network and Distributed System Security Symposium (pp. 1–15).
  Metadata ⯈Fulltext (preprint)
  

  Abstract

  Cryptography is complex and variegate and re-quires to combine different algorithms and mechanisms in non-trivial ways. This complexity is often source of vulnerabilities.Secure key management is one of the most critical aspects,since leaking a cryptographic key vanishes any advantage ofusing cryptography. In this paper we analyze Java keystores,the standard way to manage and securely store keys in Javaapplications. We consider seven keystore implementations fromOracle JDK and Bouncy Castle, a widespread cryptographiclibrary. We describe, in detail, how the various keystores enforceconfidentiality and integrity of the stored keys through password-based cryptography and we show that many of the implementa-tions do not adhere to state-of-the-art cryptographic standards.We investigate the resistance to offline attacks and we show that,for non-compliant keystores, brute-forcing can be up to threeorders of magnitude faster with respect to the most compliantkeystore. Additionally, when an attacker can tamper with thekeystore file, some implementations are vulnerable to denial ofservice attacks or, in the worst case, arbitrary code execution.Finally we discuss the fixes implemented by Oracle and BouncyCastle developers following our responsible disclosure.
• Transcompiling Firewalls
  Bodei, C., Degano, P., Focardi, R., Galletta, L., & Tempesta, M. (2018). Transcompiling Firewalls. In L. Bauer & R. Küsters (Eds.), Principles of Security and Trust (pp. 303–324). Springer International Publishing AG.
  DOI: 10.1007/978-3-319-89722-6_13 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Porting a policy from a firewall system to another is a difficult and error prone task. Indeed, network administrators have to know in detail the policy meaning, as well as the internals of the firewall systems and of their languages. Equally difficult is policy maintenance and refactoring, e.g., removing useless or redundant rules. In this paper, we present a transcompiling pipeline that automatically tackles both problems: it can be used to port a policy into an equivalent one, when the target firewall language is different from the source one; when the two languages coincide, transcompiling supports policy maintenance and refactoring. Our transcompiler and its correctness are based on a formal intermediate firewall language that we endow with a formal semantics.
• Surviving the Web
  Calzavara, S., Squarcina, M., Focardi, R., & Tempesta, M. (2018). Surviving the Web. In Companion of the The Web Conference 2018 on The Web Conference 2018 - WWW ’18. International World Wide Web Conferences Steering Committee Republic and Canton of Geneva, Switzerland ©2018, Austria. ACM.
  DOI: 10.1145/3184558.3186232 Metadata ⯈Fulltext (preprint)
  

  Abstract

  We survey the most common attacks against web sessions, i.e.,attacks which target honest web browser users establishing an au-thenticated session with a trusted web application. We then reviewexisting security solutions which prevent or mitigate the differentattacks, by evaluating them along four different axes: protection,usability, compatibility and ease of deployment. Based on this sur-vey, we identify five guidelines that, to different extents, have beentaken into account by the designers of the different proposals wereviewed. We believe that these guidelines can be helpful for thedevelopment of innovative solutions approaching web security ina more systematic and comprehensive way
• Language-Independent Synthesis of Firewall Policies
  Bodei, C., Degano, P., Galletta, L., Focardi, R., Tempesta, M., & Veronese, L. (2018). Language-Independent Synthesis of Firewall Policies. In 2018 IEEE European Symposium on Security and Privacy (EuroS&P). Institute of Electrical and Electronics Engineers ( IEEE ), Austria. IEEE.
  DOI: 10.1109/eurosp.2018.00015 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Configuring and maintaining a firewall configura-tion is notoriously hard. Policies are written in low-level,platform-specific languages where firewall rules are inspectedand enforced along non trivial control flow paths. Furtherdifficulties arise from Network Address Translation (NAT),since filters must be implemented with addresses translationsin mind. In this work, we study the problem ofdecompilinga real firewall configuration into an abstract specification.This abstract version throws the low-level details away byexposing the meaning of the configuration, i.e., the allowedconnections with possible address translations. The generatedspecification makes it easier for system administrators to checkif:(i)the intended security policy is actually implemented;(ii)two configurations are equivalent;(iii)updates have thedesired effect on the firewall behavior. The peculiarity of ourapproach is that is independent of the specific target firewallsystem and language. This independence is obtained througha generic intermediate language that provides the typicalfeatures of real configuration languages and that separatesthe specification of the rulesets, determining the destiny ofpackets, from the specification of the platform-dependent stepsneeded to elaborate packets. We present a tool that decompilesreal firewall configurations from different systems into thisintermediate language and uses the Z3 solver to synthesizethe abstract specification that succinctly represents the firewallbehavior and the NAT. Tests on real configurations show thatthe tool is effective: it synthesizes complex policies in a matterof minutes and, and it answers to specific queries in just a fewseconds. The tool can also point out policy differences beforeand after configuration updates in a simple, tabular form.
• Mind Your Credit
  Moreno-Sanchez, P., Modi, N., Songhela, R., Kate, A., & Fahmy, S. (2018). Mind Your Credit. In Proceedings of the 2018 World Wide Web Conference on World Wide Web - WWW ’18. International World Wide Web Conferences Steering Committee Republic and Canton of Geneva, Switzerland ©2018, Austria. ACM Digital Library.
  DOI: 10.1145/3178876.3186099 Metadata ⯈Fulltext (preprint)
  

  Abstract

  The Ripple credit network has emerged as a payment backbone with key advantages for financial institutions and the remittance industry. Its path-based IOweYou (IOU) settlements across different (crypto)currencies conceptually distinguishes the Ripple blockchain from cryptocurrencies (such as Bitcoin and altcoins), and makes it highly suitable to an orthogonal yet vast set of applications in the remittance world for cross-border transactions and beyond. This work studies the structure and evolution of the Ripple network since its inception, and investigates its vulnerability to devilry attacks that affect the IOU credit of linnet users» wallets. We find that about 13M USD are at risk in the current Ripple network due to inappropriate configuration of the rippling flag on credit links, facilitating undesired redistribution of credit across those links. Although the Ripple network has grown around a few highly connected hub (gateway) wallets that constitute the core of the network and provide high liquidity to users, such a credit link distribution results in a user base of around 112,000 wallets that can be financially isolated by as few as 10 highly connected gateway wallets. Indeed, today about 4.9M USD cannot be withdrawn by their owners from the Ripple network due to PayRoutes, a gateway tagged as faulty by the Ripple community. Finally, we observe that stale exchange offers pose a real problem, and exchanges (market makers) have not always been vigilant about periodically updating their exchange offers according to current real-world exchange rates. For example, stale offers were used by 84 Ripple wallets to gain more than 4.5M USD from mid-July to mid-August 2017. Our findings should prompt the Ripple community to improve the health of the network by educating its users on increasing their connectivity, and by appropriately maintaining the credit limits, rippling flags, and exchange offers on their IOU credit links.
• Information Flow Tracking for Side-Effectful Libraries
  Sjösten, A., Hedin, D., & Sabelfeld, A. (2018). Information Flow Tracking for Side-Effectful Libraries. In Formal Techniques for Distributed Objects, Components, and Systems (pp. 141–160). Springer.
  DOI: 10.1007/978-3-319-92612-4_8 Metadata
  

  Abstract

  Dynamic information flow control is a promising technique for ensuring confidentiality and integrity of applications that manipulate sensitive information. While much progress has been made on increasingly powerful programming languages ranging from low-level machine languages to high-level languages for distributed systems, surprisingly little attention has been devoted to libraries and APIs. The state of the art is largely an all-or-nothing choice: either a shallow or deep library modeling approach. Seeking to break out of this restrictive choice, we formalize a general mechanism that tracks information flow for a language that includes higher-order functions, structured data types and references. A key feature of our approach is the model heap, a part of the memory, where security information is kept to enable the interaction between the labeled program and the unlabeled library. We provide a proof-of-concept implementation and report on experiments with a file system library. The system has been proved correct using Coq.

2017

• Surviving the Web: A Journey into Web Session Security
  Calzavara, S., Focardi, R., Squarcina, M., & Tempesta, M. (2017). Surviving the Web: A Journey into Web Session Security. ACM Computing Surveys, 50(1), 1–34.
  DOI: 10.1145/3038923 Metadata ⯈Fulltext (preprint)
  

  Abstract

  In this article, we survey the most common attacks against web sessions, that is, attacks that target honest web browser users establishing an authenticated session with a trusted web application. We then review existing security solutions that prevent or mitigate the different attacks by evaluating them along four different axes: protection, usability, compatibility, and ease of deployment. We also assess several defensive solutions that aim at providing robust safeguards against multiple attacks. Based on this survey, we identify five guidelines that, to different extents, have been taken into account by the designers of the different proposals we reviewed. We believe that these guidelines can be helpful for the development of innovative solutions approaching web security in a more systematic and comprehensive way.
• Principles of Security and Trust
  Maffei, M., & Ryan, M. (Eds.). (2017). Principles of Security and Trust (Vol. 10204). Springer-Verlag.
  DOI: 10.1007/978-3-662-54455-6 Metadata ⯈Fulltext (preprint)
  

  Abstract

  This book constitutes the proceedings of the 6th International Conference on Principles of Security and Trust, POST 2017, which took place in Uppsala, Sweden in April 2017, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017. The 14 papers presented in this volume were carefully reviewed and selected from 40 submissions. They were organized in topical sections named: information flow; security protocols; security policies; and information leakage.
• Concurrency and Privacy with Payment-Channel Networks
  Maffei, M., Kate, A., Malavolta, G., Moreno-Sanchez, P., & Ravi, S. (2017). Concurrency and Privacy with Payment-Channel Networks. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. ACM Digital Library.
  DOI: 10.1145/3133956.3134096 Metadata ⯈Fulltext (preprint)
  

  Abstract

  PermissionlessblockchainsprotocolssuchasBitcoinareinherently limitedintransactionthroughputandlatency.Currenteffortsto address this key issue focus on off-chain payment channels that canbecombinedinaPayment-ChannelNetwork(PCN)toenable anunlimitednumberofpaymentswithoutrequiringtoaccessthe blockchainotherthantoregistertheinitialandfinalcapacityof eachchannel.Whilethisapproachpavesthewayforlowlatency andhighthroughputofpayments,itsdeploymentinpracticeraises severalprivacyconcernsaswellastechnicalchallengesrelatedto theinherentlyconcurrentnatureofpaymentsthathavenotbeen sufficientlystudiedsofar. In this work, we lay the foundations for privacy and concurrency in PCNs, presenting a formal definition in the Universal Composability framework as well as practical and provably securesolutions.Inparticular,wepresentFulgorandRayo.Fulgor isthefirstpaymentprotocolforPCNsthatprovidesprovableprivacyguaranteesforPCNsandisfullycompatiblewiththeBitcoin scriptingsystem.However,Fulgorisablockingprotocolandtherefore prone to deadlocks of concurrent payments as in currently available PCNs. Instead, Rayo is the first protocol for PCNs that enforcesnon-blocking progress (i.e.,atleastoneoftheconcurrent payments terminates). We show through a new impossibility result that non-blocking progress necessarily comes at the cost of weakerprivacy.AtthecoreofFulgorandRayoisMulti-HopHTLC, anewsmartcontract,compatiblewiththeBitcoinscriptingsystem, thatprovidesconditionalpaymentswhilereducingrunningtime andcommunicationoverheadwithrespecttopreviousapproaches. OurperformanceevaluationofFulgorandRayoshowsthatapaymentwith10intermediateuserstakesasfewas5seconds,thereby demonstratingtheirfeasibilitytobedeployedinpractice.
• On the Security of Frequency-Hiding Order-Preserving Encryption
  Reinert, M., Schröder, D., & Maffei, M. (2017). On the Security of Frequency-Hiding Order-Preserving Encryption. In Cryptology and Network Security (pp. 51–70). Springer International Publishing.
  DOI: 10.1007/978-3-030-02641-7_3 Metadata ⯈Fulltext (preprint)
• A Type System for Privacy Properties
  Maffei, M., Lallemand, J., Cortier, V., & Grimm, N. (2017). A Type System for Privacy Properties. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. ACM CCS 2017 Conference on Computer and Communications Security, Dallas, USA, Non-EU. ACM Digital Library.
  DOI: 10.1145/3133956.3133998 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Maturepushbuttontoolshaveemergedforcheckingtraceproperties(e.g.secrecyorauthentication)ofsecurityprotocols.Thecase ofindistinguishability-basedprivacyproperties(e.g.ballotprivacy oranonymity)ismorecomplexandconstitutesanactiveresearch topicwithseveralrecentpropositionsoftechniquesandtools. Weexploreanovelapproachbasedontypesystemsandprovide a (sound) type system for proving equivalence of protocols, for a bounded or an unbounded number of sessions. The resulting prototype implementation has been tested on various protocols of the literature. It provides a significant speed-up (by orders of magnitude)comparedtotoolsforaboundednumberofsessions andcomplementsintermsofexpressivenessotherstate-of-the-art tools,suchasProVerifandTamarin:e.g.,weshowthatouranalysis techniqueisthefirstonetohandleafaithfulencodingoftheHelios e-votingprotocolinthecontextofanuntrustedballotbox.
• SilentWhispers: Enforcing Security and Privacy in Decentralized Credit Networks
  Maffei, M., Moreno-Sanchez, P., Kate, A., & Malavolta, G. (2017). SilentWhispers: Enforcing Security and Privacy in Decentralized Credit Networks. In Proceedings 2017 Network and Distributed System Security Symposium. Internet Society.
  DOI: 10.14722/ndss.2017.23448 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Abstract-Credit networks model transitive trust (or credit) between users in a distributed environment and have recently seen a rapid increase of popularity due to their flexible design and robustness against intrusion. They serve today as a backbone of real-world IOweYou transaction settlement networks such as Ripple and Stellar, which are deployed by various banks worldwide, as well as several other systems, such as spamresistant communication protocols and Sybil-tolerant social networks.Currentsolutions,however,raiseseriousprivacyconcerns, asthenetworktopologyaswellasthecreditvalueofthelinksare madepublicforapparenttransparencypurposesandanychanges are logged. In payment scenarios, for instance, this means that all transactions have to be public and everybody knows who paid what to whom. In this work, we question the necessity of a privacy-invasive transaction ledger. In particular, we present SilentWhispers, the first distributed, privacy-preserving credit network that does not require any ledger to protect the integrity of transactions. Yet, SilentWhispers guarantees integrity and privacy of link values and transactions even in the presence of distrustful users and malicious neighbors, whose misbehavior in changing link values is detected and such users can be held accountable. We formalize these properties as ideal functionalities in the universal composability framework and present a secure realization based on a novel combination of secret-sharing-based multiparty computation and digital signature chains. SilentWhispers can handle network churn, and it is efficient as demonstrated with a prototype implementation evaluated using payments data extracted from the currently deployed Ripple payment system.
• Maliciously Secure Multi-Client ORAM
  Maffei, M., Malavolta, G., Reinert, M., & Schröder, D. (2017). Maliciously Secure Multi-Client ORAM. In D. Gollmann, A. Miyaji, & H. Kikuchi (Eds.), Applied Cryptography and Network Security (pp. 645–664). © Springer International Publishing AG 2017.
  DOI: 10.1007/978-3-319-61204-1_32 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Oblivious RAM (ORAM) has emerged as an enabling technology to secure cloud-based storage services. The goal of this cryptographic primitive is to conceal not only the data but also the access patterns from the server. While the early constructions focused on a single client scenario, a few recent works have focused on a setting where multiple clients may access the same data, which is crucial to support data sharing applications. All these works, however, either do not consider malicious clients or they significantly constrain the definition of obliviousness and the system´s practicality. It is thus an open question whether a natural definition of obliviousness can be enforced in a malicious multi-client setting and, if so, what the communication and computational lower bounds are. In this work, we formalize the notion of maliciously secure multi-client ORAM, we prove that the server-side computational complexity of any secure realization has to be Ω(n), and we present a cryptographic instantiation of this primitive based on private information retrieval techniques, which achieves an O(√N) communication complexity. We further devise an efficient access control mechanism, built upon a novel and generally applicable realization of plaintext equivalence proofs for ciphertext vectors. Finally, we demonstrate how our lower bound can be bypassed by leveraging a trusted proxy, obtaining logarithmic communication and server-side computational complexity. We implemented our scheme and conducted an experimental evaluation, demonstrating the feasibility of our approach.
• A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications
  Maffei, M., Calzavara, S., Grishchenko, I., & Koutsos, A. (2017). A Sound Flow-Sensitive Heap Abstraction for the Static Analysis of Android Applications. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). IEEE Computer Security Foundations Symposium, Santa Barbara, USA, Non-EU. IEEE Xplore Digital Library.
  DOI: 10.1109/csf.2017.19 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Android is today the most popular operating system for mobile phones and tablets, and it boasts the largest application market among all its competitors. Though the huge number of available applications is arguably one of the main reasons for the success of Android, it also poses an important security challenge: there are way too many applications to ensure that they go through a timely and thorough security vetting before their publication on the market. Automated analysis tools thus play a critical role in ensuring that security verification does not fall behind with respect to the release of malicious (or buggy) applications. There are many relevant security concerns for Android applications, e.g., privilege escalation [12], [5] and component hijacking [26], but the most important challenge in the area is arguably information flow control, since Android applications are routinely granted access to personal information and other sensitive data stored on the device where they are installed. To counter the threats posed by malicious applications, the research community has proposed a plethora of increasingly sophisticated (static) information flow control frameworks for Android [41], [42], [27], [14], [22], [3], [40], [15], [7]. Despite all this progress, however, none of these static analysis tools is able to properly reconcile soundness and precision in its treatment of heap-allocated data structures
• Obfuscation-Resilient Privacy Leak Detection for Mobile Apps Through Differential Analysis
  Continella, A., Fratantonio, Y., Lindorfer, M., Puccetti, A., Zand, A., Kruegel, C., & Vigna, G. (2017). Obfuscation-Resilient Privacy Leak Detection for Mobile Apps Through Differential Analysis. In Proceedings 2017 Network and Distributed System Security Symposium. Internet Society.
  DOI: 10.14722/ndss.2017.23465 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Mobile apps are notorious for collecting a wealth of private information from users. Despite significant effort from the research community in developing privacy leak detection tools based on data flow tracking inside the app or through network traffic analysis, it is still unclear whether apps and ad libraries can hide the fact that they are leaking private information. In fact, all existing analysis tools have limitations: data flow tracking suffers from imprecisions that cause false positives, as well as false negatives when the data flow from a source of private information to a network sink is interrupted; on the other hand, network traffic analysis cannot handle encryption or custom encoding. We propose a new approach to privacy leak detection that is not affected by such limitations, and it is also resilient to obfuscation techniques, such as encoding, formatting, encryption, or any other kind of transformation performed on private information before it is leaked. Our work is based on black- box differential analysis, and it works in two steps: first, it establishes a baseline of the network behavior of an app; then, it modifies sources of private information, such as the device ID and location, and detects leaks by observing deviations in the resulting network traffic. The basic concept of black-box differential analysis is not novel, but, unfortunately, it is not practical enough to precisely analyze modern mobile apps. In fact, their network traffic contains many sources of non-determinism, such as random identifiers, timestamps, and server-assigned session identifiers, which, when not handled properly, cause too much noise to correlate output changes with input changes. The main contribution of this work is to make black-box dif- ferential analysis practical when applied to modern Android apps. In particular, we show that the network-based non-determinism can often be explained and eliminated, and it is thus possible to reliably use variations in the network traffic as a strong signal to detect privacy leaks. We implemented this approach in a tool, called AGRIGENTO, and we evaluated it on more than one thousand Android apps. Our evaluation shows that our approach works well in practice and outperforms current state-of-the-art techniques. We conclude our study by discussing several case studies that show how popular apps and ad libraries currently exfiltrate data by using complex combinations of encoding and encryption mechanisms that other approaches fail to detect. Our results show that these apps and libraries seem to deliberately hide their data leaks from current approaches and clearly demonstrate the need for an obfuscation-resilient approach such as ours.
• Run-Time Attack Detection in Cryptographic APIs
  Squarcina, M., & Focardi, R. (2017). Run-Time Attack Detection in Cryptographic APIs. In 2017 IEEE 30th Computer Security Foundations Symposium (CSF). IEEE Computer Security Foundations Symposium, Santa Barbara, USA, Non-EU. IEEE Xplore Digital Library.
  DOI: 10.1109/csf.2017.33 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Cryptographic APIs are often vulnerable to attacks that compromise sensitive cryptographic keys. In the literature we find many proposals for preventing or mitigating such attacks but they typically require to modify the API or to configure it in a way that might break existing applications. This makes it hard to adopt such proposals, especially because security APIs are often used in highly sensitive settings, such as financial and critical infrastructures, where systems are rarely modified and legacy applications are very common. In this paper we take a different approach. We propose an effective method to monitor existing cryptographic systems in order to detect, and possibly prevent, the leakage of sensitive cryptographic keys. The method collects logs for various devices and cryptographic services and is able to detect, offline, any leakage of sensitive keys, under the assumption that a key fingerprint is provided for each sensitive key. We define key security formally and we prove that the method is sound, complete and efficient. We also show that without key fingerprinting completeness is lost, i.e., some attacks cannot be detected. We discuss possible practical implementations and we develop a proof-of-concept log analysis tool for PKCS#11 that is able to detect, on a significant fragment of the API, all key-management attacks from the literature.
• A Principled Approach to Tracking Information Flow in the Presence of Libraries
  Hedin, D., Sjösten, A., Piessens, F., & Sabelfeld, A. (2017). A Principled Approach to Tracking Information Flow in the Presence of Libraries. In Lecture Notes in Computer Science (pp. 49–70). Springer.
  DOI: 10.1007/978-3-662-54455-6_3 Metadata ⯈Fulltext (preprint)
  

  Abstract

  There has been encouraging progress on information flow control for programs in increasingly complex programming languages, tracking the propagation of information from input sources to output sinks. Yet, programs are typically deployed in an environment with rich APIs and powerful libraries, posing challenges for information flow control when the code for these APIs and libraries is either unavailable or written in a different language. This paper presents a principled approach to tracking information flow in the presence of libraries. With the goal to strike the balance between security and precision, we present a framework that explores the middle ground between the "shallow", signature-based modeling of libraries and the "deep", stateful approach, where library models need to be supplied manually. We formalize our approach for a core language, extend it with lists and higher-order functions, and establish soundness results with respect to the security condition of noninterference.
• Discovering Browser Extensions via Web Accessible Resources
  Sjösten, A., Van Acker, S., & Sabelfeld, A. (2017). Discovering Browser Extensions via Web Accessible Resources. In Proceedings of the Seventh ACM on Conference on Data and Application Security and Privacy. ACM.
  DOI: 10.1145/3029806.3029820 Metadata ⯈Fulltext (preprint)
  

  Abstract

  Browser extensions provide a powerful platform to enrich browsing experience. At the same time, they raise important security questions. From the point of view of a website, some browser extensions are invasive, removing intended features and adding unintended ones, e.g. extensions that hijack Facebook likes. Conversely, from the point of view of extensions, some websites are invasive, e.g. websites that bypass ad blockers. Motivated by security goals at clash, this paper explores browser extension discovery, through a non-behavioral technique, based on detecting extensions' web accessible resources. We report on an empirical study with free Chrome and Firefox extensions, being able to detect over 50% of the top 1,000 free Chrome extensions, including popular security- and privacy-critical extensions such as AdBlock, LastPass, Avast Online Security, and Ghostery. We also conduct an empirical study of non-behavioral extension detection on the Alexa top 100,000 websites. We present the dual measures of making extension detection easier in the interest of websites and making extension detection more difficult in the interest of extensions. Finally, we discuss a browser architecture that allows a user to take control in arbitrating the conflicting security goals.