Events 2014

Formalising and Optimising Parallel Snapshot Isolation

Alexey Gotsman
IMDEA
SWS Colloquium
19 Dec 2014, 1:00 pm - 2:00 pm
Kaiserslautern building G26, room 111
Modern Internet services often achieve dependability by relying on geo-replicated databases that provide consistency models for transactions weaker than serialisability. We investigate a promising consistency model of Sovran et al.'s parallel snapshot isolation (PSI) which weakens the classical snapshot isolation in a way that allows more efficient geo-replicated implementations. We first give a declarative specification to PSI that does not refer to implementation-level concepts and thus allows application programmers to reason about the behaviour of PSI databases more easily. We justify our high-level specification by proving its equivalence to the existing low-level one. Using our specification we develop a criterion for checking when a set of transactions executing on PSI can be chopped into smaller pieces without introducing new behaviours. This allows application programmers to optimise the code of their transactions to execute them more efficiently. We find that our criterion is more permissive than the existing one for chopping serialisable transactions. These results contribute to understanding the complex design space of consistency models for geo-replicated databases.This is joint work with Andrea Cerone (IMDEA) and Hongseok Yang (Oxford).

CoLoSL: Concurrent Local Subjective Logic

Azalea Raad
Imperial College London
SWS Colloquium
15 Dec 2014, 2:00 pm - 4:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
A key difficulty in verifying shared-memory concurrent programs is reasoning compositionally about each thread in isolation. When the footprints of threads overlap with each other existing program logics require reasoning about static global shared resource which impedes compositionality. We introduce the program logic of CoLoSL where each thread is verified with respect to its subjective view of the global shared state. This subjective view describes only that part of the global shared resource accessed by the thread. Subjective views may arbitrarily overlap with each other and expand and contract depending on the resource required by the thread thus allowing for truly compositional proofs for shared-memory concurrency.

An SMT-Based Approach to Coverability Analysis

Filip Niksic
Max Planck Institute for Software Systems
SWS Student Defense Talks - Qualifying Exam
12 Dec 2014, 2:00 pm - 4:00 pm
Kaiserslautern building G26, room 111
Model checkers based on Petri net coverability have been used successfully in recent years to verify safety properties of concurrent shared-memory or asynchronous message-passing software. We revisit a constraint approach to coverability based on classical Petri net analysis techniques. We show how to utilize an SMT solver to implement the constraint approach and additionally to generate an inductive invariant from a safety proof. We empirically evaluate our procedure on a large set of existing Petri net benchmarks. Even though our technique is incomplete it can quickly discharge most of the safe instances. Additionally the inductive invariants computed are usually orders of magnitude smaller than those produced by existing solvers.

Scaling TCP performance for multicore systems

KyoungSoo Park
KAIST
SWS Colloquium
09 Dec 2014, 11:30 am - 1:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113
Scaling the performance of short TCP connections on multicore systems is fundamentally challenging. Despite many proposals that have attempted to address various shortcomings  inefficiency of the kernel implementation still persists. For example even state-of-the-art designs spend 70% to 80% of CPU cycles in handling TCP connections in the kernel leaving only small room for innovation in the user-level program.  In this talk I will present mTCP a high-performance user-level TCP stack for multicore systems. mTCP addresses the inefficiencies from the ground up - from packet I/O and TCP connection management to the application interface. In addition to adopting well-known techniques our design (1) translates multiple expensive system calls into a single shared memory reference (2) allows efficient flow-level event aggregation and (3) performs batched packet I/O for high I/O efficiency. Our evaluations on an 8-core machine showed that mTCP improves the performance of small message transactions by a factor of 25 compared to the latest Linux TCP stack and a factor of 3 compared to the MegaPipe system. It also improves the performance of various popular applications by 33% to 320% compared to those on the Linux stack.

Authenticated Data Structures, Generically

Michael W. Hicks
University of Maryland
SWS Colloquium
05 Dec 2014, 1:30 pm - 4:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 207
An authenticated data structure (ADS) is a data structure whose operations can be carried out by an untrusted prover the results of which a verifier can efficiently check as authentic. This is done by having the prover produce a compact proof that the verifier can check along with each operation's result. ADSs thus support outsourcing data maintenance and processing tasks to untrusted servers without loss of integrity. Past work on ADSs has focused on particular data structures (or limited classes of data structures) one at a time often with support only for particular operations.

This paper presents a generic method using a simple extension to a ML-like functional programming language we call (lambda-auth) with which one can program authenticated operations over any data structure defined by standard type constructors including recursive types sums and products. The programmer writes the data structure largely as usual and it is compiled to code to be run by the prover and verifier. Using a formalization of we prove that all well-typed programs result in code that is secure under the standard cryptographic assumption of collision-resistant hash functions. We have implemented as an extension to the OCaml compiler and have used it to produce authenticated versions of many interesting data structures including binary search trees red-black+ trees skip lists and more. Performance experiments show that our approach is efficient giving up little compared to the hand-optimized data structures developed previously.

Joint work with Andrew Miller Jonathan Katz and Elaine Shi at UMD

Towards Non-tracking Web and Mobile Analytics

Istemi Ekin Akkus
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
04 Dec 2014, 2:00 pm - 4:00 pm
Kaiserslautern building G26, room 112
simultaneous videocast to Saarbrücken building E1 5, room 005
Today websites and mobile application developers commonly use third party analytics services to obtain aggregate information about users that visit their sites or use their applications. This information includes demographics other sites that are visited other applications that are used as well as user behavior within their own sites or applications. In addition website publishers utilize online social network providers' appeal to attract more users to their websites by embedding social widgets on their pages. Unfortunately this outsourcing to obtain aggregate statistics and to benefit from social networking features allow these third parties to track individual user behavior across the web. This violation of user privacy has been strongly criticized resulting in tools that block such tracking as well as anti-tracking legislation and standards such as Do-Not-Track. These efforts while improving user privacy degrade the quality of analytics information as well as prevent the engagement of users on websites. In addition such client-side tools are mostly based on a blacklist which can be difficult and error-prone to maintain and thus can cause other non-tracking services to suffer.

We propose a general interaction-based third-party cookie policy that gives more control to the users and enables social networking features when the users want them. At the same time our policy prevents third-party tracking without the requirement of a blacklist and does not interfere with non-tracking services for analytics and advertisements. We then present two systems that enable publishers to obtain rich web analytics information (e.g. user demographics other sites visited products viewed) without tracking the users across the web. The first system enables web publishers to directly query their users while preserving user privacy and thus can supply with more types of analytics information that is not available through tracking today. Our system requires no new organizational players and is practical to deploy but necessitates the publishers to pre-define answer values for the queries. While this task can be easy for certain information (e.g. age gender education level) it is not feasible in many other analytics scenarios (e.g. free-text tag values in a photo application). To complement our system (and other systems requiring pre-defined answer values [48 49 56 57]) we design and describe another system that enables analysts to discover unknown strings to be used as potential answer values. Our system employs the exclusive-OR operation as its crypto primitive and utilizes a novel method to compare the equality of two XOR-encrypted strings without revealing them. We evaluate our system with real-world string distribution data and show that our system outperforms the closest system by several orders of magnitude for client computations and reduces server computations by at least a factor of two.

Algorithmic Challenges in Computational Genomics

Tobias Marschall
MPI-INF - D3
Joint Lecture Series
03 Dec 2014, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
The talk invites you to a journey from genetics to algorithmics and back. After a (very gentle) introduction to basic concepts of genetics I will explain how genomic data stored in living cells can be "read" using DNA sequencing machines a technology that has changed research in the life sciences dramatically in the past ten years. The analysis of data produced by these machines is by far not trivial however and leads to challenging computational problems. In this talk I will discuss two such problems: the reconstruction of haplotypes of diploid organisms (such as humans) and the discovery of structural genetic variants. We will see how both problems admit formalizations in terms of graphs: the first problem is related to finding bipartite subgraphs and the second one is related to enumerating maximal cliques. Towards the end I will come back to genetics and present a number of findings of the "Genome of the Netherlands" project some of which were only made possible by the discussed algorithms.

Exploiting Social Network Structure for Person-to-Person Sentiment Analysis

Robert West
Stanford University
SWS Colloquium
26 Nov 2014, 11:00 am - 1:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
Person-to-person evaluations are prevalent in all kinds of discourse and important for establishing reputations building social bonds and shaping public opinion. Such evaluations can be analyzed separately using signed social networks and textual sentiment analysis but this misses the rich interactions between language and social context. To capture such interactions we develop a model that predicts individual A's opinion of individual B by synthesizing information from the signed social network in which A and B are embedded with sentiment analysis of the evaluative texts relating A to B. We prove that this problem is NP-hard but can be relaxed to an efficiently solvable hinge-loss Markov random field and we show that this implementation outperforms text-only and network-only versions in two very different datasets involving community-level decision-making: the Convote U.S. Congressional speech corpus and the Wikipedia Requests for Adminship corpus. (Joint work with Hristo Paskov Jure Leskovec and Christopher Potts)

