IEEE European Symposium on Security and Privacy 2017 (EuroS&P)

WALNUT: Waging Doubt on the Integrity of MEMS Accelerometers with Acoustic Injection Attacks
Timothy Trippel (University of Michigan), Ofir Weisse (University of Michigan), Wenyuan Xu (University of South Carolina), Peter Honeyman (University of Michigan), Kevin Fu (University of Michigan)

Embedded systems depend on sensors to make automated decisions. Resonant acoustic injection attacks are already known to cause malfunctions by disabling MEMS-based gyroscopes. However, an open question remains on how to move beyond denial of service attacks to achieve full adversarial control of sensor outputs. Our work investigates how analog acoustic injection attacks can damage the digital integrity of a popular type of sensor in consumer devices: the capacitive MEMS accelerometer. Spoofing such sensors with intentional acoustic interference enables an out-of-spec pathway for attackers to deliver chosen digital values to microprocessors and embedded systems that blindly trust the unvalidated integrity of sensor outputs. Our contributions include (1) modeling the physics of malicious acoustic interference on MEMS accelerometers, (2) discovering the circuit-level design flaws that cause the vulnerabilities by measuring acoustic injection attacks on MEMS accelerometers as well as systems that depend on the sensors, and (3) two software-only defenses that mitigate many of the risks to the integrity of MEMS accelerometer outputs.

We characterize two classes of acoustic injection attacks: output biasing, and output control. We test these attacks against 20 models of capacitive MEMS accelerometers representing the majority of the consumer market. Our experiments find that 75% are vulnerable to output biasing, and 65% are vulnerable to total output control. To illustrate end-to-end implications, we show how to inject fake steps into a Fitbit with a $5 speaker. In our self-stimulating attack, we play a malicious music file from a smartphone's speaker to control the on-board MEMS accelerometer trusted by a local app to pilot a toy RC car. In addition to offering hardware design fixes to eliminate the root causes of poor amplification and filtering, we introduce two low-cost defenses that mitigate output biasing attacks: randomized sampling and 180° out-of-phase sampling. These software-only approaches mitigate attacks by exploiting the periodic and predictable nature of the malicious acoustic interference signal. Our results call into question the wisdom of allowing microprocessors and embedded systems to blindly trust that hardware abstractions alone will ensure the integrity of sensor outputs.

Compiler-Agnostic Function Detection in Binaries
Dennis Andriesse (Vrije Universiteit Amsterdam), Asia Slowinska (Lastline, Inc.), Herbert Bos (Vrije Universiteit Amsterdam)

We propose Nucleus, a novel function detection algorithm for binaries. In contrast to prior work, Nucleus is compiler-agnostic, and does not require any learning phase or signature information. Instead of scanning for signatures, Nucleus detects functions at the Control Flow Graph-level, making it inherently suitable for difficult cases such as non-contiguous or multi-entry functions. We evaluate Nucleus on a diverse set of 476 C and C++ binaries, compiled with gcc, clang and Visual Studio for x86 and x64, at optimization levels O0–O3. We achieve consistently good performance, with a mean F-score of 0.93.

Open Doors for Bob and Mallory: Open Port Usage in Android Apps and Security Implications
Yunhan Jack Jia (University of Michigan), Qi Alfred Chen (University of Michigan), Yikai Lin (University of Michigan), Chao Kong (University of Michigan), Z. Morley Mao (University of Michigan)

Open ports are typically used by server software to serve remote clients, and the usage historically leads to remote exploitation due to insufficient protection. Smartphone operating systems inherit the open port support, but since they are significant different from traditional server machines in performance and availability guarantees, little is known about how smartphone applications use open ports and what the security implications are. In this paper, we perform the first systematic study of open port usage on mobile platform and their security implications. To achieve this goal, we design and implement OPAnalyzer, a static analysis tool which can effectively identify and characterize vulnerable open port usage in Android applications.

Using OPAnalyzer, we perform extensive usage and vulnerability analysis on a dataset with over 100K Android applications. OPAnalyzer successfully classifies 99% of the mobile usage of open ports into 5 distinct families, and from the output, we are able to identify several mobile-specific usage scenarios such as data sharing in physical proximity. In our subsequent vulnerability analysis, we find that nearly half of the usage is unprotected and can be directly exploited remotely. From the identified vulnerable usage, we discover 410 vulnerable applications with 956 potential exploits in total. We manually confirmed the vulnerabilities for 57 applications, including popular ones with 10 to 50 million downloads on the official market, and also an app that is pre-installed on some device models. These vulnerabilities can be exploited to cause highly-severe damage such as remotely stealing contacts, photos, and even security credentials, and also performing sensitive actions such as malware installation and malicious code execution. We have reported these vulnerabilities and already got acknowledged by the application developers for some of them. We also propose countermeasures and improved practices for each usage scenario.

Privacy-Preserving User Auditable Pseudonym Systems
Jan Camenisch (IBM Research - Zurich), Anja Lehmann (IBM Research - Zurich)

Personal information is often gathered and processed in a decentralized fashion. Examples include health records and governmental data bases. To protect the privacy of individuals, no unique user identifier should be used across the different databases. At the same time, the utility of the distributed information needs to be preserved which requires that it be nevertheless possible to link different records if they relate to the same user. Recently, Camenisch and Lehmann (CCS 15) have proposed a pseudonym scheme that addresses this problem by domain-specific pseudonyms. Although being unlinkable, these pseudonyms can be converted by a central authority (the converter). To protect the users’ privacy, conversions are done blindly without the converter learning the pseudonyms or the identity of the user. Unfortunately, their scheme sacrifices a crucial privacy feature: transparency. Users are no longer able to inquire with the converter and audit the flow of their personal data. Indeed, such auditability appears to be diametral to the goal of blind pseudonym conversion. In this paper we address these seemingly conflicting requirements and provide a system where user-centric audits logs are created by the oblivious converter while maintaining all privacy properties. We prove our protocol to be UC-secure and give an efficient instantiation using novel building blocks.

Auditable Data Structures
Michael Goodrich (University of California - Irvine), Evgenios Kornaropoulos (Brown University), Michael Mitzenmacher (Harvard University), Roberto Tamassia (Brown University)

The classic notion of history-independence guarantees that if a data structure is ever observed, only its current contents are revealed, not the history of operations that built it. This powerful concept has applications, for example, to e-voting and data retention compliance, where data structure histories should be private. The concept of weak history-independence (WHI) assumes only a single observation will ever occur, while strong history-independence (SHI) allows for multiple observations at arbitrary times. WHI constructions tend to be fast, but provide no repeatability, while SHI constructions provide unlimited repeatability, but tend to be slow.

