Cryptography plays an important role in computer and communication security. In practical implementations of cryptosystems, the cryptographic keys are usually loaded into the memory as plaintext, and then used in the cryptographic algorithms. Therefore, the private keys are subject to memory disclosure attacks that read unauthorized data from RAM. Such attacks could be performed through software methods (e.g., OpenSSL Heartbleed) even when the integrity of the victim system’s executable binaries is maintained. They could also be performed through physical methods (e.g., cold-boot attacks on RAM chips) even when the system is free of software vulnerabilities. In this paper, we propose Mimosa that protects RSA private keys against the above software-based and physical memory attacks. When the Mimosa service is in idle, private keys are encrypted and reside in memory as ciphertext. During the cryptographic computing, Mimosa uses hardware transactional memory (HTM) to ensure that (a) whenever a malicious process other than Mimosa attempts to read the plaintext private key, the transaction aborts and all sensitive data are automatically cleared with hardware mechanisms, due to the strong atomicity guarantee of HTM; and (b) all sensitive data, including private keys and intermediate states, appear as plaintext only within CPU-bound caches, and are never loaded to RAM chips. To the best of our knowledge, Mimosa is the first solution to use transactional memory to protect sensitive data against memory disclosure attacks. We have implemented Mimosa on a commodity machine with Intel Core i7 Haswell CPUs. Through extensive experiments, we show that Mimosa effectively protects cryptographic keys against various attacks that attempt to read sensitive data from memory, and it only introduces a small performance overhead.

CHERI is a hardware-software architecture that combines a capability-system security model with design choices from contemporary processors, Instruction-Set Architectures (ISAs), compilers, and operating systems. At the lowest level, CHERI's fine-grained, in-address-space memory protection mitigates many widely used exploit techniques. However, CHERI's ISA-level capability model can also act as the foundation for a software object-capability model suitable for incremental deployment in compartmentalizing C-language applications to mitigate attacks. Prototyped as an extension to the 64-bit FPGA BERI RISC soft-core processor, FreeBSD operating system, and Clang/LLVM compiler suite, we demonstrate substantial improvements to security, programmability, and scalability as compared to compartmentalization based on pure Memory-Management Unit (MMU) designs. We evaluate CHERI using several real-world UNIX libraries and applications.

We present VC3, the first practical framework that allows users to run distributed MapReduce computations in the cloud while keeping their code and data secret, and ensuring the correctness and completeness of their results. VC3 runs on unmodified Hadoop, but crucially keeps Hadoop, the operating system and the hypervisor out of the TCB; thus, confidentiality and integrity are preserved even if these large components are compromised. VC3 relies on SGX processors to isolate memory regions on individual computers, and to deploy new protocols that secure distributed MapReduce computations. VC3 optionally enforces region self-integrity invariants for all MapReduce code running within isolated regions, to prevent attacks due to unsafe memory reads and writes. Experimental results on common benchmarks show that VC3 performs well compared with unprotected Hadoop; VC3's average runtime overhead is negligible for its base security guarantees, 4.5% with write integrity and 8% with read/write integrity.

We discuss the question of how physical statements can be proven over digital communication channels between two parties (a “prover” and a “verifier”) residing in two separate local systems. Examples include: (i) “a certain object in the prover’s system has temperature X°C”, (ii) “two certain objects in the prover’s system are positioned at distance X”, or (iii) “a certain object in the prover’s system has been irreversibly altered or destroyed”. As illustrated by these examples, our treatment goes beyond classical security sensors in considering more general physical statements. Another distinctive aspect is the underlying security model: We neither assume secret keys in the prover’s system, nor do we suppose classical sensor hardware in his system which is tamperresistant and trusted by the verifier. Without an established name, we call this new type of security protocol a ”virtual proof of reality” or simply “virtual proof” (VP). In order to illustrate our novel concept, we give example VPs based on temperature sensitive integrated circuits (ICs), disordered optical scattering media, and quantum systems. The corresponding protocols prove the temperature, relative position, or destruction/modification of certain physical objects in the prover’s system to the verifier. These objects (so-called “witness objects”) are prepared by the verifier and handed over to the prover prior to the VP. In addition to these new protocols, we carry out and detail full proof-of-concept implementations for all of our optical and circuit-based VPs. Our work touches upon, and partly extends, several established concepts in cryptography and security, including physical unclonable functions, quantum cryptography, interactive proof systems, and, most recently, physical zero-knowledge proofs. We also discuss potential advancements of our method, for example “public virtual proofs” that function without exchanging witness objects between the verifier and the prover.

With the rapid proliferation of malware attacks on the Internet, understanding their malicious behavior plays a critical role in crafting effective defenses. Advanced malware analysis relies on virtualization or emulation technology to run samples in a confined environment, and analyze malicious activities by instrumenting code execution. However, virtual machines and emulators inevitably create artifacts in the execution environment, making these approaches vulnerable to detection or subversion. In this paper, we present MALT, a debugging framework that employs System Management Mode, a CPU mode in the x86 architecture, to transparently study armored malware. MALT does not depend on virtualization or emulation and thus is immune to threats targeting such environments. Our approach reduces the attack surface at the software level, and advances state-of-the-art debugging transparency. MALT embodies various debugging functions, including register/memory accesses, breakpoints, and four stepping modes. We implemented a prototype of MALT on two physical machines, and we conducted experiments by testing an array of existing anti-virtualization, anti-emulation, and packing techniques against MALT. The experimental results show that our prototype remains transparent and undetected against the samples. Furthermore, our prototype of MALT introduces moderate but manageable overheads on both Windows and Linux platforms.

Each day, millions of people are harmed in one way or another by cybercrime. While we have a good understanding of the number of systems compromised or even the profits of the attackers, the harm experienced by humans is less well understood, and reducing this harm should be the ultimate goal of any security intervention. To efficiently allocate effort for the purpose of reducing harm, we must understand how this harm is perpetrated, which perpetrators are causing it, and how much harm is being experienced due to which attacks. This paper presents a strategy for quantifying the harm caused by the cybercrime of typosquatting via a new technique we developed called intent inference. Intent inference allows us to achieve three goals: define a new metric for quantifying harm to users, develop a new methodology for identifying typosquatting domain names, and quantify the harm caused by various typosquatting perpetrators. Through synthesizing complementary datasets, we find that on average, typosquatting costs the typical user 1.3 seconds per typosquatting event over the alternative of receiving a browser error page, and legitimate sites lose approximately 3% of their mistyped traffic over the alternative of an unregistered typo. While these metrics quantify harm for typosquatting overall, there is much variation between perpetrators: while on average perpetrators increase the time it takes to find the intended site, many typosquatters actually improve the latency for users finding their intended site. Overall, we find that we are able to precisely quantify the amount of harm experienced by the primary stakeholders, and that some perpetrators of typosquatting are actually strictly utility increasing for themselves, the targeted site's owner, and the users, calling into question the necessity of harsh penalties or legal intervention against this flavor of cybercrime.

