Computer Security – ESORICS 2009

We examine some known attacks on the PIN verification framework, based on weaknesses of the security API for the tamper-resistant Hardware Security Modules used in the network. We specify this API in an imperative language with cryptographic primitives, and show how its flaws are captured by a notion of robustness that extends the one of Myers, Sabelfeld and Zdancewic to our cryptographic setting. We propose an improved API, give an extended type system for assuring integrity and for preserving confidentiality via randomized and non-randomized encryptions, and show our new API to be type-checkable.

Noninterference requires that public outputs of a program must be completely independent from secrets. While this ensures that secrets cannot be leaked, it is too restrictive for many applications. For instance, the output of a knowledge-based authentication mechanism needs to reveal whether an input matches the secret password. The research problem is to allow such exceptions without giving up too much. Though a number of solutions has been developed, the problem is not yet satisfactorily solved. In this article, we propose a framework to control what information is declassified. Our contributions include a policy language, a semantic characterization of information flow security, and a sound security type system. The main technical novelty is the explicit treatment of so called reference points, which allows us to offer substantially more flexible control of what is released than in existing approaches.

This paper explores the problem of tracking information flow in dynamic tree structures. Motivated by the problem of manipulating the Document Object Model (DOM) trees by browser-run client-side scripts, we address the dynamic nature of interactions via tree structures. We present a runtime enforcement mechanism that monitors this interaction and prevents a range of attacks, some of them missed by previous approaches, that exploit the tree structure in order to transfer sensitive information. We formalize our approach for a simple language with DOM-like tree operations and show that the monitor prevents scripts from disclosing secrets.

Accountability mechanisms, which rely on after-the-fact verification, are an attractive means to enforce authorization policies. In this paper, we describe an operational model of accountability-based distributed systems. We describe analyses which support both the design of accountability systems and the validation of auditors for finitary accountability systems. Our study provides formal foundations to explore the tradeoffs underlying the design of accountability systems including: the power of the auditor, the efficiency of the audit protocol, the requirements placed on the agents, and the requirements placed on the communication infrastructure.

Many protocols rely on audit trails to allow an impartial judge to verify

a posteriori

some property of a protocol run. However, in current practice the choice of what data to log is left to the programmer’s intuition, and there is no guarantee that it constitutes enough evidence. We give a precise definition of auditability and we show how typechecking can be used to statically verify that a protocol always logs enough evidence. We apply our approach to several examples, including a full-scale auction-like protocol programmed in ML.

By shifting the burden of proofs to the user, a proof-carrying authorization (PCA) system can automatically enforce complex access control policies. Unfortunately, managing those proofs can be a daunting task for the user. In this paper we develop a Bash-like language, PCAL, that can automate correct and efficient use of a PCA interface. Given a PCAL script, the PCAL compiler tries to statically construct the proofs required for executing the commands in the script, while re-using proofs to the extent possible and rewriting the script to construct the remaining proofs dynamically. We obtain a formal guarantee that if the policy does not change between compile time and run time, then the compiled script cannot fail due to access checks at run time.

Separation of Duties (SoD) aims to prevent fraud and errors by distributing tasks and associated privileges among multiple users. Li and Wang proposed an algebra (SoDA) for specifying SoD requirements, which is both expressive in the requirements it formalizes and abstract in that it is not bound to any specific workflow model. In this paper, we both generalize SoDA and map it to enforcement mechanisms. First, we increase SoDA’s expressiveness by extending its semantics to multisets. This better suits policy enforcement over workflows, where users may execute multiple tasks. Second, we further generalize SoDA to allow for changing role assignments. This lifts the strong restriction that authorizations do not change during workflow execution. Finally, we map SoDA terms to CSP processes, taking advantage of CSP’s operational semantics to provide the critical link between abstract specifications of SoD requirements by SoDA terms and runtime-enforcement mechanisms.