We introduce auditable data structures, where an auditor can observe data structures at arbitrary times (as in SHI), but we relax the unrealistic restriction that data structures cannot react to observations, since in most applications of history-independence, data owners know when observations have occurred. We consider two audit scenarios—secure topology, where an auditor can observe the contents and pointers of a data structure, and secure implementation, where an auditor can observe the memory layout of a data structure. We present a generic template for auditable data structures and, as a foundation for any auditable data structure, an Auditable Memory Manager (AMM), which is an efficient memory manager that translates any auditable data structure with a secure topology into one with a secure implementation. We give a prototype implementation that provides empirical evidence that the worst-case time running times of our AMM are 45× to 8,300× faster than those of a well-known SHI memory manager. Thus, auditable data structures provide a practical way of achieving time efficiency, as in WHI, while allowing for multiple audits, as in SHI.

CodeArmor: Virtualizing the Code Space to Counter Disclosure Attacks
Xi Chen (VU Amsterdam), Cristiano Giuffrida (VU Amsterdam), Herbert Bos (VU Amsterdam)

Code diversification is an effective strategy to prevent modern code-reuse exploits. Unfortunately, diversification techniques are inherently vulnerable to information disclosure. Recent diversification-aware ROP exploits have demonstrated that code disclosure attacks are a realistic threat, with an attacker able to read or execute arbitrary code memory and gather enough gadgets to bypass state-of-the-art code diversification defenses.

In this paper, we present CodeArmor, a binary-level system to harden code diversification against all the existing read-based and execution-based code disclosure attacks. To counter such attacks, CodeArmor virtualizes the code space to completely decouple code pointer values from the concrete location of their targets in the memory address space. Using a combination of run-time randomization and pervasively deployed honey gadgets, code space virtualization probabilistically ensures that only code references that can legitimately be issued by the program are effectively translated to the concrete code space. This strategy significantly reduces the attack surface, limiting the attacker to only code pointer gadgets that can be leaked from data memory. In addition, unlike existing leakage-resistant code diversification techniques that provide similar security guarantees, CodeArmor requires no access to source code, hypervisors, or special hardware support. Our experimental results show that CodeArmor provides a strong line of defense against existing and future attacks, at the cost of only low average performance overhead (6.9% on SPEC and 14.5% on popular server programs, and even lower—roughly halving such average overheads—when operating aggressive inlining optimizations at the binary level).

ARTist: The Android Runtime Instrumentation and Security Toolkit
Michael Backes (CISPA, Saarland University & MPI-SWS), Sven Bugiel (CISPA, Saarland University), Oliver Schranz (CISPA, Saarland University), Philipp von Styp-Rekowsky (CISPA, Saarland University), Sebastian Weisgerber (CISPA, Saarland University)

With the introduction of Android 5 Lollipop, the Android Runtime (ART) superseded the Dalvik Virtual Machine (DVM) by introducing ahead-of-time compilation and native execution of applications, effectively deprecating seminal works such as TaintDroid that hitherto depend on the DVM. In this paper, we discuss alternatives to overcome those restrictions and highlight advantages for the security community that can be derived from ART's novel on-device compiler dex2oat and its accompanying runtime components.

To this end, we introduce ARTist, a compiler-based application instrumentation solution for Android that does not depend on operating system modifications and solely operates on the application layer. Since dex2oat is yet uncharted, our approach required first and foremost a thorough study of the compiler suite's internals and in particular of the new default compiler backend called Optimizing. We document the results of this study in this paper to facilitate independent research on this topic and exemplify the viability of ARTist by realizing two use cases. In particular, we conduct a case study on whether taint tracking can be re-instantiated using a compiler-based app instrumentation framework. Overall, our results provide compelling arguments for the community to choose compiler-based approaches over alternative bytecode or binary rewriting approaches for security solutions on Android.

Designing and proving an EMV-compliant payment protocol for mobile devices
Véronique Cortier (Loria - CNRS), Alicia Filipiak (Loria - Orange), Jan Florent (Orange), Said Gharout (Orange), Jacques Traoré (Orange)

We devise a payment protocol that can be securely used on mobile devices, even infected by malicious applications. Our protocol only requires a light use of Secure Elements, which significantly simplify certification procedures and protocol maintenance. It is also fully compatible with the EMV-SDA protocol and allows off-line payments for the users. We provide a formal model and full security proofs of our protocol using the TAMARIN prover.

Refining Authenticated Key Agreement with Strong Adversaries
David Basin (ETH Zurich), Joseph Lallemand (ENS Cachan, Université Paris-Saclay), Christoph Sprenger (ETH Zurich)

We develop a family of key-agreement protocols that are correct by construction. Our work substantially extends prior work on developing security protocols by refinement. First, we strengthen the adversary by allowing him to compromise different resources of protocol participants, such as their long-term keys or their session keys. This enables the systematic development of protocols that ensure strong properties such as perfect-forward secrecy. Second, we substantially broaden the class of protocols supported to include those with non-atomic keys and equationally defined cryptographic operators. We use these extensions to develop key-agreement protocols including signed Diffie-Hellman and the core of IKEv1 and SKEME.

Sealed-Glass Proofs: Using Transparent Enclaves to Prove and Sell Knowledge
Florian Tramèr (EPFL), Fan Zhang (Cornell), Huang Lin (EPFL), Jean-Pierre Hubaux (EPFL), Ari Juels (Cornell Tech), Elaine Shi (Cornell)

Trusted hardware systems, such as Intel's new SGX instruction set architecture extension, aim to provide strong confidentiality and integrity assurances for applications. Recent work, however, raises serious concerns about the vulnerability of such systems to side-channel attacks.

We propose, formalize, and explore a cryptographic primitive called a Sealed-Glass Proof (SGP) that models computation possible in an isolated execution environment with unbounded leakage, and thus in the face of arbitrary side-channels. A SGP specifically models the capabilities of trusted hardware that can attest to correct execution of a piece of code, but whose execution is transparent, meaning that an application's secrets and state are visible to other processes on the same host.

Despite this strong threat model, we show that SGPs enable a range of practical applications. Our key observation is that SGPs permit safe verifiable computing in zero-knowledge, as data leakage results only in the prover learning her own secrets.
Among other applications, we describe the implementation of an end-to-end bug bounty (or zero-day solicitation) platform that couples a SGX-based SGP with a smart contract. Our platform enables a marketplace that achieves fair exchange, protects against unfair bounty withdrawals, and resists denial-of-service attacks by dishonest sellers. We also consider a slight relaxation of the SGP model that permits black-box modules instantiating minimal, side-channel resistant primitives, yielding a still broader range of applications. Our work shows how trusted hardware systems such as SGX can support trustworthy applications even in the presence of side channels.