Time permitting I will also briefly discuss the "From Cookies to Cooks" project where we leverage search-engine query logs to gain insights into what foods people consume when and where. (Joint work with Ryen White and Eric Horvitz)

Thoth: Practical Data flow protection in a search engine

Aastha Mehta
Max Planck Institute for Software Systems
SWS Student Defense Talks - Qualifying Exam
21 Nov 2014, 3:00 pm - 5:00 pm
Saarbrücken building E1 5, room 422
Online data retrieval services like commercial search engines online social networking and trading and sharing sites process large volumes of data of different origins and types. A search engine like Bing or Google for instance indexes online social network (OSN) data personal email corporate documents public web documents and blogs. Each data item potentially has its own usage policy. For example email is private OSN data and blogs may be limited to friends and corporate documents may be restricted to employees. Furthermore providers must comply with local laws and court orders requiring them for instance to filter certain data items within a given jurisdiction.

Although data items are subject to different policies scalability flexibility and the need to deliver comprehensive search results dictate that the data be handled within the same system. Ensuring compliance with applicable policies in such a complex system however is a labor-intensive and error prone challenge. The policy actually in effect for a data item may depend on access control checks and settings in many components and several layers of a system making it difficult to verify or reason about. Moreover any design flaw bug or misconfiguration in a large and quickly evolving application codebase could potentially cause a policy violation.

The Open Security Foundation's database of data losses [1] reports 1458 incidents in 2013 and Privacy Rights Clearinghouse (PRC) reports more than 860M PII breached records in 4347 breaches made public since 2005 [2]. Moreover the stakes are high: providers stand to lose customer confidence business and reputation and face stiff fines in the case of policy violations.

In this talk I will present Thoth a practical safety net for policy compliance in a search engine. In Thoth rich confidentiality integrity provenance and declassification policies are stated in a declarative policy language and associated with data conduits i.e. files and network connections. I will explain a few example policies written in the context of Apache Lucene an open source search engine service. I will describe the efficiency of the policy evaluation and conclude with a brief discussion of the future work.

[1] DataLossDB: Open Security Foundation. http://datalossdb.org. [2] Privacy Rights Clearinghouse. http://privacyrights.org.

mhmm: Making Haskell More Modular

Scott Kilpatrick
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
20 Nov 2014, 2:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
Module systems like that of Haskell permit only a weak form of modularity in which module implementations directly depend on other implementations and must be processed in dependency order. Module systems like that of ML on the other hand permit a stronger form of modularity in which explicit interfaces express assumptions about dependencies and each module can be typechecked and reasoned about independently.

In this talk I present Backpack a new language for building separately-typecheckable packages on top of a weak module system like Haskell's. Not only does Backpack make Haskell a more modular language it establishes an entirely new direction for the design of so-called package management systems: as typed module languages with dependencies expressed via typed interfaces rather than names and version ranges.

Randomized Solutions to Renaming under Crashes and Byzantine Faults

Oksana Denysyuk
INESC-ID and University of Lisbon
SWS Colloquium
17 Nov 2014, 2:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
Exploring the power and limitations of different coordination problems has always been at the heart of the theory of distributed computing. This talk addresses a coordination problem called renaming. Renaming can be seen as a dual to the classical consensus problem: instead of agreeing on a unique value in renaming correct processes must disagree by picking distinct values from an appropriate range of values. The talk consists of two parts each considering a different fault model in synchronous message-passing systems. In the first part we tackle crash faults and propose a new randomization technique called balls-into-leaves which solves renaming in sub-logarithmic number of rounds. This technique outperforms optimal deterministic algorithms by an exponential factor. In the second part we consider the more challenging Byzantine faults. We propose a randomized renaming algorithm that tolerates up to t

Yesquel: scalable SQL storage for Web applications

Marcos K. Aguilera
unaffiliated
SWS Distinguished Lecture Series
17 Nov 2014, 10:30 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Web applications (web mail web stores social networks etc) keep massive amounts of data that must be readily available to users.  The storage system underlying these applications has evolved dramatically over the past 25 years from file systems to SQL database systems to a large variety of NOSQL systems. In this talk we contemplate this fascinating history and present a new storage system called Yesquel. Yesquel combines several advantages of prior systems. It supports the SQL query language to facilitate the design of Web applications while offering performance and scalability competitive with a widely used NOSQL system.

Generalized Universality

Rachid Guerraoui
EPFL
SWS Distinguished Lecture Series
12 Nov 2014, 10:30 am - 1:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 002
Replicated state machine is a fundamental computing construct for it essentially makes a distributed system emulate a highly available centralized one using a consensus abstraction through which processes agree on common decisions. The idea is at the heart of the fault-tolerance of most data centers today. Any sequential object is modeled by a state machine that can be replicated over all processes of the system and accessed in a wait-free manner: we talk about the universality of the construct and of its underlying consensus abstraction. Yet consensus is just a special case of a more general abstraction k-set consensus where processes agree on at most k different decisions. It is natural to ask whether there exists a generalization of state machine replication with k-set agreement for otherwise distributed computing would not deserve the aura of having an underpinning Theory as 1 (k-set consensus with k=1) would be special. The talk will recall the classical state machine replication construct and show how using k-set consensus as an underlying abstraction the construct can be generalized to implement k state machines of which at least one makes progress generalizing in a precise sense the very notion of consensus universality. The work is a joint work with Eli Gafni 

Scalable personalization infrastructures

Anne-Marie Kermarrec
Inria
SWS Distinguished Lecture Series
11 Nov 2014, 11:30 am - 2:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
The ever-growing amount of data available on the Internet clearly calls for personalization. Yet the most effective personalization schemes such as those based on collaborative filtering (CF) are notoriously resource greedy. We argue that scalable infrastructures relying on  P2P design can scale to that increasing number of users data and dynamics. We will present a novel scalable k-nearest neighbor protocol which P2P flavor provides scalability by design. This protocol provides each user with an implicit social network composed of users with similar tastes in a given application. This protocol has been instanciated in various infrastructures on several applications (recommendation top-k serach etc.) (1) A P2P system WhatsUp a collaborative filtering system for disseminating news items in a large-scale dynamic setting with no central authority; (2) A hybrid recommendation infrastructure HyRec an online cost-effective scalable system for CF personalization offloading CPU-intensive recommendation tasks to front-end client browsers while retaining storage and orchestration tasks within back-end servers; (3) A cloud-based centralized  engine providing real time recommendations.

Amplification DDoS: Abusing 30-Year-Old Internet Protocols for Denial-of-Service Attacks

Christian Rossow
Cluster of Excellence - Multimodal Computing and Interaction - MMCI
Joint Lecture Series
05 Nov 2014, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
In amplification denial-of-service adversaries send requests to public servers (e.g. open recursive DNS resolvers) and spoof the IP address of a victim. These servers in turn flood the victim with valid responses and - unknowingly - exhaust its bandwidth. In 2014 such abuses have lead to highly critical attack bandwidths of 400 Gbps.

We revisit popular protocols of common network services online games P2P filesharing networks and P2P botnets in order to assess their security against such abuse. We explore how the threat of amplification attacks can be mitigated and illustrate our security notification efforts for the Network Time Protocol (NTP). As an outlook to the future we present our ongoing research that aims to track down the actual sources of spoofed traffic.

Using Twitter to study Food Consumption and Fitness Behavior

Ingmar Weber
MPI-INF - D1
SWS Colloquium
05 Nov 2014, 10:30 am - 12:30 pm
Saarbrücken building E1 5, room 029
This talk presents two ongoing lines of work looking at how Twitter can be used to track societal level health issues. You Tweet What You Eat: Studying Food Consumption Through Twitter; joint work with Yelena Mejova and Sofiane Abbar Food is an integral part of our lives cultures and well-being and is of major interest to public health. The collection of daily nutritional data involves keeping detailed diaries or periodic surveys and is limited in scope and reach. Alternatively social media is infamous for allowing its users to update the world on the minutiae of their daily lives including their eating habits. In this work we examine the potential of Twitter to provide insight into US-wide dietary choices by linking the tweeted dining experiences of 210K users to their interests demographics and social networks. We validate our approach by relating the caloric values of the foods mentioned in the tweets to the state-wide obesity rates achieving a Pearson correlation of 0.77 across the 50 US states and the District of Columbia. We then build a model to predict county-wide obesity and diabetes statistics based on a combination of demographic variables and food names mentioned on Twitter. Our results show significant improvement over previous research. We further link this data to societal and economic factors such as education and income illustrating that for example areas with higher education levels tweet about food that is significantly less caloric. Finally we address the issue of the social nature of obesity (first raised by Christakis & Fowler) by inducing two social networks using mentions and reciprocal following relationships. From Fitness Junkies to One-time Users: Determining Successful Adoptions of Fitness Applications on Twitter; joint work with Kunwoo Park and Meeyoung Cha As our world becomes more digitized and interconnected one's health status---a topic that was once thought to be private---is shared on public platforms. This trend is facilitated by scores of fitness applications that push health updates to users' social networks. This paper presents the behavioral patterns of social opt-in users of a popular fitness application MyFitnessPal. Through data gathered from Twitter we determine whether any features such as the profile fitness activities and social support can predict long-term retention and weight loss of users. We discuss implications of findings related to HCI and the design of health applications.

