S&P 2013

All Your IFCException Are Belong To Us

Existing designs for fine-grained, dynamic information-flow control assume that it is acceptable to terminate the entire system when an incorrect flow is detected – i.e, they give up availability for the sake of confidentiality and integrity. This is an unrealistic limitation for systems such as long-running servers. We identify public labels and delayed exceptions as crucial ingredients for making information-flow errors recoverable in a sound and usable language, and we propose two new error-handling mechanisms that make all errors recoverable. The first mechanism builds directly on these basic ingredients, using not-a-values (NaVs) and data flow to propagate errors. The second mechanism adapts the standard exception model to satisfy the extra constraints arising from information flow control, converting thrown exceptions to delayed ones at certain points. We prove that both mechanisms enjoy the fundamental soundness property of non-interference. Finally, we describe a prototype implementation of a full-scale language with NaVs and report on our experience building robust software components in this setting.

Catalin Hritcu (University of Pennsylvania), Michael Greenberg (University of Pennsylvania), Ben Karel (University of Pennsylvania), Benjamin C. Pierce (University of Pennsylvania), and Greg Morrisett (Harvard University)

Declarative, Temporal, and Practical Programming with Capabilities

New operating systems, such as the Capsicum capability system, allow a programmer to write an application that satisfies strong security properties by invoking security- specific system calls at a few key points in the program. However, rewriting an application to invoke such system calls correctly is an error-prone process: even the Capsicum developers have reported difficulties in rewriting programs to correctly invoke system calls. This paper describes capweave, a tool that takes as input (i) an LLVM program, and (ii) a declarative policy of the possibly-changing capabilities that a program must hold during its execution, and rewrites the program to use Capsicum system calls to enforce the policy. Our experiments demonstrate that capweave can be applied to rewrite security-critical UNIX utilities to satisfy practical security policies. capweave itself works quickly, and the runtime overhead incurred in the programs that capweave produces is generally low for practical workloads.

William R. Harris (University of Wisconsin, Madison), Somesh Jha (University of Wisconsin, Madison), Thomas Reps (University of Wisconsin, Madison), Jonathan Anderson (University of Cambridge), and Robert N. M. Watson (University of Cambridge)

Towards Practical Reactive Security Audit Using Extended Static Checkers

This paper describes our experience of performing reactive security audit of known security vulnerabilities in core operating system and browser COM components, using an extended static checker HAVOCLITE. We describe the extensions made to the tool to be applicable on such large C++ components, along with our experience of using an extended static checker in the large. We argue that the use of such checkers as a configurable static analysis in the hands of security auditors can be an effective tool for finding variations of known vulnerabilities. The effort has led to finding and fixing around 70 previously unknown security vulnerabilities in over 10 millions lines operating system and browser code.

Julien Vanegue (Bloomberg LP) and Shuvendu K. Lahiri (Microsoft Research)

SoK: Eternal War in Memory

Memory corruption bugs in software written in low-level languages like C or C++ are one of the oldest problems in computer security. The lack of safety in these languages allows attackers to alter the program’s behavior or take full control over it by hijacking its control flow. This problem has existed for more than 30 years and a vast number of potential solutions have been proposed, yet memory corruption attacks continue to pose a serious threat. Real world exploits show that all currently deployed protections can be defeated. This paper sheds light on the primary reasons for this by describing attacks that succeed on today’s systems. We systematize the current knowledge about various protection techniques by setting up a general model for memory corruption attacks. Using this model we show what policies can stop which attacks. The model identifies weaknesses of currently deployed techniques, as well as other proposed protections enforcing stricter policies. We analyze the reasons why protection mechanisms implementing stricter polices are not deployed. To achieve wide adoption, protection mechanisms must support a multitude of features and must satisfy a host of requirements. Especially important is performance, as experience shows that only solutions whose overhead is in reasonable bounds get deployed. A comparison of different enforceable policies helps designers of new protection mechanisms in finding the balance between effectiveness (security) and efficiency. We identify some open research problems, and provide suggestions on improving the adoption of newer techniques.

Laszlo Szekeres (Stony Brook University and UC Berkeley), Mathias Payer (UC Berkeley), Tao Wei (UC Berkeley and Peking University), and Dawn Song (UC Berkeley)

The Parrot is Dead: Observing Unobservable Network Communications

In response to the growing popularity of Tor and other censorship circumvention systems, censors in non-democratic countries have increased their technical capabilities and can now recognize and block network traffic generated by these systems on a nationwide scale. New censorship-resistant communication systems such as Skype Morph, Stego Torus, and Censor Spoofer aim to evade censors’ observations by imitating common protocols like Skype and HTTP. We demonstrate that these systems completely fail to achieve unobservability. Even a very weak, local censor can easily distinguish their traffic from the imitated protocols. We show dozens of passive and active methods that recognize even a single imitated session, without any need to correlate multiple network flows or perform sophisticated traffic analysis. We enumerate the requirements that a censorship-resistant system must satisfy to successfully mimic another protocol and conclude that “unobservability by imitation” is a fundamentally flawed approach. We then present our recommendations for the design of unobservable communication systems.

Amir Houmansadr (The University of Texas at Austin), Chad Brubaker (The University of Texas at Austin), and Vitaly Shmatikov (The University of Texas at Austin)