FairTest: Discovering Unwarranted Associations in Data-Driven Applications
Florian Tramèr (EPFL), Vaggelis Atlidakis (Columbia University), Roxana Geambasu (Columbia University), Daniel Hsu (Columbia University), Jean-Pierre Hubaux (EPFL), Mathias Humbert (CISPA, Saarland University), Ari Juels (Cornell Tech), Huang Lin (EPFL)

In a world where traditional notions of privacy are increasingly challenged by the myriad companies that collect and analyze our data, it is important that decision-making entities are held accountable for unfair treatments arising from irresponsible data usage. Unfortunately, a lack of appropriate methodologies and tools means that even identifying unfair or discriminatory effects can be a challenge in practice.

We introduce the unwarranted associations (UA) framework, a principled methodology for the discovery of unfair, discriminatory, or offensive user treatment in data-driven applications. The UA framework unifies and rationalizes a number of prior attempts at formalizing algorithmic fairness. It uniquely combines multiple investigative primitives and fairness metrics with broad applicability, granular exploration of unfair treatment in user subgroups, and incorporation of natural notions of utility that may account for observed disparities.

We instantiate the UA framework in FairTest, the first comprehensive tool that helps developers check data-driven applications for unfair user treatment. It enables scalable and statistically rigorous investigation of associations between application outcomes (such as prices or premiums) and sensitive user attributes (such as race or gender). Furthermore, FairTest provides debugging capabilities that let programmers rule out potential confounders for observed unfair effects.

We report on use of FairTest to investigate and in some cases address disparate impact, offensive labeling, and uneven rates of algorithmic error in four data-driven applications. As examples, our results reveal subtle biases against older populations in the distribution of error in a predictive health application and offensive racial labeling in an image tagger.

SoK: Single Sign-On Security – An Evaluation of OpenID Connect
Christian Mainka (Horst Görtz Institute for IT-Security), Vladislav Mladenov (Horst Görtz Institute for IT-Security), Tobias Wich (ecsec GmbH), Jörg Schwenk (Horst Görtz Institute for IT-Security)

OpenID Connect is the OAuth 2.0-based replacement for OpenID and one of the most important Single Sign-On (SSO) protocols used for delegated authentication. It is used by companies like Amazon, Google, Microsoft, and PayPal. In this paper, we systematically analyze well-known attacks on SSO protocols and adapt these on OpenID Connect. In addition, we introduce two novel attacks on OpenID Connect, Identity Provider Confusion and Malicious Endpoints Attack abusing lacks in the current specification and breaking the security goals of the protocol. We communicated these attacks in 2014 with the authors of the OpenID Connect specification and helped to develop a fix (currently an RFC Draft).

We categorize the described attacks in two classes: Single-Phase Attacks abusing a lack of a single security check and Cross-Phase Attacks requiring a complex attack setup and manipulating multiple messages distributed across the whole protocol workflow. In addition, we summarize different approaches to analyze SSO protocols and describe the advantages and disadvantages of each one of them. We provide an evaluation of officially referenced OpenID Connect libraries. 75% of the tested OpenID Connect implementations are vulnerable to at least one Single-Phase Attack. All the libraries are susceptible Cross-Phase Attacks which is not surprising since the attacks abuse a logic flaw in the protocol and not an implementation error.

We reported the found vulnerabilities to the developers and helped them to fix the issues. We address the existing problems in a Practical Offensive Evaluation of Single Sign-On Services (PrOfESSOS). PrOfESSOS is our open source implementation for fully automated Evaluation-as-a-Service for SSO. PrOfESSOS introduces a generic approach to improve the security of OpenID Connect implementations by systematically detecting vulnerabilities. In collaboration with the IETF OAuth and OpenID Connect working group, we integrate PrOfESSOS into the OpenID Connect certification process.

PrOfESSOS is available at https://openid.sso-security.de

9-1-1 DDoS: Attacks, Analysis and Mitigation
Mordechai Guri (Ben-Gurion University of the Negev), Yisroel Mirsky (Ben-Gurion University of the Negev), Yuval Elovici (Ben-Gurion University of the Negev)

The 911 emergency service belongs to one of the 16 critical infrastructure sectors in the United States. Distributed denial of service (DDoS) attacks launched from a mobile phone botnet pose a significant threat to the availability of this vital service.
In this paper we show how attackers can exploit the cellular network protocols in order to launch an anonymized DDoS attack on 911. The current FCC regulations require that all emergency calls be immediately routed regardless of the caller’s identifiers (e.g., IMSI and IMEI). A rootkit placed within the baseband firmware of a mobile phone can mask and randomize all cellular identifiers, causing the device to have no genuine identification within the cellular network. Such anonymized phones can issue repeated emergency calls that cannot be blocked by the network or the emergency call centers, technically or legally. We explore the 911 infrastructure and discuss why it is susceptible to this kind of attack. We then implement different forms of the attack and test our implementation on a small cellular network. Finally, we simulate and analyze anonymous attacks on a model of current 911 infrastructure in order to measure the severity of their impact. We found that with less than 6K bots (or $100K hardware), attackers can block emergency services in an entire state (e.g., North Carolina) for days. We believe that this paper will assist the respective organizations, lawmakers, and security professionals in understanding the scope of this issue in order to prevent possible 911-DDoS attacks in the future.

Outsmarting Network Security with SDN Teleportation
Kashyap Thimmaraju (TU Berlin/T-Labs), Liron Schiff (Tel Aviv University), Stefan Schmid (Aalborg University/TU Berlin)

Software-defined networking is considered a promising new paradigm, enabling more reliable and formally verifiable communication networks. However, this paper shows that the separation of the control plane from the data plane, which lies at the heart of Software-Defined Networks (SDNs), introduces a new vulnerability which we call teleportation. An attacker (e.g., a malicious switch in the data plane or a host connected to the network) can use teleportation to transmit information via the control plane and bypass critical network functions in the data plane (e.g., a firewall), and to violate security policies as well as logical and even physical separations. This paper characterizes the design space for teleportation attacks theoretically, and then identifies four different teleportation techniques. We demonstrate and discuss how these techniques can be exploited for different attacks (e.g., exfiltrating confidential data at high rates), and also initiate the discussion of possible countermeasures. Generally, and given today’s trend toward more intent-based networking, we believe that our findings are relevant beyond the use cases considered in this paper.

LUNA: Quantifying and Leveraging Uncertainty in Android Malware Analysis through Bayesian Machine Learning
Michael Backes (CISPA, Saarland University & MPI-SWS), Mohammad Nauman (MPI-SWS)