Bitcoin has emerged as the most successful cryptographic currency in history. Within two years of its quiet launch in 2009, Bitcoin grew to comprise billions of dollars of economic value, even while the body of published research and security analysis justifying the system's design was negligible. In the ensuing years, a growing literature has identified hidden-but-important properties of the system, discovered attacks, proposed promising alternatives, and singled out difficult future challenges. This interest has been complemented by a large and vibrant community of open-source developers who steward the system, while proposing and deploying numerous modifications and extensions. We provide the first systematic exposition of the second generation of cryptocurrencies, including Bitcoin and the many alternatives that have been implemented as alternate protocols or ``altcoins.'' Drawing from a scattered body of knowledge, we put forward three key components of Bitcoin's design that can be decoupled, enabling a more insightful analysis of Bitcoin's properties and its proposed modifications and extensions. We contextualize the literature into five central properties capturing blockchain stability. We map the design space for numerous proposed modification, providing comparative analyses for alternative consensus mechanisms, currency allocation mechanisms, computational puzzles, and key management tools. We focus on anonymity issues in Bitcoin and provide an evaluation framework for analyzing a variety of proposals for enhancing unlinkability. Finally we provide new insights on a what we term disintermediation protocols, which absolve the need for trusted intermediaries in an interesting set of applications. We identify three general disintermediation strategies and provide a detailed comparative cost analysis.

An open distributed system can be secured by requiring participants to present proof of work and rewarding them for participation. The Bitcoin digital currency introduced this mechanism, which is adopted by almost all contemporary digital currencies and related services. A natural process leads participants of such systems to form pools, where members aggregate their power and share the rewards. Experience with Bitcoin shows that the largest pools are often open, allowing anyone to join. It has long been known that a member can sabotage an open pool by seemingly joining it but never sharing its proofs of work. The pool shares its revenue with the attacker, and so each of its participants earns less. We define and analyze a game where pools use some of their participants to infiltrate other pools and perform such an attack. With any number of pools, no-pool-attacks is not a Nash equilibrium. With two pools, or any number of identical pools, there exists an equilibrium that constitutes a tragedy of the commons where the pools attack one another and all earn less than they would have if none had attacked. For two pools, the decision whether or not to attack is the miner's dilemma, an instance of the iterative prisoner's dilemma. The game is played daily by the active Bitcoin pools, which apparently choose not to attack. If this balance breaks, the revenue of open pools might diminish, making them unattractive to participants.

Bitcoin is a decentralized P2P digital currency in which coins are generated by a distributed set of miners and transaction are broadcasted via a peer-to-peer network. While Bitcoin provides some level of anonymity (or rather pseudonymity) by encouraging the users to have any number of random-looking Bitcoin addresses, recent research shows that this level of anonymity is rather low. This encourages users to connect to the Bitcoin network through anonymizers like Tor and motivates development of default Tor functionality for popular mobile SPV clients. In this paper we show that combining Tor and Bitcoin creates an attack vector for the deterministic and stealthy man-in-the-middle attacks. A low-resource attacker can gain full control of information flows between all users who chose to use Bitcoin over Tor. In particular the attacker can link together user's transactions regardless of pseudonyms used, control which Bitcoin blocks and transactions are relayed to the user and can delay or discard user's transactions and blocks. In collusion with a powerful miner double-spending attacks become possible and a totally virtual Bitcoin reality can be created for such set of users. Moreover, we show how an attacker can fingerprint users and then recognize them and learn their IP address when they decide to connect to the Bitcoin network directly.

Today, web injection occurs in many forms, but fundamentally occurs when malicious and unwanted actors tamper directly with browser sessions for their own profit. In this work we illuminate the scope and negative impact of one of these forms, ad injection, in which users have ads imposed on them in addition to, or different from, those that websites originally sent them. Working in partnership with Google, we develop a multi-staged pipeline that identifies ad injection in the wild and captures its distribution and revenue chains. We find that ad injection has entrenched itself as a cross-browser monetization platform impacting more than 5% of unique daily IP addresses accessing Google---tens of millions of users around the globe. Injected ads arrive on a client's machine through multiple unwanted and malicious vectors, with our measurements identifying 50,870 Chrome extensions and 34,407 Windows binaries, 38% and 17% of which are explicitly malicious. A small number of software developers support the vast majority of these injectors, who in turn syndicate from the larger ad ecosystem. We have contacted the Chrome Webstore and the advertisers targeted by ad injectors to alert each of the deceptive practices involved.

The Domain Name System (DNS) seems ideal for connectionless UDP, yet this choice results in challenges of eavesdropping that compromises privacy, source-address spoofing that simplifies denial-of-service (DoS) attacks on the server and third parties, injection attacks that exploit fragmentation, and reply-size limits that constrain keysizes and policy choices. We propose DNS-X to address these problems. It uses TCP to smoothly support large payloads and to mitigate spoofing and amplification for DoS. DNS-X uses transport-layer security (TLS) to provide privacy from users to their DNS resolvers and optionally to authoritative servers. TCP and TLS are hardly novel, and expectations about DNS suggest connections will balloon client latency and overwhelm server with state. Our contribution is to show that DNS-X significantly improves security and privacy: TCP prevents denial-of-service (DoS) amplification against others, reduces the effects of DoS on the server, and simplifies policy choices about keysize. TLS protects against eavesdroppers to the recursive resolver. Our second contribution is to show that with careful implementation choices, these benefits come at only modest cost: end-to-end latency from {TLS to the recursive resolver is only about 9% slower} when UDP is used to the authoritative server, and 22% slower with TCP to the authoritative. With diverse traces we show that connection reuse can be frequent (60--95% for stub and recursive resolvers, although half that for authoritative servers), and after connection establishment, experiments show that TCP and TLS latency is equivalent to UDP. With conservative timeouts (20s at authoritative servers and 60s elsewhere) and estimated per-connection memory, we show that server memory requirements match current hardware: a large recursive resolver may have 24k active connections requiring about 3.6GB additional RAM. Good performance requires key design and implementation decisions we identify: query pipelining, out-of-order responses, TCP fast-open and TLS connection resumption, and plausible timeouts.

Motivated by recent revelations of widespread state eavesdropping of personal communication, many solutions now claim to offer secure and private messaging. This includes both a large number of new projects and many widely adopted tools that have added security features. The intense pressure in the past two years to deliver solutions quickly has resulted in varying threat models, incomplete objectives, dubious security claims, and a lack of broad perspective on the existing cryptographic literature on secure communication. In this paper, we evaluate and systematize current secure messaging solutions and propose an evaluation framework for their security, usability, and ease-of-adoption properties. We consider solutions from academia, but also identify innovative and promising approaches used “in-the-wild” that are not considered by the academic literature. We identify three key challenges and map the design landscape for each: trust establishment, conversation security, and transport privacy. Trust establishment approaches offering strong security and privacy features perform poorly from the usability and adoption perspective, whereas some mixtures of approaches that have not been well studied in the academic literature might provide reasonable trade-offs in practice. In contrast, once trust is established, in most cases conversation security can be achieved without any user involvement in the case of two-party conversations, with conversations between larger groups still wanting for a practical solution. Finally, transport privacy appears to be the most difficult problem to solve without paying significant performance penalties.

We introduce "temporal lensing": a technique that concentrates a relatively low-bandwidth flood into a short, high-bandwidth pulse. By leveraging existing DNS infrastructure, we experimentally explore lensing and the properties of the pulses it creates. We also empirically show how attackers can use lensing to achieve peak bandwidths more than an order of magnitude greater than their upload bandwidth. While formidable by itself in a pulsing DoS attack, attackers can also combine lensing with amplification to potentially produce pulses with peak bandwidths orders of magnitude larger than their own.