Machine Learning about People from their Language

Noah Smith
Carnegie Mellon University
SWS Distinguished Lecture Series
04 Nov 2014, 3:30 pm - 5:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
This talk describes new analysis algorithms for text data aimed at understanding the social world from which the data emerged. The political world offers some excellent questions to explore: Do US presidential candidates "move to the political center" after winning a primary election? Are Supreme Court justices swayed by amicus curiae briefs documents crafted at great expense? I'll show how our computational models capture theoretical commitments and uncertainty offering new tools for exploring these kinds of questions and more. Time permitting we'll close with an analysis of a quarter million biographies discussing what can be discovered about human lives as well as those who write about them.

The primary collaborators on this research are my Ph.D. students David Bamman and Yanchuan Sim; collaborators from the Political Science Department at UNC Chapel Hill Brice Acree and Justin Gross; and Bryan Routledge from the Tepper School of Business at CMU.

MultiSE: Multi-Path Symbolic Execution using Value Summaries

Koushik Sen
UC Berkeley
SWS Colloquium
30 Oct 2014, 4:00 pm - 6:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 002
Dynamic symbolic execution (DSE) has been proposed to effectively generate test inputs for real-world programs. Unfortunately DSE techniques do not scale well for large realistic programs because often the number of feasible execution paths of a program increases exponentially with the increase in the length of an execution path.

In this paper we propose MultiSE a new technique for merging states incrementally during symbolic execution without using auxiliary variables. The key idea of MultiSE is based on an alternative representation of the state where we map each variable including the program counter to a set of guarded symbolic expressions called a value summary. MultiSE has several advantages over conventional DSE and existing state merging techniques: value summaries enable sharing of symbolic expressions and path constraints along multiple paths and thus avoid redundant execution. MultiSE does not introduce auxiliary symbolic variables which enables it to 1) make progress even when merging values not supported by the constraint solver 2) avoid expensive constraint solver calls when resolving function calls and jumps and 3) carry out most operations concretely. Moreover MultiSE updates value summaries incrementally at every assignment instructions which makes it unnecessary to identify the join points and to keep track of variables to merge at join points.

We have implemented MultiSE for JavaScript programs in a publicly available open-source tool. Our evaluation of MultiSE on several programs shows that MultiSE can run significantly faster than traditional dynamic symbolic execution and save substantial number of state merges compared to existing state merging techniques.

Vellvm: Verifying Safety in the LLVM IR

Steve Zdancewic
University of Pennsylvania
SWS Colloquium
09 Oct 2014, 10:30 am - 2:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
The Low-Level Virtual Machine (LLVM) compiler provides a modern industrial-strength SSA-based intermediate representation (IR) along with infrastructure support for many source languages and target platforms. Much of the LLVM compiler is structured as IR to IR translation passes that apply various optimizations and analyses making it an ideal target for enforcing security properties of low-level code.

In this talk I will describe the Vellvm project which seeks to provide a formal framework for developing machine-checkable proofs about LLVM IR programs and translation passes. I'll discuss some of the subtleties of modeling the LLVM IR semantics including nondeterminism and its use of SSA representation. I'll also describe some of the proof techniques that we have used for reasoning about LLVM IR transformations and describe our results about the formal verification of the SoftBound pass which hardens C programs against memory safety errors.

Vellvm which is implemented in the Coq theorem prover provides facilities for extracting LLVM IR transformation passes and plugging them into the LLVM compiler thus enabling us to create verified optimization passes for LLVM and evaluate them against their unverified counterparts. Our experimental results show that fully verified and automatically extracted implementations can yield competitive performance.

This is joint work with Jianzhou Zhao and Milo Martin (both at Penn) and Santosh Nagarakatte (at Rutgers University).

Termination of Linear Programs: Advances and Challenges

Dr. Joel Ouaknine
University of Oxford
SWS Distinguished Lecture Series
02 Oct 2014, 10:30 am - 1:30 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
In the quest for program analysis and verification program termination -- determining whether a given program will always halt or could execute forever -- has emerged as a central component. Although proven undecidable in the general case by Alan Turing over 80 years ago positive results have been obtained in a variety of restricted instances. We survey the situation with a focus on simple linear programs i.e. WHILE loops in which all assignments and guards are linear discussing recent progress as well as ongoing and emerging challenges.

Statistical Learning in Computational Biology: Incorporating and Discovering new Biological Insights

Nico Pfeifer
MPI-INF - D3
Joint Lecture Series
01 Oct 2014, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
tbd

Private-by-Design Advertising Meets the Real World

Alexey Reznichenko
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Defense
26 Sep 2014, 3:30 pm - 6:30 pm
Kaiserslautern building G26, room 111
There are a number of designs for an online advertising system that allow for behavioral targeting without revealing user online behavior or user interest profiles to the ad network. However none of the proposed designs have been deployed in real-life settings. In this talk I will present an effort to fill this gap by building and evaluating a fully functional prototype of a practical privacy-preserving ad system at a reasonably large scale. With more than 13K opted-in users our system was in operation for over two months serving an average of 4800 active users daily. During the last month alone we registered 790K ad views 417 clicks and even a small number of product purchases. In addition our prototype is equipped with a differentially private data collection mechanism which we used as the primary means for gathering experimental data. The data we collected show for example that our system obtained click-through rates comparable with those for Google display ads. In this talk I will describe our first-hand experience and lessons learned in running the first fully operational "private-by-design" behavioral advertising and analytics system.

A Privacy-Preserving Platform for Context-Aware Mobile Social Applications

Viktor Erdélyi
Max Planck Institute for Software Systems
SWS Student Defense Talks - Qualifying Exam
12 Aug 2014, 3:00 pm - 6:00 pm
Saarbrücken building E1 5, room 029
Mobile social applications provide social services to users based on their context (physical location activity nearby users interests). One example is social discovery which means discovering nearby users of interest (e.g. friends or people with similar interests). Another such feature is social sharing which means sharing other content with nearby people. However this has privacy implications. Existing applications provide social discovery and social sharing via the cloud. Thus users have to continuously upload sensitive data collected by their device to the cloud in order to use these services. However once this data leaves the device users cannot control anymore how it is used by the cloud. Our aim is to create a platform that can support such applications while giving users control over their privacy. In this talk we propose an approach that does social discovery in a device-to-device manner thereby keeping the sensitive data local to the device. In our approach we do share content via the cloud but all content is encrypted (and the cloud does not have the encryption key). Our solution is based on the concept of encounters which happen every time two devices are within Bluetooth range of each other for at least 2 minutes. We describe how we used this abstraction to capture meaningful social interactions and how they can be used to enable privacy-preserving anonymous communication and sharing with individual encounters and groups of people during of after the physical co-location. Our system also supports selective linkability which enables users to allow people of their choice to recognize them by name when they encounter while remaining anonymous to others. In order to demonstrate the capabilities and usefulness of our system we built an Android app that visualizes the encounter history on a timeline correlated with contextual information such as location and calendar entries. It allows users to create groups and share encrypted content with participants.

Leveraging Sharding in the Design of Scalable Replication Protocols

Robbert van Renesse
Cornell University
SWS Distinguished Lecture Series
08 Aug 2014, 10:30 am - 1:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 112
Most if not all datacenter services use sharding and replication for scalability and reliability. Shards are more-or-less independent of one another and individually replicated. We challenge this design philosophy and present a replication protocol where the shards interact with one another: A protocol running within shards ensures linearizable consistency while the shards interact in order to improve availability. We analyze its availability properties and evaluate a working implementation.

A Fast, Correct Time-Stamped Stack

Mike Dodds
University of York, UK
SWS Colloquium
06 Aug 2014, 3:30 pm - 6:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
Concurrent data-structures such as stacks queues and deques often implicitly enforce a total order over elements in their underlying memory layout. However much of this order is unnecessary: linearizability only requires that elements are ordered if the insert methods ran in sequence. We propose a new approach which uses timestamping to avoid unnecessary ordering. Pairs of elements can be left unordered (represented by unordered timestamps) if their associated insert operations ran concurrently and order imposed as necessary by the eventual remove operations.