Trawling for Tor Hidden Services: Detection, Measurement, Deanonymization

Tor is the most popular volunteer-based anonymity network consisting of over 3000 volunteer-operated relays. Apart from making connections to servers hard to trace to their origin it can also provide receiver privacy for Internet services through a feature called “hidden services”. In this paper we expose flaws both in the design and implementation of Tor’s hidden services that allow an attacker to measure the popularity of arbitrary hidden services, take down hidden services and deanonymize hidden services. We give a practical evaluation of our techniques by studying: (1) a recent case of a botnet using Tor hidden services for command and control channels; (2) Silk Road, a hidden service used to sell drugs and other contraband; (3) the hidden service of the DuckDuckGo search engine.

Alex Biryukov (University of Luxembourg), Ivan Pustogarov (University of Luxembourg), and RalfPhilipp Weinmann (University of Luxembourg)

SoK: P2PWNED Modeling and Evaluating the Resilience of Peer-to-Peer Botnets

Centralized botnets are easy targets for takedown efforts by computer security researchers and law enforcement. Thus, botnet controllers have sought new ways to harden the infrastructures of their botnets. In order to meet this objective, some botnet operators have (re)designed their botnets to use Peer-to-Peer (P2P) infrastructures. Many P2P botnets are far more resilient to takedown attempts than centralized botnets, because they have no single points of failure. However, P2P botnets are subject to unique classes of attacks, such as node enumeration and poisoning. In this paper, we introduce a formal graph model to capture the intrinsic properties and fundamental vulnerabilities of P2P botnets. We apply our model to current P2P botnets to assess their resilience against attacks. We provide assessments on the sizes of all eleven active P2P botnets, showing that some P2P botnet families contain over a million bots. In addition, we have prototyped several mitigation strategies to measure the resilience of existing P2P botnets. We believe that the results from our analysis can be used to assist security researchers in evaluating mitigation strategies against current and future P2P botnets.

Christian Rossow (Institute for Internet Security), Dennis Andriesse (VU University Amsterdam), Tillmann Werner (The Honeynet Project), Brett StoneGross (Dell SecureWorks), Daniel Plohmann (Fraunhofer FKIE), Christian J. Dietrich (Institute for Internet Security), and Herbert Bos (VU University Amsterdam)

Finding the Linchpins of the Dark Web: a Study on Topologically Dedicated Hosts on Malicious Web Infrastructures

Malicious Web activities continue to be a major threat to the safety of online Web users. Despite the plethora forms of attacks and the diversity of their delivery channels, in the back end, they are all orchestrated through malicious Web infrastructures, which enable miscreants to do business with each other and utilize others’ resources. Identifying the linchpins of the dark infrastructures and distinguishing those valuable to the adversaries from those disposable are critical for gaining an upper hand in the battle against them. In this paper, using nearly 4 million malicious URL paths crawled from different attack channels, we perform a large-scale study on the topological relations among hosts in the malicious Web infrastructure. Our study reveals the existence of a set of topologically dedicated malicious hosts that play orchestrating roles in malicious activities. They are well connected to other malicious hosts and do not receive traffic from legitimate sites. Motivated by their distinctive features in topology, we develop a graph-based approach that relies on a small set of known malicious hosts as seeds to detect dedicate malicious hosts in a large scale. Our method is general across the use of different types of seed data, and results in an expansion rate of over 12 times in detection with a low false detection rate of 2%. Many of the detected hosts operate as redirectors, in particular Traffic Distribution Systems (TDSes) that are long-lived and receive traffic from new attack campaigns over time. These TDSes play critical roles in managing malicious traffic flows. Detecting and taking down these dedicated malicious hosts can therefore have more impact on the malicious Web infrastructures than aiming at short-lived doorways or exploit sites.

Zhou Li (Indiana University at Bloomington), Sumayah Alrwais (Indiana University at Bloomington), Yinglian Xie (Microsoft Research), Fang Yu (Microsoft Research), and XiaoFeng Wang (Indiana University at Bloomington)

The Crossfire Attack

We present the Crossfire attack–a powerful attack that degrades and often cuts off network connections to a variety of selected server targets (e.g., servers of an enterprise, a city, a state, or a small country) by flooding only a few network links. In Crossfire, a small set of bots directs low intensity flows to a large number of publicly accessible servers. The concentration of these flows on the small set of carefully chosen links floods these links and effectively disconnects selected target servers from the Internet. The sources of the Crossfire attack are undetectable by any targeted servers, since they no longer receive any messages, and by network routers, since they receive only low- intensity, individual flows that are indistinguishable from legitimate flows. The attack persistence can be extended virtually indefinitely by changing the set of bots, publicly accessible servers, and target links while maintaining the same disconnection targets. We demonstrate the attack feasibility using Internet experiments, show its effects on a variety of chosen targets (e.g., servers of universities, US states, East and West Coasts of the US), and explore several countermeasures.

Min Suk Kang (Carnegie Mellon University), Soo Bum Lee (Carnegie Mellon University), and Virgil D. Gligor (Carnegie Mellon University)

Ghost Talk: Mitigating EMI Signal Injection Attacks against Analog Sensors

