More and more people rely on mobile devices for banking transactions or two-factor authentication (2FA), and thus trust in the security provided by the underlying operating system. Simultaneously, jailbreaks gain tremendous popularity among average users for customizing their devices. In this paper we show that both do not go well together: Jailbreaks remove vital security mechanisms, that are necessary the ensure a trusted environment that allows to protect sensitive data, such as login credentials and transaction numbers (TANs). We find that all but one banking apps available in the iOS App Store can be fully compromised by trivial means without reverse-engineering, manipulating the app, or other sophisticated attacks. Even worse, 44% of the banking apps do not even try to detect jailbreaks, revealing the prevalent, errant trust in the operating system’s security. This study assesses the current state of security of banking apps and pleads for more advanced defensive measures for protecting user data.

Buggy and flawed third-party libraries increase their host app's attack surface and put the users' privacy at risk. To avert this risk, libraries have to be kept updated to their newest versions by the app developers that integrate them into their projects. Recent researches revealed that the prevalence of outdated third-party libraries in Android apps is indeed a rampant problem, but also suggested that there is a great opportunity for drop-in replacements of outdated libraries, which would not even require cooperation by the app developers to update the libraries. However, all those conclusions are based on static app analysis, which can only provide an abstract view.

In this work, we extend the updatability analysis to the runtime of apps. We implement the first solution to update third-party libraries with drop-in replacements by their newer versions. To verify the feasibility of this developer-independent update mechanism, we dynamically test 3,000 real world apps for 3 popular libraries (78 library versions) for runtime failures stemming from incompatible library updates. To investigate the updatability of libraries in-depth, exploration enhanced dynamic testing is adopted to monitor the runtime behaviors of 15 apps before and after library updating. From our test, we find that the prior reported updatability rate is under real conditions overestimated by a factor of 1.57--2.06. Through root cause analysis, we find that the underlying problems prohibiting easy updates are intricate, such as deprecated functions, changed data structures, or entangled dependencies between different libraries and even the host app. We think our results not only put a more realistic light on the library updatability problem in Android, but also provide valuable insights for future solutions that provide automatic library updates or that try to support the app developers in better maintaining their external dependencies.

Memory corruption vulnerabilities have been around for decades and rank among the most prevalent vulnerabilities in embedded systems. Unfortunately, such constrained systems pose unique design and implementation challenges that significantly complicate and hinder the adoption of common hardening techniques. Combined with the irregular and involved nature of embedded patch management, this results in prolonged vulnerability exposure windows and vulnerabilities that are easy to exploit by an attacker. Considering the sensitive and critical nature of many embedded systems, this situation merits significant improvements.

In this paper, we present the first quantitative study of exploit mitigation adoption in 42 embedded operating systems. Our main finding is that the embedded world significantly lags behind the general-purpose world. To explain the results of our analyses, we provide a systematic identification of the underlying challenges embedded exploit mitigation adoption efforts face in practice. Based on these insights, we present µArmor, a realistic approach to address some of the key gaps identified in our quantitative analysis. Our evaluation shows that our prototype implementation of µArmor significantly raises the bar for attackers, while inducing only minimal performance and storage overhead.

Given the frequent changes in the Android framework and the continuous evolution of Android malware, it is challenging to detect malware over time in an effective and scalable manner. To address this challenge, we propose DroidEvolver, an Android malware detection system that can automatically and continually update itself during malware detection without any human involvement. While most existing malware detection systems can be updated by retraining on new applications with true labels, DroidEvolver requires neither retraining nor true labels to update itself, mainly due to the insight that DroidEvolver makes necessary and lightweight update using online learning techniques with evolving feature set and pseudo labels. The detection performance of DroidEvolver is evaluated on a dataset of 33,294 benign applications and 34,722 malicious applications developed over a period of six years. Using 6,286 applications dated in 2011 as the initial training set, DroidEvolver achieves high detection F-measure (95.27%), which only declines by 1.06% on average per year over the next five years for classifying 57,539 newly appeared applications. Note that such new applications could use new techniques and new APIs, which are not known to DroidEvolver when initialized with 2011 applications. Compared with the state-of-the-art overtime malware detection system MAMADROID, the F-measure of DroidEvolver is 2.19 times higher on average (10.21 times higher for the fifth year), and the efficiency of DroidEvolver is 28.58 times higher than MAMADROID during malware detection. DroidEvolver is also shown robust against typical code obfuscation techniques.

Applications that handle sensitive information need to express and reason about the trust relationships between security principals. Such reasoning is difficult because the trust relationships are dynamic, and must thus be reasoned about at runtime when discovering and reasoning about trust relationships might inadvertently reveal confidential information and be subject to manipulation by untrusted principals.

The Flow-Limited Authorization Model (FLAM) by Arden, Liu and Myers exactly meets these needs. However, previous attempts to use FLAM in a programming language have not reaped the full benefits of the model.

We present Flamio, an instantiation of FLAM in a language with coarse-grained information-flow control (IFC) which naturally lends itself to dynamic enforcement techniques. In our implementation of Flamio, the FLAM proof search rules for deriving trust relationships are implemented as regular Flamio computations: the IFC requirements for FLAM proof rules are a natural fit with coarse-grained information-flow mechanisms. Flamio even supports remote procedure calls, and thus seamlessly supports FLAM's distributed proof search.

We have implemented Flamio as a Haskell library, and proved that an adequate Flamio calculus enforces a noninterference-based security guarantee. We have implemented several case studies, demonstrating the expressiveness and usefulness of Flamio in distributed settings, as well as our novel approach to control label creep during proof search.