Android's growing popularity seems to be hindered only by the amount of malware surfacing for this open platform. Machine learning algorithms have been successfully used for detecting the rapidly growing number of malware families appearing on a daily basis. Existing solutions along these lines, however, have a common limitation: they are all based on classical statistical inference and thus ignore the concept of uncertainty invariably involved in any prediction task. In this paper, we show that ignoring this uncertainty leads to incorrect classification of both benign and malicious apps. To reduce these errors, we utilize Bayesian machine learning – an alternative paradigm based on Bayesian statistical inference – which preserves the concept of uncertainty in all steps of calculation. We move from a black-box to a white-box approach to identify the effects different features (such as sensitive resource usage, declared activities, services and intent filters etc.) have on the classification status of an app. We show that incorporating uncertainty in the learning pipeline helps to reduce incorrect decisions, and significantly improves the accuracy of classification. We achieve a false positive rate of 0.2% compared to the previous best of 1%. We present sufficient details to allow the reader to reproduce our results through openly available probabilistic programming tools and to extend our techniques well beyond the boundaries of this paper.

Confidante: Usable Encrypted Email – A Case Study With Lawyers and Journalists
Adam Lerner (University of Washington), Eric Zeng (University of Washington), Franziska Roesner (University of Washington)

Email encryption tools remain underused, even by people who frequently conduct sensitive business over email, such as lawyers and journalists. Usable encrypted email has remained out of reach largely because key management and verification remain difficult. However, key management has evolved in the age of social media: Keybase is a service that allows users to cryptographically link public keys to their social media accounts (e.g., Twitter), enabling key trust without out-of-band communication. We design and prototype Confidante, an encrypted email client that uses Keybase for automatic key management. We conduct a user study with 15 people (8 U.S. lawyers and 7 U.S. journalists) to evaluate Confidante’s design decisions. We find that users complete an encrypted email task more quickly and with fewer errors using Confidante than with an existing email encryption tool, and that many users report finding Confidante comparable to using ordinary email. However, we also find that lawyers and journalists have diverse operational constraints and threat models, and thus that there may not be a one-size-fits-all solution to usable encrypted email. We reflect on our findings – both specifically about Confidante and more generally about the needs and constraints of lawyers and journalists – to identify lessons and remaining security and usability challenges for encrypted email.

Reasoning about Probabilistic Defense Mechanisms against Remote Attacks
Martín Ochoa (Singapore University of Technology and Design), Sebastian Banescu (Technische Universität München), Cynthia Disenfeld (University of Toronto), Gilles Barthe (IMDEA Software), Vijay Ganesh (University of Waterloo)

Despite numerous countermeasures proposed by practitioners and researchers, remote control-flow alteration of programs with memory-safety vulnerabilities continues to be a realistic threat. Guaranteeing that complex software is completely free of memory-safety vulnerabilities is extremely expensive. Probabilistic countermeasures that depend on random secret keys are interesting, because they are an inexpensive way to raise the bar for attackers who aim to exploit memory-safety vulnerabilities. Moreover, some countermeasures even support legacy systems. However, it is unclear how to quantify and compare the effectiveness of different probabilistic countermeasures or combinations of such countermeasures. In this paper we propose a methodology to rigorously derive security bounds for probabilistic countermeasures. We argue that by representing security notions in this setting as events in probabilistic games, similarly as done with cryptographic security definitions, concrete and asymptotic guarantees can be obtained against realistic attackers. These guarantees shed light on the effectiveness of single countermeasures and their composition and allow practitioners to more precisely gauge the risk of an attack.

Privacy Threats through Ultrasonic Side Channels on Mobile Devices
Daniel Arp (Technische Universität Braunschweig), Erwin Quiring (Technische Universität Braunschweig), Christian Wressnegger (Technische Universität Braunschweig), Konrad Rieck (Technische Universität Braunschweig)

Users are nowadays exposed to a large number of tracking techniques. An emerging technique embeds inaudible beacons in sound and tracks them using the microphone of mobile devices. This side channel allows an adversary to identify a user’s current location, spy on her TV viewing habits or link together different mobile devices. A comprehensive user profile is the result. In this paper, we explore the capabilities, the current prevalence and technical limitations of this new tracking technique based on three commercial tracking solutions. To this end, we develop detection approaches for ultrasonic beacons and Android applications capable of processing these. Our findings confirm our privacy concerns: We spot ultrasonic beacons in various web media content and detect signals in 4 of 35 stores in two European cities that are used for location tracking. While we do not find inaudible beacons in TV streams from 7 countries, we spot 223 Android applications that are constantly listening for ultrasonic beacons in the background without the user’s knowledge.

Efficient and Flexible Discovery of PHP Application Vulnerabilities
Michael Backes (CISPA, Saarland University & MPI-SWS), Konrad Rieck (TU Braunschweig), Malte Skoruppa (CISPA, Saarland University), Ben Stock (CISPA, Saarland University), Fabian Yamaguchi (TU Braunschweig)

The Web today is a growing universe of pages and applications teeming with interactive content. The security of such applications is of the utmost importance, as exploits can have a devastating impact on personal and economic levels. The number one programming language in Web applications is PHP, powering more than 80% of the top ten million websites. Yet it was not designed with security in mind, and, today, bears a patchwork of fixes and inconsistently designed functions with often unexpected and hardly predictable behavior that typically yield a large attack surface. Consequently, it is prone to different types of vulnerabilities, such as SQL Injection or Cross-Site Scripting. In this paper, we present an interprocedural analysis technique for PHP applications based on code property graphs that scales well to large amounts of code and is highly adaptable in its nature. We implement our prototype using the latest features of PHP 7, leverage an efficient graph database to store code property graphs for PHP, and subsequently identify different types of Web application vulnerabilities by means of programmable graph traversals. We show the efficacy and the scalability of our approach by reporting on an analysis of 1,854 popular open-source projects, comprising almost 80 million lines of code.