We realise our approach in a new non-blocking data-structure the TS (timestamped) stack. In experiments on x86 the TS stack outperforms and outscales all its competitors -- for example it outperforms the elimination-backoff stack by factor of two. In our approach more concurrency translates into less ordering giving less-contended removal and thus higher performance and scalability. Despite this the TS stack is linearizable with respect to stack semantics.

The weak internal ordering in the TS stack presents a challenge when establishing linearizability: standard techniques such as linearization points work well when there exists a total internal order. We have developed a new stack theorem mechanised in Isabelle which characterises the orderings sufficient to establish stack semantics. By applying our stack theorem we can show that the TS stack is indeed correct.

Probabilistic Methods for the Analysis of Biological Networks

Marcel Schulz
Cluster of Excellence - Multimodal Computing and Interaction - MMCI
Joint Lecture Series
06 Aug 2014, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
The regulation of gene expression in cells is a dynamic process. Understanding the dynamics of regulatory events can lead to important insights about their connection to developmental or disease related processes like infection. In this talk we are particularly interested in the regulatory role of transcription factors (TFs) and microRNAs (miRNAs). Unfortunately rarely do genome-wide binding data for TFs and miRNAs exist to study their dynamics. However in public databases there is a wealth of available data for time series gene expression. Therefore many methods for identifying TF and miRNA targets often integrate sequence and gene expression data but lack the ability to adequately use the temporal information encoded in time-series data and thus miss important regulators and their targets.

We developed a probabilistic modeling method that uses input-output hidden Markov models to reconstruct dynamic regulatory networks that explain how temporal gene expression is jointly regulated by miRNAs and TFs. We measured miRNA and mRNA expression for postnatal lung development in mice and used studied the regulation of this process. The reconstructed dynamic network correctly identified known miRNAs and TFs. The method has also provided predictions about additional miRNAs regulating this process and the specific developmental phases they regulate several of which were experimentally validated. Our analysis uncovered links between miRNAs involved in lung development and differentially expressed miRNAs in idiopathic pulmonary fibrosis patients some of which we have experimentally validated using proliferation assays. Our results show how probabilistic models can be used to integrate diverse data sets and lead to new scientific discoveries.

Trace Complexity

Flavio Chierichetti
Sapienza University of Rome
SWS Colloquium
30 Jul 2014, 10:30 am - 1:30 pm
Saarbrücken building E1 5, room 029
Prediction tasks in machine learning usually require deducing a latent variable or structure from observed traces of activity -- sometimes these tasks can be carried out with a significant precision while sometimes getting any significance out of the prediction requires an unrealistically large number of traces.

In this talk we will study the trace complexity of (that is: the number of traces needed for) a number of prediction tasks in social networks: the network inference problem the number of signers problem and the star rating problem.

The first problem was defined by [Gomez-Rodriguez et al 2010] and consists of reconstructing the edge set of a network given traces representing the chronology of infection times as epidemics spread through the network. The second problem's goal is to predict the unknown number of signers of email-based petitions given only a small subset of the emails that circulated. The last problem aims to predict the unknown absolute "quality" of a movie using the ratings given by different users (each with their own unknown precision)

These examples will allow us to highlight some interesting general points of prediction tasks.

Joint work with subsets of Bruno Abrahao Anirban Dasgupta Bobby Kleinberg Jon Kleinberg Ravi Kumar Silvio Lattanzi and David Liben-Nowell.

Tracking information flow in web applications

Andrei Sabelfeld
Chalmers University
SWS Distinguished Lecture Series
24 Jul 2014, 10:30 am - 1:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
This talk discusses a principled approach to web application security through tracking information flow in web applications. Although the agile nature of developments in web application technology makes web application security much of a moving target we show that there are some fundamental challenges and tradeoffs that determine possibilities and limitations of automatically securing web applications. We address challenges related to mutual distrust on the policy side (as in web mashups) and tracking information flow in dynamic web programming languages (such as JavaScript) to provide a foundation for practical web application security.

Compositional Verification of Termination-Preserving Refinement of Concurrent Programs

Hongjin Liang
UST China
SWS Colloquium
23 Jul 2014, 10:30 am - 2:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
Many verification problems can be reduced to refinement verification. However existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination allowing a diverging program to trivially refine any programs or is difficult to apply in compositional thread-local reasoning. In this talk I will present a Hoare-style concurrent program logic supporting termination-preserving refinement proofs. We show two key applications of our logic i.e. verifying linearizability and lock-freedom together for fine-grained concurrent objects and verifying full correctness of optimizations of concurrent algorithms.

A Journey with Discrete Optimization: from the Real World to Theory and Back

Andreas Karrenbauer
MPI-INF - D1
Joint Lecture Series
02 Jul 2014, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Discrete Optimization problems appear in many applications as well as in interdisciplinary research. This leads to interesting theoretical questions with direct practical relevance. In this talk I will highlight several examples but I will mainly focus on optimization problems arising with flat panel displays (e.g. OLED). That is lifetime and power consumption can be improved by displaying each image in a special way. To this end a discrete optimization problem has to be solved in real-time for varying content. We abstract the computational task for several display technologies in one mathematical framework. From a combinatorial perspective this boils down to decomposing the edge set of a given bipartite graph into a few number of complete bipartite subgraphs (a.k.a. bicliques). Though we showed that even finding only suboptimal solutions is theoretically very hard i.e. in the same ballpark as the well-known graph coloring problem we developed suitable restrictions and refinements of the model by alternating theoretical analysis and experimental evaluation in an algorithm engineering process that led to a method with industrial strength. That is our algorithm is implemented on a chip that drives the world's first commercially available transparent OLED display.

I will conclude my talk with a brief discussion about two other lines of research where we (i) use integer programming for optimizing keyboard layouts and (ii) work on efficient algorithms for network flow problems arising in image processing and computer vision.

Information flow control for javascript in web browsers

Vineet Rajani
Max Planck Institute for Software Systems
SWS Student Defense Talks - Qualifying Exam
16 Jun 2014, 1:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
Websites today routinely combine JavaScript from multiple sources both trusted and untrusted. Hence JavaScript security is of paramount importance. A specific interesting problem is information flow control (IFC) for JavaScript. In this talk I will present a new approach for IFC its formalization and its empirical results. Our IFC mechanism works at the level of JavaScript bytecode  and hence leverages years of industrial effort on optimizing both the source to bytecode compiler and the bytecode interpreter. We track both explicit and implicit flows and observe only moderate overhead. Working with bytecode results in new challenges including the extensive use of unstructured control flow in bytecode (which complicates lowering of program context taints) unstructured exceptions (which complicate the matter further) and the need to make IFC analysis permissive. In the talk I will explain how we  address these challenges formally model the JavaScript bytecode semantics and our instrumentation prove the standard property of termination- insensitive non-interference and present experimental results on an optimized prototype. 

Exploratory Data Analysis

Jilles Vreeken
Cluster of Excellence - Multimodal Computing and Interaction - MMCI
Joint Lecture Series
04 Jun 2014, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
The goal of exploratory data analysis ---or data mining--- is making sense of data. We develop theory and algorithms that help you understand your data better with the lofty goal that this helps formulating (better) hypotheses. More in particular our methods give detailed insight in how data is structured: characterising distributions in easily understandable terms showing the most informative patterns associations correlations etc.

My talk will consist of three parts. I will start my talk with a quick overview of the techniques we have on offer---in terms of data analysis problems data types as well as my general approach of using information theory to formalise informativeness.

In the second part I will discuss how to find the most significant patterns from event sequence data. In short our goal is mining a small set of patterns (serial episodes) that together characterise the data well. I will go into the formulation of the problem as well as the fast heuristics we developed to find good solutions.

Third I will discuss work in progress: can we derive a causal inference rule to tell whether X causes Y or whether they are merely correlated? Can we do so in a principled manner without parameters and without having to assume distributions? Can we do so when X and Y are not iid sets of observations but objects in general? Hopefully not killing any excitement but so far the answer seems yes.

Besides this all I will also answer the frequently asked question of how to pronounce my name.

Adventures in Program Synthesis

Ras Bodik
UC Berkeley
SWS Distinguished Lecture Series
22 May 2014, 10:30 am - 2:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
If you possessed the power to synthesize any program from just a high-level description of the desired behavior how would you deploy this power? It seems that you could end programming as we know it and automate the creation of everything that can be viewed as a program including biological and economic models. This dream is not fully achievable but over the last decade we have learnt how to rephrase the synthesis problem to make it solvable and practically applicable. This talk will mine seven projects from my group for surprising lessons and future opportunities. I will first present two fresh answers to the question of "where do specifications come from?" and then argue for synergy between domain-specific languages and synthesis. I will also explain why synthesis may help rethink compiler construction necessitated by the era of unusual hardware. Looking into the next decade I will illustrate how synthesis may facilitate computational doing --- the development of tools for data science and the digital life.