Securing database-backed applications requires tracking information across the program and the database together, since securing each component in isolation may still result in an overall insecure system. Current research extends language-based techniques with models capturing the database's behavior. Previous work, however, relies on simplistic database models, which ignore security-relevant features that may leak sensitive information. We propose a novel security monitor for database-backed applications. The monitor tracks fine-grained dependencies between variables and database tuples by leveraging database theory concepts like disclosure lattices and query determinacy. It also accounts for a realistic database model that supports security-critical constructs like triggers and dynamic policies. The monitor automatically synthesizes program-level code that replicates the behavior of database features like triggers, thereby tracking information flows inside the database. We also introduce symbolic tuples, an efficient approximation of dependency-tracking over disclosure lattices. We implement the monitor for SCALA programs and demonstrate its effectiveness on four case studies.

The wide-spread adoption of system defenses such as the randomization of code, stack, and heap raises the bar for code-reuse attacks. Thus, attackers utilize a scripting engine in target programs like a web browser to prepare the code-reuse chain, e.g., relocate gadget addresses or perform a just-in-time gadget search. However, many types of programs do not provide such an execution context that an attacker can use. Recent advances in data-oriented programming (DOP) explored an orthogonal way to abuse memory corruption vulnerabilities and demonstrated that an attacker can achieve Turing-complete computations without modifying code pointers in applications. As of now, constructing DOP exploits requires a lot of manual work for every combination of application and payload anew. In this paper, we present novel techniques to automate the process of generating DOP exploits. We implemented a compiler called Steroids that leverages these techniques and compiles our high-level language Slang into low-level DOP data structures driving malicious computations at run time. This enables an attacker to specify her intent in an application- and vulnerability-independent manner to maximize reusability. We demonstrate the effectiveness of our techniques and prototype implementation by specifying four programs of varying complexity in Slang that calculate the Levenshtein distance, traverse a pointer chain to steal a private key, relocate a ROP chain, and perform a JIT-ROP attack. Steroids compiles each of those programs to low-level DOP data structures targeted at five different applications including GStreamer, Wireshark and ProFTPd, which have vastly different vulnerabilities and DOP instances. Ultimately, this shows that our compiler is versatile, can be used for both 32-bit and 64-bit applications, works across bug classes, and enables highly expressive attacks without conventional code-injection or code-reuse techniques in applications lacking a scripting engine.

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module (TPM)-backed anonymous credentials. We develop Tamarin modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol’s expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

Speculative execution vulnerabilities in microarchitecture processors have raised concerns about the security of Intel SGX. To understand clearly the security impact of this vulnerability against SGX, this paper makes the following studies: First, to demonstrate the feasibility of the attacks, we present SGXPECTRE Attacks (the SGX-variants of Spectre attacks) that exploit speculative execution vulnerabilities to subvert the confidentiality of SGX enclaves. We show that when branch prediction of the enclave code can be influenced by programs outside the enclave, the control flow of the enclave program can be temporarily altered to execute instructions that lead to observable cache-state changes. An adversary observing such changes can learn secrets inside the enclave memory or its internal registers, thus completely defeating the confidentiality guarantee offered by SGX. Second, to determine whether real-world enclave programs are impacted by the attacks, we develop techniques to automate the search of vulnerable code patterns in enclave binaries using symbolic execution. Our study suggests that nearly any enclave program could be vulnerable to SGXPECTRE Attacks since vulnerable code patterns are available in most SGX runtimes (e.g., Intel SGX SDK, Rust-SGX, and Graphene-SGX). Third, we apply SGXPECTRE Attacks to steal seal keys and attestation keys from Intel signed quoting enclaves. The seal key can be used to decrypt sealed storage outside the enclaves and forge valid sealed data; the attestation key can be used to forge attestation signatures. For these reasons, SGXPECTRE Attacks practically defeat SGX’s security protection. Finally, we evaluate Intel’s existing countermeasures against SGXPECTRE Attacks and discusses the security implications.

With the proliferation of Trusted Execution Environments (TEEs) such as Intel SGX, a number of cloud providers will soon introduce TEE capabilities within their offering (e.g., Microsoft Azure). The integration of SGX within the cloud considerably strengthens the threat model for cloud applications. However, cloud deployments depend on the ability of the cloud operator to add and remove application dynamically; this is no longer possible given the current model to deploy and provision enclaves that actively involves the application owner.

In this paper, we propose ReplicaTEE, a solution that enables seamless commissioning and decommissioning of TEE-based applications in the cloud. ReplicaTEE leverages an SGX-based provisioning service that interfaces with a Byzantine Fault-Tolerant storage service to securely orchestrate enclave replication in the cloud, without the active intervention of the application owner.

Namely, in ReplicaTEE, the application owner entrusts application secret to the provisioning service; the latter handles all enclave commissioning and decommissioning operations throughout the application lifetime. We analyze the security of ReplicaTEE and show that it is secure against attacks by a powerful adversary that can compromise a large fraction of the cloud infrastructure. We implement a prototype of ReplicaTEE in a realistic cloud environment and evaluate its performance. ReplicaTEE moderately increments the TCB by ~800 LoC. Our evaluation shows that ReplicaTEE does not add significant overhead to existing SGX-based applications.

Low-level languages like C/C++ are widely used in various applications for their performance and flexibility. Unfortunately, these languages are prone to memory corruption vulnerabilities, leading to control-flow hijacking attacks. Control flow integrity (CFI) is a universally adopted principle to enforce run-time control flows of a program to a pre-computed control- flow graph (CFG). While the traditional context-insensitive CFI falls short in protecting critical control transfers, recent context- sensitive CFI research shows promising improvements but has various limitations. We present Control Flow Integrity with Look Back (CFI-LB), a call-site sensitive CFI in which a conventional source-target control transfer is strengthened by a look back into the call-sites (return addresses). CFI-LB features the adaptive call-site sensitivity in which each indirect call has its own level of sensitivity and the multi-scope CFG to improve the security even if a precise context-sensitive static CFG is not available, especially for large programs such as gcc and NGINX. One of the CFGs is constructed by our localized concolic execution, which significantly extends the dynamic CFG with very low false positives. CFI-LB is also the first CFI system explicitly designed to protect its reference monitors from race conditions. We have built a prototype of CFI-LB. The evaluation with SPEC CPU2006 benchmarks and NGINX indicates that CFI-LB has a low-performance overhead (less than 5% on average for the full protection) while increasing the security.

