Publications
Below you find publications of our research unit.
Citations can be downloaded from reposiTUm (archive of TU Wien).
Final papers of our students are on a separate page.
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 MetadataAbstract
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., Kovács, 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 MetadataAbstract
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., & Kovács, L. (2024). Saturating Sorting without Sorts. arXiv.
DOI: 10.34726/5861 MetadataAbstract
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. -
Bridging realms: Analyzing app-to-web Interactions in IABs
Beer, P. (2024). Bridging realms: Analyzing app-to-web Interactions in IABs [Diploma Thesis, Technische Universität Wien]. reposiTUm.
DOI: 10.34726/hss.2024.118621 MetadataAbstract
In-app browsers (IABs) are heavily used components in mobile applications that allow app developers to display web content in native applications. Apart from simply rendering web content, such components provide the application with capabilities like the injection of JavaScript code and access to the website's cookies. While these features are useful for developers, they also allow potentially unwanted applications (PUAs) to perform malicious activities on benign websites, such as session hijacking using JavaScript injection. This thesis presents a novel approach to analyzing app-to-web interactions in Android WebView, the main built-in IAB component in Android. We use a combination of static and dynamic analysis techniques to first build a blueprint of an application and then dynamically drive the execution of the application to calls where IABs are launched. Our controlled environment allows us to record the interactions between the app and the web content, effectively minimizing false positives. We implement our approach as a prototype called IABInspect and apply it to 1,000 popular Android applications. In total, we are able to dynamically trigger 508 IAB launch calls in 196 applications and find an injection of JavaScript code in 50 applications. Our results show that the use of WebViews is ubiquitous in Android applications and that the injection of JavaScript code is a common practice, underscoring the need for further research in this area. -
Induction in Saturation
Kovács, L., Hozzová, P., Hajdu, M., & Voronkov, A. (2024). Induction in Saturation. In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 21–29). Springer.
DOI: 10.1007/978-3-031-63498-7_2 MetadataAbstract
Proof by induction is commonplace in modern mathematics and computational logic. This paper overviews and discusses our recent results in turning saturation-based first-order theorem proving into a powerful framework for automating inductive reasoning. We formalize applications of induction as new inference rules of the saturation process, add instances of appropriate induction schemata to the search space, and use these rules and instances immediately upon their addition for the purpose of guiding induction. Our results show, for example, that many problems from formal verification and mathematical theories can now be solved completely automatically using a first-order theorem prover. -
VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic
Schoisswohl, J., Kovács, L., & Korovin, K. (2024). VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 147–164).
DOI: 10.29007/kg4v MetadataAbstract
We introduce Virtual Integer-Real Arithmetic Substitution (Viras), a quantifier elimination procedure for deciding quantified linear mixed integer-real arithmetic problems. Viras combines the framework of virtual substitutions with conflict-driven proof search and linear integer arithmetic reasoning based on Cooper’s method. We demonstrate that Viras gives an exponential speedup over state-of-the-art methods in quantified arithmetic reasoning, proving problems that SMT-based techniques fail to solve. -
Optimizing Virtual Payment Channel Establishment in the Face of On-Path Adversaries
Aumayr, L., Ceylan, E., Kopyciok, Y., Maffei, M., Moreno-Sanchez, P., Salem, I., & Schmid, S. (2024). Optimizing Virtual Payment Channel Establishment in the Face of On-Path Adversaries. In Proceedings 2024 IFIP Networking Conference (IFIP Networking) (pp. 1–10).
DOI: 10.23919/IFIPNetworking62109.2024.10619889 MetadataAbstract
Payment channel networks (PCNs) are among the most promising solutions to the scalability issues in permissionless blockchains, by allowing parties to pay each other off-chain through a path of payment channels (PCs). However, routing transactions comes at a cost which is proportional to the number of intermediaries, since each charges a fee for the routing service. Furthermore, analogous to other networks, malicious intermediaries in the payment path can lead to security and privacy threats. Virtual channels (VCs), i.e., bridges over PC paths, mitigate the above PCN issues, as an intermediary participates only once to set up the VC and is then excluded from every future VC transaction. However, similar to PCs, creating a VC has a cost that must be paid out of the bridged PCs' balance. Currently, we are missing guidelines to where and how many VCs to set up. Ideally, VCs should minimize transaction costs while mitigating security and privacy threats from on-path adversaries. In this work, we address for the first time the VC setup problem, formalizing it as an optimization problem. We present an integer linear program (ILP) to compute the globally optimal VC setup strategy in terms of transaction costs, security, and privacy. We then accompany the computationally heavy ILP with a fast local greedy algorithm. Our model and algorithms can be used with any on-path adversary, given that its strategy can be expressed as a set of corrupted nodes that is estimated by the honest nodes. We conduct an evaluation of the greedy algorithm over a snapshot of the Lightning Network (LN), the largest Bitcoin-based PCN. Our results confirm on real-world data that our greedy strategy minimizes costs while protecting against security and privacy threats of on-path adversaries. These findings may serve the LN community as guidelines for the deployment of VCs. -
Concurrently Secure Blind Schnorr Signatures
Fuchsbauer, G., & Wolf, M. (2024). Concurrently Secure Blind Schnorr Signatures. In Advances in Cryptology – EUROCRYPT 2024 (pp. 124–160).
DOI: 10.1007/978-3-031-58723-8_5 MetadataAbstract
Many applications of blind signatures, e.g. in blockchains, require compatibility of the resulting signatures with the existing system. This makes blind issuing of Schnorr signatures (now being standardized and supported by major cryptocurrencies) desirable. Concurrent security of the signing protocol is required to thwart denial-of-service attacks. We present a concurrently secure blind-signing protocol for Schnorr signatures, using the standard primitives NIZK and PKE and assuming that Schnorr signatures themselves are unforgeable. Our protocol is the first to be compatible with standard Schnorr implementations over 256-bit elliptic curves. We cast our scheme as a generalization of blind and partially blind signatures: we introduce the notion of predicate blind signatures, in which the signer can define a predicate that the blindly signed message must satisfy. We provide implementations and benchmarks for various choices of primitives and scenarios, such as blindly signing Bitcoin transactions only when they meet certain conditions specified by the signer. -
Distillation based Robustness Verification with PAC Guarantees
Indri, P., Blohm, P., Athavale, A., Bartocci, E., Weissenbacher, G., Maffei, M., Nickovic, D., Gärtner, T., & Malhotra, S. (2024). Distillation based Robustness Verification with PAC Guarantees. In International Conference on Machine Learning 2024 - Next Generation of AI Safety Workshop. International Conference on Machine Learning 2024 - Next Generation of AI Safety Workshop, Vienna, Austria.
MetadataAbstract
We present a distillation based approach to verify the robustness of any Neural Network (NN). Conventional formal verification methods cannot tractably assess the global robustness of real-world NNs. To address this, we take advantage of a gradient-aligned distillation framework to transfer the robustness properties from a larger teacher network to a smaller student network. Given that the student NN can be formally verified for global robustness, we theoretically investigate how this guarantee can be transferred to the teacher NN. We draw from ideas in learning theory to derive a sample complexity for the distillation procedure that enables PAC-guarantees on the global robustness of the teacher network. -
How (Not) to Simulate PLONK
Sefranek, M. (2024). How (Not) to Simulate PLONK. In Security and Cryptography for Networks (pp. 96–117).
DOI: 10.1007/978-3-031-71070-4_5 MetadataAbstract
PLONK is a zk-SNARK system by Gabizon, Williamson, and Ciobotaru with proofs of constant size (0.5 KB) and sublinear verification time. Its setup is circuit-independent supporting proofs of arbitrary statements up to a certain size bound. Although deployed in several real-world applications, PLONK’s zero-knowledge property had only been argued informally. Consequently, we were able to find and fix a vulnerability in its original specification, leading to an update of PLONK in eprint version 20220629:105924. In this work, we construct a simulator for the patched version of PLONK and prove that it achieves statistical zero knowledge. Furthermore, we give an attack on the previous version of PLONK showing that it does not even satisfy the weaker notion of (statistical) witness indistinguishability. -
On Proving Equivalence Class Signatures Secure from Non-interactive Assumptions
Bauer, B., Fuchsbauer, G., & Regen, F. (2024). On Proving Equivalence Class Signatures Secure from Non-interactive Assumptions. In Public-Key Cryptography – PKC 2024 (pp. 3–36).
DOI: 10.1007/978-3-031-57718-5_1 MetadataAbstract
Equivalence class signatures (EQS), introduced by Hanser and Slamanig (AC’14, J. Crypto’19), sign vectors of elements from a bilinear group. Their main feature is “adaptivity”: given a signature on a vector, anyone can transform it to a (uniformly random) signature on any multiple of the vector. A signature thus authenticates equivalence classes and unforgeability is defined accordingly. EQS have been used to improve the efficiency of many cryptographic applications, notably (delegatable) anonymous credentials, (round-optimal) blind signatures, group signatures and anonymous tokens. EQS security implies strong anonymity (or blindness) guarantees for these schemes which holds against malicious signers without trust assumptions. Unforgeability of the original EQS construction is proven directly in the generic group model. While there are constructions from standard assumptions, these either achieve prohibitively weak security notions (PKC’18) or they require a common reference string (AC’19, PKC’22), which reintroduces trust assumptions avoided by EQS. In this work we ask whether EQS schemes that satisfy the original security model can be proved secure under standard (or even non-interactive) assumptions with standard techniques. Our answer is negative: assuming a reduction that, after running once an adversary breaking unforgeability, breaks a non-interactive computational assumption, we construct efficient meta-reductions that either break the assumption or break class-hiding, another security requirement for EQS. -
Updatable Public-Key Encryption, Revisited
Alwen, J., Fuchsbauer, G., & Mularczyk, M. (2024). Updatable Public-Key Encryption, Revisited. In Advances in Cryptology – EUROCRYPT 2024 (pp. 346–376).
DOI: 10.1007/978-3-031-58754-2_13 MetadataAbstract
We revisit Updatable Public-Key Encryption (UPKE), which was introduced as a practical mechanism for building forward-secure cryptographic protocols. We begin by observing that all UPKE notions to date are neither syntactically flexible nor secure enough for the most important multi-party protocols motivating UPKE. We provide an intuitive taxonomy of UPKE properties – some partially or completely overlooked in the past – along with an overview of known (explicit and implicit) UPKE constructions. We then introduce a formal UPKE definition capturing all intuitive properties needed for multi-party protocols. Next, we provide a practical pairing-based construction for which we provide concrete bounds under a standard assumption in the random oracle and the algebraic group model. The efficiency profile of the scheme compares very favorably with existing UPKE constructions (despite the added flexibility and stronger security). For example, when used to improve the forward security of the Messaging Layer Security protocol [RFC9420], our new UPKE construction requires less than 1.5% of the bandwidth of the next-most efficient UPKE construction satisfying the strongest UPKE notion considered so far. -
Verifying Global Two-Safety Properties in Neural Networks with Confidence
Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Ničković, D., & Weissenbacher, G. (2024). Verifying Global Two-Safety Properties in Neural Networks with Confidence. In A. Gurfinkel & V. Ganesh (Eds.), Computer Aided Verification (pp. 329–351). Springer.
DOI: 10.1007/978-3-031-65630-9_17 MetadataAbstract
We present the first automated verification technique for confidence-based 2-safety properties, such as global robustness and global fairness, in deep neural networks (DNNs). Our approach combines self-composition to leverage existing reachability analysis techniques and a novel abstraction of the softmax function, which is amenable to automated verification. We characterize and prove the soundness of our static analysis technique. Furthermore, we implement it on top of Marabou, a safety analysis tool for neural networks, conducting a performance evaluation on several publicly available benchmarks for DNN verification. -
A TPRF-based pseudo-random number generator
Andreeva, E., & Weninger, A. (2024). A TPRF-based pseudo-random number generator. Journal of Surveillance, Security and Safety, 5, 36–51.
DOI: 10.20517/jsss.2023.45 MetadataAbstract
Most cryptographic applications use randomness that is generated by pseudo-random number generators (PRNGs). A popular PRNG practical choice is the NIST standardized CTR_DRBG. In their recent ACNS 2023 publication, Andreeva and Weninger proposed a new and more efficient and secure PRNG called FCRNG. FCRNG is based on CTR_DRBG and uses the 𝑛-to-2𝑛 forkcipher expanding primitive ForkSkinny as a building block. In this work, we create a new BKRNG PRNG, which is based on FCRNG and employs the novel 𝑛-to-8𝑛 expanding primitive Butterknife. Butterknife is based on the Deoxys tweakable blockcipher (and thus AES) and realizes a tweakable expanding pseudo-random function. While both blockciphers and forkciphers are invertible primitives, tweakable expanding pseudo-random functions are not. This functional simplification enables security benefits for BKRNG in the robustness security game - the standard security goal for a PRNG. Contrary to the security bound of CTR_DRBG, we show that the security of our BKRNG construction does not degrade with the length of the random inputs, nor the number of requested output pseudo-random bits. We also empirically verify the BKRNG security with the NIST PRNG test suite and the TestU01 suite. Furthermore, we show the 𝑛-to-8𝑛 multi-branch expanding nature of Butterknife contributes to a significant speed-up in the efficiency of BKRNG compared to FCRNG. More concretely, producing random bits with BKRNG is 30.0% faster than FCRNG and 49.2% faster than CTR_DRBG. -
Are You Sure You Want To Do Coordinated Vulnerability Disclosure?
Chen, T.-H., Tagliaro, C., Lindorfer, M., Borgolte, K., & van der Ham-de Vos, J. (2024). Are You Sure You Want To Do Coordinated Vulnerability Disclosure? In 2024 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW) (pp. 307–314).
DOI: 10.1109/EuroSPW61312.2024.00039 MetadataAbstract
The rising numbers of vulnerabilities and security issues stemming from the rapid iteration and development of the Internet of Things (IoT) have introduced new challenges for the involved stakeholders to mitigate them in time. To effectively bring researchers, vendors, and end-users together to address such problems, Coordinated Vulnerability Disclosure (CVD) has become standard practice. Although general CVD procedures for practitioners to follow exist, adapting them to the specific circumstances has proven to be complicated in practice. In this paper, we document our experience of reporting various security vulnerabilities for 15,820 IoT backends. The discovery and scanning have been part of a separate research project, in this contribution we focus on the disclosure to the backends' operators in a large-scale coordinated vulnerability disclosure effort, following the latest disclosure guidelines. We discuss what we have learned to inform others who want to engage in large-scale CVD, we compare the steps and tradeoffs of our effort with current CVD suggestions, based on our measurement before and after the disclosure, and we describe how adapting our approach can improve CVD best practices. -
Exploring the Malicious Document Threat Landscape: Towards a Systematic Approach to Detection and Analysis
Saha, A., Blasco Alís, J., & Lindorfer, M. (2024). Exploring the Malicious Document Threat Landscape: Towards a Systematic Approach to Detection and Analysis. In 2024 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW) (pp. 533–544).
DOI: 10.1109/EuroSPW61312.2024.00065 MetadataAbstract
Despite being the most common initial attack vector, document-based malware delivery remains understudied compared to research on malicious executables. This limits our understanding of how attackers leverage document file formats and exploit their functionalities for malicious purposes. In this paper, we perform a measurement study that leverages existing tools and techniques to detect, extract, and analyze malicious Office documents. We collect a substantial dataset of 9,086 malicious samples and reveal a critical gap in the understanding of how attackers utilize these documents. Our in-depth analysis highlights emerging tactics used in both targeted and large-scale cyberattacks while identifying weaknesses in common document analysis methods. Through a combination of analysis techniques, we gain crucial in-sights valuable for forensic analysts to assess suspicious files, pinpoint infection origins, and ultimately contribute to the development of more robust detection models. We make our dataset and source code available to the academic community to foster further research in this area. -
Inductive Predicate Synthesis Modulo Programs (Extended)
Wesley, S., Christakis, M., Navas, J. A., Trefler, R., Wüstholz, V., & Gurfinkel, A. (2024). Inductive Predicate Synthesis Modulo Programs (Extended). arXiv.
DOI: 10.34726/7020 MetadataAbstract
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the-shelf verifiers, but makes communication with the underlying solver more challenging. Essentially, the analyzer operates at the level of input programs, whereas the solver operates at the level of problem encodings. To bridge this gap, the verifier must pass along proof-rules from the analyzer to the solver. For example, an analyzer for concurrent programs built on an inductive program verifier might need to declare Owicki-Gries style proof-rules for the underlying solver. Each such proof-rule further specifies how a program should be verified, meaning that the problem of passing proof-rules is a form of invariant synthesis. Similarly, many program analysis tasks reduce to the synthesis of pure, loop-free Boolean functions (i.e., predicates), relative to a program. From this observation, we propose Inductive Predicate Synthesis Modulo Programs (IPS-MP) which extends high-level languages with minimal synthesis features to guide analysis. In IPS-MP, unknown predicates appear under assume and assert statements, acting as specifications modulo the program semantics. Existing synthesis solvers are inefficient at IPS-MP as they target more general problems. In this paper, we show that IPS-MP admits an efficient solution in the Boolean case, despite being generally undecidable. Moreover, we show that IPS-MP reduces to the satisfiability of constrained Horn clauses, which is less general than existing synthesis problems, yet expressive enough to encode verification tasks. We provide reductions from challenging verification tasks -- such as parameterized model checking -- to IPS-MP. We realize these reductions with an efficient IPS-MP-solver based on SeaHorn, and describe a application to smart-contract verification. -
Tabbed Out: Subverting the Android Custom Tab Security Model
Beer, P., Squarcina, M., Veronese, L., & Lindorfer, M. (2024). Tabbed Out: Subverting the Android Custom Tab Security Model. In 2024 IEEE Symposium on Security and Privacy (SP) (pp. 4591–4609).
DOI: 10.1109/SP54263.2024.00105 MetadataAbstract
Mobile operating systems provide developers with various mobile-to-Web bridges to display Web pages inside native applications. A recently introduced component called Custom Tab (CT) provides an outstanding feature to overcome the usability limitations of traditional WebViews: it shares the state with the underlying browser. Similar to traditional WebViews, it can also keep the host application informed about ongoing Web navigations. In this paper, we perform the first systematic security evaluation of the CT component and show how the design of its security model did not consider cross- context state inference attacks when the feature was introduced. Additionally, we show how CTs can be exploited for fine-grained exfiltration of sensitive user browsing data, violation of Web session integrity by circumventing SameSite cookies, and how UI customization of the CT component can lead to phishing and information leakage. To assess the prevalence of CTs in the wild and the practicality of the mitigation strategies we propose, we carry out the first large-scale analysis of CT usage on over 50K Android applications. Our analysis reveals that their usage is widespread, with 83% of applications embedding CTs either directly or as part of a library. We have responsibly disclosed all our findings to Google, which has already taken steps to apply targeted mitigations, assigned three CVEs for the discovered vulnerabilities, and awarded us $10,000 in bounties. Our interaction with Google led to clarifications of the CT security model in the new Chrome Custom Tabs Security FAQ document. -
C2Miner: Tricking IoT Malware into Revealing Live Command & Control Servers
Davanian, A., Faloutsos, M., & Lindorfer, M. (2024). C2Miner: Tricking IoT Malware into Revealing Live Command & Control Servers. In ASIA CCS ’24: Proceedings of the 19th ACM Asia Conference on Computer and Communications Security (pp. 112–127).
DOI: 10.1145/3634737.3644992 MetadataAbstract
How can we identify live Command & Control (C2) servers for a given IoT malware binary? An effective solution to this problem constitutes a significant capability towards detecting and containing botnets. This task is not trivial because C2 servers are short-lived, and they use sophisticated and proprietary communication protocols. We propose C2Miner, a novel approach to trick IoT malware binaries into revealing their currently live C2 servers. Our approach weaponizes old disposable IoT malware binaries and uses them to probe active servers. We provide novel solutions to overcome the following challenges: (a) disambiguating the C2-bound traffic generated by the malware and (b) determining if a target IP:port is indeed a C2 server as opposed to a benign server. In our evaluation, based on 3M distinct exploration attempts over 150K distinct IP addresses, we show that we can identify C2 servers within a given IP:port space with an F1 score of 86%. In addition, we show how our approach can be used in practice and at scale. Conducting a large-scale probing campaign has scalability issues given that the number of probes is proportional to the IP addresses, the number of ports, and the number of binaries from distinct families which we want to explore. To address this challenge, we propose a grammar-based method to fingerprint and cluster C2 communications which, among other applications, allows us to select malware binaries for weaponization efficiently. Additionally, we use spatio-temporal features of C2 servers to narrow down our search in the entire IP space. An optimistic observation from our study is that using only 2 (more than 6 months) old IoT malware binaries, we scan 18K IP:port pairs daily for 6 days and find 6 new live C2 servers. -
On Efficient and Secure Compression Functions for Arithmetization-Oriented Hashing
Andreeva, E., Bhattacharyya, R., Roy, A., & Trevisani, S. (2024). On Efficient and Secure Compression Functions for Arithmetization-Oriented Hashing. In 2024 IEEE 37th Computer Security Foundations Symposium (CSF) (pp. 1–16).
DOI: 10.1109/CSF61375.2024.00045 MetadataAbstract
ZK-SNARKs, a fundamental component of privacyoriented payment systems, identity protocols, or anonymous voting systems, are advanced cryptographic protocols for verifiable computation: modern SNARKs allow to encode the invariants of a program, expressed as an arithmetic circuit, in an appropriate constraint language from which short, zero-knowledge proofs for correct computations can be constructed. One of the most important computations that is run through SNARK systems is the verification of Merkle tree (MT) opening proofs, which relies on the evaluation of a fixed-input-length (FIL) cryptographic compression function over binary MTs. As classical, bit-oriented hash functions like SHA-2 are not compactly representable in SNARK frameworks, Arithmetization-Oriented (AO) cryptographic designs have emerged as an alternative, efficient solution. Today, the majority of AO compression functions are built from permutation-based hashing modes, such as Sponge. While this approach allows cost savings, compared to blockcipher-based modes, as it does not require key-scheduling, AO blockcipher schedulers are often cheap to compute. Furthermore, classical bitoriented cryptography has long studied how to construct provably secure compression functions from blockciphers, following the Preneel-Govaerts-Vandewalle (PGV) framework. The potential efficiency gains together with the strong provable security foundations in the classic setting, motivate the study of AO blockcipher-based compression functions. In this work, we propose AO PGV-LC and PGV-ELC, two AO blockcipher-based FIL compression modes inspired by and extending the classical PGV approach, offering flexible input and output sizes and coming with provable security guarantees in the AO setting. We prove the collision and preimage resistance in the ideal cipher model, and give bounds for collision and opening resistance over MTs of arbitrary arity. We compare experimentally the AO PGV-ELC mode over the HADES blockcipher with its popular and widely adopted Sponge instantiation, POSEIDON, and its improved variant POSEIDON2. Our resulting constructions are up to 3× faster than POSEIDONAND 2× faster than POSEIDON2 in native x86 execution, and up to 50% faster in the Groth16 SNARK framework. Finally, we study the benefits of using MTs of arity wider than two, proposing a new strategy to obtain a compact R1CS constraint system in such case. In fact, by combining an efficient parametrization of the HADES blockcipher over the PGV-ELC mode, together with an optimal choice of the MT arity, we measured an improvement of up to 9× in native MT construction time, and up to 2.5× in proof generation time, compared to POSEIDON over binary MTs. -
Trust Me If You Can - How Usable Is Trusted Types In Practice?
Roth, S., Gröber, L., Baus, P., Krombholz, K., & Stock, B. (2024). Trust Me If You Can - How Usable Is Trusted Types In Practice? In 33rd USENIX Security Symposium (USENIX Security 24) (pp. 6003–6020).
MetadataAbstract
Many online services deal with sensitive information such as credit card data, making those applications a prime target for adversaries, e.g., through Cross-Site Scripting (XSS) attacks. Moreover, Web applications nowadays deploy their functionality via client-side code to lower the server's load, require fewer page reloads, and allow Web applications to work even if the connection is interrupted. Given this paradigm shift of increasing complexity on the browser side, client-side security issues such as client-side XSS are getting more prominent these days. A solution already deployed in server-side applications of major companies like Google is to use type-safe data, where potentially attacker-controlled string data can never be output with sanitization. The newly introduced Trusted Types API offers an analogous solution for client-side XSS. With Trusted Types, the browser enforces that no input can be passed to an execution sink without being sanitized first. Thus, a developer's only remaining task -- in theory -- is to create a proper sanitizer. This study aims to uncover roadblocks that occur during the deployment of the mechanism and strategies on how developers can circumvent those problems by conducting a semi-structured interview, including a coding task with 13 real-world Web developers. Our work also identifies key weaknesses in the design and documentation of Trusted Types, which we urge the standardization body to incorporate before the Trusted Types becomes a standard. -
Where Are the Red Lines? Towards Ethical Server-Side Scans in Security and Privacy Research
Hantke, F., Roth, S., Mrowczynski, R., Utz, C., & Stock, B. (2024). Where Are the Red Lines? Towards Ethical Server-Side Scans in Security and Privacy Research. In 2024 IEEE Symposium on Security and Privacy (S&P) (pp. 4405–4423).
DOI: 10.1109/SP54263.2024.00104 MetadataAbstract
Comprehensive and representative measurements are crucial to understand security and privacy risks on the Web. However, researchers have long been reluctant to investigate server-side vulnerabilities at scale, as this could harm servers, disrupt service, and cause financial damage. This can lead to operator backlash and problems in peer review, as the boundaries posed by the law, ethics, and operators' stance towards security research are largely unclear.In this paper, we address this research gap and investigate the boundaries of server-side scanning (3S) on the Web. To that end, we devise five typical scenarios for 3S on the Web to obtain concrete practical guidance. We analyze qualitative data from 23 interviews with legal experts, using German law as a case study, members of Research Ethics Committees, and website and server operators to learn what types of 3S are considered acceptable and which behavior would cross a red line. To verify our findings, we further conduct an online survey with 119 operators.Our analysis of these different perspectives shows that the absence of judicial decisions and clear ethical guidelines poses challenges in overcoming the risks associated with 3S, despite a slight majority (57%) of operators having a positive stance towards such academic research throughout the interviews and the survey. As a first step to mitigate these challenges, we suggest best practices for future 3S research and a pre-registration process to provide a reliable and transparent environment for 3S-based research that reduces uncertainty for researchers and operators alike. -
ADAPT it! Automating APT Campaign and Group Attribution by Leveraging and Linking Heterogeneous Files
Saha, A., Blasco, J., Cavallaro, L., & Lindorfer, M. (2024). ADAPT it! Automating APT Campaign and Group Attribution by Leveraging and Linking Heterogeneous Files. In RAID ’24: Proceedings of the 27th International Symposium on Research in Attacks, Intrusions and Defenses (pp. 114–129). Association for Computing Machinery.
DOI: 10.1145/3678890.3678909 MetadataAbstract
Recent years have witnessed a surge in the growth of Advanced Persistent Threats (APTs), with significant challenges to the security landscape, affecting industry, governance, and democracy. The ever- growing number of actors and the complexity of their campaigns have made it difficult for defenders to track and attribute these malicious activities effectively. Traditionally, researchers relied on threat intelligence to track APTs. However, this often led to fragmented information, delays in connecting campaigns with specific threat groups, and misattribution. In response to these challenges, we introduce ADAPT, a ma- chine learning-based approach for automatically attributing APTs at two levels: (1) the threat campaign level, to identify samples with similar objectives and (2) the threat group level, to identify samples operated by the same entity. ADAPT supports a variety of heterogeneous file types targeting different platforms, includ- ing executables and documents, and uses linking features to find connections between them. We evaluate ADAPT on a reference dataset from MITRE as well as a comprehensive, label-standardized dataset of 6,134 APT samples belonging to 92 threat groups. Using real-world case studies, we demonstrate that ADAPT effectively identifies clusters representing threat campaigns and associates them with their respective groups. -
Comparing Apples to Androids: Discovery, Retrieval, and Matching of iOS and Android Apps for Cross-Platform Analyses
Steinböck, M., Bleier, J., Rainer, M., Urban, T., Utz, C., & Lindorfer, M. (2024). Comparing Apples to Androids: Discovery, Retrieval, and Matching of iOS and Android Apps for Cross-Platform Analyses. In MSR ’24: Proceedings of the 21st International Conference on Mining Software Repositories (pp. 348–360).
DOI: 10.1145/3643991.3644896 MetadataAbstract
For years, researchers have been analyzing mobile Android apps to investigate diverse properties such as software engineering practices, business models, security, privacy, or usability, as well as differences between marketplaces. While similar studies on iOS have been limited, recent work has started to analyze and compare Android apps with those for iOS. To obtain the most representative analysis results across platforms, the ideal approach is to compare their characteristics and behavior for the same set of apps, e. g., to study a set of apps for iOS and their respective counterparts for Android. Previous work has only attempted to identify and evaluate such cross-platform apps to a limited degree, mostly comparing sets of apps independently drawn from app stores, manually matching small sets of apps, or relying on brittle matches based on app and developer names. This results in (1) comparing apps whose behavior and properties significantly differ, (2) limited scalability, and (3) the risk of matching only a small fraction of apps. In this work, we propose a novel approach to create an extensive dataset of cross-platform apps for the iOS and Android ecosystems. We describe an analysis pipeline for discovering, retrieving, and matching apps from the Apple App Store and Google Play Store that we used to create a set of 3,322 cross-platform apps out of 10,000 popular apps for iOS and Android, respectively. We evaluate existing and new approaches for cross-platform app matching against a set of reference pairs that we obtained from Google's data migration service. We identify a combination of seven features from app store metadata and the apps themselves to match iOS and Android apps with high confidence (95.82 %). Compared to previous attempts that identified 14 % of apps as cross-platform, we are able to match 34 % of apps in our dataset. To foster future research in the cross-platform analysis of mobile apps, we make our pipeline available to the community. -
Large-Scale Security Analysis of Real-World Backend Deployments Speaking IoT-Focused Protocols
Tagliaro, C., Komsic, M., Continella, A., Borgolte, K., & Lindorfer, M. (2024). Large-Scale Security Analysis of Real-World Backend Deployments Speaking IoT-Focused Protocols. In RAID ’24: Proceedings of the 27th International Symposium on Research in Attacks, Intrusions and Defenses (pp. 561–578).
DOI: 10.1145/3678890.3678899 MetadataAbstract
Internet-of-Things (IoT) devices, ranging from smart home assistants to health devices, are pervasive: Forecasts estimate their number to reach 29 billion by 2030. Understanding the security of their machine-to-machine communication is crucial. Prior work focused on identifying devices’ vulnerabilities or proposed protocol-specific solutions. Instead, we investigate the security of backends speaking IoT protocols, that is, the backbone of the IoT ecosystem. We focus on three real-world protocols for our large-scale analysis: MQTT, CoAP, and XMPP. We gather a dataset of over 337,000 backends, augment it with geographical and provider data, and perform non-invasive active measurements to investigate three major security threats: information leakage, weak authentication, and denial of service. Our results provide quantitative evidence of a problematic immaturity in the IoT ecosystem. Among other issues, we find that 9.44% backends expose information, 30.38% CoAP-speaking backends are vulnerable to denial of service attacks, and 99.84% of MQTT- and XMPP-speaking backends use insecure transport protocols (only 0.16% adopt TLS, of which 70.93% adopt a vulnerable version). -
Masked Iterate-Fork-Iterate: A New Design Paradigm for Tweakable Expanding Pseudorandom Function
Andreeva, E., Cogliati, B., Lallemand, V., Minier, M., Purnal, A., & Roy, A. (2024). Masked Iterate-Fork-Iterate: A New Design Paradigm for Tweakable Expanding Pseudorandom Function. In C. Pöpper & L. Batina (Eds.), Applied Cryptography and Network Security (pp. 433–459). Springer, Cham.
DOI: 10.1007/978-3-031-54773-7_17 MetadataAbstract
Many modes of operations for block ciphers or tweakable block ciphers do not require invertibility from their underlying primitive. In this work, we study fixed-length Tweakable Pseudorandom Function (TPRF) with large domain expansion, a novel primitive that can bring high security and significant performance optimizations in symmetric schemes, such as (authenticated) encryption. Our first contribution is to introduce a new design paradigm, derived from the Iterate-Fork-Iterate construction, in order to build n-to-αn-bit (α≥2), n-bit secure, domain expanding TPRF. We dub this new generic composition masked Iterate-Fork-Iterate mIFI. We then propose a concrete TPRF instantiation ButterKnife that expands an n-bit input to 8n-bit output via a public tweak and secret key. ButterKnife is built with high efficiency and security in mind. It is fully parallelizable and based on Deoxys-BC, the AES-based tweakable block cipher used in the authenticated encryption winner algorithm in the defense-in-depth category of the CAESAR competition. We analyze the resistance of ButterKnife to differential, linear, meet-in-the-middle, impossible differentials and rectangle attacks. A special care is taken to the attack scenarios made possible by the multiple branches. Our next contribution is to design and provably analyze two new TPRF-based deterministic authenticated encryption (DAE) schemes called SAFE and ZAFE that are highly efficient, parallelizable, and offer (n+min(n,t))/2 bits of security, where n, t denote respectively the input block and the tweak sizes of the underlying primitives. We further implement SAFE with ButterKnife to show that it achieves an encryption performance of 1.18 c/B for long messages on Skylake, which is 24% faster than the comparable Crypto’17 TBC-based ZAE DAE. Our second candidate ZAFE, which uses the same authentication pass as ZAE, offers a similar level of speedup. Besides, we show that ButterKnife, when used in Counter Mode, is slightly faster than AES (0.55 c/B vs 0.63 c/B on Skylake). -
Skye: An Expanding PRF based Fast KDF and its Applications
Bhati, A. S., Dufka, A., Andreeva, E., Roy, A., & Preneel, B. (2024). Skye: An Expanding PRF based Fast KDF and its Applications. In ASIA CCS ’24: Proceedings of the 19th ACM Asia Conference on Computer and Communications Security (pp. 1082–1098).
DOI: 10.1145/3634737.3637673 MetadataAbstract
A Key Derivation Function (KDF) generates a uniform and highly random key-stream from weakly random key material. KDFs are broadly used in various security protocols such as digital signatures and key exchange protocols. HKDF, the most deployed KDF in practice, is based on the extract-then-expand paradigm. It is presently used, among others, in the Signal Protocol for end-to-end encrypted messaging. HKDF is a generic KDF for general input sources and thus is not optimized for source-specific use cases such as key derivation from Diffie-Hellman (DH) sources (i.e. DH shared secrets as key material). Furthermore, the sequential HKDF design is unnecessarily slow on some general-purpose platforms that can benefit from parallelization. In this work, we propose a novel, efficient and secure KDF called Skye. Skye follows the extract-then-expand paradigm and consists of two algorithms: efficient deterministic randomness extractor and expander functions. Instantiating our extractor for dedicated source-specific (e.g. DH sources) inputs leads to a significant efficiency gain over HKDF while maintaining its security level. We provide concrete security analysis of Skye and both its underlying algorithms in the standard model. We provide a software performance comparison of Skye with the AES-based expanding PRF ButterKnife and HKDF with SHA-256 (as used in practice). Our results show that in isolation Skye performs from 4x to 47x faster than HKDF, depending on the availability of AES or SHA instruction support. We further demonstrate that with such a performance gain, when Skye is integrated within the current Signal implementation, we can achieve significant overall improvements ranging from 38% to 64% relative speedup in unidirectional messaging. Even in bidirectional messaging, that includes DH computation with dominating computational cost, Skye still contributes to 12-36% relative speedup when just 10 messages are sent and received at once. -
Inductive Predicate Synthesis Modulo Programs
Wesley, S., Christakis, M., Navas, J. A., Trefler, R., Wüstholz, V., & Gurfinkel, A. (2024). Inductive Predicate Synthesis Modulo Programs. In 38th European Conference on Object-Oriented Programming (ECOOP 2024) (pp. 1–30).
DOI: 10.4230/LIPIcs.ECOOP.2024.43 Metadata -
Wappler: Sound Reachability Analysis for WebAssembly
Scherer, M., Blaabjerg, J. F., Sjösten, A., Solitro, M. M., & Maffei, M. (2024). Wappler: Sound Reachability Analysis for WebAssembly. In L. O’Conner & P. Kellenberger (Eds.), 2024 IEEE 37th Computer Security Foundations Symposium (CSF) (pp. 249–264).
DOI: 10.1109/CSF61375.2024.00025 MetadataAbstract
WebAssembly (Wasm) is an increasingly deployed low-level language providing near-native performance to security-critical domains such as web browsers, smart contracts, and edge computing. In all of these domains, establishing the absence of bugs and security vulnerabilities is of utmost importance, which motivates the development of sound and automated static analysis techniques. This is, however, a challenging task since the Wasm formal semantics is not directly amenable to efficient static analysis, Wasm code is typically embedded in statically unknown and possibly malicious contexts, and the low-level nature of the language makes it hard to precisely and yet soundly capture memory management and other core features. In this work, we present Wappler, the first sound and automated static analysis technique for WebAssembly. The core idea is to encode the semantics into Horn clauses so as to make it accessible to automated theorem provers, such as z3. The realization of this approach, however, requires to tackle several challenges. We address the fact that the Wasm semantics is not directly amenable to automation of security proofs by introducing annotations that enable a precise, practical, and yet sound encoding. Furthermore, we devise a formalism to specify embedder behavior and introduce a sound yet precise memory abstraction. We demonstrate the expressiveness of our logical formalism by encoding several general as well as Wasm-specific security properties. Finally, we implement our static analysis technique and conduct an experimental evaluation over the official Wasm test suite to demonstrate its performance. -
The COLM Authenticated Encryption Scheme
Andreeva, E., Bogdanov, A., Datta, N., Luykx, A., Mennink, B., Nandi, M., Tischhauser, E., & Yasuda, K. (2024). The COLM Authenticated Encryption Scheme. Journal of Cryptology, 37, Article 15.
DOI: 10.1007/s00145-024-09492-8 MetadataAbstract
In this work we present the COLM authenticated encryption (AE) scheme which is the second of the two winners in the defense in depth category of the CAESAR competition. COLM realizes a nonce-based authenticated encryption with associated data and uses the popular AES blockcipher as its underlying primitive. We propose two possible blockcipher instantiations (with key of length 128 or 256 bits). We also define two COLM modes of operation variants: a primary COLM₀ mode for general purpose applications, and a COLMτ variant with intermediate tag generation/verification geared to support low-end devices and applications where frequent verification is required. COLM is designed with security, simplicity, and efficiency in mind. The main design goal of COLM is high security: a primary feature of the defense in depth CAESAR category. COLM provides security beyond the traditional AE security. First, COLM is secure against nonce misuse, namely, it enables security in adversarial settings where the nonce inputs to the AE scheme repeat. In contrast to standardized and popular AE algorithms, such as GCM and OCB1-3 modes, whose AE security trivially breaks down when the nonce is repeated, COLM ensures both confidentiality and authenticity (AE) security with repeated nonces. Second, our COLMτ variant enables increased security levels in situations where release of unverified ciphertext (RUP) occurs due to its ability to limit a potential leakage by frequent verifications. In this work we prove COLM secure with respect to both confidentiality and authenticity (AE) security under nonce misuse in the well-known provable security framework. Our proofs show that COLM maintains n/2-bit security levels for block sizes of n bits. Furthermore, due to the inherent parallelism on both mode and primitive levels, our software performance results show that the price paid for enhanced security does come at the cost of minimal efficiency losses. More concretely, we implement GCM, COLM, and Deoxys-II on the Kaby Lake and Coffee lake Intel platforms. Compared to the other winner in the defense in depth category Deoxys-II, our AE design COLM₀ performs 10–20% faster for the 128-bit key version. Regarding the 256-bit key versions COLM₀ is around 5% faster for short and 2% slower than Deoxys-II for the longer messages. -
CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model
Jeanteur, S., Kovács, L., Maffei, M., & Rawson, M. (2024). CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In 2024 IEEE Symposium on Security and Privacy (SP) (pp. 3165–3183). IEEE.
DOI: 10.1109/SP54263.2024.00246 MetadataAbstract
Cryptographic protocols are hard to design and prove correct, as witnessed by the ever-growing list of attacks even on protocol standards. Symbolic models of cryptography enable automated formal security proofs of such protocols against an idealized cryptographic model, which abstracts away from the algebraic properties of cryptographic schemes and thus misses attacks. Computational models of cryptography yield rigorous guarantees but support at present only interactive proofs and/or restricted classes of protocols (e.g., stateless ones). A promising approach is given by the computationally complete symbolic attacker (CCSA) model, formalized in the BC Logic, which aims at bridging and getting the best of the two worlds, obtaining cryptographic guarantees by symbolic protocol analysis. The BC Logic is supported by a recently developed interactive theorem prover, namely Squirrel, which enables machine-checked interactive security proofs, as opposed to automated ones, thus requiring expert knowledge both in the cryptographic space as well as on the reasoning side.In this paper, we introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. The key technical contribution is a first-order formalization of protocol properties with tailored handling of subterm relations. As such, we overcome the burden of interactive proving in higher-order logic and automatically establish soundness of cryptographic protocols using only first-order reasoning. Our first-order encoding of cryptographic protocols is challenging for various reasons. On the theoretical side, we restrict full first-order logic with cryptographic axioms to ensure that, by losing the expressivity of the higher-order BC Logic, we do not lose soundness of cryptographic protocols in our first-order encoding. On the practical side, CryptoVampire integrates dedicated proof techniques using first-order saturation algorithms and heuristics, which all together enable leveraging the state-of-the-art Vampire first-order automated theorem prover as the underlying proving engine of CryptoVampire. Our experimental results showcase the effectiveness of CryptoVampire as a standalone verifier as well as in terms of automation support for Squirrel. -
Message from General Chairs; EuroSP 2024
Weippl, E., & Maffei, M. (2024). Message from General Chairs; EuroSP 2024. In 2024 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW). 9th IEEE European Symposium on Security and Privacy Workshops (EUROS&PW 2024), Wien, Austria.
DOI: 10.1109/EuroSPW61312.2024.00005 MetadataAbstract
A warm welcome to Vienna! We're excited to host the IEEE EuroS&P 2024 at the University of Vienna's Faculty of Informatics from July 8th to 12th. It brings together researchers and enthusiasts in security&privacy from all over the world for in-person discussions and collaborations. Huge thanks to the organizers and everyone involved in making this event possible! -
Bribe & Fork: Cheap PCN Bribing Attacks via Forking Threat
Avarikioti, Z., Kędzior, P., Lizurej, T., & Michalak, T. (2024). Bribe & Fork: Cheap PCN Bribing Attacks via Forking Threat. In R. Böhme & L. Kiffer (Eds.), 6th Conference on Advances in Financial Technologies (AFT 2024) (pp. 1–22).
DOI: 10.4230/LIPIcs.AFT.2024.11 MetadataAbstract
In this work, we reexamine the vulnerability of Payment Channel Networks (PCNs) to bribing attacks, where an adversary incentivizes blockchain miners to deliberately ignore a specific transaction to undermine the punishment mechanism of PCNs. While previous studies have posited a prohibitive cost for such attacks, we show that this cost can be dramatically reduced (to approximately $125), thereby increasing the likelihood of these attacks. To this end, we introduce Bribe & Fork, a modified bribing attack that leverages the threat of a so-called feather fork which we analyze with a novel formal model for the mining game with forking. We empirically analyze historical data of some real-world blockchain implementations to evaluate the scale of this cost reduction. Our findings shed more light on the potential vulnerability of PCNs and highlight the need for robust solutions. -
Brief Announcement: Musketeer - Incentive-Compatible Rebalancing for Payment Channel Networks
Avarikioti, Z., Schmid, S., & Tiwari, S. (2024). Brief Announcement: Musketeer - Incentive-Compatible Rebalancing for Payment Channel Networks. In PODC ’24: Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing (pp. 306–309).
DOI: 10.1145/3662158.3662809 MetadataAbstract
We revisit the severely limited throughput problem of cryptocurrencies and propose a novel rebalancing approach for Payment Channel Networks (PCNs). PCNs are a popular solution for increasing the blockchain throughput, however, their benefit depends on the overall users' liquidity. Rebalancing mechanisms are the state-of-the-art approach to maintaining high liquidity PCNs. However, existing opt-in rebalancing mechanisms exclude users that may assist in rebalancing for small service fees, leading to suboptimal solutions and under-utilization of the PCNs' bounded liquidity.We introduce the first rebalancing approach for PCNs that includes all users, following a "all for one and one for all" design philosophy that yields optimal throughput. The proposed approach introduces a double-auction rebalancing problem, which we term Musketeer, where users can participate as buyers (paying fees to rebalance) or sellers (charging fees to route transactions). The desired properties are tailored to the unique characteristics of PCNs, including the novel game-theoretic property of cyclic budget balance that is a stronger variation of strong budget balance.Basic results derived from auction theory, including an impossibility and multiple mechanisms that either achieve all desiderata under a relaxed model or sacrifice one of the properties, are presented. We also propose a novel mechanism that leverages time delays as an additional cost to users. This mechanism is provably truthful, cyclic budget balanced, individually rational and economic efficient but only with respect to liquidity. -
OAE-RUP: A Strong Online AEAD Security Notion and Its Application to SAEF
Bhati, A. S., Andreeva, E., & Vizár, D. (2024). OAE-RUP: A Strong Online AEAD Security Notion and Its Application to SAEF. In Security and Cryptography for Networks (pp. 117–139). Springer.
DOI: 10.1007/978-3-031-71073-5_6 MetadataAbstract
Release of unverified plaintexts (RUP) security is an important target for robustness in AE schemes. It is also highly crucial for lightweight (LW) implementations of online AE schemes on memory-constrained devices. Surprisingly, very few online AEAD schemes come with provable guarantees against RUP integrity and not one with any well-defined RUP confidentiality. In this work, we first propose a new strong security notion for online AE schemes called OAE-RUP that captures security under blockwise processing of both encryption (which includes nonce-misuse) and decryption (which includes RUP). Formally, OAE-RUP combines the standard RUP integrity notion INT-RUP with a new RUP confidentiality notion sOPRPF (strong Online PseudoRandom Permutation followed by a pseudorandom Function). sOPRPF is based on the concept of “strong online permutations” and can be seen as an extension of the well-known CCA3 notion (Abed et al., FSE 2014) that captures arbitrary-length inputs. An OAE-RUP-secure scheme is resistant against nonce-misuse as well as leakage of unverified plaintexts where the integrity remains unaffected, and the confidentiality of any encrypted plaintext is preserved up to the leakage of the longest prefix with the leaked plaintexts and the leakage of the length of the longest prefix with the nonce-repeating ciphertexts. We then prove the OAE-RUP security of the SAEF mode. SAEF is a ForkAE mode (Asiacrypt 2019) that is optimized for authenticated encryption of short messages and processes the message blocks sequentially and in an online manner. At SAC 2020, it was shown that SAEF is also an online nonce misuse-resistant AE (OAE), offering enhanced security against adversaries that make blockwise adaptive encryption queries. It has remained an open question if SAEF also resists attacks against blockwise adaptive decryption adversaries or, more generally, when the decrypted plaintext is released before verification (RUP). Our proofs are conducted using the coefficients H technique, and they show that, without any modifications, SAEF is OAE-RUP secure up to the birthday bound, i.e., up to 2n/2 processed data blocks, where n is the block size of the forkcipher. -
Web Platform Threats: Automated Detection of Web Security Issues With WPT
Bernardo, P., Veronese, L., DALLA VALLE, V., Calzavara, S., Squarcina, M., Adão, P., & Maffei, M. (2024). Web Platform Threats: Automated Detection of Web Security Issues With WPT. In Proceedings of the 33rd USENIX Security Symposium (pp. 757–774).
MetadataAbstract
Client-side security mechanisms implemented by Web browsers, such as cookie security attributes and the Mixed Content policy, are of paramount importance to protect Web applications. Unfortunately, the design and implementation of such mechanisms are complicated and error-prone, potentially exposing Web applications to security vulnerabilities. In this paper, we present a practical framework to formally and automatically detect security flaws in client-side security mechanisms. In particular, we leverage Web Platform Tests (WPT), a popular cross-browser test suite, to automatically collect browser execution traces and match them against Web invariants, i.e., intended security properties of Web mechanisms expressed in first-order logic. We demonstrate the effectiveness of our approach by validating 9 invariants against the WPT test suite, discovering violations with clear security implications in 104 tests for Firefox, Chromium and Safari. We disclosed the root causes of these violations to browser vendors and standard bodies, which resulted in 8 individual reports and one CVE on Safari. -
Musketeer: Incentive-Compatible Rebalancing for Payment Channel Networks
Avarikioti, Z., Schmid, S., & Tiwari, S. (2024). Musketeer: Incentive-Compatible Rebalancing for Payment Channel Networks. In R. Böhme & L. Kiffer (Eds.), 6th Conference on Advances in Financial Technologies (AFT 2024) (pp. 1–22).
DOI: 10.4230/LIPIcs.AFT.2024.13 MetadataAbstract
In this work, we revisit the severely limited throughput problem of cryptocurrencies and propose a novel rebalancing approach for Payment Channel Networks (PCNs). PCNs are a popular solution for increasing the blockchain throughput, however, their benefit depends on the overall users’ liquidity. Rebalancing mechanisms are the state-of-the-art approach to maintaining high liquidity in PCNs. However, existing opt-in rebalancing mechanisms exclude users that may assist in rebalancing for small service fees, leading to suboptimal solutions and under-utilization of the PCNs’ bounded liquidity. We introduce the first rebalancing approach for PCNs that includes all users, following a “all for one and one for all” design philosophy that yields optimal throughput. The proposed approach introduces a double-auction rebalancing problem, which we term Musketeer, where users can participate as buyers (paying fees to rebalance) or sellers (charging fees to route transactions). The desired properties tailored to the unique characteristics of PCNs are formally defined, including the novel game-theoretic property of cyclic budget balance that is a stronger variation of strong budget balance. Basic results derived from auction theory, including an impossibility and multiple mechanisms that either achieve all desiderata under a relaxed model or sacrifice one of the properties, are presented. We also propose a novel mechanism that leverages time delays as an additional cost to users. This mechanism is provably truthful, cyclic budget balanced, individually rational and economic efficient but only with respect to liquidity. -
Pitfalls in Machine Learning for Computer Security
Arp, D., Quiring, E., Pendlebury, F., Warnecke, A., Pierazzi, F., Wressnegger, C., Cavallaro, L., & Rieck, K. (2024). Pitfalls in Machine Learning for Computer Security. Communications of the ACM, 67(11), 104–112.
DOI: 10.1145/3643456 MetadataAbstract
With the growing processing power of computing systems and the increasing availability of massive datasets, machine learning algorithms have led to major breakthroughs in many different areas. This development has influenced computer security, spawning a series of work on learning-based security systems, such as for malware detection, vulnerability discovery, and binary code analysis. Despite great potential, machine learning in security is prone to subtle pitfalls that undermine its performance and render learning-based systems potentially unsuitable for security tasks and practical deployment. In this paper, we look at this problem with critical eyes. First, we identify common pitfalls in the design, implementation, and evaluation of learning-based security systems. We conduct a study of 30 papers from top-tier security conferences within the past 10 years, confirming that these pitfalls are widespread in the current security literature. In an empirical analysis, we further demonstrate how individual pitfalls can lead to unrealistic performance and interpretations, obstructing the understanding of the security problem at hand. As a remedy, we propose actionable recommendations to support researchers in avoiding or mitigating the pitfalls where possible. Furthermore, we identify open problems when applying machine learning in security and provide directions for further research. -
Olympia: Fuzzer Benchmarking for Solidity
Chadt, J., Hochrainer, C., Wüstholz, V., & Christakis, M. (2024). Olympia: Fuzzer Benchmarking for Solidity. In ASE ’24: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering (pp. 2362–2365). Association for Computing Machinery.
DOI: 10.1145/3691620.3695352 MetadataAbstract
Over the last few years, smart-contract hacks have resulted in the loss of billions of assets. To efficiently identify such vulnerabilities, academic and industrial researchers have developed several popular smart-contract fuzzers. However, it has been challenging to objectively compare their bug-finding effectiveness. In this paper, we present Olympia, the first benchmark-generation tool that is designed for smart-contract, rather than general-purpose, fuzzers. We have used Olympia to evaluate the effectiveness of four well known, open-source fuzzers for Solidity smart contracts. -
Computer-aided formal security analysis of the Web platform
Veronese, L. (2024). Computer-aided formal security analysis of the Web platform [Dissertation, Technische Universität Wien]. reposiTUm.
DOI: 10.34726/hss.2024.127183 MetadataAbstract
Over the last two decades, a set of standards published by the W3C, IETF and WHATWG was consolidated to form the Web Platform, a full-fledged application platform as opposed to the initial design of the Web as a set of hyperlinked documents. The current state of the standardization of the Web, fragmented into a multitude of documents maintained by different organizations, complicates the process of reasoning about the security of the platform as a whole. This led to the introduction of vulnerabilities originating from unforeseen interactions between different Web components. This situation stems from the fact that Web specification often include informally-defined or implicit assumptions about the security of other features. In this thesis we argue for the need of a rigorous and formal definition of Web security in terms of invariants that are guaranteed to be valid across the Web platform. In particular, in this work, we study the security mechanisms of the modern Web and formalize them in the form of Web invariants. We propose two methodologies for validating Web invariants on a new model of Web specifications (WebSpec) and on browser implementations (Chromium, Firefox, Safari) that allowed us to discover new inconsistencies and propose sound mitigations. We then focus on application security and study the lesser-known Web threat model of the related domain attacker, measuring its impact on the security of the most popular sites on the Web. Finally, we turn our attention to cookies and their long history of vulnerabilities, discussing new violations of their integrity protections and new attacks enabled by related-domain attackers. -
Fuzzing Processing Pipelines for Zero-Knowledge Circuits
Hochrainer, C., Isychev, A., Wüstholz, V., & Christakis, M. (2024). Fuzzing Processing Pipelines for Zero-Knowledge Circuits. arXiv.
DOI: 10.48550/arXiv.2411.02077 MetadataAbstract
Zero-knowledge (ZK) protocols have recently found numerous practical applications, such as in authentication, online-voting, and blockchain systems. These protocols are powered by highly complex pipelines that process deterministic programs, called circuits, written in one of many domain-specific programming languages, e.g., Circom, Noir, and others. Logic bugs in circuit-processing pipelines could have catastrophic consequences and cause significant financial and reputational damage. As an example, consider that a logic bug in a ZK pipeline could result in attackers stealing identities or assets. It is, therefore, critical to develop effective techniques for checking their correctness. In this paper, we present the first systematic fuzzing technique for ZK pipelines, which uses metamorphic test oracles to detect critical logic bugs. We have implemented our technique in an open-source tool called Circuzz. We used Circuzz to test four significantly different ZK pipelines and found a total of 16 logic bugs in all pipelines. Due to their critical nature, 15 of our bugs have already been fixed by the pipeline developers. -
On Security Proofs of Existing Equivalence Class Signature Schemes
Bauer, B., Fuchsbauer, G., & Regen, F. (2024). On Security Proofs of Existing Equivalence Class Signature Schemes. In K.-M. Chung & Y. Sakaki (Eds.), Advances in Cryptology – ASIACRYPT 2024 : 30th International Conference on the Theory and Application of Cryptology and Information Security, Kolkata, India, December 9–13, 2024, Proceedings, Part II (pp. 3–37). Springer.
DOI: 10.1007/978-981-96-0888-1_1 MetadataAbstract
Equivalence class signatures (EQS; Asiacrypt ’14), sign vectors of elements from a bilinear group. Anyone can transform a signature on a vector to a signature on any multiple of that vector; signatures thus authenticate equivalence classes. A transformed signature/message pair is indistinguishable from a random signature on a random message. EQS have been used to efficiently instantiate (delegatable) anonymous credentials, (round-optimal) blind signatures, ring and group signatures, anonymous tokens and contact-tracing schemes, to name a few. The original EQS construction (J. Crypto ’19) is proven secure in the generic group model, and the first scheme from standard assumptions (PKC ’18) satisfies a weaker model insufficient for most applications. Two works (Asiacrypt ’19, PKC ’22) propose applicable schemes that assume trusted parameters. Their unforgeability is argued via a security proof from standard (or non-interactive) assumptions. We show that their security proofs are flawed and explain the subtle issue. While the schemes might be provable in the algebraic group model (AGM), we instead show that the original construction, which is more efficient and has found applications in many works, is secure in the AGM under a parametrized non-interactive hardness assumption. -
MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper)
Hader, T., Kaufmann, D., Irfan, A., Graham-Lengrand, S., & Kovács, L. (2024). MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). In Automated Reasoning: 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3–6, 2024, Proceedings, Part I (pp. 386–395). Springer International Publishing.
DOI: 10.1007/978-3-031-63498-7_23 MetadataAbstract
This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2 ’s frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory. -
Rewriting and Inductive Reasoning
Hajdu, M., Kovács, L., & Rawson, M. (2024). Rewriting and Inductive Reasoning. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 278–294).
DOI: 10.29007/vbfp MetadataAbstract
Rewriting techniques based on reduction orderings generate “just enough” consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem proving, but for at least one approach to inductive reasoning we show that we are missing crucial consequences. We therefore extend the superposition calculus with rewriting-based techniques to generate sufficient consequences for automating induction in saturation. When applying our work within the unit-equational fragment, our experiments with the theorem prover Vampire show significant improvements for inductive reasoning. -
Saturating Sorting without Sorts
Georgiou, P., Hajdu, M., & Kovacs, L. (2024). Saturating Sorting without Sorts. In N. Bjørner, M. Heule, & A. Voronkov (Eds.), Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning (pp. 88–105).
DOI: 10.29007/rg9z MetadataAbstract
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 induction 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. -
Securing Lightning Channels against Rational Miners
Aumayr, L., Avarikioti, Z., Maffei, M., & Mazumdar, S. (2024). Securing Lightning Channels against Rational Miners. In B. Luo, X. Liao, & J. Xu (Eds.), Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security (pp. 393–407).
DOI: 10.1145/3658644.3670373 MetadataAbstract
Payment channel networks (e.g., the Lightning Network in Bit- coin) constitute one of the most popular scalability solutions for blockchains. Their safety relies on parties being online to detect fraud attempts on-chain and being able to timely react by pub- lishing certain transactions on-chain. However, a cheating party may bribe miners in order to censor those transactions, resulting in loss of funds for the cheated party: these attacks are known in the literature as timelock bribing attacks. In this work, we present the first channel construction that does not require parties to be online and, at the same time, is resistant to timelock bribing attacks. We start by proving for the first time that Lightning channels are secure against timelock bribing attacks in the presence of rational channel parties under the assumption that these parties constantly monitor the mempool and never deplete the channel in one di- rection. The latter underscores the importance of keeping a coin reserve in each channel as implemented in the Lightning Network, albeit for different reasons. We show, however, that the security of the Lightning Network against Byzantine channel parties does not carry over to a setting in which miners are rational and accept timelock bribes. Next, we introduce CRAB, the first Lightning-compatible chan- nel construction that provides security against Byzantine channel parties and rational miners. CRAB leverages miners’ incentives to safeguard the channel, thereby also forgoing the unrealistic assump- tion of channel parties constantly monitoring the mempool. Finally, we show how our construction can be refined to elimi- nate the major assumption behind payment channels, i.e., the need for online participation. To that end, we present Sleepy CRAB the first provably secure channel construction under rational miners that enables participants to go offline indefinitely. We also provide a proof-of-concept implementation of Sleepy CRAB and evaluate its cost in Bitcoin, thereby demonstrating its practicality. This -
SAT solving for variants of first-order subsumption
Coutelier, R., Rath, J., Rawson, M., Biere, A., & Kovacs, L. (2024). SAT solving for variants of first-order subsumption. Formal Methods in System Design.
DOI: 10.1007/s10703-024-00454-1 MetadataAbstract
Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system verification, program synthesis, and cybersecurity. Automation in these domains crucially depends on the efficiency of the underlying reasoners towards finding proofs and/or counterexamples of the task to be enforced. In order to gain efficiency, automated reasoners use dedicated proof rules to keep proof search tractable. To this end, (variants of) subsumption is one of the most important proof rules used by automated reasoners, ranging from SAT solvers to first-order theorem provers and beyond. It is common that millions of subsumption checks are performed during proof search, necessitating efficient implementations. However, in contrast to propositional subsumption as used by SAT solvers and implemented using sophisticated polynomial algorithms, first-order subsumption in first-order theorem provers involves NP-complete search queries, turning the efficient use of first-order subsumption into a huge practical burden. In this paper we argue that the integration of a dedicated SAT solver opens up new venues for efficient implementations of first-order subsumption and related rules. We show that, by using a flexible learning approach to choose between various SAT encodings of subsumption variants, we greatly improve the scalability of first-order theorem proving. Our experimental results demonstrate that, by using a tailored SAT solver within first-order reasoning, we gain a large speedup in solving state-of-the-art benchmarks. -
Route Discovery in Private Payment Channel Networks
Avarikioti, G., Bastankhah, M., Maddah-Ali, M. A., Pietrzak, K., Svoboda, J., & Yeo, M. (2024). Route Discovery in Private Payment Channel Networks. In DPM & CBT 2024 Pre-proceedings (pp. 195–211).
MetadataAbstract
In this work, we explore route discovery in private payment channel networks. We first determine what “ideal” privacy for a routing protocol means in this setting. We observe that protocols achieving this strong privacy definition exist by leveraging Multi-Party Computation but they are inherently inefficient as they must involve the entire network. We then present protocols with weaker privacy guarantees but much better efficiency (involving only a small fraction of the nodes). The core idea is that both sender and receiver gossip a message which propagates through the network, and the moment any node in the network receives both messages, a path is found. In our first protocol the message is always sent to all neighbouring nodes with a delay proportional to the fees of that edge. In our second protocol the message is only sent to one neighbour chosen randomly with a probability proportional to its degree.We additionally propose a more realistic notion of privacy in order to measure the privacy leakage of our protocols in practice. Our realistic notion of privacy challenges an adversary that join the network with a fixed budget to create channels to guess the sender and receiver of a transaction upon receiving messages from our protocols. Simulations of our protocols on the Lightning network topology (for random transactions and uniform fees) show that 1) forming edges with high degree nodes is a more effective attack strategy for the adversary, 2) there is a tradeoff between the number of nodes involved in our protocols (privacy) and the optimality of the discovered path, and 3) our protocols involve a very small fraction of the network on average. -
Lazy Reimplication in Chronological Backtracking
Coutelier, R., Fleury, M., & Kovacs, L. (2024). Lazy Reimplication in Chronological Backtracking. In S. Chakraborty & J.-H. R. Jiang (Eds.), 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) (pp. 9:1-9:19). Schloss Dagstuhl.
DOI: 10.4230/LIPIcs.SAT.2024.9 MetadataAbstract
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose. -
PolySAT: Word-level Bit-vector Reasoning in Z3
Rath, J., Eisenhofer, C., Kaufmann, D., Bjørner, N., & Kovacs, L. (2024, October 14). PolySAT: Word-level Bit-vector Reasoning in Z3 [Conference Presentation]. VSTTE 2024, Prague, Czechia.
MetadataAbstract
PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. Addressing challenges of verified software, PolySAT integrates the theoretical development of SMT-based calculi with a proof of concept implementation and empirical evaluation. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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
Landman, M., Rain, S., Kovács, L., & 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 MetadataAbstract
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).
MetadataAbstract
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 MetadataAbstract
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.
MetadataAbstract
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 MetadataAbstract
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).
MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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., & Mazumdar, S. (2023). Chrisimos: A useful Proof-of-Work for finding Minimal Dominating Set of a graph. arXiv.
DOI: 10.34726/5301 MetadataAbstract
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
Squarcina, M., 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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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. -
The Threat of Surveillance and the Need for Privacy Protections
Lindorfer, M. (2023). The Threat of Surveillance and the Need for Privacy Protections. In H. Werthner, C. Ghezzi, J. Kramer, J. Nida-Rümelin, B. Nuseibeh, E. Prem, & A. Stanger (Eds.), Introduction to Digital Humanism : A Textbook (pp. 593–609). Springer.
DOI: 10.1007/978-3-031-45304-5_37 MetadataAbstract
In recent years, and since the introduction of the General Data Protection Regulation (GDPR) in particular, we have seen an increased interest (and concern) about the amount of private information that is collected by the applications and services we use in our daily lives. The widespread collection and commodification of personal data has been mainly driven by companies collecting, mining, and selling user profiles for targeted advertisement, a practice also referred to as “surveillance capitalism.” However, as we detail in this chapter, this is not the only form of surveillance and can be necessary and even beneficial by increasing the safety of citizens—if it is aligned with the principles of digital humanisms in providing transparency, oversight, and accountability. We also detail mechanisms users can deploy to protect their own privacy, as well as mechanisms that help to develop more privacy-friendly technologies. -
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 MetadataAbstract
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 MetadataAbstract
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., Kovács, 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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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. -
Investigating HbbTV Privacy Invasiveness Across European Countries
Tagliaro, C., Hahn, F., Sepe, R., Aceti, A., & Lindorfer, M. (2023). Investigating HbbTV Privacy Invasiveness Across European Countries. In Learning from Authoritative Security Experiment Results (LASER) 2023. Workshop on Learning from Authoritative Security Experiment Results (LASER 2023), San Diego, United States of America (the).
DOI: 10.14722/laser-ndss.2023.24102 MetadataAbstract
Smart TVs enable the integration of the traditional broadcast signal with services offered by the Internet. Specifically, the Hybrid Broadcast Broadband TV (HbbTV) protocol allows broadcasters to offer consumers additional features via the Internet (e.g., quizzes and the ability to restart programs), enriching their viewing experience. For broadcasters its bi-directional nature also enables them to measure viewing preferences and provide targeted advertisements (marketed as “Addressable TV”). HbbTV works using standard web technologies as transparent overlays over a TV channel, thus, porting web security and privacy concerns to the Smart TV. However, despite the increasing adoption of HbbTV worldwide, studies on security and privacy issues in its deployments are scarce. In this paper, we discuss how we tested a range of 36 channels across five European countries and which challenges we faced; Specifically, every country adopts different ways of delivering the broadcast signal to the TVs. Thus, we provide a common experiment setup and detailed instructions on how we assess the TV channels’ privacy level in each country. We also show how the URLs pointing to the HbbTV applications we extracted can foster further replicability and studies. Finally, to complement our technical experiments we also measured Italian users’ awareness (N=174) of the security and privacy risks HbbTV introduces and we discuss our methodology to do so.
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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.
MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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).
MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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 MetadataAbstract
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. -
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 MetadataAbstract
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. -
A2L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs
Tairi, E., Moreno-Sanchez, P., & Maffei, M. (2021). A2L: 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 MetadataAbstract
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 MetadataAbstract
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 Advances in Cryptology – ASIACRYPT 2021 27th International Conference on the Theory and Application of Cryptology and Information Security, Singapore, December 6–10, 2021, Proceedings, Part IV (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 Advances in Cryptology – EUROCRYPT 2021 40th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Zagreb, Croatia, October 17–21, 2021, Proceedings, Part II (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 Financial Cryptography and Data Security 25th International Conference, FC 2021, Virtual Event, March 1–5, 2021, Revised Selected Papers, Part I. Springer Verlag, Austria. Springer LNCS.
DOI: 10.1007/978-3-662-64322-8_9 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 Advances in Cryptology – ASIACRYPT 2021 27th International Conference on the Theory and Application of Cryptology and Information Security, Singapore, December 6–10, 2021, Proceedings, Part II (pp. 635–664). Springer.
DOI: 10.1007/978-3-030-92075-3_22 MetadataAbstract
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 MetadataAbstract
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. Cryptology ePrint Archive.
MetadataAbstract
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 33rd Computer Security Foundations Symposium (CSF), Santa Barbara, United States of America (the). 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, United States of America (the). 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 T. Margaria & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Applications. ISoLA 2020, Proceedings, Part III (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, Italy. 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 Security and Cryptography for Networks (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 Security and Cryptography for Networks (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 Intelligent Computer Mathematics 13th International Conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020, Proceedings (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 MetadataAbstract
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, Italy.
MetadataAbstract
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 MetadataAbstract
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 -
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 Advances in Cryptology – ASIACRYPT 2019 25th International Conference on the Theory and Application of Cryptology and Information Security, Kobe, Japan, December 8–12, 2019, Proceedings, Part II (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), San Diego, United States of America (the).
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, United States of America (the).
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.
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 Principles of Security and Trust 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (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), United States of America (the).
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 MetadataAbstract
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, United States of America (the). 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, United States of America (the). 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, United States of America (the). 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 Principles of Security and Trust 6th International Conference, POST 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (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.