Modeling and representing materials in the wild

Kavita Bala
Cornell University
SWS Distinguished Lecture Series
08 May 2014, 10:30 am - 1:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
Our everyday life brings us in contact with a rich range of materials that contribute to both the utility and aesthetics of our environment. Human beings are very good at using subtle distinctions in appearance to distinguish between materials (e.g. silk vs. cotton laminate vs. granite). In my group we are working on understanding how we perceive materials to drive better graphics and vision algorithms.

In this talk I will present OpenSurfaces a rich labeled database consisting of thousands of examples of surfaces segmented from consumer photographs of interiors and annotated with material parameters texture information and contextual information. We demonstrate the use of this database in applications like surface retexturing intrinsic image decomposition intelligent material-based image browsing and material design. I will also briefly describe our work on light scattering for translucent materials and realistic micron-resolution models for fabrics. Our work has applications in many domains: in virtual and augmented reality fueled by the advent of devices like Google Glass in virtual prototyping for industrial design in ecommerce and retail in textile design and prototyping in interior design and remodeling and in games and movies.

Approximation Algorithms for Packing Problems

Andreas Wiese
MPI-INF - D1
Joint Lecture Series
07 May 2014, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Packing problems belong to the classical problems in combinatorial optimization. The most well-known problem of this type is probably the Knapsack problem in which one seeks to select the most profitable subset of some given items such that the selected items fit into a knapsack of bounded size. In this talk I will first present some recent approximation results on a problem which can be seen as the temporal extension of Knapsack: each item needs space in the knapsack only during some given time interval and one has to ensure that at each point in time the items being active at this time fit into the knapsack. Surprisingly this problem has connections to a geometric version of the well-studied Independent Set problem: given a set of axis-parallel rectangles in the plane one seeks to find a subset of maximum total weight such that the selected rectangles are non-overlapping. In the second part of the talk I will show some new results for this problem whose methods are inspired by techniques for the above generalization of Knapsack.

Lazy Bit-vector Solving and Witnessing Compiler Transformations

Liana Hadarean
NYU
SWS Colloquium
05 May 2014, 2:00 pm - 5:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
The Satisfiability Modulo Theories (SMT) problem is a generalization of the Boolean satisfiability problem to first-order logic. SMT solvers are now at the forefront of automated reasoning and they are increasingly used in a number of diverse applications. In this talk I will first present a new decision procedure for the theory of fixed-width bit-vectors and then describe an application of SMT techniques to verifying compiler transformations.

Most SMT solvers decide bit-vector constraints via eager reduction to propositional logic after first applying powerful word-level rewrite techniques. While often efficient in practice this method does not scale on problems for which top-level rewrites cannot reduce the problem size sufficiently. We present a lazy solver that targets such problems by maintaining the word-level structure during search. This approach also enables efficient combination with the theory of arrays using variants of the Nelson-Oppen combination procedure.

The combination of the array and bit-vector theories offers a natural way of encoding the semantics of compiler intermediate representation languages. We show how to integrate an SMT solver with a compiler to build a "self-certifying" compiler: a compiler that generates a verifiable justification for its own correctness on every run. Our compiler produces as justification a refinement relation between the source and target programs of every optimization step. This "witness" relation is produced by an auxiliary witness generator and is untrusted: its correctness is checked by an external SMT solver. Our implementation is based on the LLVM compiler: we have written generators for a number of intra-procedural optimizations. Preliminary results suggest the overhead of witness generation and checking compilation is manageable.

Modular Reasoning about Heap Paths via Effectively Propositional Formulas

Ori Lahav
Tel Aviv University
SWS Colloquium
24 Apr 2014, 10:30 am - 1:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
First order logic with transitive closure and separation logic enable elegant interactive verification of heap-manipulating programs. However undecidabilty results and high asymptotic complexity of checking validity preclude complete automatic verification of such programs even when loop invariants and procedure contracts are specified as formulas in these logics. We tackle the problem of procedure-modular verification of reachability properties of heap-manipulating programs using efficient decision procedures that are complete: that is a SAT solver must generate a counterexample whenever a program does not satisfy its specification. By (a) requiring each procedure modifies a fixed set of heap partitions and creates a bounded amount of heap sharing and (b) restricting program contracts and loop invariants to use only deterministic paths in the heap we show that heap reachability updates can be described in a simple manner. The restrictions force program specifications and verification conditions to lie within a fragment of first-order logic with transitive closure that is reducible to effectively propositional logic and hence facilitate sound complete and efficient verification. We implemented a tool atop Z3 and report on preliminary experiments that establish the correctness of several programs that manipulate linked data structures.

Presented in POPL'14.

Joint work with: Shachar Itzhaky (Tel Aviv University) Anindya Banerjee (IMDEA Software Institute) Neil Immerman (University of Massachusetts) Aleksandar Nanevski (IMDEA Software Institute) Mooly Sagiv (Tel Aviv University)

Mobile multi-cores: power and performance

Aaron Carroll
NICTA, Sydney
SWS Colloquium
23 Apr 2014, 11:00 am - 2:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113
The modern smartphone is a power hungry device and due largely to the proliferation of multi-core CPUs the applications processor is one of the main energy drivers. Indeed a current-generation mobile multi-core can drain your battery in well under one hour. In this talk I will discuss how to manage mobile multi-cores more effectively. I will start with some ground-truth about the energy consumption inside a smartphone based on circuit-level measurements of real devices. Noting that the applications processor continues to be relevant I will discuss some techniques for regulating multi-core CPU power showing the importance of static power and its surprising variance among devices. Finally I will conclude the talk discussing current and future work on exploring alternate ways to utilize the parallelism available in mobile multi-cores.

Practical Real-Time with Look-Ahead Scheduling

Dr. Michael Roitzsch
TU Dresden
SWS Colloquium
23 Apr 2014, 10:00 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
From video and music to responsive UIs a lot of real-time workloads run on today's desktops and mobile devices but real-time scheduling interfaces in commodity operating systems have not gained traction. As a result the CPU scheduler receives no explicit knowledge about applications' needs and thus falls back to heuristics or best-effort operation. I present ATLAS - the Auto-Training Look-Ahead Scheduler. ATLAS improves service to applications with regard to two non-functional properties: timeliness and overload detection. ATLAS provides timely service to applications accessible through an easy-to-use interface. Deadlines specify timing requirements workload metrics describe jobs. ATLAS employs machine learning to predict job execution times. Deadline misses are detected before they occur so applications can react early. ATLAS is currently a single-core scheduler so after presenting the status quo I will discuss the planned multicore extension and the new application scenarios it enables.

Increasing security and performance with higher-level abstractions for distributed programming.

Dr. Andrew Myers
Cornell University, Ithaca
SWS Distinguished Lecture Series
10 Apr 2014, 10:30 am - 1:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
Code and data are exchanged and reused freely across the Internet and the Web. But both are vectors for attacks on confidentiality and integrity. Current systems are vulnerable because they're built at too low a level of abstraction without principled security assurance. The Fabric project has been developing higher-level abstractions that securely support future open extensible applications. Unlike current Web abstractions Fabric has a principled basis for security: language-based information flow which works even for distrusted mobile code. Warranties a new abstraction for distributed computation enable scalability even with a strong consistency model that simplifies programmer reasoning.

Incremental Parallel and Distributed Systems

Pramod Bhatotia
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
07 Apr 2014, 5:00 pm - 8:00 pm
Saarbrücken building E1 5, room 029
Many applications exhibit the property that small localized changes to the input result in only minor changes to the output. Incremental computations seek to exploit this observation to speed-up successive runs of an application by tracking control and data dependencies and re-executing only those parts of the computation that are affected by a given input change. To realize the benefits of incremental computation researchers and practitioners are developing new systems where the programmer can provide efficient update mechanisms for changing application data. Unfortunately most of the existing solutions are limiting because they either depart from existing programming models or require programmers to devise an incremental update mechanism (or a dynamic algorithm) on a per-application basis.

The high-level goal of my thesis research is to enable practical automatic and efficient incremental computations in parallel and distributed systems. My approach neither requires a radical departure from current models of programming nor complex application-specific dynamic algorithms.

In this talk I will first present a high-level description of my thesis research. Thereafter as a concrete example I will describe my recent project "iThreads". iThreads is a POSIX-compliant threading library to support parallel incremental computation targeting unmodified C/C++ multithreaded programs. The iThreads library can be used as a drop-in replacement for the pthreads library making it trivial to obtain the benefits of incremental computation by a simple exchange of libraries linked without even recompiling the application code. To achieve this result we design our algorithms and implementation to operate at the compiled binary code level by leveraging operating system-specific mechanisms. Our design choice of iThreads tries to strike a balance between efficiency of incremental computation and transparency for unmodified C/C++ pthreads-based programs. Our evaluation on a multicore platform using benchmarks from the PARSEC and Phoenix suites shows significant performance improvements for the majority of applications.