Bitcoin, introduced in 2008 and launched in 2009, is the first digital currency which solved the double spending problem without relying on a trusted third party. Bitcoin provides a way to transact without any trusted intermediary, but its privacy guarantees are questionable. Despite the fact that Bitcoin addresses are not linked to any identity, multiple deanonymization attacks have been proposed. Alternative cryptocurrencies such as Dash, Monero, and Zcash aim to provide stronger privacy by using sophisticated cryptographic techniques to obfuscate transaction data.

Previous work in cryptocurrency privacy mostly focused on applying data mining algorithms to the transaction graph extracted from the blockchain. We focus on a less well researched vector for privacy attacks: network analysis. We argue that timings of transaction messages leak information about their origin, which can be exploited by a well connected adversarial node. This paper is the first one to specifically study network-level attacks in the three major privacy-focused cryptocurrencies, in addition to Bitcoin. We describe the message propagation mechanics and privacy guarantees in Bitcoin, Dash, Monero, and Zcash. We propose a novel technique for linking transaction based on transaction propagation analysis. We also unpack address advertisement messages (ADDR), which under certain assumptions may help in linking transaction clusters to IP addresses of nodes. We implement and evaluate our method, deanonymizing our own transactions in Bitcoin and Zcash with a high level of accuracy. We also show that our technique is applicable to Dash and Monero. We estimate the cost of a full-scale attack on the Bitcoin mainnet at hundreds of US dollars, which available even to a low budget adversary.

Smart contracts are applications that execute on blockchains. Today they manage billions of dollars in value and motivate visionary plans for pervasive blockchain deployment. While smart contracts inherit the availability and other security assurances of blockchains, however, they are impeded by blockchains’ lack of confidentiality and poor performance.

We present Ekiden, a system that addresses these critical gaps by combining blockchains with Trusted Execution Environments (TEEs). Ekiden leverages a novel architecture that separates consensus from execution, enabling efficient TEE-backed confidentiality-preserving smart-contracts and high scalability. Our prototype (with Tendermint as the consensus layer) achieves example performance of 600x more throughput and 400x less latency at 1000x less cost than the Ethereum mainnet.

Another contribution of this paper is that we systematically identify and treat the pitfalls arising from harmonizing TEEs and blockchains. Treated separately, both TEEs and blockchains provide powerful guarantees, but hybridized, though, they engender new attacks. For example, in naïve designs, privacy in TEE-backed contracts can be jeopardized by forgery of blocks, a seemingly unrelated attack vector. We believe the insights learned from Ekiden will prove to be of broad importance in hybridized TEE-blockchain systems.

In this paper, we describe a new type of online fraud, referred to as 'eWhoring' by offenders. This crime script analysis provides an overview of the 'eWhoring' business model, drawing on more than 6,500 posts crawled from an online underground forum. This is an unusual fraud type, in that offenders readily share information about how it is committed in a way that is almost prescriptive. There are economic factors at play here, as providing information about how to make money from 'eWhoring' can increase the demand for the types of images that enable it to happen. We find that sexualised images are typically stolen and shared online. While some images are shared for free, these can quickly become 'saturated', leading to the demand for (and trade in) more exclusive 'packs'. These images are then sold to unwitting customers who believe they have paid for a virtual sexual encounter. A variety of online services are used for carrying out this fraud type, including email, video, dating sites, social media, classified advertisements, and payment platforms. This analysis reveals potential interventions that could be applied to each stage of the crime commission process to prevent and disrupt this crime type.

Abstract: Radically Open Security is the world’s first non-profit computer security consultancy company. With core principles of openness, transparency, and open-source, ROS innovated the "Peek Over Our Shoulder" style of penetration testing, and developed the supporting platform OWASP PenText. Despite initial skepticism about ROS's unusual workflow and business model, ROS has grown to 40+ staff and 80+ customers. In this presentation, Dr. Melanie Rieback will describe her journey and lessons learned, and explain why the future of pentesting is "Radically Open".

Biography: Dr. Melanie Rieback is the CEO/Co-founder of Radically Open Security and Nonprofit Ventures. She is also a former Assistant Professor of Computer Science at VU who performed RFID security research (RFID Virus and RFID Guardian), that attracted worldwide press coverage, and won several awards (VU Mediakomeet, ISOC Award, NWO I/O award, IEEE Percom Best Paper, USENIX Lisa Best Paper). Melanie worked as a Senior Engineering Manager on XenClient at Citrix, where she led their Vancouver office. She was also the head researcher in the CSIRT at ING Bank, where she spearheaded their Analysis Lab and the ING Core Threat Intelligence Project. For fun, she co-founded the Dutch Girl Geek Dinner in 2008. Melanie was named 2010 ICT Professional of the Year (Finalist) by WomeninIT, one of the 400 most successful women in the Netherlands by Viva Magazine (Viva400) in 2010 and 2017, one of the fifty most inspiring women in tech (Inspiring Fifty Netherlands) in 2016 and 2017, and the Most Innovative IT Leader by CIO Magazine NL (TIM Award) in 2017. Her company, Radically Open Security was also named the 50th Most Innovative SME by the Dutch Chamber of Commerce (MKB Innovatie Top 100) in 2016.