Secure Queries on an Encrypted Multi-Writer Table
Angelo Massimo Perillo (Università di Salerno, Italy), Giuseppe Persiano (Università di Salerno, Italy), Alberto Trombetta (Università dell'Insubria, Italy)

Performing searches on encrypted data is a very current and active area.Several efficient solutions have been provided for the single-writer scenario in which all sensitive data originates with one party (the Data Owner) that encrypts it and uploads it to a public repository. Subsequently, the Data Owner (or authorized clients, the Query Sources) perform queries on the encrypted data through a Query Processor which has direct access to the public repository.

In this paper,we consider a multi-writer scenario in which data originates with several, not necessarily trusted, parties. The scenario is motivated, among others, by the recent trend in pervasive computing and data collection. In this new scenario the Data Owner provides public parameters for encryption and keeps some related secret information needed to generate tokens to perform queries. We consider the case in which data comes in tabular form (i.e., rows with a fixed number of cells or columns) and we provide support for queries that correspond to a subset of SELECT-FROM-WHERE queries. Current public-key functional encryption schemes provide a straightforward albeit impractical implementation of the scenario of interest. We thus propose a new public-key primitive, Amortized Orthogonality Encryption, derived from Inner-Product Encryption, that can be used to encrypt rows of the table so that ciphertexts have size proportional to the un-encrypted row and encryption and decryption of a row take time proportional to the number of columns. Previous schemes exhibited complexity at least quadratic.

We provide a construction of Amortized Orthogonality Encryption and prove its security under standard assumptions in a bilinear setting with prime order group. Using Amortized Orthogonality Encryption, we implement all the basic operations in our multi-writer scenario in one round of communication.

We demonstrate the feasibility and effectiveness of our proposal by providing an implementation of our scenario in C/C++. As a rough measure of performance, we mention that, for a level of security comparable to AES-128, encryption of a row takes about 3.7 ms per cell and decryption about 1.8 ms per cell. Times have been measured on an Intel Xeon server with a CPU with 2 GHz clock and 32 cores and 128 GB RAM.

Replay Attacks on Zero Round-Trip Time: The Case of the TLS 1.3 Handshake Candidates
Marc Fischlin (Technische Universität Darmstadt, Germany), Felix Günther (Technische Universität Darmstadt, Germany)

We investigate security of key exchange protocols supporting so-called zero round-trip time (0-RTT), enabling a client to establish a fresh provisional key without interaction, based only on cryptographic material obtained in previous connections. This key can then be already used to protect early application data, transmitted to the server before both parties interact further to switch to fully secure keys. Two recent prominent examples supporting such 0-RTT modes are Google's QUIC protocol and the latest drafts for the upcoming TLS version 1.3.

We are especially interested in the question how replay attacks, enabled through the lack of contribution from the server, affect security in the 0-RTT case. Whereas the first proposal of QUIC uses state on the server side to thwart such attacks, the latest version of QUIC and TLS 1.3 rather accept them as inevitable. We analyze what this means for the key secrecy of both the preshared-key-based 0-RTT handshake in the latest draft-14 of TLS 1.3 as well as the Diffie–Hellman-based 0-RTT handshake in TLS 1.3 draft-12. As part of this we extend previous security models to capture such cases, also shedding light on the limitations and options for 0-RTT security under replay attacks.

A Formal Security Analysis of the Signal Messaging Protocol
Katriel Cohn-Gordon (University of Oxford), Cas Cremers (University of Oxford), Benjamin Dowling (Queensland University of Technology), Luke Garratt (University of Oxford), Douglas Stebila (McMaster University)

Signal is a new security protocol that provides end-to-end encryption for instant messaging. It has recently been adopted by WhatsApp, Facebook Messenger and Google Allo among many others; the first two of these have at least 1 billion active users. Signal includes several uncommon security properties (such as "future secrecy"), enabled by a novel technique called *ratcheting* in which session keys are updated with every message sent. Despite its importance and novelty, there has been little to no academic analysis of the Signal protocol, and it is challenging even to find a clear definition of the message flow and protocol algorithms.

We conduct the first security analysis of Signal as a multi-stage key exchange protocol. We extract from the implementation a formal description of the abstract protocol, define a security model which can capture the "ratcheting" key update structure, and prove security of Signal in our model. Our presentation and results can serve as a starting point for other analyses of this widely adopted protocol.

Symbolic Models for Isolated Execution Environments
Charlie Jacomme (ENS Cachan, Université Paris-Saclay), Steve Kremer (LORIA, Inria Nancy & CNRS & Université de Lorraine), Guillaume Scerri (University of Bristol)

Isolated Execution Environments (IEEs), such as ARM TrustZone and Intel SGX, offer the possibility to execute sensitive code in isolation from other malicious programs, running on the same machine, or a potentially corrupted OS. A key feature of IEEs is the ability to produce reports binding cryptographically a message to the program that produced it, typically ensuring that this message is the result of the given program running on an IEE. We present a symbolic model for specifying and verifying applications that make use of such features. For this we introduce the SℓAPiC process calculus, that allows to reason about reports issued at given locations. We also provide tool support, extending the SAPIC/TAMARIN toolchain and demonstrate the applicability of our framework on several examples implementing secure outsourced computation (SOC), a secure licensing protocol and a one-time password protocol that all rely on such IEEs.

Automated Verification for Secure Messaging Protocols and their Implementations: A Symbolic and Computational Approach
Nadim Kobeissi (INRIA Paris), Karthikeyan Bhargavan (INRIA Paris), Bruno Blanchet (INRIA Paris)

An increasing number of popular applications now use end-to-end secure messaging protocols, the most popular being the Signal Protocol which now operates on more than a billion devices. However, these implementations exist in environments where bugs and protocol flaws lead to attacks on a variety of real-world applications. We advocate the use of automated verification tools to systematically find and eliminate such attacks. We focus on Signal Protocol and provide automated symbolic verification from source code and novel semi-automated proofs in the computational model using CryptoVerif. We find new and previously-known attacks on this protocol and suggest practical countermeasures.

To provide automatic verification of source code, we designed ProScript, a protocol programming and verification framework based on a typed subset of JavaScript. The ProScript compiler extracts formal models in the applied pi calculus directly from protocol code in JavaScript. These models are human-readable and can be seen as reference specifications for protocols that were previously only specified in code. Furthermore, they can be automatically verified for desired security properties against sophisticated threat models using the ProVerif protocol analyzer. We prove our framework's viability by releasing the first secure messenger with a formally verified protocol core, for the general public, with an isolated and formally verified Signal Protocol implementation in ProScript. Our results indicate that, with a little programming discipline, the automated security verification of complex real-world web-based cryptographic protocol implementations is now practical.

Revisiting Browser Security in the Modern Era: New Data-only Attacks and Defenses
Roman Rogowski (University of North Carolina at Chapel Hill), Micah Morton (University of North Carolina at Chapel Hill), Forrest Li (University of North Carolina at Chapel Hill), Kevin Z. Snow (University of North Carolina at Chapel Hill), Fabian Monrose (University of North Carolina at Chapel Hill), Michalis Polychronakis (Stony Brook University)

The continuous discovery of exploitable vulnerabilities in popular applications (e.g., web browsers and document viewers), along with their heightening protections against control flow hijacking, has opened the door to an often neglected attack strategy—namely, data-only attacks. In this paper, we demonstrate the practicality of the threat posed by data-only attacks that harness the power of memory disclosure vulnerabilities. To do so, we introduce memory cartography, a technique that simplifies the construction of data-only attacks in a reliable manner. Specifically, we show how an adversary can use a provided memory mapping primitive to navigate through process memory at runtime, and safely reach security-critical data that can then be modified at will. We demonstrate this capability by using our cross-platform memory cartography framework implementation to construct data-only exploits against Internet Explorer and Chrome. The outcome of these exploits ranges from simple HTTP cookie leakage, to the alteration of the same origin policy for targeted domains, which enables the cross-origin execution of arbitrary script code.

The ease with which we can undermine the security of modern browsers stems from the fact that although isolation policies (such as the same origin policy) are enforced at the script level, these policies are not well reflected in the underlying sandbox process models used for compartmentalization. This gap exists because the complex demands of today’s web functionality make the goal of enforcing the same origin policy through process isolation a difficult one to realize in practice, especially when backward compatibility is a priority (e.g., for support of cross-origin iframes). While fixing the underlying problems likely requires a major refactoring of the security architecture of modern browsers (in the long term), we explore several defenses, including global variable randomization, that can limit the power of the attacks presented herein.

Block Me If You Can: A Large-Scale Study of Tracker-Blocking Tools
Georg Merzdovnik (SBA Research), Markus Huber (Fachhochschule St. Pölten), Damjan Buhov (SBA Research), Nick Nikiforakis (Stony Brook University), Sebastian Neuner (SBA Research), Martin Schmiedecker (SBA Research), Edgar Weippl (SBA Research)

Online third-party tracking has become a widespread practice on the Internet, with serious implications for the privacy of users. While users are often unaware that their online behaviour is being monitored by omnipresent third-party trackers, trackers continuously expand their coverage and the methods by which they ensure the longevity of their tracking identifiers. In this paper, we quantify the effectiveness of third-party tracker blockers on a large scale. First, we analyze the architecture of various, state-of-the-art blocking solutions and discuss the advantages and disadvantages of each method. Second, we perform a two-part measurement study on the effectiveness of popular tracker-blocking tools. Our analysis quantifies the protection offered against trackers present on more than 100,000 popular websites and 10,000 popular Android applications. We provide novel insights into the ongoing arms race between trackers and developers of blocking tools, and which tools, under what circumstances, achieve the best results. Among others, we discover that rule-based browser extensions outperform learning-based ones, trackers with smaller footprints are more successful at avoiding being blocked, and CDNs pose a major threat towards the future of tracker-blocking tools. Overall, the contributions of this paper advance the field of web privacy by providing not only the largest, to date, study on the effectiveness of tracker-blocking tools, but also highlighting the most pressing challenges and privacy issues of third-party tracking.

A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange
Michael Backes (CISPA, Saarland University & MPI-SWS), Jannik Dreier (INRIA), Steve Kremer (INRIA), Robert Kuennemann (CISPA, Saarland University)

In this paper, we provide the first methodology for reasoning about liveness properties of cryptographic protocols in a machine-assisted manner without imposing any artificial, finite bounds on the protocols and execution models. To this end, we design an extension of the SAPiC process calculus so that it supports key concepts for stating and reasoning about liveness properties, along with a corresponding translation into the formalism of multiset rewriting that the state-of-the-art theorem prover Tamarin relies upon. We prove that this translation is sound and complete and can thereby automatically generate sound Tamarin specifications and automate the protocol analysis.

Second, we applied our methodology to two widely investigated fair exchange protocols – ASW and GJM – and to the Secure Conversation Protocol standard for industrial control systems, deployed by major players such as Siemens, SAP and ABB. For the fair exchange protocols, we not only re-discovered known attacks, but also uncovered novel attacks that previous analyses based on finite models and restricted number of sessions did not detect. We suggest fixed versions of these protocols for which we prove both fairness and timeliness, yielding the first automated proofs for fair exchange protocols that rely on a general model without restricting the number of sessions and message size. For the Secure Conversation Protocol, we prove several strong security properties that are vital for the safety of industrial systems, in particular that all messages (e.g., commands) are eventually delivered in order.

Content delivery over TLS: a cryptographic analysis of Keyless SSL
Karthikeyan Bhargavan (Inria de Paris), Ioana Boureanu Carlson (Imperial College London), Pierre-Alain Fouque (Université de Rennes 1/IRISA), Cristina Onete (INSA/IRISA Rennes), Benjamin Richard (Orange/ IRISA Rennes)

The Transport Layer Security (TLS) protocol is designed to allow two parties, a client and a server, to communicate securely over an insecure network. However, when TLS connections are proxied through an intermediate middlebox, like a Content Delivery Network (CDN), the standard endtoend security guarantees of the protocol no longer apply. In this paper, we investigate the security guarantees provided by Keyless SSL, a CDN architecture currently deployed by CloudFlare that composes two TLS 1.2 handshakes to obtain a proxied TLS connection. We demonstrate new attacks that show that Keyless SSL does not meet its intended security goals. These attacks have been reported to CloudFlare and we are in the process of discussing fixes. We argue that proxied TLS handshakes require a new, stronger, 3-party security definition. We present 3(S)ACCE-security, a generalization of the commonly-used 2-party security definition, called ACCE, used in previous proofs for TLS. We modify Keyless SSL and prove that our modifications guarantee 3(S)ACCE-security, assuming 2-ACCE-security for the individual TLS 1.2 connections. We also propose a new design for Keyless TLS 1.3 and prove that it achieves 3(S)ACCE-security, assuming standard 2-party security for TLS 1.3. A notable result is that secure proxying for TLS 1.3 is significantly easier than TLS 1.2; our proposed Keyless TLS 1.3 is computationally lighter and uses simpler assumptions on the certificate infrastructure than our proposed fix for Keyless SSL. Our attacks and proofs indicate that new proxied TLS architectures, as currently used by a number of CDNs, are vulnerable to subtle attacks and deserve close attention.

Efficient Accumulators with Applications to Anonymity-Preserving Revocation
Foteini Baldimtsi (Boston University), Jan Camenisch (IBM Zurich), Maria Dubovitskaya (IBM Zurich), Anna Lysyanskaya (Brown University), Leo Reyzin (Boston University), Kai Samelin (IBM Zurich), Sophia Yakoubov (Boston University)

Membership revocation is essential for cryptographic applications, from traditional PKIs to group signatures and anonymous credentials. Of the various solutions for the revocation problem that have been proposed, dynamic accumulators are one of the most promising. In this work we propose Braavos, a new, RSA-based, accumulator. It has optimal communication complexity and, when combined with efficient zero-knowledge proofs, provides an ideal solution for the anonymous revocation scenario. For the construction of Braavos we use a modular approach: we show how to build an accumulator with better functionality and security from accummulators with fewer features and weaker security guarantees. In the second part of the paper, we describe an anonymous revocation component (ARC) that can be instantiated using any dynamic accumulator. ARC can be added to any anonymous system, such as anonymous credentials or group signatures, in order to equip it with a revocation functionality. Finally, we implement ARC with Braavos and plug it into the leading implementation of anonymous credentials (IDEMIX). Coupled with implementations results, this work resolves, for the first time, the problem of practical revocation for anonymous credential systems.

Redactable Blockchain - or - Rewriting History in Bitcoin and Friends
Giuseppe Ateniese (Stevens Institute of Technology), Bernardo Magri (Sapienza University of Rome), Daniele Venturi (University of Trento), Ewerton Andrade (University of São Paulo)

We put forward a new framework that makes it possible to re-write and/or compress the content of any number of blocks in ecentralized services exploiting the blockchain technology. As we argue, there are several reasons to prefer an editable blockchain, spanning from the necessity to remove improper content and the possibility to support applications requiring re-writable storage, to "the right to be forgotten".

Our approach generically leverages so-called chameleon hash functions (Krawczyk and Rabin, NDSS '00), which allow to efficiently determine hash collisions given a secret trapdoor information. We detail how to integrate a chameleon hash function in virtually any blockchain-based technology, for both cases where the power of redacting the blockchain content is in the hands of a single trusted entity and where such a capability is distributed among several distrustful parties (as is the case in Bitcoin).

We also report on a proof-of-concept implementation of a redactable blockchain, building on top of Nakamoto's Bitcoin core. The implementation only requires minimal changes to the way current client software interprets information stored in the blockchain and to the current blockchain, block, or transaction structures. Moreover, our experiments show that the overhead imposed by a redactable blockchain is small compared to the case of an immutable one.

Reputation Metrics Design to Improve Intermediary Incentives for Security of TLDs
Maciej Korczynski (Delft University of Technology), Samaneh Tajalizadehkhoob (Delft University of Technology), Arman Noroozian (Delft University of Technology), Maarten Wullink (SIDN Labs), Cristian Hesselman (SIDN Labs), Michel van Eeten (Delft University of Technology)

Over the years cybercriminals have misused the Domain Name System (DNS) – a critical component of the Internet – to gain profit. Despite this persisting trend, little empirical information about the security performance of Top-Level Domains (TLDs) and of the overall ‘health’ of the DNS ecosystem exists currently. In this paper, we present security metrics for this ecosystem and measure the operational values of such metrics using three representative phishing and malware datasets. We benchmark entire TLDs against their market. However, we explicitly distinguish the metrics from the idea of measuring security performance because the measured values are driven by multiple factors, not just by the performance of the particular market player. We consider two types of security metrics: occurrence of abuse and persistence of abuse that in conjunction provide a better understanding of the overall health of a TLD. We demonstrate that attackers abuse a variety of free services with good reputation, affecting the reputation of associated services and entire TLDs. We find that old TLDs like .com host more bad content than new generic TLDs, when normalized by size. Moreover, we propose a statistical regression model to analyze how the different properties of TLD intermediaries relate to abuse counts. We find that next to TLD size, abuse is positively associated with domain pricing (i.e. registries who provide free domain registrations witness more abuse) and strict registration policies. Last but not least, we observe a negative significant relation between the DNSSEC deployment rate and the count of phishing domains.

When Cellular Networks Met IPv6: Security Problems of Middleboxes in IPv6 Cellular Networks
Hyunwook Hong (KAIST), Hyunwoo Choi (KAIST), Dongkwan Kim (KAIST), Hongil Kim (KAIST), Byeongdo Hong (KAIST), Jiseong Noh (KAIST), Yongdae Kim (KAIST)

Recently, cellular operators have started migrating to IPv6 in response to the increasing demand for IP addresses. With the introduction of IPv6, cellular middleboxes, such as firewalls for preventing malicious traffic from the Internet and NAT64 boxes for providing backward compatibility with legacy IPv4 services, have become crucial to maintain stability of cellular networks. This paper presents security problems of the currently deployed IPv6 middleboxes of five major operators. To this end, we first investigate several key features of the current IPv6 deployment that can harm the safety of a cellular network as well as its customers. These features combined with the currently deployed IPv6 middlebox allow an adversary to launch six different attacks. First, firewalls in IPv6 cellular networks fail to block incoming packets properly. Thus, an adversary could fingerprint cellular devices with scanning, and further, she could launch denial-of-service or over-billing attacks. Second, vulnerabilities in the NAT64 box, a middlebox that maps an IPv6 address to an IPv4 address (and vice versa), allow an adversary to launch three different attacks: 1) NAT overflow attack that allows an adversary to overflow the NAT resources, 2) NAT wiping attack that removes active NAT mappings by exploiting the lack of TCP sequence number verification of firewalls, and 3) NAT bricking attack that targets services adopting IP-based blacklisting by preventing the shared external IPv4 address from accessing the service. We confirmed the feasibility of these attacks with an empirical analysis. We also propose effective countermeasures for each attack.