QUIC is a secure transport protocol developed by Google and implemented in Chrome in 2013 representing one of the most promising solutions to decreasing latency while intending to provide security properties similar with TLS. In this work we shed some light on QUIC's strengths and weaknesses in terms of its provable security and performance guarantees in the presence of attackers. We first introduce a security model for analyzing performance-driven protocols like QUIC and prove that QUIC satisfies our definition under reasonable assumptions on the protocol's building blocks. However, we find that QUIC does not satisfy the traditional notion of forward secrecy that are provided by some modes of TLS, e.g., TLS-DHE. Our analyses also reveal that with simple bit-flipping and replay attacks on some public parameters exchanged during the handshake, an adversary could easily destroy some of QUIC's minimal latency advantages either by having it fall back to TCP or by causing the client and server to have an inconsistent view of their handshake leading to a failure to complete the connection. We have implemented these attacks and demonstrated that they are practical. Our results suggest that QUIC's security weaknesses are introduced by the very mechanisms used to reduce latency, which highlights the seemingly inherent trade off between minimizing latency and providing `good' security guarantees.

We propose a new approach for securely verifying sequences of location claims from mobile nodes. The key idea is to exploit the inherent mobility of the nodes in order to constrain the degree of freedom of an attacker when spoofing consecutive location updates along a claimed track. We show that in the absence of noise, our approach is able to securely verify any 2-D track with a minimum of three verifiers or any 3-D track with four verifiers. Our approach is lightweight in the sense that it considerably relaxes the system requirements compared to previous secure location verification schemes which are all agnostic to mobility. As opposed to previous schemes, our track verification solution is at the same time (i) passive, (ii) does not require any time synchronization among the verifiers, (iii) does not need to keep the location of the verifiers secret, (iv) nor does it require specialized hardware. This makes our solution particularly suitable for large-scale deployments. We have evaluated our solution in a realistic air traffic monitoring scenario using real-world data. Our results show that 25 position claims from a track are sufficient to detect spoofing attacks with a false positive rate of 1.4% and a false negative rate of 1.2%. For tracks with more than 40 claims, the false positive and false negative rates drop to zero.

This paper presents Riposte, a new system for anonymous broadcast messaging. Riposte is the first such system, to our knowledge, that simultaneously protects against traffic-analysis attacks, prevents anonymous denial-of-service by malicious clients, and scales to million-user anonymity sets. To achieve these properties, Riposte makes novel use of techniques used in private information retrieval and secure multi-party computation. In a configuration allowing 10,000 users to upload messages to the system, our prototype Riposte cluster handles 48 posts per second. For latency-tolerant workloads with many more readers than writers (e.g. Twitter, Wikileaks), we demonstrate that, in 32 hours, Riposte can build an anonymity set of 2,895,216 users.

Cloud computing sparked interest in Verifiable Computation (VC) protocols, which allow a weak client to securely outsource computations to remote parties. Recent improvements in theory and implementation have dramatically reduced the client's cost to verify the correctness of results, but the overhead to produce proofs largely remains impractical. Geppetto introduces a series of complementary techniques for reducing prover overhead and increasing prover flexibility. With MultiQAPs, Geppetto reduces the cost of sharing state between computations (e.g., for MapReduce) or within a single computation by up to two orders of magnitude. Via a careful instantiation of cryptographic primitives, Geppetto also brings down the cost of verifying outsourced cryptographic computations (e.g., verifiably computing on signed data); combining these techniques with Geppetto's notion of bounded proof bootstrapping, Geppetto improves on prior bootstrapped systems by several orders of magnitude. As a result, Geppetto scales to programs that are larger than prior work by an order of magntitude while still producing a constant-sized proof. Geppetto also supports qualitatively new properties like verifying the correct execution of proprietary (i.e., secret) algorithms. Finally, Geppetto's use of energy-saving circuits brings the prover's costs more in line with the program's actual (rather than worst-case) execution time. Geppetto is implemented in a full-fledged, scalable compiler that consumes LLVM code generated from a variety of apps, as well as a large cryptographic library.

We study the problem of privacy-preserving proofs on authenticated data, where a party receives data from a trusted source and is requested to prove computations over the data to third parties in a correct and private way, i.e., the third party learns no information on the data but is still assured that the claimed proof is valid. Our work particularly focuses on the challenging requirement that the third party should be able to verify the validity with respect to the specific data authenticated by the source --- even without having access to that source. This problem is motivated by various scenarios emerging from several application areas such as wearable computing, smart metering, or general business-to-business interactions. Furthermore, these applications also demand any meaningful solution to satisfy additional properties related to usability and scalability. In this paper, we formalize the above three-party model, discuss concrete application scenarios, and then we design, build, and evaluate ADSNARK, a nearly practical system for proving arbitrary computations over authenticated data in a privacy-preserving manner. ADSNARK improves significantly over state-of-the-art solutions for this model. For instance, compared to corresponding solutions based on Pinocchio (Oakland'13), ADSNARK achieves up to 25x improvement in proof-computation time and a 20x reduction in prover storage space.

Non-interactive zero-knowledge proofs (NIZKs) are a powerful cryptographic tool, with numerous potential applications. However, succinct NIZKs (e.g., zk-SNARK schemes) necessitate a trusted party to generate and publish some public parameters, to be used by all provers and verifiers. This party is trusted to *correctly* run a probabilistic algorithm (specified by the the proof system) that outputs the public parameters, and publish them, without *leaking* any other information (such as the internal randomness used by the algorithm); violating either requirement may allow producing convincing "proofs" of false statements. This trust requirement poses a serious impediment to deploying NIZKs in many applications, because a party that is trusted by all users of the envisioned system may simply not exist. In this work, we show how public parameters for a class of NIZKs can be generated by a multi-party protocol, such that if at least one of the parties is honest, then the result is secure (in both aforementioned senses) and can be subsequently used for generating and verifying numerous proofs without any further trust. We design and implement such a protocol, tailored to efficiently support the state-of-the-art NIZK constructions with short and easy-to-verify proofs (Parno et al. IEEE S&P '13; Ben-Sasson et al. USENIX Sec '14; Danezis et al. ASIACRYPT '14). Applications of our system include generating public parameters for systems such as Zerocash (Ben-Sasson et al. IEEE S&P '13) and the scalable zero-knowledge proof system of (Ben-Sasson et al. CRYPTO '14).

In this paper we propose a new mechanism for achieving forward secure encryption in store and for- ward messaging systems such as email and SMS. In a forward secure encryption scheme, a user periodically updates her secret key so that past messages remain confidential in the event that her key is compromised. A primary contribution of our work is to introduce a new form of encryption that we name puncturable encryption. Using a puncturable encryption scheme, recipients may repeatedly update their decryption keys to revoke decryption capability for selected messages, recipients or time periods. Most importantly, this up- date process does not require the recipients to commu- nicate with or distribute new key material to senders. We show how to combine puncturable encryption with the forward-secure public key encryption proposal of Canetti et al. to achieve practical forward-secure messaging with low overhead. We implement our schemes and provide experimental evidence that this new construction is practical.

Cloud storage has rapidly become a cornerstone of many IT infrastructures, constituting a seamless solution for the backup, synchronization, and sharing of large amounts of data. Putting user data in the direct control of cloud service providers, however, raises security and privacy concerns related to the integrity of outsourced data, the accidental or intentional leakage of sensitive information, the profiling of user activities and so on. Furthermore, even if the cloud provider is trusted, users having access to outsourced files might be malicious and misbehave. These concerns are particularly serious in sensitive applications like personal health records and credit score systems. To tackle this problem, we present GORAM, a cryptographic system that protects the secrecy and integrity of outsourced data with respect to both an untrusted server and malicious clients, guarantees the anonymity and unlinkability of accesses to such data, and allows the data owner to share outsourced data with other clients, selectively granting them read and write permissions. GORAM is the first system to achieve such a wide range of security and privacy properties for outsourced storage. In the process of designing an efficient construction, we developed two new, generally applicable cryptographic schemes, namely, batched zero-knowledge proofs of shuffle and an accountability technique based on chameleon signatures, which we consider of independent interest. We implemented GORAM in Amazon Elastic Compute Cloud (EC2) and ran a performance evaluation demonstrating the scalability and efficiency of our construction.

We introduce TinyGarble, a novel automated methodology for generating compressed Boolean circuits for Yao’s Garbled Circuit (GC) protocol. TinyGarble achieves an unprecedented level of compactness and scalability by introducing sequential function description to GC. It also allows adaptation of powerful logic synthesis tools for optimizing the generated circuit using newly created custom libraries. While our approach is in contrast with the state-of-the-art garbling methods that only operate on the combinational logic, we introduce new transformations such that our sequential circuits can be securely evaluated by interfacing with the earlier frontend garbling schemes. TinyGarble’s ultra compact circuit representations can fit merely on the processor cache, which results in fewer cache misses and thereby leads to less number of CPU cycles. Proof-of-concept implementation of TinyGarble on benchmark circuits demonstrates a high degree of compactness and scalability. We improve the results of the best known automatic tool for GC generation reported in [36] by several orders of magnitude: for example, TinyGarble can compact the 1024-bit multiplication by 4172 times, while decreasing the number of non-XOR’s by 67% in comparison. Moreover, TinyGarble is able to implement functions that have never been reported before, such as RSA-8192 and SHA-3, which can be represented as circuits requiring about 7.87MB and 160KB of memory respectively. Finally, our sequential description enables us to design a secure calculator based on a stack machine. This is the first scalable emulation of a universal circuit for semi-private function evaluation where the number of instruction invocations is not limited by the circuit size.

To allow the benefits of analysis that machine learning algorithms bring, while simultaneously providing user data privacy, we need secure computation models for a broad set of data mining algorithms. We propose to bring secure computation to programming frameworks that support data mining on massively parallel architectures. To address this challenge, we propose a solution that (i) develops a programming paradigm to allow non-cryptography experts to write secure code; (ii) brings parallelism to the secure version of these algorithms; and (iii) that meets the needs for obliviousness, thereby not leaking any private information. For example, we show how to hide the graph structure. Our technique efficiently converts many graph based algorithms (including many machine learning ones) to a distributed oblivious version with minimal communication overhead due to parallelism. Our solution scales linearly with input size and with the number of machines. Importantly, our secure version of graph based algorithms incurs a small overhead, log in the number of graph edges, in comparison to the non-secure parallel version. We demonstrate with 4 common data mining algorithms, that secure computation can be brought into the realm of practicality for big data analysis. Our secure matrix factorization implementation can process 1 million ratings in 13 hours, which is a multiple order-of-magnitude improvement over the only other attempt that needed 3 hours to process 16K ratings.

The Blind Seer system (Oakland 2014) is an efficient and scalable DBMS that affords both client query privacy and server data protection. It also provides the ability to en- force authorization policies on the system, restricting client’s queries while maintaining the privacy of both query and pol- icy. Blind Seer supports a rich query set, including arbitrary boolean formulas, and is provably secure with respect to a controlled amount of search pattern leakage. No other system to date achieves this tradeoff of performance, generality, and provable privacy. A major shortcoming of Blind Seer is its reliance on semi-honest security, particularly for access control and data protection. A malicious client could easily cheat the query authorization policy and obtain any database records satisfying any query of its choice, thus violating basic security features of any standard DBMS. In sum, Blind Seer offers additional privacy to a client, but sacrifices a basic security tenet of DBMS. In the present work, we completely resolve the issue of a malicious client. We show how to achieve robust access control and data protection in Blind Seer with virtually no added cost to performance or privacy. Our approach also involves a novel technique for a semi-private function secure function evaluation (SPF-SFE) that may have independent applications. We fully implement our solution and report on its performance.

We design and develop CreST, a new generation, automated secure computation framework, that aims to bridge the gap between generality and custom optimizations. We show how this framework allowed us to easily implement efficient oblivious algorithms that was previously insurmountable to implement due to limitations of existing secure computation frameworks. We also show how this framework inspired us to create new oblivious algorithms and solve several open questions of interest to the algorithms community. We will open source CreST and our rich libraries to the community, offering a reusable framework to implement and distribute new cryptographic algorithms.

Immersive experiences that mix digital and real-world objects are becoming reality. These experiences are already present on smartphones and game consoles via Kinect, and will eventually emerge on the device-agnostic web platform. These experiences raise serious privacy concerns, as they require real-time sensor input to appropriately intermingle digital and real-world objects. Previous research focuses on controlling application access to sensor input through filtering, access control, and sandboxing, which do not directly address the display tasks inherent to immersive experiences. Furthermore, these low-level solutions are a poor fit for integration with the high-level GUI toolkit in the web platform. This paper describes how to extend the existing web platform to enable least privilege for immersive rendering, and implements these extensions in a 3D web browser called SurroundWeb. The room skeleton lets applications place content in response to the physical dimensions and locations of renderable surfaces in a room. The detection sandbox lets applications declaratively place content near recognized objects in the room without revealing if the object is present. We demonstrate that these extensions reveal an acceptable amount of information to applications, can be used to implement a wide range of previously proposed immersive experiences with least privilege, and can be implemented with acceptable runtime overhead.

Today’s systems produce a wealth of data every day, and the data further generates more data, i.e., the derived data, forming into a complex data propagation network, defined as the data’s lineage. There are many reasons for users and administrators to forget certain data including the data’s lineage. From the privacy perspective, a system may leak private information of certain users, and those users unhappy about privacy leaks naturally want to forget their data and its lineage. From the security perspective, an anomaly detection system can be polluted by adversaries through injecting manually crafted data into the training set. Therefore, we envision forgetting systems, capable of completely forgetting certain data and its lineage. In this paper, we focus on making learning systems forget, the process of which is defined as machine unlearning or unlearning. To perform unlearning upon learning system, we present general unlearning criteria, i.e., converting a learning system or part of it into a summation form of statistical query learning model, and updating all the summations to achieve unlearning. Then, we integrate our unlearning criteria into an unlearning architecture that interacts with all the components of a learning system, such as sample clustering and feature selection. To demonstrate our unlearning criteria and architecture, we select four real-world learning systems, including an item-item recommendation system, an online social network spam filter, and a malware detection system. These systems are first exposed to an adversarial environment, e.g., if the system is potentially vulnerable to training data pollution, we first pollute the training data set and show that the detection rate drops significantly. Then, we apply our unlearning technique upon those affected systems, either polluted or leaking private information. Our results show that after unlearning, the detection rate of a polluted system increases back to the one before pollution, and a system leaking a particular user’s private information completely forgets that information.

Secure storage of genomic data is of great and increasing importance. The scientific community's improving ability to interpret individuals' genetic materials and the growing size of genetic database populations have been aggravating the potential consequences of data breaches. The prevalent use of passwords to generate encryption keys thus poses an especially serious problem when applied to genetic data. Weak passwords can jeopardize genetic data in the short term; given the multi-decade lifespan of genetic data, even the use of strong passwords with conventional encryption can lead to compromise. We present a tool called GenoGuard to provide strong protection for genomic data both today and in the long term. GenoGuard incorporates a new theoretical framework for encryption called honey encryption (HE) that can in principle provide information-theoretic confidentiality guarantees for encrypted data. Previously proposed HE schemes, however, can unfortunately be applied to messages from only a very restricted set of probability distributions. GenoGuard thus addresses the open problem of applying HE techniques to the highly non-uniform probability distributions characterizing sequences of genetic data. In GenoGuard, a potential adversary can attempt to guess keys or passwords exhaustively and decrypt via a brute-force attack. We prove that decryption under any key, however, will yield a plausible genome sequence; thus GenoGuard offers an information-theoretic security guarantee against message-recovery attacks. We also explore attacks using side information. Finally, we present an efficient and parallelized software implementation of GenoGuard.

We critically survey game-based security definitions for the privacy of voting schemes. In addition to known limitations, we unveil several previously unnoticed shortcomings. Surprisingly, the conclusion of our study is that none of the existing definitions is satisfactory: they either provide only weak guarantees, or can be applied only to a limited class of schemes, or both. Based on our findings, we propose a new game-based definition of privacy which we call BPRIV. We also identify a new property which we call strong consistency, needed to express that tallying does not leak sensitive information. We validate our security notions by showing that BPRIV, strong consistency and strong correctness for a voting scheme imply its security in a simulation-based sense. This result also yields a proof technique for proving entropy-based notions of privacy which offer the strongest security guarantees but are hard to prove directly: first prove your scheme BPRIV and strongly consistent, then study the entropy-based privacy of the result function of the election, which is a much easier task.

Password vaults are increasingly popular applications that store multiple passwords encrypted with a single master password that the user memorizes. This promises to greatly reduce the burden on users to remember passwords, but introduces a single point of failure. An attacker that obtains a user's encrypted vault can mount offline brute-force attacks and, if successful, compromise all of the user's passwords in the vault. In this paper, we investigate building encrypted vaults that resist such cracking attacks, forcing attackers to move to an online attack. Our contributions are the following. We give an attack and supporting analysis showing that a previous design for cracking-resistant vaults actually degrades security relative to conventional password-based approaches. This was the only previous attempt we are aware of, and so we explore new approaches. In particular we introduce a new type of secure encoding scheme that we call natural-language encoders (NLEs). These support building vaults that, when decrypted with the wrong password, produce plausible-looking decoy passwords. We show how to build NLEs using existing tools from natural-language processing, such as $n$-gram models and probabilistic context-free grammars, and evaluate their ability to provide plausible decoys. Finally, we design and a full cracking-resistant vault system, called NoCrack. It incorporates combines our best NLE scheme with a number of other mechanisms. We report on an initial implementation and evaluation of the system.

J-PAKE is an efficient password-authenticated key exchange protocol that is included in the OpenSSL library and is currently being used in practice. We present the first proof of security for this protocol in a well-known and accepted model for authenticated key-exchange, that incorporates online and offline password guessing, concurrent sessions, forward secrecy, server compromise, and loss of session keys. This proof relies on the Decision Square Diffie-Hellman assumption, as well as a strong security assumption for the non-interactive zero-knowledge (NIZK) proofs in the protocol (specifically, simulation-sound extractability). We show that the Schnorr proof-of-knowledge protocol, which was recommended for the J-PAKE protocol, satisfies this strong security assumption in a model with algebraic adversaries and random oracles, and extend the full J-PAKE proof of security to this model. Finally, we show that by modifying the recommended labels in the Schnorr protocol used in J-PAKE, we can achieve a security proof for J-PAKE with a tighter security reduction

Lattice-based cryptographic primitives are believed to offer resilience against attacks by quantum computers. We demonstrate the practicality of post-quantum key exchange by constructing ciphersuites for the Transport Layer Security (TLS) protocol that provide key exchange based on the ring learning with errors (R-LWE) problem; we accompany these ciphersuites with a rigorous proof of security. Our approach ties lattice-based key exchange together with traditional authentication using RSA or elliptic curve digital signatures: the post-quantum key exchange provides forward secrecy against future quantum attackers, while authentication can be provided using RSA keys that are issued by today's commercial certificate authorities, smoothing the path to adoption. Our cryptographically secure implementation, aimed at the 128-bit security level, reveals that the performance price when switching from non-quantum-safe key exchange is not too high. With our R-LWE ciphersuites integrated into the OpenSSL library and using the Apache web server on a 2-core desktop computer, we could serve 506 RLWE-ECDSA-AES128-GCM-SHA256 HTTPS connections per second for a 10 KiB payload. Compared to elliptic curve Diffie--Hellman, this means an 8 KiB increased handshake size and a reduction in throughput of only 21%. This demonstrates that post-quantum key-exchange can already be considered practical.

Implementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes and key exchange methods, where each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years (they are now in the process of being patched). We argue that these vulnerabilities stem from incorrect compositions of individually correct state machines. We present the first verified implementation of a composite TLS state machine in C that can be embedded into OpenSSL and accounts for all its supported ciphersuites. Our attacks expose the need for the formal verification of core components in cryptographic protocol libraries; our implementation demonstrates that such mechanized proofs are within reach, even for mainstream TLS implementations.

Secure Sockets Layer (SSL) and Transport Layer Security (TLS) protocols have become the security backbone of the Web and Internet today. Many systems including mobile and desktop applications are protected by SSL/TLS protocols against network attacks. However, many vulnerabilities caused by incorrect use of SSL/TLS APIs have been uncovered in recent years. Such vulnerabilities, many of which are caused due to poor API design and inexperience of the application developers, often lead to confidential data leakage or man-in-the-middle attacks. In order to guarantee code quality and logic correctness in applications that use SSL/TLS, a scalable automated approach for security analysis is needed. In this paper, we design and implement SSLINT, a scalable automated system for detecting in- correct use of SSL/TLS APIs. By using static analysis techniques, it is capable of performing automatic logic verification with high efficiency and good accuracy. To demonstrate the feasibility of our approach as well as advantages of SSLINT, we apply it to one of the most popular Linux distributions – Ubuntu. We find 27 unknown SSL/TLS vulnerabilities in Ubuntu applications, most of which are also distributed with other Linux distributions.

The presence of large numbers of security vulnerabilities in popular feature-rich commodity operating systems has inspired a long line of work on excluding these operating systems from the trusted computing base of applications, while retaining many of their benefits. Legacy applications continue to run on the untrusted operating system, while a small hypervisor or trusted hardware prevents the operating system from accessing the applications' memory. In this paper, we introduce Controlled Channel attacks, a new type of side channel attack that allows an untrusted operating system to extract large amounts of sensitive information from protected applications on systems like Overshadow, InkTag or Haven. We implement the attacks on Haven and InkTag and demonstrate their power by extracting complete text documents and outlines of JPEG images from widely deployed application libraries.

The cloud computing infrastructure relies on virtualized servers that provide isolation across guest OS’s through sandboxing. This isolation was demonstrated to be imperfect in past work which exploited hardware level information leakages to gain access to sensitive information across co-located virtual machines (VMs). In response virtualization companies and cloud services providers have disabled features such as deduplication to prevent such attacks. In this work, we introduce a fine-grain cross-core cache attack that exploits access time variations on the last level cache. The attack exploits huge pages to work across VM boundaries without requiring deduplication. No configuration changes on the victim OS are needed, making the attack quite viable. Furthermore, only machine co-location is required, while the target and victim OS can still reside on different cores of the machine. Our new attack is a variation of the prime and probe cache attack whose applicability at the time is limited to L1 cache. In contrast, our attack works in the spirit of the flush and reload attack instead targeting the shared L3 cache. Indeed, by adjusting the huge page size our attack can be customized to work virtually at any cache level/size. We demonstrate the viability of the attack by targeting an OpenSSL1.0.1f implementation of AES. The attack recovers AES keys in the cross-VM setting on Xen 4.1 with deduplication disabled, being only slightly less efficient than the flush and reload attack. Given that huge pages are a standard feature enabled in the memory management unit of OS’s and that besides co-location no additional assumptions are needed, the attack we present poses a significant risk to existing cloud servers.

We present an effective implementation of the Prime+Probe side-channel attack against the last-level cache. We measure the capacity of the covert channel the attack creates and demonstrate a cross-core, cross-VM attack on multiple versions of GnuPG. Our technique achieves a high attack resolution without relying on weaknesses in the OS or hypervisor or on sharing memory between attacker and victim.

We identify a timing channel in the floating point instructions of modern x86 processors: the running time of floating point addition and multiplication instructions can vary by two orders of magnitude depending on their operands. We develop a benchmark measuring the timing variability of floating point operations and report on its results. We use floating point data timing variability to demonstrate practical attacks on the security of the Firefox browser (versions 23 through 27) and the Fuzz differentially private database. Finally, we initiate the study of mitigations to floating-point data timing channels with libfixedtimefixedpoint, a new fixed-point, constant-time math library. Modern floating point standards and implementations are sophisticated, complex, and subtle, a fact that has not been sufficiently recognized by the security community. More work is needed to assess the implications of the use of floating-point instructions in security-relevant software. Our attacks show that data timing channels are not a hypothetical threat but a real and pervasive danger to software security. More work is needed to search for, identify, and mitigate data timing channels in popular CPUs and in emerging computing platforms like GPGPUs.

With the general availability of closed-source software for various CPU architectures, there is a need to identify security-critical vulnerabilities at the binary level to perform a vulnerability assessment. Unfortunately, existing bug finding methods fall short in that they i) require source code, ii) only work on a single architecture (typically x86), or iii) rely on dynamic analysis, which is inherently difficult for embedded devices. In this paper, we propose a system to derive bug signatures for known bugs. We then use these signatures to find bugs in binaries that have been deployed on different CPU architectures (e.g., x86 vs. MIPS). The variety of CPU architectures imposes many challenges, such as the incomparability of instruction set architectures between the CPU models. We solve this by first translating the binary code to an intermediate representation, resulting in assignment formulas with input and output variables. We then sample concrete inputs to observe the I/O behavior of basic blocks, which grasps their semantics. Finally, we use the I/O behaviors to find code parts that behave similar to the bug signature, effectively revealing code parts that contain the bug. We have designed and implemented a tool for cross-architecture bug search in executables. Our prototype currently supports three instruction set architectures (x86, ARM, and MIPS) and can find vulnerabilities in buggy binary code for any of these architectures. We show that we can find Heartbleed vulnerabilities, regardless of the underlying software instruction set. Similarly, we apply our method to find backdoors in closed- source firmware images of MIPS- and ARM-based routers.

Vulnerability exploits remain an important mech- anism for malware delivery, despite efforts to speed up the creation of patches and improvements in software updating mech- anisms. Vulnerabilities in client applications are often exploited in spear phishing attacks and cannot be discovered using network vulnerability scanners. Analyzing their lifecycle is challenging because it requires observing the deployment of patches on hosts around the world. Using 5-year data collected on 8.4 million hosts, available through Symantec’s WINE platform, we present the first systematic study of patch deployment in client-side vulnerabilities. Our analysis of the vulnerability lifecycle of 10 popular client applications identifies several new threats presented by multiple installations of the same program and shared libraries that may be distributed with multiple applications. We find that 80 vulnerabilities in our data set affect common code shared by two applications. In these cases, the time between patch releases in the different applications is up to to 118 days (with a median of 11 days). Furthermore, as the patching rates differ between applications, many hosts patch the vulnerability in one application but not in the other one. We demonstrate two novel attacks that enable exploitation by invoking old versions of applications that are used infrequently, but that remain installed. We also find that the patch rate is affected by user-specific and application-specific factors; for example, hosts belonging to security analysts and applications with an automated updating mechanism have significantly lower median times to patch.

Run-time packers are typically used by malware-writers to obfuscate their code and hinder static analysis. The packer problem has been widely studied, and several solutions have been proposed in order to generically unpacked these protected binaries. Nevertheless, these solutions commonly rely on certain assumptions that may not necessarily be met by certain types of packers. In this paper, we propose a taxonomy to measure runtime packer complexity, and evaluate it over two datasets composed of both off-the-shelf packers and custom packed binaries. Also, we propose a set of heuristics to improve the feasibility of multi-path exploration approaches for recovering the code of packers that unprotect their code on demand.

Malicious software are usually obfuscated to avoid detection and resist analysis. When new malware is encountered, such obfuscations have to be penetrated or removed (``deobfuscated'') in order to understand the internal logic of the code and devise countermeasures. This paper discusses a generic approach for deobfuscation of obfuscated executable code. Our approach does not make any assumptions about the nature of the obfuscations used, but instead uses semantics-preserving program transformations to simplify away obfuscation code. We have applied a prototype implementation of our ideas to a variety of different kinds of obfuscation, including emulation-based obfuscation, emulation-based obfuscation with runtime code unpacking, and return-oriented programming. Our experimental results are encouraging and suggest that this approach can be effective in extracting the internal logic from code obfuscated using a variety of obfuscation techniques, including tools such as Themida that previous approaches could not handle.

In this work, we propose a novel way to maximize the number of bugs found for black-box mutational fuzzing given a program and a seed input. The major intuition is to leverage a white-box symbolic analysis on an execution trace for a given program-seed pair to optimize parameters for mutational fuzzing. The result is promising: we found 25% more bugs than the state- of-the-art fuzzers over 8 applications, given a limited resource. We make our code publicly available to foster open science.

Recent advances in hardware design have demonstrated mechanisms allowing a wide range of low-level security policies micro-policies to be expressed using rules on metadata tags. We propose a methodology for defining and reasoning about such tag-based reference monitors in terms of a high-level "symbolic machine," and we use this methodology to define and formally verify micro-policies for dynamic sealing, compartmentalization, control-flow integrity, and memory safety; in addition, we show how to use the tagging mechanism to protect its own integrity. For each micro-policy, we prove by refinement that the symbolic machine instantiated with the policy's rules embodies a high-level specification characterizing a useful security property. Last, we show how the symbolic machine itself can be implemented in terms of a hardware rule cache and a software controller.

Code reuse attacks such as return-oriented programming (ROP) are prevalent and powerful and are widely used to exploit memory corruption vulnerabilities in software programs. Recently, many defenses were proposed to mitigate code reuse attacks, but some of them have already been successfully broken. In this paper, we perform a systematic assessment of recently proposed CFI solutions and other defenses against code reuse attacks in the context of object-oriented languages. We focus on C++ since this programming language is used by a large number of today's most attacked software projects (e.g., web browsers, document viewers, and other programming languages' runtime interpreters). We demonstrate that almost all CFI solutions and many other defenses that do not consider object-oriented C++ semantics can be bypassed in practice. Our novel attack technique, denoted as COOP (counterfeit object-oriented programming), induces malicious program behavior by only invoking chains of a program's existing virtual functions through legitimate call sites. COOP is Turing complete under realistic conditions and we demonstrate its viability by developing complex, real-world exploit codes for Internet Explorer 10 on Windows and Firefox 36 on Linux. We also show that even recently proposed defenses (Code-Pointer Separation, T-VIP, vfGuard, and VTint) that specifically target C++ are vulnerable to COOP. Our observation is that no strong defense against COOP exists today that does not require access to source code, and constructing such a defense seems to be challenging. We believe that our investigation and results are helpful contributions to the design and implementation of future defense systems against the severe threat of control-flow hijacking attacks that has sustained in the wild for more than two decades.

Taint-style vulnerabilities are a persistent problem in software development, as the recently discovered "Heartbleed"vulnerability strikingly illustrates. In this class of vulnerabil- ities, attacker-controlled data is passed unsanitized from an input source to a sensitive sink. While simple instances of this vulnerability class can be detected automatically, more subtle defects involving data flow across several functions or project- specific APIs are mainly discovered by manual auditing. Different techniques have been proposed to accelerate this process by searching for typical patterns of vulnerable code. However, all of these approaches require a security expert to manually model and specify appropriate patterns in practice. In this paper, we propose a method for automatically inferring search patterns for taint-style vulnerabilities in C code. Given a security-sensitive sink, such as a memory function, our method automatically identifies corresponding source-sink systems and constructs patterns that model the data flow and sanitization in these systems. The inferred patterns are expressed as traversals in a code property graph and enable efficiently searching for unsanitized data flows—across several functions as well as with project-specific APIs. We demonstrate the efficacy of this approach in different experiments with 5 open-source projects. The inferred search patterns reduce the amount of code to inspect for finding known vulnerabilities by a factor of 19.5 (94.9%) and also enable us to uncover 8 previously unknown vulnerabilities.

Code-reuse attacks such as return-oriented programming (ROP) pose a severe threat to modern software. Designing practical and effective defenses against code-reuse attacks is highly challenging. One line of defense builds upon fine-grained code diversification to prevent the adversary from constructing a reliable code-reuse attack. However, all solutions proposed so far are either vulnerable to memory disclosure or are impractical for deployment on commodity systems. In this paper, we address the deficiencies of existing solutions and present the first practical, fine-grained code randomization defense, called Readactor, resilient to both static and dynamic ROP attacks. We distinguish between direct memory disclosure, where the attacker reads code pages, and indirect memory disclosure, where attackers use code pointers on data pages to infer the code layout without reading code pages. Unlike previous work, Readactor resists both types of memory disclosure. Moreover, our technique protects both statically and dynamically generated code. We use a new compiler-based code generation paradigm that uses hardware features provided by modern CPUs to enable execute-only memory and hide code pointers from leakage to the adversary. Finally, our extensive evaluation shows that our approach is practical---we protect the entire Google Chromium browser and its V8 JIT compiler---and efficient with an average SPEC CPU2006 performance overhead of only 6.4%.

Memory corruption attacks have been known for decades, but they are still a major vector of attack for compromising modern systems. Numerous defenses have been proposed against memory corruption attacks, but they all have their limitations and weaknesses. Stronger defenses such as complete memory safety incur a large overhead, while weaker ones such as practical control flow integrity have been shown to be ineffective. A recent technique called code pointer integrity (CPI) promises to provide the best of both security and performance worlds, preventing control hijacking attacks while maintaining low overhead. In this paper, we show that the assumptions made by CPI are fundamentally flawed and in fact CPI can be bypassed using existing, known types of vulnerabilities. We show that CPI’s safe region can be leaked and then maliciously modified by using data pointer overwrites. Although many other implementation bugs exist in CPI, for this work we assume the weakest assumptions for the attacker and the strongest implementation of CPI and show that just by controlling the stack, an attacker can easily bypass CPI. Our attack was implemented as a proof-of-concept against Nginx and could successfully bypass CPI in 6 seconds with 13 observed crashes. We also present an attack that generates no crashes and is able to bypass CPI in 98 hours.

The prevalence of security flaws in multiparty online services (e.g., single-sign-on, third-party payment, etc.) calls for rigorous engineering supported by formal program verification. However, the adoption of program verification faces several hurdles in the real world: how to specify security properties given that protocol specifications are often informal and vague; how to precisely model the attacker and the runtime platform; how to deal with the unbounded set of all potential transactions. We introduce Certified Symbolic Transaction (CST), an approach that significantly lowers these hurdles: CST tries to verify a protocol-independent property jointly defined over all parties, thus avoids the burden of individually specifying every party's security property for every protocol; CST invokes static verifications at runtime, i.e., it symbolically verifies every transaction on-the-fly, and thus (1) avoids the burden of modeling the attacker and the runtime platform, (2) reduces the proof obligation from considering all possible transactions to considering only the one at hand. We have applied CST on five commercially deployed applications, and show that, with only tens (or 100+) of lines of code changes per party, the original implementations are enhanced to be provably secure. Our security analysis shows that 12 out of 14 logic vulnerabilities reported in the literature will be prevented by CST. We also stress-tested CST by building a gambling system integrating four different services, for which there is no existing protocol to follow. Because transactions are symbolic and cacheable, CST has near-zero amortized runtime overhead. We make the source code of these implementations public, which are ready to be deployed for real-world uses.

Cloud storage services such as Amazon S3, DropBox, Google Drive and Microsoft OneDrive have become increasingly pop- ular. However, users may be reluctant to completely trust a cloud service. Current proposals in the literature to protect the confidentiality, integrity and consistency of data stored in the cloud all have shortcomings when used on battery-powered devices – they either require devices to be on longer so they can communicate directly with each other, rely on a trusted service to relay messages, or cannot provide timely detection of attacks. We propose Caelus, which addresses these shortcoming. The key insight that enables Caelus to do this is having the cloud service declare the timing and order of operations on the cloud service. This relieves Caelus devices from having to record and send the timing and order of operations to each other – instead, they need to only ensure that the timing and order of operations both conforms to the cloud’s promised consistency model and that it is perceived identically on all devices. In addition, we show that Caelus is general enough to support popular consistency models such as strong, eventual and causal consistency. Our experiments show that Caelus can detect consistency violations on Amazon’s S3 service when the desired consistency requirements set by the user are stricter than what S3 provides. Caelus achieves this with a roughly 12.6% increase in CPU utilization on clients, 1.3% of network bandwidth overhead and negligible impact on the battery life of devices.

Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like memory accesses. Alas, the induced slowdown usually exceeds by a wide margin what system users are willing to tolerate in production, so these tools are hardly ever used. As a result, the insecurity of real-world systems persists. We present an approach in which developers/operators can specify what level of overhead they find acceptable for a given workload (e.g., 5%); our proposed tool ASAP then automatically instruments the program to maximize its security while staying within the specified "overhead budget." Two insights make this approach effective: most overhead in existing tools is due to only a few "hot" checks, whereas the checks most useful to security are typically "cold"and cheap. We evaluate ASAP on programs from the Phoronix and SPEC benchmark suites. It can precisely select the best points in the security-performance spectrum. Moreover, we analyzed existing bugs and security vulnerabilities in RIPE, OpenSSL, and the Python interpreter, and found that the protection level offered by the ASAP approach is sufficient to protect against all of them.

Modern web applications make frequent use of third-party scripts, often in ways that allow scripts loaded from external servers to make unrestricted changes to the embedding page and access critical resources including private user information. In this paper, we describe tools we developed to assist site administrators in understanding, monitoring, and restricting the behavior of third-party scripts embedded in their site. We developed a modified browser that can intercept, record, and check third-party script accesses to critical resources against security policies, along with a Visualizer tool that allows users to conveniently view recorded script behaviors and candidate policies and a PolicyGenerator tool that aids script providers and site administrators in writing policies. Site administrators can manually refine these policies with minimal effort to produce policies that effectively and robustly limit the behavior of embedded scripts. PolicyGenerator is able to generate effective policies for all scripts embedded on 72 out of the 100 test sites with minor human assistance. In this paper, we present the designs of our tools, report on what we've learned about script behaviors using them, evaluate the value of our approach for website administrators.

Mobile applications can access various sensitive personal data stored on mobile devices. This gives rise to threats of data leaks. App auditing is a fundamental program analysis task to reveal data-leaking code paths. Currently, static analysis is the de facto technique in use since it can pinpoint problematic data flows in the whole program. However, static analysis generates false alarms for being over-estimating and requires manual validation. Also existing approaches need minutes or even hours to examine an app, which causes obstacles to be used on mobile devices or development machines and requires lots of resources for market-scale use cases. To overcome these limitations, we design AppAudit to use an efficient but over-estimating static API analysis first and then relies on a dynamic analysis to prune its false positives. Overall, AppAudit achieves a low false positive rate as the dynamic analysis only explores possible code paths during real execution. AppAudit also achieves short analysis time by combining an efficient static stage with a highly parallelizable dynamic stage. AppAudit enables three important use cases with its improved accuracy and performance. First, market operators can get rid of tedious human checks and fully automate the app auditing task with fewer resources than before. Second, app developers can quickly perform self-check before publishing apps, to avoid using data-leaking 3rd-party libraries. Third, mobile users can scan an app from untrusted sources before installation and get real-time auditing results. We apply AppAudit to more than 1,000 known malware and 400 real apps from various markets. Overall, AppAudit reports as many data leaks as existing approaches, while eliminating all false positives, being 8.3x faster and using 90% less memory. AppAudit also uncovers 30 data leaks in real apps and reveals the common properties behind these leaks. We find that most leaks are caused by 3rd-party advertising libraries and they commonly utilize HTTP requests to leak data. We believe AppAudit serves as an effective tool to annihilate data-leaking apps and provides guidance to design promising runtime techniques against data leaks.

Mobile applications are part of the everyday lives of billions of people, who often trust them with sensitive information (for example, banking apps). These users identify the currently focused app solely by its visual appearance, since the GUIs of the most popular mobile OSes do not show any trusted indication of the app origin. In this paper, we analyze in detail the many ways in which Android users can be confused into misidentifying an app, thus, for instance, being deceived into giving sensitive information to a malicious app. Our analysis of the Android platform APIs, assisted by an automated state-exploration tool, led us to identify and categorize a variety of attack vectors (some previously known, others novel, such as a non-escapable fullscreen overlay) that allow a malicious app to surreptitiously replace or mimic the GUI of other apps and mount phishing and click-jacking attacks. Limitations in the system GUI make these attacks significantly harder to notice than on a desktop, leaving users completely defenseless against them. To mitigate GUI attacks, we have developed a two-layer defense. To detect malicious apps at the market level, we developed a tool that uses static analysis to identify code that could launch UI confusion attacks. We show how this tool detects apps that might launch GUI attacks, such as ransomware programs. Since these attacks are meant to confuse humans, we have also designed and implemented an on-device defense that addresses the underlying issue of the lack of a security indicator in the Android GUI. We add such an indicator to the system navigation bar; this indicator securely informs the user about the origin of the app that the user is interacting with (e.g., the PayPal app is backed by ``PayPal, Inc.''). We demonstrate the effectiveness of our attacks and the proposed on-device defense with a user study involving 250 human subjects, whose ability to detect our attack increased significantly when using a system equipped with our defense.

Stealing of sensitive information from apps is always considered to be one of the most critical threats to Android security. Recent studies show that this can happen even to the apps without explicit implementation flaws, through exploiting some design weaknesses of the operating system, e.g., shared communication channels such as audio and Bluetooth, and side channels like CPU, memory, network-data usages, etc. In all these attacks, a malicious app needs to run side-by-side with the target app (the victim) to collect its runtime information. Examples include recording phone conversations from the phone app, gathering network-data usages of WebMD to infer the disease condition the user looks at, etc. This runtime-information-gathering (RIG) threat is both realistic and serious, as demonstrated by prior research and our new findings, which reveal that the adversary monitoring daily operations of popular Android-based home security systems can easily figure out when the house is empty and the user is not looking at surveillance cameras, and even turn off the alarm delivered to the user's phone. To defend against this new category of attacks, we propose a novel technique that changes neither the operating system nor the target apps, and provides immediate protection as soon as an ordinary app (with only normal and dangerous permissions) is installed. This new approach, called App Guardian, thwarts a malicious app's runtime monitoring attempt by pausing all suspicious background processes when the target app (called principal) is running in the foreground, and resuming them after the app stops and its runtime environment is cleaned up. Our technique leverages a unique feature of Android, on which third-party apps running in the background are often considered to be disposable and can be stopped anytime with only a minor performance and utility implication. We further limit such an impact by only focusing on a small set of suspicious background apps, which are identified based upon their behaviors inferred from their side channels, such as thread names, CPU scheduling data and kernel time. App Guardian is also carefully designed to choose the right moments to start and end the protection procedure, and effectively protect itself against malicious apps. Our experimental studies show that this new technique defeated all known RIG attacks, ranging from phone taping to keylogging through various side channels. In the meantime, the inconvenience it introduces is found to be minimal, with negligible impacts on the utility of legitimate apps and the performance of the OS.