Electromagnetic interference (EMI) affects circuits by inducing voltages on conductors. Analog sensing of signals on the order of a few millivolts is particularly sensitive to interference. This work (1) measures the susceptibility of analog sensor systems to signal injection attacks by intentional, low-power emission of chosen electromagnetic waveforms, and (2) proposes defense mechanisms to reduce the risks. Our experiments use specially crafted EMI at varying power and distance to measure susceptibility of sensors in implantable medical devices and consumer electronics. Results show that at distances of 1 – 2m, consumer electronic devices containing microphones are vulnerable to the injection of bogus audio signals. Our measurements show that in free air, intentional EMI under 10 W can inhibit pacing and induce defibrillation shocks at distances up to 1 – 2m on implantable cardiac electronic devices. However, with the sensing leads and medical devices immersed in a saline bath to better approximate the human body, the same experiment decreases to about 5 cm. Our defenses range from prevention with simple analog shielding to detection with a signal contamination metric based on the root mean square of waveform amplitudes. Our contribution to securing cardiac devices includes a novel defense mechanism that probes for forged pacing pulses inconsistent with the refractory period of cardiac tissue.

Denis Foo Kune (University of Michigan), John Backes (University of Minnesota), Shane Clark (University of Massachusetts Amherst), Dan Kramer, MD (Beth Israel Deaconess Medical Center), Matthew Reynolds, MD (Harvard Clinical Research Institute), Kevin Fu (University of Michigan), Yongdae Kim (KAIST), Wenyuan Xu (University of South Carolina)

On Limitations of Friendly Jamming for Confidentiality

Wireless communication provides unique security challenges, but also enables novel ways to defend against attacks. In the past few years, a number of works discussed the use of friendly jamming to protect the confidentiality of the communicated data as well as to enable message authentication and access control. In this work, we analytically and experimentally evaluate the confidentiality that can be achieved by the use of friendly jamming, given an attacker with multiple receiving antennas. We construct a MIMO-based attack that allows the attacker to recover data protected by friendly jamming and refine the conditions for which this attack is most effective. Our attack shows that friendly jamming cannot provide strong confidentiality guarantees in all settings. We further test our attack in a setting where friendly jamming is used to protect the communication to medical implants.

Nils Ole Tippenhauer (ETH Zurich), Luka Malisa (ETH Zurich), Aanjhan Ranganathan (ETH Zurich), and Srdjan Capkun (ETH Zurich)

Ally Friendly Jamming: How to Jam Your Enemy and Maintain Your Own Wireless Connectivity at the Same Time

This paper presents a novel mechanism, called Ally Friendly Jamming, which aims at providing an intelligent jamming capability that can disable unauthorized (enemy) wireless communication but at the same time still allow authorized wireless devices to communicate, even if all these devices operate at the same frequency. The basic idea is to jam the wireless channel continuously but properly control the jamming signals with secret keys, so that the jamming signals are unpredictable interference to unauthorized devices, but are recoverable by authorized ones equipped with the secret keys. To achieve the ally friendly jamming capability, we develop new techniques to generate ally jamming signals, to identify and synchronize with multiple ally jammers. This paper also reports the analysis, implementation, and experimental evaluation of ally friendly jamming on a software defined radio platform. Both the analytical and experimental results indicate that the proposed techniques can effectively disable enemy wireless communication and at the same time maintain wireless communication between authorized devices.

Wenbo Shen (North Carolina State University), Peng Ning (North Carolina State University), Xiaofan He (North Carolina State University), Huaiyu Dai (North Carolina State University)

Practical Timing Side Channel Attacks Against Kernel Space ASLR

Due to the prevalence of control-flow hijacking attacks, a wide variety of defense methods to protect both user space and kernel space code have been developed in the past years. A few examples that have received widespread adoption include stack canaries, non-executable memory, and Address Space Layout Randomization (ASLR). When implemented correctly (i.e., a given system fully supports these protection methods and no information leak exists), the attack surface is significantly reduced and typical exploitation strategies are severely thwarted. All modern desktop and server operating systems support these techniques and ASLR has also been added to different mobile operating systems recently. In this paper, we study the limitations of kernel space ASLR against a local attacker with restricted privileges. We show that an adversary can implement a generic side channel attack against the memory management system to deduce information about the privileged address space layout. Our approach is based on the intrinsic property that the different caches are shared resources on computer systems. We introduce three implementations of our methodology and show that our attacks are feasible on four different x86-based CPUs (both 32- and 64-bit architectures) and also applicable to virtual machines. As a result, we can successfully circumvent kernel space ASLR on current operating systems. Furthermore, we also discuss mitigation strategies against our attacks, and propose and implement a defense solution with negligible performance overhead.

Ralf Hund (Ruhr-University Bochum), Carsten Willems (Ruhr-University Bochum), and Thorsten Holz (Ruhr-University Bochum)

PrivExec: Private Execution as an Operating System Service

Privacy has become an issue of paramount importance for many users. As a result, encryption tools such as True Crypt, OS-based full-disk encryption such as File Vault, and privacy modes in all modern browsers have become popular. However, although such tools are useful, they are not perfect. For example, prior work has shown that browsers still leave many traces of user information on disk even if they are started in private browsing mode. In addition, disk encryption alone is not sufficient, as key disclosure through coercion remains possible. Clearly, it would be useful and highly desirable to have OS-level support that provides strong privacy guarantees for any application–not only browsers. In this paper, we present the design and implementation of PrivExec, the first operating system service for private execution. PrivExec provides strong, general guarantees of private execution, allowing any application to execute in a mode where storage writes, either to the filesystem or to swap, will not be recoverable by others during or after execution. PrivExec does not require explicit application support, recompilation, or any other preconditions. We have implemented a prototype of PrivExec by extending the Linux kernel that is performant, practical, and that secures sensitive data against disclosure.