The Cyberspace Battle for Information: Combating Internet Censorship

Amir Houmansadr
University of Texas at Austin
SWS Colloquium
07 Apr 2014, 10:30 am - 2:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
The Internet has become ubiquitous bringing many benefits to people across the globe. Unfortunately Internet users face threats to their security and privacy: repressive regimes deprive them of freedom of speech and open access to information governments and corporations monitor their online behavior advertisers collect and sell their private data and cybercriminals hurt them financially through security breaches. My research aims to make Internet communications more secure and privacy-preserving. In this talk I will focus on the design implementation and analysis of tools that help users bypass Internet censorship. I will discuss the major challenges in building robust censorship circumvention tools introduce two novel classes of systems that we have developed to overcome these challenges and conclude with several directions for future research.

Towards a Secure Client-side for the Web Platform

Devdatta Akhawe
UC Berkeley
SWS Colloquium
03 Apr 2014, 10:30 am - 2:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
With the tremendous growth in cloud-based services the web platform is now easily the most widely used application platform. In this talk I will present work done we have done at Berkeley towards developing a secure client-side for web applications. I will discuss three directions: secure protocols secure applications and secure user experience.

First I will present work on providing a formal foundation for web security protocols. We formalize the typical web attacker model and identify broadly applicable security goals. We also identify an abstraction of the web platform that is amenable to automated analysis yet able to express subtle attacks missed by humans. Using a model checker we automatically identified a previously unknown flaw in a widely used Kerberos-like authentication protocol for the web.

Second I will present work on improving assurance in client-side web applications. We identify pervasive over-privileging in client-side web applications and present a new architecture that relies on privilege separation to mitigate vulnerabilities. Our design uses standard primitives and enables a 6x to 10000x reduction in the trusted computing base with less than 13 lines modified.

Lastly I will present the results of a large-scale measurement study to empirically assess whether browser security warnings are as ineffective as popular opinion suggests. We used Mozilla Firefox and Google Chrome's in-browser telemetry to observe over 25 million warning impressions in situ. Our results demonstrate that security warnings can be effective in practice; security practitioners should not dismiss the goal of communicating security information to end users.

A hybrid moment closure approach to stochastic chemical kinetics

Verena Wolf
Fachrichtung Informatik - Saarbrücken
Joint Lecture Series
02 Apr 2014, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Stochastic modeling of biochemically reacting systems is an important branch of quantitative systems biology. Stochastic simulation is in widespread use for analyzing such models but it is computationally expensive and only provides estimates that are subject to statistical uncertainty. Recently fast numerical simulation methods have been developed which are based on a moment representation of the underlying probability distribution. In this talk I will present a hybrid scheme for the fast numerical simulation of such models which uses a moment representation only for the distribution of chemical species that are present in high copy numbers. The distribution of the remaining small molecular populations are obtained via the integration of the corresponding chemical master equation. Based on a number of case studies I will show that the approach is accurate and very efficient and thus suitable for computationally expensive tasks such as the estimation of kinetic constants.

Logic-based frameworks for automated verification of programs with dynamically allocated data structures

Cezara Dragoi
IST Austria
SWS Colloquium
27 Mar 2014, 10:30 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
Dynamically allocated data structures are heavily used in software nowadays to organize and facilitate the access to data. This poses new challenges to software verification due to various aspects either related to the control structure or to the data. In this talk we present logic-based frameworks for automatic verification of programs manipulating data structures that store unbounded data. First we are concerned with designing decidable logics that can be used to automate deductive verification in the Hoare-style of reasoning. This method relies on user provided annotations such as loop invariants. Second we introduce static analyses that can automatically synthesize such annotations. Classically static analysis has been used to prove correctness of non-functional properties such as null pointer deference. In this talk we present static analyses that can prove complex functional properties describing the values stored in the data structure.

Equivalence checking of stack-based infinite-state systems

Stefan Goeller
University of Bremen
SWS Colloquium
24 Mar 2014, 10:30 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
In the context of program refinement it is of particular interest to be able to automatically check whether the implementation of a specification before the refinement step behaves equivalently to the implementation after the refinement step.

Since equivalence checking of programs is generally undecidable one is typically confronted with a trade-off problem. On the one hand one wishes to carry out the equivalence check fully automatically and therefore needs to model/abstract the program in such a way that equivalence checking remains at least decidable. On the other hand the modeling/abstraction of the program should be expressive enough to model the program as faithfully as possible.

Infinite-state systems are a suitable means for faithfully modeling computer programs. For instance the call and return behavior of recursive programs can faithfully be modeled using pushdown systems (the transition graphs induced by pushdown automata).

The focus of my talk will be on some recent work on bisimulation equivalence checking of stack-based infinite-state systems i.e. infinite-state systems whose states and transitions involve the manipulation of a stack.

I will present in a bit more detail a PSPACE upper bound on deciding bisimulation equivalence of one-counter systems which are pushdown systems over a unary stack alphabet and an NLOGSPACE upper bound on bisimulation equivalence of deterministic one-counter systems closing a long-standing complexity gap. Furthermore I will give some intuition why bisimulation equivalence checking of pushdown systems and higher-order pushdown systems is much more difficult to decide from a computational perspective being nonelementary and undecidable respectively. I will conclude with some challenging open problems in this area of research.

Structure and Dynamics of Diffusion Networks

Manuel Gomez Rodriguez
Max Planck Institute for Intelligent Systems
SWS Colloquium
13 Mar 2014, 10:30 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
Networks represent a fundamental medium for spreading and diffusion of various types of information behavior and rumors. However observing a diffusion process often reduces to noting when nodes (people blogs etc.) reproduce a piece of information adopt a behavior buy a product or more generally adopt a contagion. We often observe where and when but not how or why contagions propagate through a network. The mechanism underlying the process is hidden. However the mechanism is of outstanding interest in all cases since understanding diffusion is necessary for predicting meme propagation stopping rumors or maximizing sales of a product.

In this talk I will present a flexible probabilistic model of diffusion over networks that makes minimal assumptions about the physical biological or cognitive mechanisms responsible for diffusion. This is possible since the model is data-driven and relies primarily on the visible temporal traces that diffusion processes generate. I apply the model to information diffusion among 3.3 million blogs and mainstream media sites during a one year period. The model allows us to predict future events it sheds light on the hidden underlying structure and temporal dynamics of diffusion and provides insights into the positions and roles various nodes play in the diffusion process.

Can You Hide in an Internet Panopticon?

Bryan Ford
Yale University
SWS Colloquium
12 Mar 2014, 10:30 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
Many people have legitimate needs to avoid their online activities being tracked and linked to their real-world identities - from citizens of authoritarian regimes to everyday victims of domestic abuse or law enforcement officers investigating organized crime. Current state-of-the-art anonymous communication systems are based on onion routing an approach effective against localized adversaries with a limited ability to monitor or tamper with network traffic. In an environment of increasingly powerful and all-seeing state-level adversaries however onion routing is showing cracks and may not offer reliable security for much longer. All current anonymity systems are vulnerable in varying degrees to five major classes of attacks: global passive traffic analysis active attacks "denial-of-security" or DoSec attacks intersection attacks and software exploits.

The Dissent project is prototyping a next-generation anonymity system representing a ground-up redesign of current approaches. Dissent is the first anonymity and pseudonymity architecture incorporating protection against the five major classes of known attacks. By switching from onion routing to alternate anonymity primitives offering provable resistance to traffic analysis Dissent makes anonymity possible even against an adversary who can monitor most or all network communication. A collective control plane renders a group of participants in an online community indistinguishable even if an adversary interferes actively such as by delaying messages or forcing users offline. Protocol-level accountability enables groups to identify and expel misbehaving nodes preserving availability and preventing adversaries from using denial-of-service attacks to weaken anonymity. The system computes anonymity metrics that give users realistic indicators of anonymity protection even against adversaries capable of long-term intersection and statistical disclosure attacks and gives users control over tradeoffs between anonymity loss and communication responsiveness. Finally virtual machine isolation offers anonymity protection against browser software exploits of the kind recently employed to de-anonymize Tor users. While Dissent is still a proof-of-concept prototype with important functionality and performance limitations preliminary evidence suggests that it may in principle be possible - though by no means easy - to hide in an Internet panopticon.

I-Ting Angelina Lee (Computer Science and Artificial Intelligence Laboratory (CSAIL) at MIT ) talks about "Linguistic and System Support for Structured Parallel Programming"