Since the introduction of Bitcoin in 2008, cryptocurrency has been undergoing a quick and explosive development. At the same time, privacy protection, one of the key merits of cryptocurrency, has attracted much attention by the community. A deterministic wallet algorithm and a stealth address algorithm have been widely adopted in the community, due to their virtues on functionality and privacy protection, which come from a key derivation mechanism that an arbitrary number of derived keys can be generated from a master key. However, these algorithms suffer a vulnerability. In particular, when a minor fault happens (say, one derived key is compromised somehow), the damage is not limited to the leaked derived key, instead, it spreads to the master key and all derived keys are compromised.

In this paper, to provide a formal treatment for the problem, we introduce and formalize a new signature variant, called Key-Insulated and Privacy-Preserving Signature Scheme with Publicly Derived Public Key (PDPKS), which forms a convenient and robust cryptographic tool for offering the virtues of deterministic wallet and stealth address, while eliminating the security vulnerabilities. Specifically, PDPKS allows anyone to derive new signature verification keys for a user, say Alice, based on her long-term public key, while only Alice can derive the signing keys corresponding to those verification keys. In terms of privacy, given a derived verification key and valid signatures with respect to it, an adversary is not able to tell which long-term public key, out of a set of known long-term public keys, is the one from which the verification key was derived. A distinguishing security feature of PDPKS, with the above functionality and privacy features, is that the derived keys are independent/insulated from each other, namely, compromising the signing key associated with a verification key does not allow an adversary to forge a valid signature for another verification key, even if both verification keys are derived from the same long-term public key.

We formalize the notion of PDPKS and propose a practical and proven secure construction, which could be a convenient and secure cryptographic tool for building privacy-preserving cryptocurrencies and supporting promising use cases in practice, as it can used to implement secure stealth addresses, and can be used to implement deterministic wallets and the related appealing use cases, without security concerns.

WireGuard is a free and open source Virtual Private Network (VPN) that aims to replace IPsec and OpenVPN. It is based on a new cryptographic protocol derived from the Noise Protocol Framework. This paper presents the first mechanised cryptographic proof of the protocol underlying WireGuard, using the CryptoVerif proof assistant.

We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard.

Our work provides novel contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in Diffie-Hellman groups such as Curve25519, which WireGuard's authenticated key exchange is based upon. To our knowledge, this is the first mechanised proof employing such a precise model. Second, we prove, partly using CryptoVerif, several indifferentiability lemmas, useful to simplify random oracle calls.

Computing similarity between high-dimensional data is a fundamental problem in data mining and information retrieval, with numerous applications---such as e-discovery and patient similarity. To address the relevant performance and scalability challenges, approximation methods are employed. A common characteristic among all privacy-preserving approximation protocols based on sketching is that the sketching is performed locally and is based on common randomness.

Inspired by the power of attacks on machine learning models, we introduce the study of adversarial inputs for secure similarity approximations. To formally capture the framework of this family of attacks we present a new threat model where a party is assumed to use the common randomness to perturb her input 1) offline, and 2) before the execution of any secure protocol, so as to steer the approximation result to a maliciously chosen output. We define perturbation attacks under this adversarial model and propose attacks for the techniques of minhash and cosine sketching. We demonstrate the simplicity and effectiveness of the attacks by measuring their success on synthetic and real data from the areas of e-discovery and patient similarity.

To mitigate such perturbation attacks we propose a server-aided architecture, where an additional party, the server, assists in the secure similarity approximation by handling the common randomness as private data. We revise and introduce the necessary secure protocols so as to apply minhash and cosine sketching techniques in the server-aided architecture. Our implementation demonstrates that this new design can mitigate offline perturbation attacks without sacrificing the efficiency and scalability of the reconstruction protocol.

With the recent advent of the Internet of Things (IoT), embedded devices increasingly operate collaboratively in autonomous networks. A key technique to guard the secure and safe operation of connected embedded devices is remote attestation. It allows a third party, the verifier, to ensure the integrity of a remote devices, the prover. Unfortunately, existing attestation protocols are impractical when applied in autonomous networks of embedded systems due to their limited scalability, performance, robustness, and security guarantees.

In this work, we propose a novel attestation protocol that is particularly suited for autonomous embedded systems. Our protocol is the first that (i) enables many low-end prover devices to attest their integrity towards many potentially untrustworthy low-end verifier devices, (ii) is fully decentralized, thus, able to withstand network disruptions and arbitrary device outages, and (iii) is in addition to software attacks capable of detecting physical attacks in a much more robust way than any existing protocol. We implemented our protocol, conducted measurements, and simulated large networks. The results show that our protocol is practical on low-end embedded devices, scales to large networks with millions of devices, and improves robustness by multiple orders of magnitudes compared with the best existing protocols.

As messaging applications are becoming increasingly popular, it is of utmost importance to analyze their security and mitigate existing weaknesses. This paper focuses on one of the most acclaimed messaging applications: Signal.

Signal is a protocol that provides end-to-end channel security, forward secrecy, and post-compromise security. These features are achieved thanks to a key-ratcheting mechanism that updates the key material at every message. Due to its high security impact, Signal's key-ratcheting has recently been formalized, along with an analysis of its security.

In this paper, we revisit Signal, describing some attacks against the original design and proposing SAID: Signal Authenticated and IDentity-based. As the name indicates, our protocol relies on an identity-based setup, which allows us to dispense with Signal's centralized server. We use the identity-based long-term secrets to obtain persistent and explicit authentication, such that SAID achieves higher security guarantees than Signal.

We prove the security of SAID not only in the Authenticated Key Exchange (AKE) model (as done by previous work), but also in the Authenticated and Confidential Channel Establishment (ACCE) model, which we adapted and redefined for SAID and asynchronous messaging protocols in general into a model we call identity-based Multistage Asynchronous Messaging (iMAM). We believe our model to be more faithful in particular to the true security of Signal, whose use of the message keys prevents them from achieving the composable guarantee claimed by previous analysis.

