Events 2014

Formalising and Optimising Parallel Snapshot Isolation

Alexey Gotsman IMDEA
19 Dec 2014, 1:00 pm
Kaiserslautern building G26, room 111
SWS Colloquium
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. ...
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).
Read more

CoLoSL: Concurrent Local Subjective Logic

Azalea Raad Imperial College London
15 Dec 2014, 2:00 pm - 3:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Colloquium
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. ...
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.
Read more

An SMT-Based Approach to Coverability Analysis

Filip Niksic Max Planck Institute for Software Systems
12 Dec 2014, 2:00 pm - 3:00 pm
Kaiserslautern building G26, room 111
SWS Student Defense Talks - Qualifying Exam
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. ...
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.
Read more

Scaling TCP performance for multicore systems

KyoungSoo Park KAIST
09 Dec 2014, 11:30 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Colloquium
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. ...
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.
Read more

Authenticated Data Structures, Generically

Michael W. Hicks University of Maryland
05 Dec 2014, 1:30 pm - 3:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 207
SWS Colloquium
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), ...
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
Read more

Towards Non-tracking Web and Mobile Analytics

Istemi Ekin Akkus Max Planck Institute for Software Systems
04 Dec 2014, 2:00 pm - 3:00 pm
Kaiserslautern building G26, room 112
simultaneous videocast to Saarbrücken building E1 5, room 005
SWS Student Defense Talks - Thesis Proposal
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, ...
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.
Read more

Algorithmic Challenges in Computational Genomics

Tobias Marschall MPI-INF - D3
03 Dec 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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. ...
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.
Read more

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

Robert West Stanford University
26 Nov 2014, 11:00 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Colloquium
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. ...
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)
Read more

Thoth: Practical Data flow protection in a search engine

Aastha Mehta Max Planck Institute for Software Systems
21 Nov 2014, 3:00 pm - 4:00 pm
Saarbrücken building E1 5, room 422
SWS Student Defense Talks - Qualifying Exam
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. ...
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.
Read more

mhmm: Making Haskell More Modular

Scott Kilpatrick Max Planck Institute for Software Systems
20 Nov 2014, 2:00 pm - 3:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Student Defense Talks - Thesis Proposal
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. ...
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.
Read more

Randomized Solutions to Renaming under Crashes and Byzantine Faults

Oksana Denysyuk INESC-ID and University of Lisbon
17 Nov 2014, 2:00 pm - 3:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Colloquium
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. ...
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 Read more

Yesquel: scalable SQL storage for Web applications

Marcos K. Aguilera unaffiliated
17 Nov 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
SWS Distinguished Lecture Series
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, ...
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.
Read more

Generalized Universality

Rachid Guerraoui EPFL
12 Nov 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 002
SWS Distinguished Lecture Series
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. ...
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 
Read more

Scalable personalization infrastructures

Anne-Marie Kermarrec Inria
11 Nov 2014, 11:30 am - 1:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
SWS Distinguished Lecture Series
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.  ...
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.
Read more

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

Christian Rossow Cluster of Excellence - Multimodal Computing and Interaction - MMCI
05 Nov 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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. ...
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.
Read more

Using Twitter to study Food Consumption and Fitness Behavior

Ingmar Weber MPI-INF - D1
05 Nov 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

Machine Learning about People from their Language

Noah Smith Carnegie Mellon University
04 Nov 2014, 3:30 pm - 4:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Distinguished Lecture Series
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. ...
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.
Read more

MultiSE: Multi-Path Symbolic Execution using Value Summaries

Koushik Sen UC Berkeley
30 Oct 2014, 4:00 pm - 5:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 002
SWS Colloquium
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, ...
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.
Read more

Vellvm: Verifying Safety in the LLVM IR

Steve Zdancewic University of Pennsylvania
09 Oct 2014, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Colloquium
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. ...
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).
Read more

Termination of Linear Programs: Advances and Challenges

Dr. Joel Ouaknine University of Oxford
02 Oct 2014, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Distinguished Lecture Series
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, ...
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.
Read more

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

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

Private-by-Design Advertising Meets the Real World

Alexey Reznichenko Max Planck Institute for Software Systems
26 Sep 2014, 3:30 pm - 4:30 pm
Kaiserslautern building G26, room 111
SWS Student Defense Talks - Thesis Defense
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, ...
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.
Read more

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

Viktor Erdélyi Max Planck Institute for Software Systems
12 Aug 2014, 3:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Qualifying Exam
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. ...
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.
Read more

Leveraging Sharding in the Design of Scalable Replication Protocols

Robbert van Renesse Cornell University
08 Aug 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Distinguished Lecture Series
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
06 Aug 2014, 3:30 pm - 4:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
SWS Colloquium
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. ...
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.
Read more

Probabilistic Methods for the Analysis of Biological Networks

Marcel Schulz Cluster of Excellence - Multimodal Computing and Interaction - MMCI
06 Aug 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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. ...
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.
Read more

Trace Complexity

Flavio Chierichetti Sapienza University of Rome
30 Jul 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
SWS Colloquium
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, ...
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.

Read more

Tracking information flow in web applications

Andrei Sabelfeld Chalmers University
24 Jul 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Distinguished Lecture Series
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. ...
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.
Read more

Compositional Verification of Termination-Preserving Refinement of Concurrent Programs

Hongjin Liang UST China
23 Jul 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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, ...
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.
Read more

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