Kaan Onarlioglu (Northeastern University), Collin Mulliner (Northeastern University), William Robertson (Northeastern University), Engin Kirda (Northeastern University)

A Hybrid Architecture for Interactive Verifiable Computation

We consider interactive, proof-based verifiable computation: how can a client machine specify a computation to a server, receive an answer, and then engage the server in an interactive protocol that convinces the client that the answer is correct, with less work for the client than executing the computation in the first place? Complexity theory and cryptography offer solutions in principle, but if implemented naively, they are ludicrously expensive. Recently, however, several strands of work have refined this theory and implemented the resulting protocols in actual systems. This work is promising but suffers from one of two problems: either it relies on expensive cryptography, or else it applies to a restricted class of computations. Worse, it is not always clear which protocol will perform better for a given problem.We describe a system that (a) extends optimized refinements of the non-cryptographic protocols to a much broader class of computations, (b) uses static analysis to fail over to the cryptographic ones when the non-cryptographic ones would be more expensive, and (c) incorporates this core into a built system that includes a compiler for a high-level language, a distributed server, and GPU acceleration. Experimental results indicate that our system performs better and applies more widely than the best in the literature.

Victor Vu (University of Texas, Austin), Srinath Setty (University of Texas, Austin), Andrew J. Blumberg (University of Texas, Austin), and Michael Walfish (University of Texas, Austin)

Pinocchio: Nearly Practical Veriable Computation

To instill greater confidence in computations outsourced to the cloud, clients should be able to verify the correctness of the results returned. To this end, we introduce Pinocchio, a built system for efficiently verifying general computations while relying only on cryptographic assumptions. With Pinocchio, the client creates a public evaluation key to describe her computation; this setup is proportional to evaluating the computation once. The worker then evaluates the computation on a particular input and uses the evaluation key to produce a proof of correctness. The proof is only 288 bytes, regardless of the computation performed or the size of the inputs and outputs. Anyone can use a public verification key to check the proof. Crucially, our evaluation on seven applications demonstrates that Pinocchio is efficient in practice too. Pinocchio’s verification time is typically 10ms: 5-7 orders of magnitude less than previous work; indeed Pinocchio is the first general-purpose system to demonstrate verification cheaper than native execution (for some apps). Pinocchio also reduces the worker’s proof effort by an additional 19-60x. As an additional feature, Pinocchio generalizes to zero-knowledge proofs at a negligible cost over the base protocol. Finally, to aid development, Pinocchio provides an end-to-end toolchain that compiles a subset of C into programs that implement the verifiable computation protocol.

Bryan Parno (Microsoft Research), Craig Gentry (IBM Research), Jon Howell (Microsoft Research), and Mariana Raykova (IBM Research)

ObliviStore: High Performance Oblivious Cloud Storage

We design and build ObliviStore, a high performance, distributed ORAM-based cloud data store secure in the malicious model. To the best of our knowledge, ObliviStore is the fastest ORAM implementation known to date, and is faster by 10X or more in comparison with the best known ORAM implementation. ObliviStore achieves high throughput by making I/O operations asynchronous. Asynchrony introduces security challenges, i.e., we must prevent information leakage not only through access patterns, but also through timing of I/O events. We propose various practical optimizations which are key to achieving high performance, as well as techniques for a data center to dynamically scale up a distributed ORAM. We show that with 11 trusted machines (each with a modern CPU), and 20 Solid State Drives, ObliviStore achieves a throughput of 31.5MB/s with a block size of 4KB.

Emil Stefanov (UC Berkeley) and Elaine Shi (University of Maryland)

Hiding Information in Flash Memory

This paper introduces a novel information hiding technique for Flash memory. The method hides data within an analog characteristic of Flash, the program time of individual bits. Because the technique uses analog behaviors, normal Flash memory operations are not affected and hidden information is invisible in the data stored in the memory. Even if an attacker checks a Flash chip’s analog characteristics, experimental results indicate that the hidden information is difficult to distinguish from inherent manufacturing variation or normal wear on the device. Moreover, the hidden data can survive erasure of the Flash memory data, and the technique can be used on current Flash chips without hardware changes.

Yinglei Wang (Cornell University), Wing-kei Yu (Cornell University), Sarah Q. Xu (Cornell University), Edwin Kan (Cornell University), and G. Edward Suh (Cornell University)

PUFs in Security Protocols: Attack Models and Security Evaluations

Traditional models of concurrency resort to peculiarly indirect means to express interaction and study its properties. Formalisms such as process algebras/calculi, concurrent objects, actors, agents, shared memory, message passing, etc., all are primarily action-based models that provide constructs for the direct specification of things that interact, rather than a direct specification of interaction (protocols). Consequently, interaction in these formalisms becomes a derived or secondary concept whose properties can be studied only indirectly, as the side-effects of the (intended or coincidental) couplings or clashes of the actions whose compositions comprise a model. Treating interaction as an explicit first-class concept, complete with its own composition operators, allows to specify more complex interaction protocols by combining simpler, and eventually primitive, protocols. Reo [20,11,12,6] serves as a premier example of such an interaction-based model of concurrency. In this paper, we describe Reo and its support tools. We show how exogenous coordination in Reo reflects an interaction-centric model of concurrency where an interaction (protocol) consists of nothing but a relational constraint on communication actions. In this setting, interaction protocols become explicit, concrete, tangible (software) constructs that can be specified, verified, composed, and reused, independently of the actors that they may engage in disparate applications.

