Dreyer D.,MPI SWS |
Neis G.,MPI SWS |
Birkedal L.,IT University of Copenhagen
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP | Year: 2010
Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages - languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the "semantic cube": fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences. In this paper, we marry the aspirations of the semantic cube to the powerful proof method of step-indexed Kripke logical relations. Building on recent work of Ahmed, Dreyer, and Rossberg, we define the first fully abstract logical relation for an ML-like language with recursive types, abstract types, general references and call/cc. We then show how, under orthogonal restrictions to the expressive power our language - namely, the restriction to first-order state and/or the removal of call/cc - we can enhance the proving power of our possible-worlds model in correspondingly orthogonal ways, and we demonstrate this proving power on a range of interesting examples. Central to our story is the use of state transition systems to model the way in which properties of local state evolve over time. © 2010 ACM.
Vafeiadis V.,MPI SWS |
Zappa Nardelli F.,French Institute for Research in Computer Science and Automation
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | Year: 2011
We consider simple compiler optimisations for removing redundant memory fences in programs running on top of the x86-TSO relaxed memory model. While the optimisations are performed using standard thread-local control flow analyses, their correctness is subtle and relies on a non-standard global simulation argument. The implementation and the proof of correctness are programmed in Coq as part of CompCertTSO, a fully-fledged certified compiler from a concurrent extension of a C-like language to x86 assembler. In this article, we describe the soundness proof of the optimisations and evaluate their effectiveness. © 2011 Springer-Verlag Berlin Heidelberg.
Liu Y.,Northeastern University |
Gummadi K.P.,MPI SWS |
Krishnamurthy B.,At And T Labs Research |
Mislove A.,Northeastern University
Proceedings of the ACM SIGCOMM Internet Measurement Conference, IMC | Year: 2011
The sharing of personal data has emerged as a popular activity over online social networking sites like Facebook. As a result, the issue of online social network privacy has received significant attention in both the research literature and the mainstream media. Our overarching goal is to improve defaults and provide better tools for managing privacy, but we are limited by the fact that the full extent of the privacy problem remains unknown; there is little quantification of the incidence of incorrect privacy settings or the difficulty users face when managing their privacy. In this paper, we focus on measuring the disparity between the desired and actual privacy settings, quantifying the magnitude of the problem of managing privacy. We deploy a survey, implemented as a Facebook application, to 200 Facebook users recruited via Amazon Mechanical Turk. We find that 36% of content remains shared with the default privacy settings. We also find that, overall, privacy settings match users' expectations only 37% of the time, and when incorrect, almost always expose content to more users than expected. Finally, we explore how our results have potential to assist users in selecting appropriate privacy settings by examining the user-created friend lists. We find that these have significant correlation with the social network, suggesting that information from the social network may be helpful in implementing new tools for managing privacy. © 2011 ACM.
Backes M.,Saarland University |
Fiore D.,MPI SWS |
Reischuk R.M.,Saarland University
Proceedings of the ACM Conference on Computer and Communications Security | Year: 2013
We address the problem in which a client stores a large amount of data with an untrusted server in such a way that, at any moment, the client can ask the server to compute a function on some portion of its outsourced data. In this scenario, the client must be able to efficiently verify the correctness of the result despite no longer knowing the inputs of the delegated computation, it must be able to keep adding elements to its remote storage, and it does not have to fix in advance (i.e., at data outsourcing time) the functions that it will delegate. Even more ambitiously, clients should be able to verify in time independent of the input-size - a very appealing property for computations over huge amounts of data. In this work we propose novel cryptographic techniques that solve the above problem for the class of computations of quadratic polynomials over a large number of variables. This class covers a wide range of significant arithmetic computations - notably, many important statistics. To confirm the efficiency of our solution, we show encouraging performance results, e.g., correctness proofs have size below 1 kB and are verifiable by clients in less than 10 milliseconds. © 2013 ACM.
Alvisi L.,University of Texas at Austin |
Clement A.,MPI SWS |
Epasto A.,University of Rome La Sapienza |
Lattanzi S.,Google |
Panconesi A.,University of Rome La Sapienza
Proceedings - IEEE Symposium on Security and Privacy | Year: 2013
Sybil attacks in which an adversary forges a potentially unbounded number of identities are a danger to distributed systems and online social networks. The goal of sybil defense is to accurately identify sybil identities. This paper surveys the evolution of sybil defense protocols that leverage the structural properties of the social graph underlying a distributed system to identify sybil identities. We make two main contributions. First, we clarify the deep connection between sybil defense and the theory of random walks. This leads us to identify a community detection algorithm that, for the first time, offers provable guarantees in the context of sybil defense. Second, we advocate a new goal for sybil defense that addresses the more limited, but practically useful, goal of securely white-listing a local region of the graph. © 2013 IEEE.
Nanevski A.,IMDEA Madrid Institute for Advanced Studies |
Banerjee A.,IMDEA Madrid Institute for Advanced Studies |
Garg D.,MPI SWS
ACM Transactions on Programming Languages and Systems | Year: 2013
We present Relational Hoare Type Theory (RHTT), a novel language and verification system capable of expressing and verifying rich information flow and access control policies via dependent types. We show that a number of security policies which have been formalized separately in the literature can all be expressed in RHTT using only standard type-theoretic constructions such as monads, higher-order functions, abstract types, abstract predicates, and modules. Example security policies include conditional declassification, information erasure, and state-dependent information flow and access control. RHTT can reason about such policies in the presence of dynamic memory allocation, deallocation, pointer aliasing and arithmetic.©2013 ACM 0164-0925/2013/07-ART7 $15.00.
Sevcik J.,Microsoft |
Vafeiadis V.,MPI SWS |
Nardelli F.Z.,French Institute for Research in Computer Science and Automation |
Jagannathan S.,Purdue University |
Sewell P.,University of Cambridge
Journal of the ACM | Year: 2013
In this article, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation on x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behavior of the hardware, the effects of compiler optimization on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified compilation both essential and challenging. We describe ClightTSO, a concurrent extension of CompCert's Clight in which the TSO-based memory model of x86 multiprocessors is exposed for high-performance code, and CompCertTSO, a formally verified compiler from ClightTSO to x86 assembly language, building on CompCert. CompCertTSO is verified in Coq: for any well-behaved and successfully compiled ClightTSO source program, any permitted observable behavior of the generated assembly code (if it does not run out of memory) is also possible in the source semantics. We also describe some verified fence-elimination optimizations, integrated into CompCertTSO. © ACM 2013.
Ganty P.,IMDEA Madrid Institute for Advanced Studies |
Majumdar R.,MPI SWS
ACM Transactions on Programming Languages and Systems | Year: 2012
Asynchronous programming is a ubiquitous systems programming idiom for managing concurrent interactions with the environment. In this style, instead of waiting for time-consuming operations to complete, the programmer makes a non-blocking call to the operation and posts a callback task to a task buffer that is executed later when the time-consuming operation completes. A cooperative scheduler mediates the interaction by picking and executing callback tasks from the task buffer to completion (and these callbacks can post further callbacks to be executed later). Writing correct asynchronous programs is hard because the use of callbacks, while efficient, obscures program control flow. We provide a formal model underlying asynchronous programs and study verification problems for this model. We show that the safety verification problem for finite-data asynchronous programs is EXPSPACE- complete. We show that liveness verification for finite-data asynchronous programs is decidable and polynomial-time equivalent to Petri net reachability. Decidability is not obvious, since even if the data is finite-state, asynchronous programs constitute infinite-state transition systems: both the program stack for an executing task and the task buffer of pending calls to tasks can be potentially unbounded. Our main technical constructions are polynomial-time, semantics-preserving reductions from asynchronous programs to Petri nets and back. The first reduction allows the use of algorithmic techniques on Petri nets for the verification of asynchronous programs, and the second allows lower bounds on Petri nets to apply also to asynchronous programs. We also study several extensions to the basic models of asynchronous programs that are inspired by additional capabilities provided by implementations of asynchronous libraries and classify the decidability and undecidability of verification questions on these extensions. © 2012 ACM.
Kopf B.,MPI SWS |
Smith G.,Florida International University
Proceedings - IEEE Computer Security Foundations Symposium | Year: 2010
We establish formal bounds for the number of min-entropy bits that can be extracted in a timing attack against a cryptosystem that is protected by blinding, the state-of-the art countermeasure against timing attacks. Compared with existing bounds, our bounds are both tighter and of greater operational significance, in that they directly address the key's one-guess vulnerability. Moreover, we show that any semantically secure public-key cryptosystem remains semantically secure in the presence of timing attacks, if the implementation is protected by blinding and bucketing. This result shows that, by considering (and justifying) more optimistic models of leakage than recent proposals for leakage-resilient cryptosystems, one can achieve provable resistance against side-channel attacks for standard cryptographic primitives. © 2010 IEEE.
Kopf B.,MPI SWS |
Proceedings - IEEE Computer Security Foundations Symposium | Year: 2010
Quantitative information-flow analysis (QIF) is an emerging technique for establishing information-theoretic confidentiality properties. Automation of QIF is an important step towards ensuring its practical applicability, since manual reasoning about program security has been shown to be a tedious and expensive task. Existing automated techniques for QIF fall short of providing full coverage of all program executions, especially in the presence of unbounded loops and data structures, which are notoriously dificult to analyze automatically. In this paper we propose a blend of approximation and randomization techniques to bear on the challenge of suficiently precise, yet eficient computation of quantitative information flow properties. Our approach relies on a sampling method to enumerate large or unbounded secret spaces, and applies both static and dynamic program analysis techniques to deliver necessary over- and underapproximationsof information-theoretic characteristics. © 2010 IEEE.