SWS Colloquium
10 Mar 2014, 10:30 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
Parallel programming is hard.  Most parallel programs today deal with the complexities of parallel programming such as scheduling and synchronization using low-level system primitives such as pthreads locks and condition variables.  Although these low-level primitives are flexible like goto statements they lack structure and make it difficult for the programmer to reason locally about the program state.  Just as goto has been mostly deprecated in ordinary serial programming in favor of structured control constructs we can simplify parallel programming by replacing these low-level concurrency primitives with linguistic constructs that enable well structured parallel programs.  Of course elegant linguistic structure is only half the battle.  The underlying system must also efficiently support the linguistics allowing the programmer to write fast code.

I have developed several new parallel linguistic constructs and devised new more efficient runtime support for other constructs invented by others.  In this talk I will focus largely on one example: a pipe_while construct that supports pipeline parallelism a programming pattern commonly used in streaming applications.   This example provides a case study of how well-designed linguistics for structured parallel programming can simplify parallel programming while allowing the runtime system to execute the linguistic model efficiently.  This work has had some impact since its publication --- Intel released an experimental branch of Cilk Plus that incorporates support for parallel pipelining based on this work.  I will also mention other examples from my research to demonstrate how novel mechanisms in operating systems and hardware not just the runtime can help provide efficient support for parallel-programming linguistics.

On the importance of Internet eXchange Points for today's Internet ecosystem

Anja Feldmann
Telekom Innovation Laboratories, TU Berlin
SWS Distinguished Lecture Series
06 Mar 2014, 2:15 pm - 4:15 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
Internet eXchange Points (IXPs) are generally considered to be the successors of the four Network Access Points that were mandated as part of the decommissioning of the NSFNET in 1994/95 to facilitate the transition to "public Internet" as we know it today. While this does not tell the whole story of the early beginnings what is true is that since around 1994 the number of IXPs has grown to more than 300 with the largest IXPs handling traffic volumes comparable to those of Tier-1 ISPs. But IXPs have never attracted much attention from the research community. At first glance this lack of interest seems understandable as IXPs have apparently little to do with current "hot" topic areas such as data centers and cloud services or software defined networking (SDN) and mobile communication. However we argue that in fact IXPs are not only cool monitoring points with huge visibility but are all about Internet connectivity data centers and cloud services and even SDN and mobile communication. To this end we in this talk start with an overview of the basic technical and operational aspects of IXPs and then highlight some of our research results regarding application mix AS-graph Internet infrastructure distribution and traffic flows.

Machine Learning for Social Systems: Modeling Opinions, Activities, and Interactions

Julian McAuley
Stanford University
SWS Colloquium
06 Mar 2014, 11:30 am - 2:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
The proliferation of user-generated content on the web provides a wealth of opportunity to study humans through their online traces. I will discuss three aspects of my research which aims to model and understand people's behavior online. First I will develop rich models of opinions by combining structured data (such as ratings) with unstructured data (such as text). Second I will describe how preferences and behavior evolve over time in order to characterize the process by which people "acquire tastes" for products such as beer and wine. Finally I will discuss how people organize their personal social networks into communities with common interests and interactions. These lines of research require models that are capable of handling high-dimensional interdependent and time-evolving data in order to gain insights into how humans behave.

Formal Reasoning about Relaxed Concurrency

Viktor Vafeiadis
Max Planck Institute for Software Systems
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
05 Mar 2014, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Despite what most reasoning techniques assume concurrent programs do run under sequentially consistency but rather under a relaxed memory model such as the recent C/C++ model. There has been a lot of work on specifying such relaxed models but very little yet on reasoning about programs under relaxed concurrency semantics. Recently at MPI-SWS we have tackled this problem and developed a bunch of relaxed program logics that encompass sound reasoning principles for concurrent programs running under the C/C++ relaxed memory model. The talk will provide a gentle introduction to the C/C++ memory model and our newly developed reasoning principles.

How to find a good program abstraction automatically?

Hongseok Yang
University of Oxford
SWS Distinguished Lecture Series
04 Mar 2014, 10:30 am - 12:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
Recent years have seen the development of successful commercial programming tools based on static analysis technologies which automatically verify intended properties of programs or find tricky bugs that are difficult to detect by testing techniques. One of the key reasons for this success is that these tools use clever strategies for abstracting programs -- most details about a given program are abstracted away by these strategies unless they are predicted to be crucial for proving a given property about the program or detecting a type of program errors of interest. Developing such a strategy is however nontrivial and is currently done by a large amount of manual engineering efforts in most tool projects. Finding a good abstraction strategy automatically or even reducing these manual efforts involved in the development of such a strategy is considered one of the main open challenges in the area of program analysis.

In this talk I will explain how I tried to address this challenge with colleagues in the US and Korea in the past few years. During this time we worked on parametric program analyses where parameters for controlling the degree of program abstraction are expressed explicitly in the specification of the analyses. For those analyses we developed algorithms for searching for a desired parameter value with respect to a given program and a given property which use ideas from the neighboring areas of program analysis such as testing searching and optimisation. In my talk I will describe the main ideas behind these algorithms without going into technical details. I will focus on intuitions about why and when these algorithms work. I will also talk briefly about a few lessons that I learnt while working on this problem.

This talk is based on the joint work with Mayur Naik Xin Zhang Ravi Mangal Radu Grigore Hakjoo Oh Wonchan Lee Kihong Heo and Kwangkeun Yi.

Automating Construction of Provably Correct Software

Prof. Viktor Kuncak
EPFL, Switzerland
SWS Distinguished Lecture Series
27 Feb 2014, 10:30 am - 12:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
I will present techniques my research group has been developing to transform reusable software specifications suitable for users and designers into executable implementations suitable for efficient execution. I outline deductive synthesis techniques that transform input/output behavior descriptions (such as postconditions invariants and examples) into conventional functions form inputs to outputs. We have applied these techniques to complex functional data structures out of core database algorithms as well as numerical computations.

Privacy Preserving Technologies and an Application to Public Transit Systems

Foteini Baldimtsi,
Brown University
SWS Colloquium
26 Feb 2014, 11:30 am - 1:30 pm
Saarbrücken building E1 5, room 029
Ubiquitous electronic transactions give us efficiency and convenience but introduce security and reliability issues and affect user privacy. Consider for example how much more private information is revealed during online shopping compared to what leaks in physical transactions that are paid in cash. Luckily cryptographic research gives us the tools to achieve efficient and secure electronic transactions that at the same time preserve user privacy. Anonymous credentials is one such tool that allows users to prove possession of credentials while revealing the minimum amount of information required. In the first part of this talk we present "Anonymous Credentials Light": the first provably secure construction of anonymous credentials that is based on the DDH assumption and can work in the elliptic group setting without bilinear pairings. Our construction requires just a few exponentiations in a prime-order group in which the DDH problem is hard which makes it suitable for mobile devices RFIDs and smartcards.

In the second part of the talk we explain how we can get secure e-cash with attributes from our construction and we show implementation results in an NFC enabled smartphone. The efficiency of our scheme is comparable to Brands e-cash which is known to be the most efficient e-cash scheme in the literature but as a recently work of us shows it is impossible to prove it secure under the currently known techniques.

Decidable Verification of Database-powered Business Processes

Prof. Alin Deutsch
University of California, San Diego
SWS Distinguished Lecture Series
24 Feb 2014, 10:30 am - 12:30 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
This talk addresses the static verification problem for data-centric business processes using as vehicle the "business artifact" model recently deployed by IBM in commercial products and consulting services and studied in an increasing line of research papers.

Artifacts are records of variables that correspond to business-relevant objects and are updated by a set of services equipped with pre-and post-conditions that implement business process tasks. For the purpose of this talk the verification problem consists in statically checking whether all runs of an artifact system satisfy desirable properties expressed in (some first order extension of) a temporal logic.

The talk surveys results that identify various practically significant classes of business artifact systems with decidable verification problem. The talk is based on a series of prior and current work conducted jointly with Elio Damagio David Lorant Yuliang Li Victor Vianu (UCSD) and Richard Hull (IBM TJ Watson).

Exposing and Detecting Concurrency Bugs in Large-Scale Software

Pedro Fonseca
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
18 Feb 2014, 11:00 am - 1:00 pm
Saarbrücken building E1 5, room 029
In the current multi-core era concurrency bugs are a serious threat to software reliability. As hardware becomes more parallel concurrent programming will become increasingly pervasive. However correct concurrent programming is known to be extremely challenging for developers and a source of concurrency bugs. In this work we propose to develop mechanisms to help developers to expose and detect concurrency bugs.