Ulrich Rührmair (Technische Universität München) and Marten van Dijk (MIT)

SoK: Secure Data Deletion

Secure data deletion is the task of deleting data irrecoverably from a physical medium. In the digital world, data is not securely deleted by default; instead, many approaches add secure deletion to existing physical medium interfaces. Interfaces to the physical medium exist at different layers, such as user-level applications, the file system, the device driver, etc. Depending on which interface is used, the properties of an approach can differ significantly. In this paper, we survey the related work in detail and organize existing approaches in terms of their interfaces to physical media. We further present a taxonomy of adversaries differing in their capabilities as well as a systematization for the characteristics of secure deletion approaches. Characteristics include environmental assumptions, such as how the interface’s use affects the physical medium, as well as behavioural properties of the approach such as the deletion latency and physical wear. We perform experiments to test a selection of approaches on a variety of file systems and analyze the assumptions made in practice.

Joel Reardon (ETH Zurich), Srdjan Capkun (ETH Zurich), and David Basin (ETH Zurich)

Anon-Pass: Practical Anonymous Subscriptions

We present the design, security proof, and implementation of an anonymous subscription service. Users register for the service by providing some form of identity, which might or might not be linked to a real-world identity such as a credit card, a web login, or a public key. A user logs on to the system by presenting a credential derived from information received at registration. Each credential allows only a single login in any authentication window, or epoch. Logins are anonymous in the sense that the service cannot distinguish which user is logging in any better than random guessing. This implies unlinkability of a user across different logins. We find that a central tension in an anonymous subscription service is the service provider’s desire for a long epoch (to reduce server-side computation) versus users’ desire for a short epoch (so they can repeatedly “re-anonymize” their sessions). We balance this tension by having short epochs, but adding an efficient operation for clients who do not need unlinkability to cheaply re-authenticate themselves for the next time period. We measure performance of a research prototype of our protocol that allows an independent service to offer anonymous access to existing services. We implement a music service, an Android-based subway-pass application, and a web proxy, and show that adding anonymity adds minimal client latency and only requires 33 KB of server memory per active user.

Michael Z. Lee (The University of Texas at Austin), Alan M. Dunn (The University of Texas at Austin), Jonathan Katz (University of Maryland), Brent Waters (The University of Texas at Austin), and Emmett Witchel (The University of Texas at Austin)

Privacy-Preserving Ridge Regression on Hundreds of Millions of Records

Ridge regression is an algorithm that takes as input a large number of data points and finds the best-fit linear curve through these points. The algorithm is a building block for many machine-learning operations. We present a system for privacy-preserving ridge regression. The system outputs the best-fit curve in the clear, but exposes no other information about the input data. Our approach combines both homomorphic encryption and Yao garbled circuits, where each is used in a different part of the algorithm to obtain the best performance. We implement the complete system and experiment with it on real data-sets, and show that it significantly outperforms pure implementations based only on homomorphic encryption or Yao circuits.

Valeria Nikolaenko (Stanford University), Udi Weinsberg (Technicolor), Stratis Ioannidis (Technicolor), Marc Joye (Technicolor), Dan Boneh (Stanford University), Nina Taft (Technicolor)

A Scanner Darkly: Protecting User Privacy From Perceptual Applications

Perceptual, “context-aware” applications that observe their environment and interact with users via cameras and other sensors are becoming ubiquitous on personal computers, mobile phones, gaming platforms, household robots, and augmented-reality devices. This raises new privacy risks. We describe the design and implementation of DARKLY, a practical privacy protection system for the increasingly common scenario where an untrusted, third-party perceptual application is running on a trusted device. DARKLY is integrated with OpenCV, a popular computer vision library used by such applications to access visual inputs. It deploys multiple privacy protection mechanisms, including access control, algorithmic privacy transforms, and user audit. We evaluate DARKLY on 20 perceptual applications that perform diverse tasks such as image recognition, object tracking, security surveillance, and face detection. These applications run on DARKLY unmodified or with very few modifications and minimal performance overheads vs. native OpenCV. In most cases, privacy enforcement does not reduce the applications’ functionality or accuracy. For the rest, we quantify the tradeoff between privacy and utility and demonstrate that utility remains acceptable even with strong privacy protection.

Suman Jana (The University of Texas at Austin), Arvind Narayanan (Princeton University), Vitaly Shmatikov (University of Texas at Austin)

Caveat Coercitor: Coercion-Evidence in Electronic Voting