Towards Practical Attacks on Argon2i and Balloon Hashing
Joel Alwen (IST Austria), Jeremiah Blocki (Purdue University)

The algorithm Argon2i-B of Biryukov, Dinu and Khovratovich is currently being considered by the IRTF (Internet Research Task Force) as a new de-facto standard for password hashing. An older version (Argon2i-A) of the same algorithm was chosen as the winner of the recent Password Hashing Competition. An important competitor to Argon2i-B is the recently introduced Balloon Hashing (BH) algorithm of Corrigan-Gibs, Boneh and Schechter.

A key security desiderata for any such algorithm is that evaluating it (even using a custom device) requires a large amount of memory amortized across multiple instances. Alwen and Blocki (CRYPTO 2016) introduced a class of theoretical attacks against Argon2i-A and BH. While these attacks yield large asymptotic reductions in the amount of memory, it was not, a priori, clear if (1) they can be extended to the newer Argon2i-B, (2) the attacks are effective on any algorithm for practical parameter ranges (e.g., 1GB of memory) and (3) if they can be effectively instantiated against any algorithm under realistic hardware constrains.

In this work we answer all three of these questions to the affirmative for all three algorithms. It is also the first work to analyze the security of Argon2i-B. In more detail, we extend the theoretical attacks of Alwen and Blocki (CRYPTO 2016) to the recent Argon2i-B proposal demonstrating severe asymptotic deficiencies in its security. Next we introduce several novel heuristics for improving the attack's concrete memory efficiency even when on-chip memory bandwidth is bounded. We then simulate our attacks on randomly sampled Argon2i-A, Argon2i-B and BH instances and measure the resulting memory consumption for various practical parameter ranges and for a variety of upperbounds on the amount of parallelism available to the attacker. Finally we describe, implement and test a new heuristic for applying the Alwen-Blocki attack to functions employing a technique developed by Corrigan-Gibs et al. for improving concrete security of memory-hard functions.