We conducted a real-world concurrency bug study to better understand the external and internal effects of real-world concurrency bugs. In this study we found that a significant fraction of concurrency bugs qualify as semantic or latent bugs which are two particularly challenging classes of concurrency bugs. Based on the insights from our study we propose a concurrency bug detector that analyzes the behavior of program executions to infer whether concurrency bugs have been triggered during a concurrent execution. Our bug detector analyzes the external behavior (i.e. output produced) and the internal behavior (i.e. state changes) of a program execution to detect these particularly challenging classes of concurrency bugs. It compares the program output of different executions to detect concurrency bugs that manifest themselves by providing wrong results to the user (i.e. semantic concurrency bugs). In addition it also compares the internal state of different executions to detect concurrency bugs that do not immediately manifest themselves to the user when they are triggered (i.e. latent concurrency bugs). We applied our bug detector to MySQL and we were able to find various instances of concurrency bugs of both of these classes.

In addition we propose a testing tool to allow developers to test operating system kernels for concurrency bugs. The goal of our tool is to bridge the gap between user-mode testing and kernel-mode testing by enabling systematic exploration of the kernel thread interleaving space. We will achieve this systematic exploration through fine-grained control over the execution of individual threads. Unlike similar tools for the user-mode context achieving fine-grained control over the execution of kernel threads is hard because the kernel is itself the software layer that implements the thread abstraction the scheduler and the synchronization primitives. This process is further complicated by the existence in the kernel of additional concurrency mechanisms (i.e. interrupts) and synchronization mechanisms. Our proposed system will allow developers to efficiently expose concurrency bugs by combining the fine-grained control mechanism with smart heuristics that determine which thread interleavings to explore first. In addition our approach does not require modifications to the kernel which is an important characteristic to make the tool practical. The key idea of our approach is to use a modified virtual machine implementing a custom scheduling algorithm to control the thread interleavings. In turn this virtual machine is combined with existing concurrency bug detectors to flag the executions that trigger concurrency bugs.

Operating System Services for High-Throughput Accelerators

Mark Silberstein
Technion, Israel Institute of Technology
SWS Colloquium
17 Feb 2014, 2:00 pm - 4:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
Future applications will need to use programmable high-throughput accelerators like GPUs to achieve their performance and power goals. However building efficient systems that use accelerators today is incredibly difficult. I argue that the main problem lies in the lack of appropriate OS support for accelerators -- while OSes provide optimized resource management and I/O services to CPU applications they make no such services available to accelerator programs.

I propose to build an operating system layer for GPUs which provides I/O services via familiar OS abstractions directly to programs running on GPUs. This layer effectively transforms GPUs into first-class computing devices with full I/O support extending the constrained GPU-as-coprocessor programming model.

As a concrete example I will describe GPUfs a software layer which enables GPU programs to access host files. GPUfs provides a POSIX-like API exploits parallelism for efficiency and optimizes for access locality by extending a CPU buffer cache into physical memories of all GPUs and CPUs in a single machine. Using real benchmarks I will show that GPUfs simplifies the development of efficient applications by eliminating the GPU management complexity and broadens the range of applications that can be accelerated by GPUs. For example a simple self-contained GPU program which searches for a set of strings in the entire tree of Linux kernel source files completes in about third of the time of an 8-core CPU run.

I will then describe my ongoing work on native network support for GPUs current open problems and future directions.

The talk is self-contained no background in GPU computing is necessary.

This is a joint work with Emmett Witchel Bryan Ford Idit Keidar and UT Austin students.

A Type System for Incremental Computational Complexity

Ezgi Cicek
Max Planck Institute for Software Systems
SWS Student Defense Talks - Qualifying Exam
13 Feb 2014, 2:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
With recent advances in incremental computation programs can be compiled to automatically respond to incremental input changes. However there is no language-level support for reasoning about the asymptotic time complexity of incremental updates. Motivated by this gap we equip a list-processing language with a cost-accounting semantics and a type system for compositionally proving the complexity of such updates. Our type system includes novel refinements that bound changes to inputs and captures dynamic stability a measure of the time required to re-run a program given the trace of an earlier execution with boundedly different inputs. Effectively our type system proves a computational continuity property that bounds not only output changes but also changes to the trace as a function of input changes. We prove our type system sound relative to the cost semantics and verify experimentally that the cost semantics is realistic in practice.

Beyond Multi-Touch: User Interfaces for Flexible Displays and Surfaces

Jürgen Steimle
Cluster of Excellence - Multimodal Computing and Interaction - MMCI
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
12 Feb 2014, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Present-day computers are rectangular and rigid. This limits mobile computing on-body interfaces and ubiquitous computing. The aim of my research is to contribute to defining and understanding a new paradigm of Human-Computer Interaction: deformable paper-thin and flexibly shaped interfaces. This paradigm has the potential to revolutionize Human-Computer Interaction. As one example I envision that future interactive devices will have the form factor of paper-thin stickers. These stickers are deformable of various shapes and sizes provide high resolution display output and support touch and deformation sensing for input. They enable to easily make any surface interactive including human skin clothing or physical objects. By radically redefining the form factor of computing devices flexibility opens up previously impossible scenarios of use for more mobile more direct and more versatile interaction with computers. This poses unique scientific challenges regarding interaction technologies and interaction techniques. My research addresses these challenges from a user-centered perspective driven by visions of future computing. 1) Interaction technologies: Conventional sensors and displays are based on rigid electronics. Substantially different technical solutions are required to meet the demands of flexibility ultra-thin form factors and arbitrary shapes. Moreover flexibility yields novel input modalities that need to be captured e.g. deformation pressure or cutting. Informed by user needs that we derive from empirical studies we develop novel multi-modal sensors and displays to technically enable flexible interfaces. 2) Interaction techniques: Novel modalities of interaction and novel contexts of use open a design space of interaction techniques which is largely unstudied. We systematically model and study mappings between input and output to define a vocabulary of interactions and inform applications that are useful and usable meaningful and make the most of the differentiating properties of this new paradigm. In my talk I will present this research agenda and first results achieved. I will present PrintSense a paper-thin fully flexible multi-modal sensor surface. In addition to multi-touch input this sensor captures proximity pressure input and deformation. Moreover it can be cut to various shapes while remaining functional. The sensor can be easily produced and deployed in a variety of scenarios including deformable smart phones and tablets interactive paper smart products and on-body interfaces.

Real-time Scheduling and Mixed-Criticality Systems

Sanjoy Baruah
University of North Carolina at Chapel Hill
SWS Distinguished Lecture Series
10 Feb 2014, 2:00 pm - 4:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
In the context of computer systems scheduling theory seeks to enable the efficient utilization of computing resources in order to optimize specified system-wide objectives. In this presentation we will examine how real-time scheduling theory is dealing with the recent trend in embedded systems towards implementing functionalities of different levels of importance or criticalities upon a shared platform. We will explore the factors that motivated this trend towards mixed-criticality (MC) systems discuss how these MC systems pose new challenges to real-time scheduling theory and describe how real-time scheduling theory is responding to these challenges by devising new models and methods for the design and analysis of MC systems.

Components for Building Secure Decentralized Networks

Christian Grothoff
TU Muenchen
SWS Colloquium
23 Jan 2014, 4:00 pm - 6:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
This talk will present technical solutions towards a secure and fully decentralized future Internet with focus on the GNU Name System. The GNU Name System is a new decentralized public key infrastructure which we propose as an alternative to DNS(SEC) and X.509 in particular for online social networking applications. I will also give an overview of the GNUnet architecture and give pointers to ongoing related research.

Differential Guarantees for Cryptographic Systems

Aniket Kate
Cluster of Excellence - Multimodal Computing and Interaction - MMCI
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
08 Jan 2014, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Differential privacy aims at learning information about the population as a whole while protecting the privacy of each individual. With its quantifiable privacy and utility guarantees differential privacy is becoming standard in the field of privacy-preserving data analysis. On the other hand most cryptographic systems for their privacy properties rely on a stronger notion of indistinguishability where an adversary should not be able to (non-negligibly) distinguish between two scenarios. Nevertheless there exists some cryptographic system scenarios for which the notion of indistinguishability is known to be impossible to achieve. It is natural to ask if one can define differential privacy-motivated privacy notions to accurately quantify the privacy loss in those scenarios. In this talk we will study two such scenarios.

Our first scenario will consider (non-)uniform randomness employed in cryptographic primitives. It is well-known that indistinguishability-based definitions of cryptographic primitives are impossible to realize in systems where parties only have access to non-extractable sources of randomness. I will demonstrate that it is nevertheless possible to quantify this secrecy (or privacy) loss due to some non-extractable sources (such as the Santha-Vazirani sources) using a generalization of indistinguishability inspired by differential privacy.

Our second scenario will capture privacy properties of anonymous communication networks (e.g. Tor). In particular I will present our AnoA framework that relies on a novel relaxation of differential privacy to enables a unified quantitative analysis of properties such as sender anonymity sender unlinkability and relationship anonymity.