We study attribute-based access control for resource sharing in collaborative work environments. The goal of our work is to encourage sharing within an organization by striking a balance between usability and security. Inspired by the great success of a number of collaboration-based Web 2.0 systems, such as Wikipedia and Del.icio.us, we propose a novel attribute-based access control framework that acquires information on users’ attributes from the collaborative efforts of all users in a system, instead of from a small number of trusted agents. Intuitively, if several users say that someone has a certain attribute, our system believes that the latter indeed has the attribute. In order to allow users to specify and maintain the attributes of each other, we employ the mechanism of people-tagging, where users can tag each other with the terms they want, and tags from different users are combined and viewable by all users in the system. In this article, we describe the system framework of our solution, propose a language to specify access control policies, and design an example-based policy specification method that is friendly to ordinary users. We have implemented a prototype of our solution based on a real-world and large-scale people-tagging system in IBM. Experiments have been performed on the data collected by the system.

Inference control aims at disabling a participant to gain a piece of information to be kept confidential. Considering a provider-client architecture for information systems, we present transaction-based protocols for provider-client interactions and prove that the incorporated inference control performed by the provider is effective indeed. The interactions include the provider answering a client’s query and processing update requests of two forms. Such a request is either initiated by the provider and thus possibly to be forwarded to clients in order to refresh their views, or initiated by a client according to his view and thus to be translated to the repository maintained by the provider.

Recent years have seen unprecedented growth in the popularity of social network systems, with Facebook being an archetypical example. The access control paradigm behind the privacy preservation mechanism of Facebook is distinctly different from such existing access control paradigms as Discretionary Access Control, Role-Based Access Control, Capability Systems, and Trust Management Systems. This work takes a first step in deepening the understanding of this access control paradigm, by proposing an access control model that formalizes and generalizes the privacy preservation mechanism of Facebook. The model can be instantiated into a family of Facebook-style social network systems, each with a recognizably different access control mechanism, so that Facebook is but one instantiation of the model. We also demonstrate that the model can be instantiated to express policies that are not currently supported by Facebook but possess rich and natural social significance. This work thus delineates the design space of privacy preservation mechanisms for Facebook-style social network systems, and lays out a formal framework for policy analysis in these systems.

Many RFID authentication protocols with randomized tag response have been proposed to avoid simple tag tracing. These protocols are symmetric in common due to the lack of computational power to perform expensive asymmetric cryptography calculations in low-cost tags. Protocols with constantly changing tag key have also been proposed to avoid more advanced tag tracing attacks. With both the symmetric and constant-changing properties, tag and reader re-synchronization is unavoidable as the key of a tag can be made desynchronized with the reader due to offline attacks or incomplete protocol runs. In this paper, our contribution is to classify these synchronized RFID authentication protocols into different types and then examine their highest achievable levels of privacy protections using the privacy model proposed by Vaudenay in Asiacrypt 2007 and later extended by Ng et al. in ESORICS 2008. Our new privacy results show the separation between

weak privacy

and

narrow-forward privacy

in these protocols, which effectively fills the missing relationship of these two privacy levels in Vaudenay’s paper and answer the question raised by Paise and Vaudenay in ASIACCS 2008 on why they cannot find a candidate protocol that can achieve both privacy levels at the same time. We also show that

forward privacy

is impossible with these synchronized protocols.

Channels are an abstraction of the many concrete techniques to enforce particular properties of message transmissions such as encryption. We consider here three basic kinds of channels—authentic, confidential, and secure—where agents may be identified by pseudonyms rather than by their real names. We define the meaning of channels

as assumptions

, i.e. when a protocol relies on channels with particular properties for the transmission of some of its messages. We also define the meaning of channels as

goals

, i.e. when a protocol aims at establishing a particular kind of channel. This gives rise to an interesting question: given that we have verified that a protocol

P

2

provides its goals under the assumption of a particular kind of channel, can we then replace the assumed channel with an arbitrary protocol