Properly benchmarking a system is a difficult and intricate task. Unfortunately, even a seemingly innocuous benchmarking mistake can compromise the guarantees provided by a given systems security defense and also put its reproducibility and comparability at risk. This threat is particularly insidious as it is generally not a result of malice and can easily go undetected by both authors and reviewers. Moreover, as modern defenses often trade off security for performance in an attempt to find an ideal design point in the performance-security space, the damage caused by benchmarking mistakes is increasingly worrisome.

To analyze the magnitude of the phenomenon, we identify a set of 22 “benchmarking crimes” that threaten the validity of systems security evaluations and perform a survey of 50 defense papers published in top venues. To ensure the validity of our results, we perform the complete survey twice, with two independent readers. We find only a very small number of disagreements between readers, showing that our assessment of benchmarking crimes is highly reproducible.

We show that benchmarking crimes are widespread even in papers published at tier-1 venues. We find that tier-1 papers commit an average of five benchmarking crimes and we find only a single paper in our sample that committed no benchmarking crimes. Moreover, we find that the scale of the problem is constant over time, suggesting that the community is not yet addressing it despite the problem being now more relevant than ever. This threatens the scientific process, which relies on reproducibility and comparability to ensure that published research advances the state of the art. We hope to raise awareness of these issues and provide recommendations to improve benchmarking quality and safeguard the scientific process in our community.

Mechanisms for large-scale vulnerability notifications have been confronted with disappointing remediation rates. It has proven difficult to reach the relevant party and, once reached, to incentivize them to act. We present the first empirical study of a potentially more effective mechanism: quarantining the vulnerable resource until it is remediated. We have measured the remediation rates achieved by a medium-sized ISP for 1,688 retail customers running open DNS resolvers or Multicast DNS services. These servers can be abused in UDP-based amplification attacks. We assess the effectiveness of quarantining by comparing remediation with two other groups: one group which was notified but not quarantined and another group where no action was taken. We find very high remediation rates for the quarantined users, 87%, even though they can self-release from the quarantine environment. Of those who received the email-only notification, 76% remediated. Surprisingly, over half of the customers who were not notified at all also remediated, though this is tied to the fact that many observations of vulnerable servers are transient. All in all, quarantining appears more effective than other notification and remediation mechanisms, but it is also clear that it can not be deployed as a general solution for Internet-wide notifications.

In order to supervise the security of a large infrastructure, the administrator deploys multiple sensors and intrusion detection systems on several critical places in the system. It is easier to explain and detect attacks if more events are logged. Starting from a suspicious event (appearing as a log entry), the administrator can start his investigation by manually building the set of previous events that are linked to this event of interest. Accordingly, the administrator attempts to identify links among the logged events in order to retrieve those that correspond to the traces of the attacker's actions in the supervised system; previous work is aimed at building these connections. In practice, however, this type of link is not trivial to define and discover. Hence, there is a real necessity to describe and define formally the semantics of these links in literature. In this paper, a clear definition of this relationship, called contextual event causal dependency, is introduced and proposed. The work presented in this paper aims at defining a formal model that would ideally unify previous work on causal dependencies among heterogeneous events. We define a relationship among events that enables the discovery of all events, which can be considered as the cause (in the past) or the effect (in the future) of an event of interest (e.g., an indicator of compromise, produced by an attacker action). This model is gradually introduced and defined by merging two previously defined causality models from the distributed system and operating system research areas (i.e., Lamport's and d'Ausbourg's). Our model takes into consideration heterogeneous events that emanate from different abstraction layers (e.g., network, system, and application) with the main objective of formally defining a causal relationship among logged events. Thereafter, we show how existing implementations separately allow the computation of parts of the model. Finally, we describe the implementation and assessment of the model according to real attacks on distributed environments and its accuracy to extract all causally linked events related to a given attack event trace.

The Noise Protocol Framework, introduced recently, allows for the design and construction of secure channel protocols by describing them through a simple, restricted language from which complex key derivation and local state transitions are automatically inferred. Noise “Handshake Patterns” can support mutual authentication, forward secrecy, zero round-trip encryption, identity hiding and other advanced features. Since the framework’s release, Noise-based protocols have been adopted by WhatsApp, WireGuard and other high-profile applications.

We present Noise Explorer, an online engine for designing, reasoning about and formally verifying arbitrary Noise Handshake Patterns. Based on our formal treatment of the Noise Protocol Framework, Noise Explorer can validate any Noise Handshake Pattern and then translate it into a model ready for automated verification. We use Noise Explorer to analyze 50 Noise Handshake Patterns.

We confirm the stated security goals for 12 fundamental patterns and provide precise properties for the rest. We also analyze unsafe Noise patterns and discover potential attacks. All of this work is consolidated into a usable online tool that presents a compendium of results and can parse formal verification results to generate detailed-but-pedagogical reports regarding the exact security guarantees of each message of a Noise Handshake Pattern with respect to each party, under an active attacker and including malicious principals. Noise Explorer evolves alongside the standard Noise Protocol Framework, having already contributed new security goal verification results and stronger definitions for pattern validation and security parameters.

This paper presents IFAL, a provably secure and privacy conscious scheme for Vehicle-to-Vehicle and Vehicle-to-Infrastructure (V2X) communication. Issue First Activate Later (IFAL) is a practical and secure improvement to the leading European candidate for V2X (ETSI) and one which also merits over the leading US standard. IFAL incorporates a novel cryptographic mechanism which both avoids the need for certificate revocation and which supports vehicles with limited and intermittent connectivity. We introduce a new construction which is equivalent to symmetric key diversification in the public key setting with short, time-delayed activation. We also present a new formalisation of V2X security and privacy which we apply to IFAL to show that it is a provably secure and privacy conscious V2X scheme. IFAL is ETSI compliant and ready for integration into the standard.

