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.

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 

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.

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.

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.

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.

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.

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).

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.

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.

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.

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.

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.

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.

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.

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.

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.

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. 

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.

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.

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.

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.

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.

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)

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.

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.

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.

Many applications exhibit the property that small, localized changes to the input result in only minor changes to the output. Incremental computations seek to exploit this observation to speed-up successive runs of an application by tracking control and data dependencies, and re-executing only those parts of the computation that are affected by a given input change. To realize the benefits of incremental computation, researchers and practitioners are developing new systems where the programmer can provide efficient update mechanisms for changing application data. Unfortunately, most of the existing solutions are limiting because they either depart from existing programming models, or require programmers to devise an incremental update mechanism (or a dynamic algorithm) on a per-application basis.

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

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

The 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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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).

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.

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.

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.

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.

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.

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.