P

1

that provides such a channel? In general, the answer is negative, while we prove that under certain restrictions such a compositionality result is possible.

Cloud Computing has been envisioned as the next-generation architecture of IT Enterprise. It moves the application software and databases to the centralized large data centers, where the management of the data and services may not be fully trustworthy. This unique paradigm brings about many new security challenges, which have not been well understood. This work studies the problem of ensuring the integrity of data storage in Cloud Computing. In particular, we consider the task of allowing a third party auditor (TPA), on behalf of the cloud client, to verify the integrity of the dynamic data stored in the cloud. The introduction of TPA eliminates the involvement of client through the auditing of whether his data stored in the cloud is indeed intact, which can be important in achieving economies of scale for Cloud Computing. The support for data dynamics via the most general forms of data operation, such as block modification, insertion and deletion, is also a significant step toward practicality, since services in Cloud Computing are not limited to archive or backup data only. While prior works on ensuring remote data integrity often lacks the support of either public verifiability or dynamic data operations, this paper achieves both. We first identify the difficulties and potential security problems of direct extensions with fully dynamic data updates from prior works and then show how to construct an elegant verification scheme for seamless integration of these two salient features in our protocol design. In particular, to achieve efficient data dynamics, we improve the Proof of Retrievability model [1] by manipulating the classic Merkle Hash Tree (MHT) construction for block tag authentication. Extensive security and performance analysis show that the proposed scheme is highly efficient and provably secure.

Content Delivery Networks (CDNs) are commonly believed to offer their customers protection against application-level denial of service (DoS) attacks. Indeed, a typical CDN with its vast resources can absorb these attacks without noticeable effect. This paper uncovers a vulnerability which not only allows an attacker to penetrate CDN’s protection, but to actually use a content delivery network to amplify the attack against a customer Web site. We show that leading commercial CDNs – Akamai and Limelight – and an influential research CDN – Coral – can be recruited for this attack. By mounting an attack against our own Web site, we demonstrate an order of magnitude attack amplification though leveraging the Coral CDN. We present measures that both content providers and CDNs can take to defend against our attack. We believe it is important that CDN operators and their customers be aware of this attack so that they could protect themselves accordingly.

Current techniques for the formal modeling analysis of DoS attacks do not adequately deal with

amplification attacks

that may target a complex distributed system as a whole rather than a specific server. Such threats have emerged for important applications such as the VoIP Session Initiation Protocol (SIP). We demonstrate a model-checking technique for finding amplification threats using a strategy we call

measure checking

that checks for a quantitative assessment of attacker impact using term rewriting. We illustrate the effectiveness of this technique with a study of SIP. In particular, we show how to automatically find known attacks and verify that proposed patches for these attacks achieve their aim. Beyond this, we demonstrate a new amplification attack based on the compromise of one or more SIP proxies. We show how to address this threat with a protocol change and formally analyze the effectiveness of the new protocol against amplification attacks.

We present a traffic analysis of the ADU anonymity scheme presented at ESORICS 2008, and the related RADU scheme. We show that optimal attacks are able to de-anonymize messages more effectively than believed before. Our analysis applies to single messages as well as long term observations using multiple messages. The search of a “better” scheme is bound to fail, since we prove that the original Crowds anonymity system provides the best security for any given mean messaging latency. Finally we present

D

-Crowds, a scheme that supports any path length distribution, while leaking the least possible information, and quantify the optimal attacks against it.

Diagnostic and classification algorithms play an important role in data analysis, with applications in areas such as health care, fault diagnostics, or benchmarking. Branching programs (BP) is a popular representation model for describing the underlying classification/diagnostics algorithms. Typical application scenarios involve a client who provides data and a service provider (server) whose diagnostic program is run on client’s data. Both parties need to keep their inputs private.