We analyze the collected data and show the effects various parameters have on the memory consumption of the attack. In particular, we can draw several interesting conclusions about the level of security provided by these functions.

For the Alwen-Blocki attack to fail against practical memory parameters, Argon2i-B must be instantiated with more than 10 passes on memory. The current IRTF proposal calls even just 6 passes as the recommended "paranoid" setting.
More generally, the parameter selection process in the proposal is flawed in that it tends towards producing parameters for which the attack is successful (even under realistic constraints on parallelism).
The technique of Corrigan-Gibs for improving security can also be overcome by the Alwen-Blocki attack under realistic hardware constraints.
On a positive note, both the asymptotic and concrete security of Argon2i-B seem to improve on that of Argon2i-A.

SoK: Fraud in Telephony Networks
Merve Sahin (Eurecom), Aurélien Francillon (Eurecom), Payas Gupta (New York University Abu Dhabi), Mustaque Ahamad (Georgia Institute of Technology)

Telephone networks first appeared more than a hundred years ago, long before transistors were invented. They, therefore, form the oldest large scale network that has grown to touch over 7 billion people. Telephony is now merging many complex technologies and because numerous services enabled by these technologies can be monetized, telephony attracts a lot of fraud. In 2015, a telecom fraud association study estimated that the loss of revenue due to global telecom fraud was worth 38 billion US dollars per year. Because of the convergence of telephony with the Internet, fraud in telephony networks can also have a negative impact on security of online services. However, there is little academic work on this topic, in part because of the complexity of such networks and their closed nature. This paper aims to systematically explore fraud in telephony networks. Our taxonomy differentiates the root causes, the vulnerabilities, the exploitation techniques, the fraud types and finally the way fraud benefits to the fraudsters. We present an overview of each of these and use CAller NAMe (CNAM) revenue share fraud as a concrete example to illustrate how our taxonomy helps in better understanding the fraud and to mitigate it by understanding the consequences of some actions that can be taken.