In this paper, we describe several practically exploitable fault attacks against OpenSSL's implementation of elliptic curve cryptography, related to the singular curve point decompression attacks of Blömer and Günther (FDTC2015) and the degenerate curve attacks of Neves and Tibouchi (PKC 2016).

In particular, we show that OpenSSL allows to construct EC key files containing explicit curve parameters with a compressed base point. A simple single fault injection upon loading such a file yields a full key recovery attack when the key file is used for signing with ECDSA, and a complete recovery of the plaintext when the file is used for encryption using an algorithm like ECIES. The attack is especially devastating against curves with $j$-invariant equal to 0 such as the Bitcoin curve secp256k1, for which key recovery reduces to a single division in the base field.

Additionally, we apply the present fault attack technique to OpenSSL's implementation of ECDH, by combining it with Neves and Tibouchi's degenerate curve attack. This verion of the attack applies to usual named curve parameters with nonzero $j$-invariant, such as P192 and P256. Although it is typically more computationally expensive than the one against signatures and encryption, and requires multiple faulty outputs from the server, it can recover the entire static secret key of the server even in the presence of point validation.

These various attacks can be mounted with only a single instruction skipping fault, and therefore can be easily injected using low-cost voltage glitches on embedded devices. We validated them in practice using concrete fault injection experiments on a Rapsberry Pi single board computer running the up to date OpenSSL command line tools---a setting where the threat of fault attacks is quite significant.

A key question for characterizing a system's vulnerability against timing attacks is whether or not it allows an adversary to aggregate information about a secret over multiple timing measurements. Existing approaches for reasoning about this aggregate information rely on strong assumptions about the capabilities of the adversary in terms of measurement and computation, which is why they fall short in modeling, explaining, or synthesizing real-world attacks against cryptosystems such as RSA or AES.

In this paper we present a novel model for reasoning about information aggregation in timing attacks. The model is based on an a novel abstraction of timing measurements that better captures the capabilities of real-world adversaries, and a notion of compositionality of programs that explains attacks by divide-and-conquer. Our model thus lifts important limiting assumptions made in prior work and enables us to give the first uniform explanation of high-profile timing attacks in the language of information-flow analysis.

With WhatsApp's adoption of the Signal Protocol as its default, end-to-end encryption by the masses happened almost overnight. Unlike iMessage, WhatsApp notifies users that encryption is enabled, explicitly informing users about improved privacy. This rare feature gives us an opportunity to study people's understandings and perceptions of secure messaging pre- and post-mass messenger encryption (post-MME). To study changes in perceptions, we compared the results of two mental models studies: one conducted in 2015 pre-MME and one in 2017 post-MME. Our primary finding is that users do not trust encryption as currently offered. When asked about encryption in the study, most stated that they had heard of encryption, but only a few understood the implications, even on a high level. Their consensus view was that no technical solution to stop skilled attackers from getting their data exists. Even with a major development, such as WhatsApp rolling out end-to-end encryption, people still do not feel well protected by their technology. Surprisingly, despite WhatsApp's end-to-end security info messages and the high media attention, the majority of the participants were not even aware of encryption. Most participants had an almost correct threat model, but overestimated the power of all attackers. Using technology made them feel vulnerable.

Location Privacy-Preserving Mechanisms (LPPMs) in the literature largely consider that users' data is available for training, and that it wholly characterizes their mobility patterns. Thus, they *hardwire* this information in their designs and evaluate their privacy properties with these same data. In this paper, we aim to understand the impact of this decision on the level of privacy these LPPMs may offer in real life when the users' mobility data may be different from the data used in the design phase. Our results show that, in many cases, training data does not capture users' behavior accurately and, thus, the level of privacy provided by the LPPM is often overestimated. To address this gap between theory and practice, we propose to use *blank-slate models* for LPPM design. Contrary to the hardwired approach, that assumes known users' behavior, blank-slate models *learn* the user's behavior from the queries to the service provider. We leverage this blank-slate approach to develop a new family of LPPMs, that we call Profile Estimation-Based LPPMs. Using real data, we empirically show that our proposal outperforms optimal state-of-the-art mechanisms designed on *sporadic* hardwired models. On *non-sporadic* location privacy scenarios, our method is only better if the location release is not continuous. It is our hope that eliminating the need to bootstrap the mechanisms with training data and ensuring that the mechanisms are lightweight and easy to compute help fostering the integration of location privacy protections in deployed systems.

Public key infrastructure (PKI) based on certificate authorities is one of the cornerstones of secure communication over the internet. Certificates issued as part of this PKI provide authentication of web servers among others. Yet, the PKI ecosystem is susceptible to certificate misissuance and misuse attacks. To prevent those attacks, Certificate Transparency (CT) facilitates auditing of issued certificates and detecting certificates issued without authorization. Users that want to verify inclusion of certificates on CT log servers contact the CT server directly to retrieve inclusion proofs. This direct contact with the log server creates a privacy problem since the users' browsing activities could be recorded by the log server owner.

Lueks and Goldberg (FC 2015) suggested the use of Private Information Retrieval (PIR) in order to protect the users' privacy in the CT ecosystem. With the immense amount of certificates included on CT log servers, their approach runs into performance issues, though. Nevertheless, we build on this approach and extend it using multi-tier Merkle trees, and render it practical using multi-server PIR protocols based on distributed point functions (DPFs). Our approach leads to a scalable design suitable to handle the increasing number of certificates, and is in addition generic allowing instantiations using secure accumulators and PIRs.

We implement and test this mechanism for privacy-preserving membership proof retrieval and show that it can be integrated without disrupting existing CT infrastructure. Most importantly, even for future-proof CT log sizes of 2^31 certificates, the performance overhead is less than 9 milliseconds in total.