Andreas Karrenbauer MPI-INF - D1
02 Jul 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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. ...
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.
Read more

Information flow control for javascript in web browsers

Vineet Rajani Max Planck Institute for Software Systems
16 Jun 2014, 1:00 pm - 2:00 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Qualifying Exam
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. ...
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. 
Read more

Exploratory Data Analysis

Jilles Vreeken Cluster of Excellence - Multimodal Computing and Interaction - MMCI
04 Jun 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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, ...
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.
Read more

Adventures in Program Synthesis

Ras Bodik UC Berkeley
22 May 2014, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Distinguished Lecture Series
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. ...
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.
Read more

Modeling and representing materials in the wild

Kavita Bala Cornell University
08 May 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Distinguished Lecture Series
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, ...
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.
Read more

Approximation Algorithms for Packing Problems

Andreas Wiese MPI-INF - D1
07 May 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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. ...
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.
Read more

Lazy Bit-vector Solving and Witnessing Compiler Transformations

Liana Hadarean NYU
05 May 2014, 2:00 pm - 3:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

Modular Reasoning about Heap Paths via Effectively Propositional Formulas

Ori Lahav Tel Aviv University
24 Apr 2014, 10:30 am - 11:30 am
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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)
Read more

Mobile multi-cores: power and performance

Aaron Carroll NICTA, Sydney
23 Apr 2014, 11:00 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Colloquium
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, ...
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.
Read more

Practical Real-Time with Look-Ahead Scheduling

Dr. Michael Roitzsch TU Dresden
23 Apr 2014, 10:00 am - 11:00 am
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

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

Dr. Andrew Myers Cornell University, Ithaca
10 Apr 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Distinguished Lecture Series
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. ...
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.
Read more

Incremental Parallel and Distributed Systems

Pramod Bhatotia Max Planck Institute for Software Systems
07 Apr 2014, 5:00 pm - 6:00 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Thesis Proposal
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. ...
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.
Read more

The Cyberspace Battle for Information: Combating Internet Censorship

Amir Houmansadr University of Texas at Austin
07 Apr 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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, ...
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.
Read more

Towards a Secure Client-side for the Web Platform

Devdatta Akhawe UC Berkeley
03 Apr 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

A hybrid moment closure approach to stochastic chemical kinetics

Verena Wolf Fachrichtung Informatik - Saarbrücken
02 Apr 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
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. ...
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.
Read more

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

Cezara Dragoi IST Austria
27 Mar 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

Equivalence checking of stack-based infinite-state systems

Stefan Goeller University of Bremen
24 Mar 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

Structure and Dynamics of Diffusion Networks

Manuel Gomez Rodriguez Max Planck Institute for Intelligent Systems
13 Mar 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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, ...
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.
Read more

Can You Hide in an Internet Panopticon?

Bryan Ford Yale University
12 Mar 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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, ...
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.
Read more

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

10 Mar 2014, 10:30 am - 12:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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.   ...
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.
Read more

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

Anja Feldmann Telekom Innovation Laboratories, TU Berlin
06 Mar 2014, 2:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
SWS Distinguished Lecture Series
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. ...
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.
Read more

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

Julian McAuley Stanford University
06 Mar 2014, 11:30 am - 1:00 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

Formal Reasoning about Relaxed Concurrency

Viktor Vafeiadis Max Planck Institute for Software Systems
05 Mar 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
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. ...
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.
Read more

How to find a good program abstraction automatically?

Hongseok Yang University of Oxford
04 Mar 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
SWS Distinguished Lecture Series
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. ...
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.
Read more

Automating Construction of Provably Correct Software

Prof. Viktor Kuncak EPFL, Switzerland
27 Feb 2014, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 111
SWS Distinguished Lecture Series
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
26 Feb 2014, 11:30 am - 12:30 pm
Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.

Read more

Decidable Verification of Database-powered Business Processes

Prof. Alin Deutsch University of California, San Diego
24 Feb 2014, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Distinguished Lecture Series
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. ...
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).
Read more

Exposing and Detecting Concurrency Bugs in Large-Scale Software

Pedro Fonseca Max Planck Institute for Software Systems
18 Feb 2014, 11:00 am - 12:00 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Thesis Proposal
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 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.
Read more

Operating System Services for High-Throughput Accelerators

Mark Silberstein Technion, Israel Institute of Technology
17 Feb 2014, 2:00 pm - 3:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Colloquium
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. ...
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.
Read more

A Type System for Incremental Computational Complexity

Ezgi Cicek Max Planck Institute for Software Systems
13 Feb 2014, 2:00 pm - 3:00 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Qualifying Exam
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, ...
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.
Read more

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

Jürgen Steimle Cluster of Excellence - Multimodal Computing and Interaction - MMCI
12 Feb 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
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, ...
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.
Read more

Real-time Scheduling and Mixed-Criticality Systems

Sanjoy Baruah University of North Carolina at Chapel Hill
10 Feb 2014, 2:00 pm - 3:30 pm
Kaiserslautern building G26, room 113
simultaneous videocast to Saarbrücken building E1 5, room 029
SWS Distinguished Lecture Series
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, ...
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.
Read more

Components for Building Secure Decentralized Networks

Christian Grothoff TU Muenchen
23 Jan 2014, 4:00 pm - 5:00 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 113
SWS Colloquium
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
08 Jan 2014, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series of MPI-INF, MPI-SWS and MMCI
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. ...
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.
Read more