We present new, more efficient privacy-protecting protocols for remote evaluation of such classification/diagnostic programs. In addition to efficiency improvements, we generalize previous solutions – we securely evaluate private linear branching programs (LBP), a useful generalization of BP that we introduce. We show practicality of our solutions: we apply our protocols to the privacy-preserving classification of medical ElectroCardioGram (ECG) signals and present implementation results. Finally, we discover and fix a subtle security weakness of the most recent remote diagnostic proposal, which allowed malicious clients to learn partial information about the program.

We put forward a novel paradigm for preserving privacy in data outsourcing which departs from encryption. The basic idea behind our proposal is to involve the owner in storing a limited portion of the data, and maintaining all data (either at the owner or at external servers) in the clear. We assume a relational context, where the data to be outsourced is contained in a relational table. We then analyze how the relational table can be fragmented, minimizing the load for the data owner. We propose several metrics and present a general framework capturing all of them, with a corresponding algorithm finding a heuristic solution to a family of NP-hard problems.

A range of attacks on network components, such as algorithmic denial-of-service attacks and cryptanalysis via timing attacks, are enabled by data structures for which an adversary can predict the durations of operations that he will induce on the data structure. In this paper we introduce the problem of designing data structures that confound an adversary attempting to predict the timing of future operations he induces, even if he has adaptive and exclusive access to the data structure and the timings of past operations. We also design a data structure for implementing a set (supporting membership query, insertion, and deletion) that exhibits timing unpredictability and that retains its efficiency despite adversarial attacks. To demonstrate these advantages, we develop a framework by which an adversary tracks a probability distribution on the data structure’s state based on the timings it emitted, and infers invocations to meet his attack goals.

As the number and scope of government regulations and rules mandating trustworthy retention of data keep growing, businesses today are facing a higher degree of regulation and accountability than ever. Existing compliance storage solutions focus on providing WORM (Write-Once Read-Many) support and rely on software enforcement of the WORM property, due to performance and cost reasons. Such an approach, however, offers limited protection in the regulatory compliance setting where the threat of insider attacks is high and the data is indexed and dynamically updated (e.g., append-only access logs indexed by the creator). In this paper, we propose a solution that can greatly improve the trustworthiness of a compliance storage system, by reducing the scope of trust in the system to a tamper-resistant Trusted Computing Base (TCB). We show how trustworthy retention and verification of append-only data can be achieved through the TCB. Due to the resource constraints on the TCB, we develop a novel authentication data structure that we call Homomorphic Hash Tree (HHT). HHT drastically reduces the TCB workload. Our experimental results demonstrate the effectiveness of our approach.

Collision-intractable hashing is an important cryptographic primitive with numerous applications including efficient integrity checking for transmitted and stored data, and software. In several of these applications, it is important that in addition to detecting corruption of the data we also localize the corruptions. This motivates us to introduce and investigate the new notion of

corruption-localizing hashing

, defined as a natural extension of collision-intractable hashing. Our main contribution is in formally defining corruption-localizing hash schemes and designing two such schemes, one starting from any collision-intractable hash function, and the other starting from any collision-intractable keyed hash function. Both schemes have attractive efficiency properties in three important metrics: localization factor, tag length and localization running time, capturing the quality of localization, and performance in terms of storage and time complexity, respectively. The closest previous results, when modified to satisfy our formal definitions, only achieve similar properties in the case of a single corruption.

We study methods that allow web sites to safely combine JavaScript from untrusted sources. If implemented properly, filters can prevent dangerous code from loading into the execution environment, while rewriting allows greater expressiveness by inserting run-time checks.

Wrapping properties of the execution environment can prevent misuse without requiring changes to imported JavaScript. Using a formal semantics for the ECMA 262-3 standard language, we prove security properties of a subset of JavaScript, comparable in expressiveness to Facebook FBJS, obtained by combining three isolation mechanisms. The isolation guarantees of the three mechanisms are interdependent, with rewriting and wrapper functions relying on the absence of JavaScript constructs eliminated by language filters.