In the last decade, we observed a constantly growing number of Location-Based Services (LBSs) used in indoor environments, such as for targeted advertising in shopping malls or finding nearby friends. Although privacy-preserving LBSs were addressed in the literature, there was a lack of attention to the problem of enhancing privacy of indoor localization, i.e., the process of obtaining the users' locations indoors and, thus, a prerequisite for any indoor LBS.

In this work we present PILOT, the first practically efficient solution for Privacy-Preserving Indoor Localization (PPIL) that was obtained by a synergy of the research areas indoor localization and applied cryptography. We design, implement, and evaluate protocols for Wi-Fi fingerprint-based PPIL that rely on 4 different distance metrics. To save energy and network bandwidth for the mobile end devices in PPIL, we securely outsource the computations to two non-colluding semi-honest parties. Our solution mixes different secure two-party computation protocols and we design size- and depth-optimized circuits for PPIL. We construct efficient circuit building blocks that are of independent interest: Single Instruction Multiple Data (SIMD) capable oblivious access to an array with low circuit depth and selection of the $k$-Nearest Neighbors with small circuit size. Additionally, we reduce Received Signal Strength (RSS) values from 8 bits to 4 bits without any significant accuracy reduction. Our most efficient PPIL protocol is 553x faster than that of Li et al. (INFOCOM'14) and 500x faster than that of Ziegeldorf et al. (WiSec'14). Our implementation on commodity hardware has practical run-times of less than 1 second even for the most accurate distance metrics, and it can process more than half a million PPIL queries per day.

We study the 5G-AKA authentication protocol described in the 5G mobile communication standards. This version of AKA tries to achieve a better privacy than the 3G and 4G versions through the use of asymmetric randomized encryption. Nonetheless, we show that except for the IMSI-catcher attack, all known attacks against 5G-AKA privacy still apply.

Next, we modify the 5G-AKA protocol to prevent these attacks, while satisfying the cost and efficiency constraints of the 5G-AKA protocol. We then formally prove that our protocol is σ-unlinkable. This is a new security notion, which allows for a fine-grained quantification of a protocol privacy. Our security proof is carried out in the Bana-Comon indistinguishability logic. We also prove mutual authentication as a secondary result.

Wide adoption of artificial neural networks in various domains has led to an increasing interest in defending adversarial attacks against them. Preprocessing defense methods such as pixel discretization are particularly attractive in practice due to their simplicity, low computational overhead, and applicability to various systems. It is observed that such methods work well on simple datasets like MNIST, but break on more complicated ones like ImageNet under recently proposed strong white-box attacks. To understand the conditions for success and potentials for improvement, we study the pixel discretization defense method, including more sophisticated variants that take into account the properties of the dataset being discretized. Our results again show poor resistance against the strong attacks. We analyze our results in a theoretical framework and offer strong evidence that pixel discretization is unlikely to work on all but the simplest of the datasets. Furthermore, our arguments present insights why some other preprocessing defenses may be insecure.

We present EZPC, a secure two-party computation (2PC) framework that generates efficient 2PC protocols from high-level, easy-to-write programs. EZPC provides formal correctness and security guarantees while maintaining performance and scalability. Previous language frameworks, such as CBMCGC, ObliVM, SMCL, and Wysteria, generate protocols that use either arithmetic or boolean circuits exclusively. Our compiler is the first to generate protocols that combine both arithmetic and boolean circuits for better performance. We empirically demonstrate that the protocols generated by our framework match or outperform (up to 19x) recent works that provide hand-crafted protocols for various functionalities such as secure prediction and matrix factorization.

Machine learning (ML) applications are increasingly prevalent. Protecting the confidentiality of ML models becomes paramount for two reasons: (a) a model can be a business advantage to its owner, and (b) an adversary may use a stolen model to find transferable adversarial examples that can evade classification by the original model. Access to the model can be restricted to be only via well-defined prediction APIs. Nevertheless, prediction APIs still provide enough information to allow an adversary to mount model extraction attacks by sending repeated queries via the prediction API.

In this paper, we describe new model extraction attacks using novel approaches for generating synthetic queries, and optimizing training hyperparameters. Our attacks outperform state-of-the-art model extraction in terms of transferability of both targeted and non-targeted adversarial examples (up to +29-44 percentage points, pp), and prediction accuracy (up to +46 pp) on two datasets. We provide take-aways on how to perform effective model extraction attacks.

We then propose PRADA, the first step towards generic and effective detection of DNN model extraction attacks. It analyzes the distribution of consecutive API queries and raises an alarm when this distribution deviates from benign behavior. We show that PRADA can detect all prior model extraction attacks with no false positives.

Cross-Site Request Forgery (CSRF) is one of the oldest and simplest attacks on the Web, yet it is still effective on many websites and it can lead to severe consequences, such as money losses and account takeovers. Unfortunately, tools and techniques proposed so far to identify CSRF vulnerabilities either need manual reviewing by human experts or assume the availability of the source code of the web application.

In this paper we present Mitch, the first machine learning solution for the black-box detection of CSRF vulnerabilities. At the core of Mitch there is an automated detector of sensitive HTTP requests, i.e., requests which require protection against CSRF for security reasons. We trained the detector using supervised learning techniques on a dataset of 5,828 HTTP requests collected on popular websites and make it available to other security researchers. Our solution outperforms existing detection heuristics proposed in the literature, allowing us to identify 35 new CSRF vulnerabilities on 20 major websites and 3 previously undetected CSRF vulnerabilities on production software already analyzed using a state-of-the-art tool.

Web security relies on the assumption that certificate authorities (CAs) issue certificates to rightful domain owners only. However, we show that CAs expose vulnerabilities which allow an attacker to obtain certificates from major CAs for domains he does not own. We present a passive measurement method that allows us to check CAs for a list of technical weaknesses during their domain validation procedures. Our results show that all tested CAs are vulnerable in one or even multiple ways, because they rely on a combination of insecure protocols like DNS and HTTP and do not implement existing secure alternatives like DNSSEC and TLS. We verified our results experimentally and disclosed these vulnerabilities to CAs. Based upon our findings we provide recommendations to domain owners and CAs to close this fundamental weakness in web security.