The balance between coercion-resistance, election verifiability and usability remains unresolved in remote electronic voting despite significant research over the last few years. We propose a change of perspective, replacing the requirement of coercion-resistance with a new requirement of coercion- evidence: there should be public evidence of the amount of coercion that has taken place during a particular execution of the voting system. We provide a formal definition of coercion-evidence that has two parts. Firstly, there should be a coercion-evidence test that can be performed against the bulletin board to accurately determine the degree of coercion that has taken place in any given run. Secondly, we require coercer independence, that is the ability of the voter to follow the protocol without being detected by the coercer. To show how coercion-evidence can be achieved, we propose a new remote voting scheme, Caveat Coercitor, and we prove that it satisfies coercion-evidence. Moreover, Caveat Coercitor makes weaker trust assumptions than other remote voting systems, such as JCJ/Civitas and Helios, and has better usability properties.

Gurchetan S. Grewal (University of Birmingham), Mark D. Ryan (University of Birmingham), Sergiu Bursuc (Queen’s University Belfast), and Peter Y. A. Ryan (University of Luxembourg)

SoK: The Evolution of Sybil Defense via Social Networks

Sybil attacks in which an adversary forges a potentially unbounded number of identities are a danger to distributed systems and online social networks. The goal of sybil defense is to accurately identify sybil identities. This paper surveys the evolution of sybil defense protocols that leverage the structural properties of the social graph underlying a distributed system to identify sybil identities. We make two main contributions. First, we clarify the deep connection between sybil defense and the theory of random walks. This leads us to identify a community detection algorithm that, for the first time, offers provable guarantees in the context of sybil defense. Second, we advocate a new goal for sybil defense that addresses the more limited, but practically useful, goal of securely white-listing a local region of the graph.

Lorenzo Alvisi (University of Texas Austin), Allen Clement (MPI-SWS), Alessandro Epasto (Sapienza University of Rome), Silvio Lattanzi (Google, Inc), and Alessandro Panconesi (Sapienza University of Rome)

Zerocoin: Anonymous Distributed E-Cash from Bitcoin

Bitcoin is the first e-cash system to see widespread adoption. While Bitcoin offers the potential for new types of financial interaction, it has significant limitations regarding privacy. Specifically, because the Bitcoin transaction log is completely public, users’ privacy is protected only through the use of pseudonyms. In this paper we propose Zerocoin, a cryptographic extension to Bitcoin that augments the protocol to allow for fully anonymous currency transactions. Our system uses standard cryptographic assumptions and does not introduce new trusted parties or otherwise change the security model of Bitcoin. We detail Zerocoin’s cryptographic construction, its integration into Bitcoin, and examine its performance both in terms of computation and impact on the Bitcoin protocol.

Ian Miers (The Johns Hopkins University), Christina Garman (The Johns Hopkins University), Matthew Green (The Johns Hopkins University), and Aviel D. Rubin (The Johns Hopkins University)

seL4: from General Purpose to a Proof of Information Flow Enforcement

In contrast to testing, mathematical reasoning and formal verification can show the absence of whole classes of security vulnerabilities. We present the, to our knowledge, first complete, formal, machine-checked verification of information flow security for the implementation of a general-purpose microkernel; namely seL4. Unlike previous proofs of information flow security for operating system kernels, ours applies to the actual 8, 830 lines of C code that implement seL4, and so rules out the possibility of invalidation by implementation errors in this code. We assume correctness of compiler, assembly code, hardware, and boot code. We prove everything else. This proof is strong evidence of seL4’s utility as a separation kernel, and describes precisely how the general purpose kernel should be configured to enforce isolation and mandatory information flow control. We describe the information flow security statement we proved (a variant of intransitive noninterference), including the assumptions on which it rests, as well as the modifications that had to be made to seL4 to ensure it was enforced. We discuss the practical limitations and implications of this result, including covert channels not covered by the formal proof.

Toby Murray (NICTA and University of New South Wales), Daniel Matichuk (NICTA), Matthew Brassil (NICTA), Peter Gammie (NICTA), Timothy Bourke (NICTA), Sean Seefried (NICTA), Corey Lewis (NICTA), Xin Gao (NICTA), and Gerwin Klein (NICTA and University of New South Wales)

Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework

We present the design, implementation, and verification of XMHF- an eXtensible and Modular Hypervisor Framework. XMHF is designed to achieve three goals– modular extensibility, automated verification, and high performance. XMHF includes a core that provides functionality common to many hypervisor-based security architectures and supports extensions that augment the core with additional security or functional properties while preserving the fundamental hypervisor security property of memory integrity (i.e., ensuring that the hypervisor’s memory is not modified by software running at a lower privilege level). We verify the memory integrity of the XMHF core–6018 lines of code– using a combination of automated and manual techniques. The model checker CBMC automatically verifies 5208 lines of C code in about 80 seconds using less than 2GB of RAM. We manually audit the remaining 422 lines of C code and 388 lines of assembly language code that are stable and unlikely to change as development proceeds. Our experiments indicate that XMHF’s performance is comparable to popular high-performance general-purpose hypervisors for the single guest that it supports.

Amit Vasudevan (CyLab, Carnegie Mellon University), Sagar Chaki (SEI, Carnegie Mellon University), Limin Jia (CyLab, Carnegie Mellon University), Jonathan M. McCune (Google Inc.), James Newsome, and Anupam Datta (CyLab, Carnegie Mellon University)

Implementing TLS with Verified Cryptographic Security