Online advertising has been suffering serious click fraud problem. Fraudulent publishers can generate false clicks using malicious scripts embedded in their web pages. Even widely-used security techniques like

iframe

cannot prevent such attack. In this paper, we propose a framework and associated methodologies to automatically and quickly detect and filter false clicks generated by malicious scripts. We propose to create an impression-click identifier which is able to link corresponding impressions and clicks together with a predefined lifetime. The impression-click identifiers are stored in a special data structure and can be later validated upon a click is received. The framework has the nice features of constant-time inserting and querying, low false positive rate and low quantifiable false negative rate. From our experimental evaluation on a primitive PC machine, our approach can achieve a false negative rate 0.00008 using 120MB memory and average inserting and querying time is 3 and 1 microseconds, respectively.

Cross-site scripting (XSS) vulnerabilities make it possible for worms to spread quickly to a broad range of users on popular Web sites. To date, the detection of XSS worms has been largely unexplored. This paper proposes the first purely client-side solution to detect XSS worms. Our insight is that an XSS worm must spread from one user to another by reconstructing and propagating its payload. Our approach prevents the propagation of XSS worms by monitoring outgoing requests that send self-replicating payloads. We intercept all HTTP requests on the client side and compare them with currently embedded scripts. We have implemented a cross-platform Firefox extension that is able to detect all existing self-replicating XSS worms that propagate on the client side. Our test results show that it incurs low performance overhead and reports no false positives when tested on popular Web sites.

Several generic constructions for transforming one-way functions to asymmetric encryption schemes have been proposed. One-way functions only guarantee the weak secrecy of their arguments. That is, given the image by a one-way function of a random value, an adversary has only negligible probability to compute this random value. Encryption schemes must guarantee a stronger secrecy notion. They must be at least resistant against indistinguishability-attacks under chosen plaintext text (IND-CPA). Most practical constructions have been proved in the random oracle model (ROM for short). Such computational proofs turn out to be complex and error prone. Bana et al. have introduced

Formal Indistinguishability Relations (FIR)

, as an abstraction of computational indistinguishability. In this paper, we extend the notion of FIR to cope with the ROM on one hand and adaptive adversaries on the other hand. Indeed, when dealing with hash functions in the ROM and one-way functions, it is important to correctly abstract the notion of weak secrecy. Moreover, one needs to extend frames to include adversaries in order to capture security notions as IND-CPA. To fix these problems, we consider pairs of formal indistinguishability relations and

formal non-derivability relations

. We provide a general framework along with general theorems, that ensure soundness of our approach and then we use our new framework to verify several examples of encryption schemes among which the construction of Bellare Rogaway and Hashed ElGamal.

We propose a probabilistic contract signing protocol that achieves balance even in the presence of an adversary that may delay messages sent over secure channels. To show that this property holds in a computational setting, we first propose a probabilistic framework for protocol analysis, then prove that in a symbolic setting the protocol satisfies a probabilistic alternating-time temporal formula expressing balance, and finally establish a general result stating that the validity of formulas such as our balance formula is preserved when passing from the symbolic to a computational setting. The key idea of the protocol is to take a “gradual commitment” approach.

In distributed systems users need to share sensitive objects with others based on the recipients’ ability to satisfy a policy. Attribute-Based Encryption (ABE) is a new paradigm where such policies are specified and cryptographically enforced in the encryption algorithm itself. Ciphertext-Policy ABE (CP-ABE) is a form of ABE where policies are associated with encrypted data and attributes are associated with keys. In this work we focus on improving the flexibility of representing user attributes in keys. Specifically, we propose Ciphertext Policy Attribute Set Based Encryption (CP-ASBE) - a new form of CP-ABE - which, unlike existing CP-ABE schemes that represent user attributes as a monolithic set in keys, organizes user attributes into a recursive set based structure and allows users to impose dynamic constraints on how those attributes may be combined to satisfy a policy. We show that the proposed scheme is more versatile and supports many practical scenarios more naturally and efficiently. We provide a prototype implementation of our scheme and evaluate its performance overhead.