An Expressive (Zero-Knowledge) Set Accumulator
Jonathan Katz (University of Maryland), Charalampos Papamanthou (University of Maryland), Yupeng Zhang (University of Maryland)

We present a new construction of an expressive set accumulator. Unlike existing cryptographic accumulators, ours provides succinct proofs for a large collection of operations over accumulated sets, including intersection, union, set difference,SUM, COUNT, MIN, MAX, and RANGE, as well as arbitrary nestings of the above. We also show how to extend our accumulator to be zero-knowledge. The security of our accumulator is based on extractability assumptions and other assumptions that hold in the generic group model.

Our construction achieves asymptotically optimal verification complexity and proof size, constant update complexity, and public verifiability/updatability - namely, any client with access to the public key and the last accumulator value can verify the supported operations and update the accumulator. The enhanced expressiveness of our accumulator comes at the cost of quadratic prover time. However, we show that the cryptographic operations involved are cheap compared to those incurred by generic approaches (e.g., SNARKs) that are equally expressive: our prover runs faster for sets of up to 5 million items.

Our accumulator serves as a powerful cryptographic tool with many applications. For example, it can be applied to efficiently support verification of a rich collection of SQL queries when used as a drop-in replacement in existing verifiable database systems (e.g., IntegriDB, CCS 2015).

Internet Censorship in Thailand: User practices, potential threats and necessary responses
Genevieve Gebhart (University of Washington Information School), Tadayoshi Kohno (University of Washington Computer Science & Engineering), Anonymous

The "cat-and-mouse" game of Internet censorship and circumvention cannot be won by capable technology alone. Instead, that technology must be available, comprehensible, and trustworthy to users. However, the field largely focuses only on censors and the technical means to circumvent them. Thailand, with its superlatives in Internet use and government information controls, offers a rich case study for exploring users' assessments of and interactions with censorship. We survey 229 and interview 13 regular Internet users in Thailand, and report on their current practices, experienced and perceived threats, and unresolved problems regarding censorship and digital security. Our findings indicate that existing circumvention tools were adequate for respondents to access blocked information; that respondents relied to some extent on risky tool selection and inaccurate assessment of blocked content; and that attempts to take action with sensitive content on social media led to the most concrete threats with the least available technical defenses. Based on these findings and in direct response to these problems, we make recommendations for shifting objectives in anti-censorship work, as well as for technical directions and future research to address users' on-the-ground needs.

On the Effectiveness of Virtualization Based Memory Isolation on Multicore Platforms
Siqi Zhao (Singapore Management University), Xuhua Ding (Singapore Management University)

Virtualization based memory isolation has been widely used as a security primitive in many security systems. This paper is the first in the literature that provides an in-depth analysis of its effectiveness in the multicore setting. Our study reveals that memory isolation by itself is inadequate for security. Due to the fundamental design defect, it faces several challenging issues including page table maintenance, address mapping validation and thread identification. As demonstrated by our attacks implemented on XMHF and BitVisor, these issues undermine the security of memory isolation. We propose a new isolation approach that is immune to the aforementioned problems. In our design, the hypervisor constructs a fully isolated micro computing environment (FIMCE) that exposes a minimal attack surface to an untrusted OS on a multicore platform. By virtue of its architectural niche, FIMCE offers stronger assurance and greater versatility than memory isolation. We have built a prototype of FIMCE and measured its performance. To show the benefits of using FIMCE as a building block, we have also implemented several practical applications which cannot be securely realized by using memory isolation alone.

Large-scale Analysis & Detection of Authentication Cross-Site Request Forgeries
Avinash Sudhodanan (Fondazione Bruno Kessler), Nicolas Dolgin (SAP Labs France), Roberto Carbone (Fondazione Bruno Kessler), Umberto Morelli (Fondazione Bruno Kessler), Luca Compagna (SAP Labs France), Alessandro Armando (Fondazione Bruno Kessler)

Cross-Site Request Forgery (CSRF) attacks are one of the critical threats for web applications. In this paper we focus on Auth-CSRF attacks, i.e. CSRF attacks on web sites’ authentication and identity management functionalities. We collect several Auth-CSRF attacks reported in literature, analyze the strategies underlying them and identify seven testing strategies that can help a manual tester uncover a large majority of Auth-CSRF attacks. In order to check the effectiveness of our testing strategies and to estimate the incidence of Auth-CSRF, we run a large-scale experimental analysis considering 300 Alexa global top web sites belonging to three different rank ranges. The results of our experimental analysis are alarming. Out of the 300 web sites we considered, 133 qualified for conducting our experiments and 93 of these suffered from at least one vulnerability enabling Auth-CSRF attacks (i.e. 70%). We further generalize our testing strategies, enhance them with the knowledge we acquired during our experiments and implement them as an extension (namely CSRF-checker) to the open-source penetration testing tool OWASP ZAP. In the end we conduct further experiments with CSRF-checker and not only identify more Auth-CSRF attacks but also save up to 60.9% time with respect to our experiments without CSRF-checker. Our findings include serious vulnerabilities in prominent web sites such as Google, eBay etc.

Accepted Papers