SSL/TLS is possibly the most used and most studied protocol for secure communications, with a 19-year history of flaws and fixes, ranging from its protocol logic to its cryptographic design, and from the Internet standard to its diverse implementations. We develop a new, verified, reference implementation of TLS 1.2. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms such as AES and RSA. Our implementation is written in F# and specified in F7. We present security specifications for its main components, such as authenticated stream encryption for the record layer and key establishment for the handshake. We describe their automated verification using the F7 refinement typechecker. To this end, we equip each cryptographic primitive and construction of TLS with a new typed interface that captures its security properties, and we gradually replace concrete implementations with ideal functionalities. We finally typecheck the protocol state machine, and thus obtain precise security theorems for TLS, as it is implemented and deployed. We also revisit classic attacks and report a few new ones.

Karthikeyan Bhargavan (INRIA), Cedric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), and Pierre-Yves Strub (IMDEA)

An Ideal-Security Protocol for Order-Preserving Encoding

Order-preserving encryption – an encryption scheme where the sort order of ciphertexts matches the sort order of the corresponding plaintexts – allows databases and other applications to process queries involving order over encrypted data efficiently. The ideal security guarantee for order-preserving encryption put forth in the literature is for the ciphertexts to reveal no information about the plaintexts besides order. Even though more than a dozen schemes were proposed, all these schemes leak more information than order. This paper presents the first order-preserving scheme that achieves ideal security. Our main technique is mutable ciphertexts, meaning that over time, the ciphertexts for a small number of plaintext values change, and we prove that mutable ciphertexts are needed for ideal security. Our resulting protocol is interactive, with a small number of interactions. We implemented our scheme and evaluated it on microbenchmarks and in the context of an encrypted MySQL database application. We show that in addition to providing ideal security, our scheme achieves 1 – 2 orders of magnitude higher performance than the state-of- the-art order-preserving encryption scheme, which is less secure than our scheme.

Raluca Ada Popa (MIT CSAIL), Frank Li (MIT CSAIL), and Nickolai Zeldovich (MIT CSAIL)

Efficient Garbling from a FixedKey Blockcipher

We advocate schemes based on fixed-key AES as the best route to highly efficient circuit-garbling. We provide such schemes making only one AES call per garbled- gate evaluation. On the theoretical side, we justify the security of these methods in the random-permutation model, where parties have access to a public random permutation. On the practical side, we provide the Just Garble system, which implements our schemes. Just Garble evaluates moderate-sized garbled- circuits at an amortized cost of 23.2 cycles per gate (7.25 nsec), far faster than any prior reported results.

Mihir Bellare (University of California, San Diego), Viet Tung Hoang (University of California, Davis), Sriram Keelveedhi (University of California, San Diego), and Phillip Rogaway (University of California, Davis)

Circuit Structures for Improving Efficiency of Security and Privacy Tools

Several techniques in computer security, including generic protocols for secure computation and symbolic execution, depend on implementing algorithms in static circuits. Despite substantial improvements in recent years, tools built using these techniques remain too slow for most practical uses. They require transforming arbitrary programs into either Boolean logic circuits, constraint sets on Boolean variables, or other equivalent representations, and the costs of using these tools scale directly with the size of the input circuit. Hence, techniques for more efficient circuit constructions have benefits across these tools. We show efficient circuit constructions for various simple but commonly used data structures including stacks, queues, and associative maps. While current practice requires effectively copying the entire structure for each operation, our techniques take advantage of locality and batching to provide amortized costs that scale polylogarithmically in the size of the structure. We demonstrate how many common array usage patterns can be significantly improved with the help of these circuit structures. We report on experiments using our circuit structures for both generic secure computation using garbled circuits and automated test input generation using symbolic execution, and demonstrate order of magnitude improvements for both applications.

Samee Zahur (University of Virginia) and David Evans (University of Virginia)

SoK: SSL and HTTPS: Revisiting Past Challenges and Evaluating Certificate Trust Model Enhancements

Internet users today depend daily on HTTPS for secure communication with sites they intend to visit. Over the years, many attacks on HTTPS and the certificate trust model it uses have been hypothesized, executed, and/or evolved. Meanwhile the number of browser-trusted (and thus, de facto, user-trusted) certificate authorities has proliferated, while the due diligence in baseline certificate issuance has declined. We survey and categorize prominent security issues with HTTPS and provide a systematic treatment of the history and on-going challenges, intending to provide context for future directions. We also provide a comparative evaluation of current proposals for enhancing the certificate infrastructure used in practice.

Jeremy Clark (Carleton University) and Paul C. van Oorschot (Carleton University)

Lucky Thirteen: Breaking the TLS and DTLS Record Protocols

The Transport Layer Security (TLS) protocol aims to provide confidentiality and integrity of data in transit across untrusted networks. TLS has become the de facto secure protocol of choice for Internet and mobile applications. DTLS is a variant of TLS that is growing in importance. In this paper, we present distinguishing and plaintext recovery attacks against TLS and DTLS. The attacks are based on a delicate timing analysis of decryption processing in the two protocols. We include experimental results demonstrating the feasibility of the attacks in realistic network environments for several different implementations of TLS and DTLS, including the leading OpenSSL implementations. We provide countermeasures for the attacks. Finally, we discuss the wider implications of our attacks for the cryptographic design used by TLS and DTLS.

Nadhem J. AlFardan (Royal Holloway, University of London) and Kenneth G. Paterson (Royal Holloway, University of London)