Security APIs are used to define the boundary between trusted and untrusted code. The security properties of existing APIs are not always clear. In this paper, we give a new generic API for managing symmetric keys on a trusted cryptographic device. We state and prove security properties for our API. In particular, our API offers a high level of security even when the host machine is controlled by an attacker.

Our API is generic in the sense that it can implement a wide variety of (symmetric key) protocols. As a proof of concept, we give an algorithm for automatically instantiating the API commands for a given key management protocol. We demonstrate the algorithm on a set of key establishment protocols from the Clark-Jacob suite.

In this paper, we propose a novel ID-based secure distance bounding protocol. Unlike traditional secure distance measurement protocols, our protocol is based on standard insecure distance measurement as elemental building block, and enables the implementation of secure distance bounding using commercial off-the-shelf (COTS) ranging devices. We use the proposed protocol to implement secure radio frequency (RF) Time-of-Arrival (ToA) distance measurements on an ultra-wideband (UWB) ranging platform. Based on this, we implement Verifiable Multilateration — a secure localization scheme that enables the computation of a correct device location in the presence of an adversary. To the best of our knowledge, this is the first implementation of an RF ToA secure localization system.

We present a formal model for stateful security protocols. This model is used to define ownership and ownership transfer as concepts as well as security properties. These definitions are based on an intuitive notion of ownership related to physical ownership. They are aimed at RFID systems, but should be applicable to any scenario sharing the same intuition of ownership.

We discuss the connection between ownership and the notion of desynchronization resistance and give the first formal definition of the latter. We apply our definitions to existing RFID protocols, exhibiting attacks on desynchronization resistance, secure ownership, and secure ownership transfer.

There are increasing deployments of networked embedded systems and rising threats of malware intrusions on such systems. To mitigate this threat, it is desirable to enable commonly-used embedded processors known as flash MCUs to provide remote attestation assurances like the Trusted Platform Module (TPM) provides for PCs. However, flash MCUs have special limitations concerning cost, power efficiency, computation, and memory that influence how this goal can be achieved. Moreover, many types of applications require integrity guarantees for the system over an interval of time rather than just at a given instant. The aim of this paper is to demonstrate how an architecture we call a

Cumulative Attestation Kernel (CAK)

can address these concerns by providing cryptographically secure firmware auditing on networked embedded systems. To illustrate the value of CAKs, we demonstrate practical remote attestation for Advanced Metering Infrastructure (AMI), a core technology in emerging smart power grid systems that requires cumulative integrity guarantees. To this end, we show how to implement a CAK in less than one quarter of the memory available on low end AVR32 flash MCUs similar to those used in AMI deployments. We analyze one of the specialized features of such applications by formally proving that remote attestation requirements are met by our implementation even if no battery backup is available to prevent sudden halt conditions.

Authenticated dictionaries allow users to send lookup requests to an untrusted server and get authenticated answers. Persistent authenticated dictionaries (PADs) add queries against historical versions. We consider a variety of different trust models for PADs and we present several extensions, including support for aggregation and a rich query language, as well as hiding information about the order in which PADs were constructed. We consider variations on tree-like data structures as well as a design that improves efficiency by speculative future predictions. We improve on prior constructions and feature two designs that can authenticate historical queries with constant storage per update and several designs that can return constant-sized authentication results.

Interest in role-based access control has generated considerable research activity in recent years. A number of interesting problems related to the well known set cover problem have come to light as a result of this activity. However, the computational complexity of some of these problems is still not known. In this paper, we explore some variations on the set cover problem and use these variations to establish the computational complexity of these problems. Most significantly, we introduce the minimal cover problem – a generalization of the set cover problem – which we use to determine the complexity of the inter-domain role mapping problem.