Illicit traffic monetization is a type of Internet fraud that hijacks users' web requests and reroutes them to a traffic network (e.g., advertising network), in order to unethically gain monetary rewards. Despite its popularity among Internet fraudsters, our understanding of the problem is still limited. Since the behavior is highly dynamic (can happen at any place including client-side, transport-layer and server-side) and selective (could target a regional network), prior approaches like active probing can only reveal a small piece of the entire ecosystem. So far, questions including how this fraud works at a global scale and what fraudsters' preferred methods are, still remain unanswered.

To fill the missing pieces, we developed TraffickStop the first system that can detect this fraud \textit{passively}. Our key contribution is a novel algorithm that works on large-scale DNS logs and efficiently discovers abnormal domain correlations. TraffickStop enables the first landscape study of this fraud, and we have some interesting findings. By analyzing over 231 billion DNS logs of two weeks, we discovered 1,457 fraud sites. Regarding its scale, the fraud sites receive more than 53 billion DNS requests within one year, and a company could lose up to 53K dollars per day due to fraud traffic. We also discovered two new strategies that are leveraged by fraudsters to evade inspection. Our work provides new insights into illicit traffic monetization, raises its public awareness, and contributes to a better understanding and ultimate elimination of this threat.

Practitioners who seek to defend password-protected resources from online guessing attacks will find a shortage of tooling and techniques to help them. Little research suggests anything beyond blocking or throttling traffic from IP addresses sending suspicious traffic; counting failed authentication requests, or some variant, is often the sole feature used to determine suspicion. In this paper we show that several other features can greatly help distinguishing benign and attack traffic. First, we increase the penalties for clients responsible for fail events involving passwords frequently-guessed by attackers. Second, we reduce the threshold (and thus protect better) for accounts with weak passwords. Third, we detect, and are more forgiving of, login failures caused by users mistyping their passwords. Most importantly, we achieve all of these goals without needing any marker that indicates weak accounts, changing the format in which passwords are stored (i.e. we do not store passwords plaintext or in any recoverable form), or storing any information that might be harmful if leaked. We present an open-source implementation of this system and demonstrate it's improvement over simpler blocking strategies in various simulated scenarios.

Law enforcement agencies regularly take down botnets as the ultimate defense against global malware operations. By arresting malware authors, and simultaneously infiltrating or shutting down a botnet's network infrastructures (such as C2 servers), defenders stop global threats and mitigate pending infections. In this paper, we propose an orthogonal defense that does not require seizing botnet infrastructures, and at the same time can also be used to slow down malware spreading and infiltrate its monetization techniques. We describe how to non-intrusively exploit *tarpit* vulnerabilities in malware to slow down or, ideally, even stop malware. Our basic idea is to automatically identify network operations used by malware that will *block* the malware either forever or for a significant amount of time. Using dynamic malware analysis, we monitor how malware interacts with the POSIX and Winsock socket APIs. From this, we infer network operations that would have blocked when provided certain network inputs. We augment this vulnerability search with an automated generation of tarpits that exploit the identified vulnerabilities. We apply our prototype MALPITY on six popular malware families and discover 12 previously-unknown tarpit vulnerabilities, revealing that all families are susceptible to our defense. We demonstrate how to, e.g., halt Pushdo's DGA-based C2 communication, hinder SalityP2P peers from receiving commands or updates, and stop Bashlite's spreading engine.

Modern e-voting systems deploy cryptographic protocols on a complex infrastructure involving different computing platforms and agents. It is crucial to have appropriate specification and evaluation methods to perform rigorous analysis of such systems, taking into account the corruption and computational capabilities of a potential attacker. In particular, the platform used for voting may be corrupted, e.g. infected by malware, and we need to ensure privacy and integrity of votes even in that case.

We propose a new definition of vote privacy, formalized as a computational indistinguishability game, that allows to take into account such refined attacker models; we show that the definition captures both known and novel attacks against several voting schemes; and we propose a scheme that is provably secure in this setting. We moreover formalize and machine-check the proof in the EasyCrypt theorem prover.

In an ongoing discussion comparing the security properties of electronic and paper voting, decreased privacy is often presented as an argument against remote Internet voting. We contribute to this discussion by presenting a side-channel attack against the physical environment of traditional paper-based elections. More precisely, we build a device based on an Arduino development board and cheap electret microphones, capable of triangulating the locations of marks made on wooden tables with high precision. In the best configuration, we are able to determine the correct cell having dimensions 4 × 5 cm with more than 90% accuracy. This will allow breaching privacy of ballot sheet designs that rely on the voter marking her choice(s) between a potentially high number of candidates printed on one large sheet. We complement our attack with a study on various aspects of deployment of facial recognition. This gives rise to the setup where the attacker installs cameras in the polling stations, aiming at automated detection of people leaving the voting booths. Combining the two approaches, we will have a completely automated (and hence relatively well scalable) attack against the privacy of paper-based voting.

We advance the state-of-the-art in automated symbolic analysis of ballot secrecy for e-voting protocols by proposing a method based on analysing three conditions that together imply ballot secrecy. Our approach has two main advantages over existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: our approach can systematically deal with (a) honest authorities present in different phases, (b) threat models in which no dishonest voters occur, and (c) protocols whose ballot secrecy depends on fresh data coming from other phases. The second advantage is that our approach can significantly improve verification efficiency, as the individual conditions are often simpler to verify. E.g., for the LEE protocol, we obtain a speedup of over two orders of magnitude. We show the scope and effectiveness of our approach using ProVerif in several case studies, including the FOO, LEE, JCJ, and Belenios protocols.