Cookieless Monster: Exploring the Ecosystem of Web-based Device Fingerprinting

The web has become an essential part of our society and is currently the main medium of information delivery. Billions of users browse the web on a daily basis, and there are single websites that have reached over one billion user accounts. In this environment, the ability to track users and their online habits can be very lucrative for advertising companies, yet very intrusive for the privacy of users. In this paper, we examine how web-based device fingerprinting currently works on the Internet. By analyzing the code of three popular browser-fingerprinting code providers, we reveal the techniques that allow websites to track users without the need of client-side identifiers. Among these techniques, we show how current commercial fingerprinting approaches use questionable practices, such as the circumvention of HTTP proxies to discover a user’s real IP address and the installation of intrusive browser plugins. At the same time, we show how fragile the browser ecosystem is against fingerprinting through the use of novel browser-identifying techniques. With so many different vendors involved in browser development, we demonstrate how one can use diversions in the browsers’ implementation to distinguish successfully not only the browser-family, but also specific major and minor versions. Browser extensions that help users spoof the user-agent of their browsers are also evaluated. We show that current commercial approaches can bypass the extensions, and, in addition, take advantage of their shortcomings by using them as additional fingerprinting features.

Nick Nikiforakis (KU Leuven), Alexandros Kapravelos (University of California, Santa Barbara), Wouter Joosen (KU Leuven), Christopher Kruegel (University of California, Santa Barbara), Frank Piessens (KU Leuven), Giovanni Vigna (University of California, Santa Barbara)

Practical Control Flow Integrity & Randomization for Binary Executables

Control Flow Integrity (CFI) provides a strong protection against modern control-flow hijacking attacks. However, performance and compatibility issues limit its adoption. We propose a new practical and realistic protection method called CCFIR (Compact Control Flow Integrity and Randomization), which addresses the main barriers to CFI adoption. CCFIR collects all legal targets of indirect control-transfer instructions, puts them into a dedicated “Springboard section” in a random order, and then limits indirect transfers to flow only to them. Using the Springboard section for targets, CCFIR can validate a target more simply and faster than traditional CFI, and provide support for on-site target- randomization as well as better compatibility. Based on these approaches, CCFIR can stop control-flow hijacking attacks including ROP and return-into-libc. Results show that ROP gadgets are all eliminated. We observe that with the wide deployment of ASLR, Windows/x86 PE executables contain enough information in relocation tables which CCFIR can use to find all legal instructions and jump targets reliably, without source code or symbol information. We evaluate our prototype implementation on common web browsers and the SPEC CPU2000 suite: CCFIR protects large applications such as GCC and Firefox completely automatically, and has low performance overhead of about 3.6%/8.6% (average/max) using SPECint2000. Experiments on real-world exploits also show that CCFIR- hardened versions of IE6, Firefox 3.6 and other applications are protected effectively.

Chao Zhang (Peking University), Tao Wei (Peking University and UC Berkeley), Zhaofeng Chen (Peking University), Lei Duan (Peking University), Stephen McCamant (University of Minnesota), László Szekeres (Stony Brook University), Dawn Song (UC Berkeley), and Wei Zou (Peking University)

Just-In-Time Code Reuse: On the Effectiveness of Fine-Grained Address Space Layout Randomization

Fine-grained address space layout randomization (ASLR) has recently been proposed as a method of efficiently mitigating runtime attacks. In this paper, we introduce the design and implementation of a framework based on a novel attack strategy, dubbed just-in-time code reuse, that undermines the benefits of fine-grained ASLR. Specifically, we derail the assumptions embodied in fine- grained ASLR by exploiting the ability to repeatedly abuse a memory disclosure to map an application’s memory layout on-the-fly, dynamically discover API functions and gadgets, and JIT-compile a target program using those gadgets – all within a script environment at the time an exploit is launched. We demonstrate the power of our framework by using it in conjunction with a real- world exploit against Internet Explorer, and also provide extensive evaluations that demonstrate the practicality of just-in-time code reuse attacks. Our findings suggest that fine-grained ASLR may not be as promising as first thought.

Kevin Z. Snow (The University of North Carolina at Chapel Hill), Lucas Davi (Technische Universität Darmstadt), Alexandra Dmitrienko (Fraunhofer SIT, Darmstadt), Christopher Liebchen (Technische Universität Darmstadt), Fabian Monrose (The University of North Carolina at Chapel Hill), and Ahmad-Reza Sadeghi (Technische Universität Darmstadt)

Welcome to the Entropics: BootTime Entropy in Embedded Devices

We present three techniques for extracting entropy during boot on embedded devices. Our first technique times the execution of code blocks early in the Linux kernel boot process. It is simple to implement and has a negligible runtime overhead, but, on many of the devices we test, gathers hundreds of bits of entropy. Our second and third techniques, which run in the bootloader, use hardware features – DRAM decay behavior and PLL locking latency, respectively – and are therefore less portable and less generally applicable, but their behavior is easier to explain based on physically unpredictable processes. We implement and measure the effectiveness of our techniques on ARM-, MIPS-, and AVR32-based systems-on-a-chip from a variety of vendors.

Keaton Mowery (UC San Diego), Michael Wei (UC San Diego), David Kohlbrenner (UC San Diego), Hovav Shacham (UC San Diego), and Steven Swanson (UC San Diego)