The goal of under-approximating logics, such as incorrectness logic, is to reason about the existence of bugs  by specifying a subset of possible program behaviour. While this approach allows for the specification of a broad range of bugs, it does not account for divergence bugs (such as infinite loops), since the nature of the triple itself does not allow statements about infinite execution traces.     To fill this gap, I will present a divergent variant of the forward under-approximating (FUA) triple. This new separation logic reasons functionally compositionally about divergence bugs and is under-approximating in the sense that all specified bugs are true bugs, that is, reachable. It can detect divergence originating from loops, recursive function calls and goto-cycles.     I will motivate the talk by defining the type of divergent programs we are aiming to reason about, and show how previously introduced logics fall short of specifying their divergent behaviour. After introducing the FUA triple, I will outline how this triple differs from traditional over-approximating  and under-approximating approaches such as (partial) Hoare logic and incorrectness logic. Finally, I will discuss the mechanisms within the FUX framework that enable reasoning about divergence, with a focus on how to prove divergence arising from goto-cycles.

--

Please contact the office team for the Zoom link details.

Presburger arithmetic, or linear integer arithmetic, is known to have decision procedures that work in triply exponential time.

Jointly with M. Benedikt (Oxford) and A. Mansutti (IMDEA Software Institute), we have recently considered two decidable extensions of Presburger arithmetic: with the power function and with the predicate for the set of powers of 2. No elementary decision procedures were known for these two theories.

In this talk, I will introduce this work and outline ideas behind our results. Namely, we have shown that existence of solutions over N to systems of linear equations and constraints of the form $y = 2^x$ can be decided in nondeterministic exponential time. Also, linear integer arithmetic extended with a predicate for powers of 2 can be decided in triply exponential time.

(Based on a paper in ICALP'23.)

Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce.

Despite rigorous testing, concurrency bugs such as races conditions often find their way into production software, and manifest as critical security issues. Consequently, considerable effort has been made towards developing efficient techniques for detecting them automatically.

The preferred approach to detect data races is through dynamic analysis, where one executes the software with some test inputs, and checks for the presence of bugs in the execution observed.

Traditional bug detectors however are often unable to discover simple bugs present in the underlying software, even after executing the program several times, because these bugs are sensitive to thread scheduling.

In this talk, I will discuss how runtime predictive analysis can help. Runtime predictive analyses aim to expose concurrency bugs, that can be otherwise missed by traditional dynamic analysis techniques (such as the race detector TSan), by inferring the presence of these bugs in alternate executions of the underlying software, without explicitly re-executing the software program.

I will talk about the fundamentals of and recent algorithmic advances for building highly scalable and sound predictive analysis techniques.

After discovering, back in 2011, that Language Models are useful for modeling repetitive patterns in source code (c.f. The "Naturalness" of software ), and exploring some applications thereof, more recently (since about 2019) our group at UC Davis has focused on the observation that Software, as usually written, is bimodal, admitting both the well-known formal, deterministic semantics (mostly for machines) and probabilistic, noisy semantics (for humans). This bimodality property affords both new approaches to software tool construction (using machine-learning) and new ways of studying human code reading. In this talk, I'll give an overview of the Naturalness/Bimodality program, and some recent work we have done on calibrating the quality of code produced by large language models, and also on "bimodal prompting".

--

Please contact the office team for link information

Machine learning algorithms curate much of the content we encounter online. However, there is concern that these algorithms may unintentionally amplify hostile discourse and perpetuate divisive 'us versus them' mentalities. How can we re-engineer algorithms to bridge diverse perspectives and facilitate constructive conflict? First, I will discuss results from our randomized experiment measuring effects of Twitter’s engagement-based ranking algorithm on downstream sociopolitical outcomes like the amplification of divisive content and users’ perceptions of their in-group and out-group. Crucially, we found that an alternative ranking, based on users’ stated preferences rather than their engagement, reduced amplification of negative, partisan, and out-group hostile content. Second, I will discuss how we applied these insights in practice to design an objective function for algorithmic ranking at Twitter. The core idea to the approach is to interpret users' actions in a way that is consistent with their stated, reflective preferences. Finally, I will discuss lessons learned and open questions for designing algorithms that support a plurality of viewpoints, with an emphasis on the emerging paradigm of bridging-based ranking.

With the development of big data, machine learning, and AI, existing software engineering techniques must be re-imagined to provide the productivity gains that developers desire. Furthermore, specialized hardware accelerators like GPUs or FPGAs have become a prominent part of the current computing landscape. However, developing heterogeneous applications is limited to a small subset of programmers with specialized hardware knowledge. To improve productivity and performance for data-intensive and compute-intensive development, now is the time that the software engineering community should design new waves of refactoring, testing, and debugging tools for big data analytics and heterogeneous application development.

In this talk, we overview software development challenges in this new data-intensive scalable computing and heterogeneous computing domain. We describe examples of automated software engineering (debugging, testing, and refactoring) techniques that target this new domain and share lessons learned from building these techniques.

Machine learning provides us with an amazing set of tools to make predictions, but how much should we trust particular predictions? To answer this, we need a way of estimating the confidence we should have in particular predictions of black-box models. Standard tools for doing this give guarantees that are averages over predictions. For instance, in a medical application, such tools might paper over poor performance on one medically relevant demographic group if it is made up for by higher performance on another group. Standard methods also depend on the data distribution being static — in other words, the future should be like the past.

In this talk, I will describe new techniques to address both these problems: a way to produce prediction sets for arbitrary black-box prediction methods that have correct empirical coverage even when the data distribution might change in arbitrary, unanticipated ways and such that we have correct coverage even when we zoom in to focus on demographic groups that can be arbitrary and intersecting. When we just want correct group-wise coverage and are willing to assume that the future will look like the past, our algorithms are especially simple.

This talk is based on two papers, that are joint work with Osbert Bastani, Varun Gupta, Chris Jung, Georgy Noarov, and Ramya Ramalingam.

Please contact the office team for link information

In recent years, humanity has been faced with a new resource - artificial intelligence. AI can be a boon to society, or can also have negative impacts, especially with inappropriate use. My research agenda studies the societal impact of AI, particularly focusing on AI as a resource and on the strategic decisions that agents make in deciding how to use it. In this talk, I will consider some of the key strategic questions that arise in this framework: the decisions that agents make in jointly constructing and sharing AI models, and the decisions that they make in dividing tasks between their own expertise and the expertise of a model. The first of these questions has motivated my work on "model-sharing games", which models scenarios such as federated learning or data cooperatives. In this setting, we view agents with data as game-theoretic players and analyze questions of stability, optimality, and fairness (https://arxiv.org/abs/2010.00753, https://arxiv.org/abs/2106.09580, https:// arxiv.org/abs/2112.00818). Secondly, I will describe some of my ongoing work in modeling human-algorithm collaboration. In particular, I will describe work on best-item recovery in categorical prediction, showing how differential accuracy rates and anchoring on algorithmic suggestions can influence overall performance (https://arxiv.org/abs/2308.11721).

Large language Models (LLMs, e.g., GPT-3, OPT, TNLG,…) are shown to have a remarkably high performance on standard benchmarks, due to their high parameter count, extremely large training datasets, and significant compute. Although the high parameter count in these models leads to more expressiveness, it can also lead to higher memorization, which, coupled with large unvetted, web-scraped datasets can cause different negative societal and ethical impacts such as leakage of private, sensitive information and generation of harmful text. In this talk, we will go over how these issues affect the trustworthiness of LLMs, and zoom in on how we can measure the leakage and memorization of these models, and mitigate it through differentially private training. Finally we will discuss what it would actually mean for LLMs to be privacy preserving, and what are the future research directions on making large models trustworthy.

In this talk, I will explore three elements of designing next-generation machine learning systems: congestion control, network topology, and computation frequency. I will show that fair sharing, the holy grail of congestion control algorithms, is not necessarily desirable for deep neural network training clusters. Then I will introduce a new optical fabric that optimally combines network topology and parallelization strategies for machine learning training clusters. Finally, I will demonstrate the benefits of leveraging photonic computing systems for real-time, energy-efficient inference via analog computing. I will discuss that pushing the frontiers of optical networks for machine learning workloads will enable us to fully harness the potential of deep neural networks and achieve improved performance and scalability.

Given a sentence $\forall X \exists Y \varphi(X, Y)$ in a first-order theory, it is well-known that there exists a function $F(X)$ for $Y$ in $\varphi$ such that $\exists Y \varphi(X, Y)\leftrightarrow \varphi(X, F(X))$ holds for all values of the universal variables X. Such a function is also called a Skolem function, in honour of Thoralf Skolem who first made us of this in proving what are now known as the Lowenheim-Skolem theorems. The existence of a Skolem function for a given formula is technically analogous to the Axiom of Choice -- it doesn't give us any any hint about how to compute the function, although we know such a function exists. Nevertheless, since Skolem functions are often very useful in practical applications (like finding a strategy for a reactive controller), we investigate when is it possible to algorithmically construct a Turing machine that computes a Skolem function for a given first-order formula. We show that under fairly relaxed conditions, this cannot be done. Does this mean the end of the road for automatic synthesis of Skolem functions? Fortunately, no. We show model-theoretic necessary and sufficient condition for the existence and algorithmic synthesizability of Turing machines implementing Skolem functions. We show that several useful first-order theories satisfy these conditions, and hence admit algorithms that can synthesize Turing machines implementing Skolem functions. We conclude by presenting several open problems in this area.

Efficient data-intensive systems translate data into value for decision making. As data is collected at unprecedented rates for timely analysis, the model-centric paradigm of machine learning (ML) is shifting towards a data-centric and system-centric paradigm. Recent breakthroughs in large ML models (e.g., GPT 4 and ChatGPT) and the remarkable outcomes of reinforcement learning (e.g., AlphaFold and AlphaCode) have shown that scalable data management and its optimizations are critical to obtain state-of-the-art performance. This talk aims to answer the question "how to co-design multiple layers of the software/system stack to improve scalability, performance, and energy efficiency of ML and data-intensive systems". It addresses the challenges to build fully automated data-intensive systems that integrate the ML layer, the data management layer, and the compilation-based optimization layer. Finally, this talk will sketch and explore the vision to leverage the computational advantage of quantum computing on hybrid classic/quantum systems in the post-Moore era.

Please contact office for zoom link information.

In this talk, we consider synthesis of reactive systems interacting with environments using an infinite data domain. A popular formalism for specifying and modelling those systems is register automata and transducers. They extend finite-state automata by adding registers to store data values and to compare the incoming data values against stored ones. Synthesis from nondeterministic or universal register automata is undecidable in general. However, its register-bounded variant, where additionally a bound on the number of registers in a sought transducer is given, is known to be decidable for universal register automata which can compare data for equality, i.e., for data domain (N,=).

After briefly reviewing this result, we extend it to the domain (N,<) of natural numbers with linear order. Our solution is generic: we define a sufficient condition on data domains (regular approximability) for decidability of register-bounded synthesis. It allows one to use simple language-theoretic arguments and avoid technical game-theoretic reasoning. Further, by defining a generic notion of reducibility between data domains, we show the decidability of synthesis in the domain (N^d,<^d) of tuples of numbers equipped with the component-wise partial order and in the domain (Σ*, ≺) of finite strings with the prefix relation.

In the zoo of programming languages there are two cute yet rather misbehaved animals, typically found in the Dynamic Languages section: Duck Typing and Monkey Patching.

Duck Typing is hardly seen. You hear a "quack!", but you can’t easily tell if it’s coming form an actual duck, a parrot, or a recording. Monkey Patching, like the name suggests, patches any existing creature to change their behavior. It can even make a dog quack!

While these two animals bring lots of joy, they are also quite dangerous when used in the wild, as they can bring unexpected behavior to the rest of the creatures.

Crystal is a rarity among Static Languages in that it has Duck Typing and Monkey Patching. Given the strong —yet barely visible— fences of types, it manages to properly contain these beasts. In this talk I will present Crystal and provide a glimpse at how it manages to feel so dynamic.

Please contact office for zoom link information.

Smart contract languages are increasingly popular and numerous, and their programming models and challenges are somewhat unusual. The ubiquitous presence of untrusted external code in such a system makes classical contracts unsuitable for safety verification, while the intentional presence of (potentially-mutating) callbacks via unknown code makes standard static analysis techniques imprecise in general. On the other hand, smart contract languages such as Vyper (for Ethereum) tightly encapsulate direct access to the program's state. In this talk I'll present a methodology for expressing contracts for this language, in a way that supports sound verification of safety properties, with deductive verification tooling (converting Vyper to Viper) to automate the corresponding proofs.

Based on joint work with Christian Bräm, Marco Eilers, Peter Müller and Robin Sierra; see also the accompanying paper at OOPSLA 2021. --- Please contact Office for Zoom link information.

Cryptography provides the data protection mechanisms that underlie security and privacy in the modern connected world. Given this pivotal role, implementations of cryptographic code must not only be correct, but also meet stringent performance and security requirements. Achieving these aims is often difficult and requires significant investment in software development and manual tuning.

This talk presents two approaches for automating the task of generating correct, secure, and efficient cryptographic code. The first, Rosita, uses a power consumption emulator to detect unintended leaky interactions between values in the microarchitecture. It then rewrites the code to eliminate these interactions and produce code that is resistant to power analysis. The second, CryptOpt, uses evolutionary computation to search for the most efficient constant-time implementation of a cryptographic function. It then formally verifies that the produced implementation is semantically equivalent to the original code.

Rosita is a joint work with Lejla Batina, Łukasz Chmielewski, Francesco Regazzoni, Niels Samwel, Madura A. Shelton, and Markus Wagner.CryptOpt is a joint work with Adam Chlipala, Chitchanok Chuengsatiansup, Owen Conoly, Andres Erbsen, Daniel Genkin, Jason Gross, Joel Kuepper, Chuyue Sun, Samuel Tian, Markus Wagner, and David Wu.

Please contact office for zoom link information.

Abstract: Quantum pseudorandom states are efficiently constructable states which nevertheless masquerade as Haar-random states to poly-time observers. First defined by Ji, Liu and Song, such states have found a number of applications ranging from cryptography to the AdS/CFT correspondence. A fundamental question is exactly how much entanglement is required to create such states. Haar-random states, as well as t-designs for t≥2, exhibit near-maximal entanglement. Here we provide the first construction of pseudorandom states with only polylogarithmic entanglement entropy across an equipartition of the qubits, which is the minimum possible. Our construction can be based on any one-way function secure against quantum attack. We additionally show that the entanglement in our construction is fully "tunable", in the sense that one can have pseudorandom states with entanglement Θ(f(n)) for any desired function ω(logn)≤f(n)≤O(n). More fundamentally, our work calls into question to what extent entanglement is a "feelable" quantity of quantum systems. Inspired by recent work of Gheorghiu and Hoban, we define a new notion which we call "pseudoentanglement", which are ensembles of efficiently constructable quantum states which hide their entanglement entropy. We show such states exist in the strongest form possible while simultaneously being pseudorandom states. We also describe diverse applications of our result from entanglement distillation to property testing to quantum gravity.



Based on joint work with Bill Fefferman, Soumik Ghosh, Umesh Vazirani, and Zixin Zhou, arXiv:2211.00747

The vast amount of digital data we create and collect has revolutionized many scientific fields and industrial sectors. Yet, despite our success in harnessing this transformative power of data, computational and societal trends emerging from the current practices of data science necessitate upgrading our toolkit for data analysis. In this talk, we discuss how practical considerations such as privacy and memory limits affect statistical inference tasks. In particular, we focus on two examples: First, we consider hypothesis testing with privacy constraints. More specifically, how one can design an algorithm that tests whether two data features are independent or correlated with a nearly-optimal number of data points while preserving the privacy of the individuals participating in the data set. Second, we study the problem of entropy estimation of a distribution by streaming over i.i.d. samples from it. We determine how bounded memory affects the number of samples we need to solve this problem. Please contact office for zoom link information

Feedback allows systems to seamlessly and instantaneously adapt their behavior to their environment and is thereby the fundamental principle of life and technology -- it lets animals breathe, it stabilizes the climate, it allows airplanes to fly, and the energy grid to operate. During the last century, control technology excelled at using this power of feedback to engineer extremely stable, robust, and reliable technological systems.

With the ubiquity of computing devices in modern technological systems, feedback loops become cyber-physical -- the laws of physics governing technological, social or biological processes interact with (cyber) computing systems in a highly nontrivial manner, pushing towards higher and higher levels of autonomy and self-regulation. While reliability of these systems remains of utmost importance, a fundamental understanding of cyber-physical feedback loops for large-scale CPS is lacking far behind.

In this talk I will discuss how a control-inspired view on formal methods for reliable software design enables us to utilize the power of feedback for robust and reliable self-adaptation in cyber-physical system design.

Please contact office team for link information.

We entrust large parts of our daily lives to computer systems, which are becoming increasingly more complex. Developing scalable yet trustworthy techniques for designing and verifying such systems is an important problem. In this talk, our focus will be on automated synthesis, a technique that uses formal specifications to automatically generate systems (such as functions, programs, or circuits) that provably satisfy the requirements of the specification. I will introduce a state-of-the-art synthesis algorithm that leverages artificial intelligence to provide an initial guess for the system, and then uses formal methods to repair and verify the guess to synthesize probably correct system. I will conclude by exploring the potential for combining AI and formal methods to address real-world scenarios. Please contact the office team for link information.

Machine learning systems are deployed in diverse decision-making settings in service of stakeholders characterized by complex preferences. For example, in healthcare and finance, we ought to account for various levels of risk tolerance; and in personalized recommender systems, we face users whose preferences evolve dynamically over time. Building systems better aligned with stakeholder needs requires that we take the rich nature of human preferences into account. In this talk, I will give an overview of my research on the statistical and algorithmic foundations for building such human-centered machine learning systems. First, I will present a line of work that draws inspiration from the economics literature to develop learning algorithms that account for the risk preferences of stakeholders. Subsequently, I will discuss a line of work that draws insights from the psychology literature to develop online learning algorithms for personalized recommender systems that account for users’ evolving preferences. Please contact the office team for link information

Please note that this is a virtual talk which will be video casted to Saarbrücken and Kaiserslautern.

Traditionally, multimodal information consumption has been entity-centric with a focus on concrete concepts (such as objects, object types, physical relations, e.g., a person in a car), but lacks ability to understand abstract semantics (such as events and semantic roles of objects, e.g., driver, passenger, mechanic). However, such event-centric semantics are the core knowledge communicated, regardless whether in the form of text, images, videos, or other data modalities.

At the core of my research in Multimodal Information Extraction (IE) is to bring such deep semantic understanding ability to the multimodal world. My work opens up a new research direction Event-Centric Multimodal Knowledge Acquisition to transform traditional entity-centric single-modal knowledge into event-centric multi-modal knowledge. Such a transformation poses two significant challenges: (1) understanding multimodal semantic structures that are abstract (such as events and semantic roles of objects): I will present my solution of zero-shot cross-modal transfer (CLIP-Event), which is the first to model event semantic structures for vision-language pretraining, and supports zero-shot multimodal event extraction for the first time; (2) understanding long-horizon temporal dynamics: I will introduce Event Graph Model, which empowers machines to capture complex timelines, intertwined relations and multiple alternative outcomes. I will also show its positive results on long-standing open problems, such as timeline generation, meeting summarization, and question answering. Such Event-Centric Multimodal Knowledge starts the next generation of information access, which allows us to effectively access historical scenarios and reason about the future. I will lay out how I plan to grow a deep semantic understanding of language world and vision world, moving from concrete to abstract, from static to dynamic, and ultimately from perception to cognition. Please contact the Office team for Zoom link information.

We consider Kitaev's quantum double model based on a finite group G and describe quantum circuits for (a) preparation of the ground state, (b) creation of anyon pairs separated by an arbitrary distance, and (c) non-destructive topological charge measurement. We show that for any solvable group G all above tasks can be realized by constant-depth adaptive circuits with geometrically local unitary gates and mid-circuit measurements. Each gate may be chosen adaptively depending on previous measurement outcomes. Constant-depth circuits are well suited for implementation on a noisy hardware since it may be possible to execute the entire circuit within the qubit coherence time. Thus our results could facilitate an experimental study of exotic phases of matter with a non-abelian particle statistics. We also show that adaptiveness is essential for our circuit construction. Namely, task (b) cannot be realized by non-adaptive constant-depth local circuits for any non-abelian group G. This is in a sharp contrast with abelian anyons which can be created and moved over an arbitrary distance by a depth-1 circuit composed of generalized Pauli gates.

This is joint work with S. Bravyi, I. Kim and A. Kliesch, arXiv:2205.01933.

Memory safety is a major source of vulnerabilities in computer systems. Capability machines are a type of CPUs that support fine-grained privilege separation using capabilities, machine words that include forms of authority. Over the last decade, CHERI, a family of capability machines, has matured into an extensive design featuring, among other, a full UNIX-style operating system, CheriBSD. Building on ideas from CHERI, capability machines are even becoming a reality in industry; the Arm Morello program is a research program led by Arm to create a prototype system on chip with capabilities. One of the promises of capability machines is that they can enforce security properties that we expect from high-level languages, in particular stack safety, even when machine code is linked with other untrusted and possibly adversarial machine code. In this talk, I will discuss what it takes to realise that promise in practice. Since stack safety properties can be quite subtle, it is crucial to formally reason about the enforcement mechanisms enabled by capabilities. This is a complex task that involves reasoning about the interaction between known code, and unknown untrusted code. We use Iris to formally reason about the deep semantic properties of capability machines.

The feedback that users provide through their choices (e.g. clicks, purchases) is one of the most common types of data readily available for training autonomous systems, and it is widely used in online platforms. However, naively training systems based on choice data may only improve short-term engagement, but not the long-term sustainability of the platform. In this talk, I will discuss some of the pitfalls of engagement-maximization, and explore methods that allow us to supplement engagement with additional criteria that are not limited to individual action-response metrics. The goal is to give platform operators a new set of macroscopic interventions for steering the dynamics of the platform, providing a new level of abstraction that goes beyond the engagement with individual recommendations or rankings.

Please contact the Office team for Zoom link information.

AI can enhance programming experiences for a diverse set of programmers: from professional developers and data scientists (proficient programmers) who need help in software engineering and data wrangling, all the way to spreadsheet users (low-code programmers) who need help in authoring formulas, and students (novice programmers) who seek hints when stuck with their programming homework. To communicate their need to AI, users can express their intent explicitly—as input-output examples or natural-language specification—or implicitly—where they encounter a bug (and expect AI to suggest a fix), or simply allow AI to observe their last few lines of code or edits (to have it suggest the next steps).

The task of synthesizing an intended program snippet from the user’s intent is both a search and a ranking problem. Search is required to discover candidate programs that correspond to the (often ambiguous) intent, and ranking is required to pick the best program from multiple plausible alternatives. This creates a fertile playground for combining symbolic-reasoning techniques, which model the semantics of programming operators, and machine-learning techniques, which can model human preferences in programming. Recent advances in large language models like Codex offer further promise to advance such neuro-symbolic techniques.

Finally, a few critical requirements in AI-assisted programming are usability, precision, and trust; and they create opportunities for innovative user experiences and interactivity paradigms. In this talk, I will explain these concepts using some existing successes, including the Flash Fill feature in Excel, Data Connectors in PowerQuery, and IntelliCode/CoPilot in Visual Studio. I will also describe several new opportunities in AI-assisted programming, which can drive the next set of foundational neuro-symbolic advances.

This talk will be a hybrid event. You can join the meeting in E1 5 room 002 in Saarbrücken, in G26 room 111 in Kaiserlautern or via Zoom. Please contact the Office team for Zoom link information.

Theoretical Reflections on Quantum Supremacy

Google's 2019 experiment and their announcement of quantum supremacy relied on the inability of classical computers to efficiently carry out a task called random quantum circuit sampling (RCS). I will describe recent theoretical developments on the complexity of RCS. I will also describe a different line of work that provides scalable and rigorous proofs of quantumness based on an approach called the cryptographic leash, and the prospects of a concrete experimental challenge based on this approach.

Quantum money is a cryptographic protocol where one party (the mint) can prepare quantum states (each with a unique serial number) that can be verified but not duplicated. We sketch our 2010 quantum money protocol based on knot invariants and planar embeddings of knots, and sketch other proposals for quantum money that have been made since then, including our recent failed protocol.

"Analogue" Hamiltonian simulation involves engineering a Hamiltonian of interest in the laboratory and studying its properties experimentally. Large-scale Hamiltonian simulation experiments have been carried out in optical lattices, ion traps and other systems for two decades. This is often touted as the most promising near-term application of quantum computing technology, as it is argued it does not require a scalable, fault-tolerant quantum computer.

Despite this, the theoretical basis for Hamiltonian simulation is surprisingly sparse. Even a precise definition of what it means to simulate a Hamiltonian was lacking. In my talk, I will explain how we put analogue Hamiltonian simulation on a rigorous theoretical footing, by drawing on techniques from Hamiltonian complexity theory in computer science, and Jordan and C* algebra results in mathematics.

I will then explain how this proved to be far more fruitful than a mere mathematical tidying-up exercise. It led to the discovery of universal quantum Hamiltonians [Science, 351:6 278, p.1180 (2016); Proc. Natl. Acad. Sci. 115:38 p.9497, (2018); J. Stat. Phys. 176:1 p228\u2013261 (2019); [[[01]https://link.springer.com/article/10.1007/s00023-021-01111-7][Annales Henri Poincar?, 23 p.223 (2021)], later shown to have a deep connection back to quantum complexity theory [PRX Quantum 3:010308 (2022)]. The theory has also found applications in developing new and more efficient fermionic encodings for quantum computing [Phys. Rev. B 104:035118 (2021)], leading to dramatic reductions in the resource requirements for Hamiltonian simulation on near-term quantum computers [Nature Commun. 12:1, 4929 (2021)]. It has even found applications in quantum gravity, leading to the first toy models of AdS/CFT to encompass energy scales, dynamics, and (toy models of) black hole formation [J. High Energy Phys. 2019:17 (2019); J. High Energy Phys. 2022:52 (2022)].

Given an integer n ≥ 2, let P (n) stand for its largest prime factor. Given integers k ≥ 2 and ℓ ≥ 2, consider the set Ek,ℓ of those integers n ≥ 2 for which P (n + i)ℓ | n + i for i = 0, 1, . . . , k. Each of these sets is very small. For instance, the smallest element of E3,2 is 1 294 298, the smallest known element of E3,3 has 77 digits and no elements of E4,2 are known, even though all these sets are believed to be infinite. In this talk, using elementary, analytic and probabilistic approaches, we will shed some light on these sets and raise several open problems. This is joint work with Nicolas Doyon, Florian Luca and Matthieu Moineau.

---

This talk will be a hybrid event. You can join the meeting in E1 5 room 002 in Saarbrücken, in G26 room 111 in Kaiserlautern or via Zoom. Please contact the Office team for Zoom link information.

The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, its decidability has been open for nearly a century! In this talk, I will present a brief survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.

---

This talk will be a hybrid event. You can join the meeting in E1 5 room 002 in Saarbrücken, in G26 room 111 in Kaiserlautern or via Zoom. Please contact the Office team for Zoom link information.

Mistrust over traditional financial institutions is motivating the development of decentralized financial infrastructures based on blockchains. In particular, Consortium blockchains (such as the Linux Foundation Hyperledger and Facebook’s diem) are emerging as the approach preferred by businesses. These systems allow only a well-known set of mutually distrustful parties to add blocks to the blockchain; in this way, they aim to retain the benefits of decentralization without embracing the cyberpunk philosophy that informed Nakamoto’s disruptive vision. At the core of consortium blockchains is State Machine Replication, a classic technique borrowed from fault tolerant distributed computing; to ensure the robustness of their infrastructure, consortium blockchains actually borrow the Byzantine-tolerant version of this technique, which guarantees that the blockchain will operate correctly even if as many as about a third of the contributing parties are bent on cheating.

But, sometimes, "a borrowing is a sorrowing".

I will discuss why Byzantine-tolerant state machine replication is fundamentally incapable of recognizing, never mind preventing, an ever present scourge of financial exchanges: the fraudulent manipulation of the order in which transactions are processed — and how its specification needs to be expanded to give it a fighting chance.

But is it possible to completely eliminate the ability of Byzantine parties to engage in order manipulation? What meaningful ordering guarantees can be enforced? And at what cost?

---

This talk will be a hybrid event. You can either attend in room 002 or via Zoom. Please contact the office team for zoom link information.

Quantum algorithms are useful for a variety of problems in search and > optimization. This line of work started with Grover's quantum search algorithm > which achieved a quadratic speedup over naive exhaustive search but has now > developed far beyond it. > > In this talk, we describe three recent results in this area: > > 1. We show that, for any classical algorithm that uses a random walk to find an > object with some property (by walking until the random walker reaches such an > object), there is an almost quadratically faster quantum algorithm > (https://arxiv.org/abs/1903.07493 ). > > 2. We show that the best known exponential time algorithms for solving several > NP-complete problems (such as Travelling Salesman Problem or TSP) can be > improved quantumly  (https://arxiv.org/abs/1807.05209 > ). For example, for the > TSP, the best known classical algorithm needs time O(2^n) but our quantum > algorithm solves the problem in time O(1.728...^n). > > 3. We show a almost quadratic quantum speedup for a number of geometric problems > such as finding three points that are on the same line > (https://arxiv.org/abs/2004.08949 ).

In this paper, we study how bandit algorithms in a bounded reward setting can be contaminated and fooled to learn wrong actions. In particular, we consider a strong attacker model in which the attacker aims to fool the learning algorithm to learn a suboptimal bandit policy. To do so, this attacker can observe both the selected actions and their corresponding rewards, and can contaminate the rewards with additive noise. We show that any bandit algorithm with regret O(\log T) can be forced to suffer a linear regret with an expected amount of contamination O(\log T). We show that this amount of contamination is also necessary, as we prove that there exists a no-regret bandit algorithm, specifically the classical UCB, that requires \Omega(\log T) amount of contamination to suffer linear regret. To combat such poisoning attacks, our second main contribution is to propose verification-based mechanisms, which use a verification scheme to access a limited number of uncontaminated rewards. In particular, for the case of unlimited verifications, we show that with O(\log T) expected number of verifications, a simple modified version of the Explore-then-Commit type bandit algorithm can restore the order optimal O(\log T) regret irrespective of the amount of contamination used by the attacker. We also provide a UCB-like verification scheme, called Secure-UCB, that also enjoys full recovery from any attacks, also with O(\log T) expected number of verifications. To derive a matching lower bound on the number of verifications, we also prove that for any order-optimal bandit algorithm, this number of verifications O(\log T) is necessary to recover the order-optimal regret. On the other hand, when the number of verifications is bounded above by a budget B, we propose a novel algorithm, Secure-BARBAR, which provably achieves O(\min\{C,T/sqrt{B} \}) regret with high probability against weak attackers (i.e., attackers who have to place the contamination \emph{before} seeing the actual pulls of the bandit algorithm), where C is the total amount of contamination by the attacker. This new result breaks the known \Omega(C) lower bound of the non-verified setting if C is large.  

This is joint work with Anshuka Rangi and Haifeng Xu.

Please contact crichter@mpi-sws.org for link information

The classic textbook approach to designing and analyzing algorithms for combinatorialproblems considers worst-case instances of the problem, about which the algorithm designer has no prior information. Since for many problems such worst-case guarantees are quite weak, practitioners often employ a data-driven algorithm design approach; specifically,they use machine learning and instances of the problem from their specific domain to learn a method that works well in that domain. Historically, such data-driven algorithmic techniques have come with no performance guarantees. In this talk, I will describeour recent work on providing performance guarantees for data-driven algorithm design both in the distributional and online learning formalizations.

--

Please contact the office team for zoom link information.

Scale appears to be the winning recipe in today's AI leaderboards. And yet, extreme-scale neural models are still brittle to make errors that are often nonsensical and even counterintuitive. In this talk, I will argue for the importance of knowledge, especially commonsense knowledge, and demonstrate how smaller models developed in academia can still have an edge over larger industry-scale models, if powered with knowledge.

First, I will introduce "symbolic knowledge distillation", a new framework to distill larger neural language models into smaller commonsense models, which leads to a machine-authored KB that wins, for the first time, over a human-authored KB in all criteria: scale, accuracy, and diversity. Next, I will present an experimental conceptual framework toward computational social norms and commonsense morality, so that neural language models can learn to reason that "helping a friend" is generally a good thing to do, but "helping a friend spread fake news" is not. Finally, I will discuss an approach to multimodal script knowledge demonstrating the power of complex raw data, which leads to new SOTA performances on a dozen leaderboards that require grounded, temporal, and causal commonsense reasoning.

The internet has had a revolutionary impact on our world. The vision of a quantum internet is to provide fundamentally new internet technology by enabling quantum communication between any two points on Earth. Such a quantum internet can —in synergy with the "classical" internet that we have today—connect quantum information processors in order to achieve unparalleled capabilities that are provably impossible by using only classical information. At present, such technology is under development in physics labs around the globe, but no large-scale quantum network systems exist. We start by providing a gentle introduction to quantum networks for computer scientists, and briefly review the state of the art. We highlight some of the many open questions to computer science in the domain of quantum networking, illustrated with a very recent result realizing the first quantum link layer protocol on a programmable 3 node quantum network based on Nitrogen-Vacancy Centers in Diamond. We close by providing a series of pointers to learn more, as well as tools to download that allow play with simulated quantum networks without leaving your home.

Information about the series and recordings of previous talks can be found at https://www.mpi-inf.mpg.de/departments/algorithms-complexity/quantum-lecture-ser ies

Storage technologies are entering the market with performance vastly superior to conventional storage devices. This technology shift requires a complete rethinking of the software storage stack.

In this talk I will give two examples of our work with Optane-based solid-state (block) devices that illustrate the need for and the benefit of a wholesale redesign.

First, I will describe the Kvell key-value (KV) store. The key observation underlying Kvell is that conventional KV software on fast devices is bottlenecked by the CPU rather than by the device. Kvell therefore focuses on minimizing CPU intervention.

Second, I will describe the Kvell+ OLTP/OLAP system built on top of Kvell. The key underlying observation here is that these storage devices have become so fast that the conventional implementation of snapshot isolation – maintaining multiple versions – quickly leads to the device filling up. Kvell therefore focuses processes new versions as they are created.

This talk describes joint work with Oana Balmau (McGill University), Karan Gupta (Nutanix) and Baptiste Lepers (University of Sydney).

---

Please contact the MPI-SWS Office Team for the ZOOM link information. .

Data analytics in the cloud has become an integral part of enterprise businesses. Big data analytics systems, however, still lack the ability to take task objectives such as user performance goals and budgetary constraints and automatically configure an analytical job to achieve these objectives. This talk presents UDAO, a Unified Data Analytics Optimizer, that can automatically determine a cluster configuration with a suitable number of cores as well as other system parameters that best meet the task objectives. At a core of our work is a principled multi-objective optimization (MOO) approach that computes a Pareto optimal set of configurations to reveal tradeoffs between different objectives, recommends a new cluster configuration that best explores such tradeoffs, and employs novel optimizations to enable such recommendations within a few seconds. Such optimization is further enabled by a Deep Learning-based modeling approach that can learn a model for each user objective as complex as necessary for the underlying computing environment. Detailed experiments using a Spark-based prototype and benchmark workloads show that our MOO techniques provide a 2-50x speedup over existing MOO methods, while offering good coverage of the Pareto frontier. Compared to Ottertune, a state-of-the-art performance tuning system, UDAO recommends Spark configurations that yield 26%-49% reduction of running time of the TPCx-BB benchmark while adapting to different user preferences on multiple objectives. This talk ends by outlining remaining research challenges in automated resource management and performance optimization for cloud data analytics.

In supervised machine learning, in an abstract sense, a concept in a given reference class has to be inferred from a small set of labeled examples. Machine teaching refers to the inverse problem, namely the problem to compress any concept in the reference class to a "teaching set" of labeled examples in a way that the concept can be reconstructed. The goal is to minimize the worst-case teaching set size taken over all concepts in the reference class, while at the same time adhering to certain conditions that disallow unfair collusion between the teacher and the learner. Applications of machine teaching include multi-agent systems and program synthesis. In this presentation, it is first shown how preference relations over concepts can be used in order to guarantee collusion-free teaching and learning. Intuitive examples are presented in which quite natural preference relations result in data-efficient collusion-free teaching of complex classes of concepts. Further, it is demonstrated that optimal collusion-free teaching cannot always be attained by the preference-based approach. Finally, we will challenge the standard notion of collusion-freeness and show that a more stringent notion characterizes teaching with the preference-based approach. This presentation summarizes joint work with Shaun Fallat, Ziyuan Gao, David G. Kirkpatrick, Christoph Ries, Hans U. Simon, and Abolghasem Soltani.

Abstract: Support for hardware acceleration and parallel software workloads on heterogeneous multiprocessor platforms is becoming increasingly relevant in the design of high-performance and power-efficient real-time embedded systems. Communication between jobs dispatched on different cores and specialized hardware accelerators such as FPGAs and GPUs is most often implemented using asynchronous events. The delays incurred by each task due to the time spent waiting for such events should appropriately be accounted for in the timing analysis of the resulting scheduling behavior. This talk presents the event-driven delay-induced (EDD) task model, which is suitable to represent and analyze the timing behavior of complex computing workloads that incur event-related delays in the communication and synchronization between different processing elements. The EDD task model generalizes several existing task models, providing enhanced expressiveness towards the timing analysis of parallel processing workloads that involve both synchronous and asynchronous hardware acceleration requests. Two analysis techniques for EDD tasks executing on single-core platforms under fixed-priority scheduling are presented; then, a model transformation technique is provided to analyze parallel real-time tasks executing under partitioned multiprocessor scheduling by means of a set of EDD tasks. In the experiments, partitioned scheduling of parallel tasks is shown to outperform federated scheduling when the proposed analysis approach is combined with specialized partitioning heuristics.

Please contact the office team for link information.

Software 2.0 – the augmentation and replacement of traditional code with models, especially deep neural networks – is changing how we develop, deploy, and maintain software. In this talk, I will describe the challenges and opportunities that this change brings with it, focusing on its impact on database systems.

Enzian is a research computer built at ETH Zurich which combines a server-class CPU with a large FPGA in an asymmetric 2-socket NUMA system. It is designed to be used individually or in a cluster to explore the design space for future hardware and its implications for system software. Enzian is deliberately over-engineered, and (as I'll show) can replicate the use-cases of almost all other FPGA platforms used in academic research today. Perhaps unique to Enzian is exposing the CPU's native cache-coherence protocol to applications on the FPGA, and I'll discuss the additional opportunities this offers for research as well as the challenges we faced in interoperating with an existing coherence protocol not designed for this use-case. There are nine Enzian systems operational so far, being used locally at ETH and remotely by collaborators.

---

Please contact the MPI-SWS Office Team for the ZOOM link information. .

We introduce Concurrent NetKAT (CNetKAT), an extension of the network programming language NetKAT with multiple packets and with operators to specify and reason about concurrency and state in a network We provide a model of the language based on partially ordered multisets, well-established mathematical structures in the denotational semantics of concurrent languages. We prove that CNetKAT is a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through various examples. More generally, CNetKAT is analgebraic framework to reason about programs with both local and global state. In our model these are, respectively, the packets and the global variable store, but the scope of applications is much more general, including reasoning about hardware pipelines inside an SDN switch. This is joint work with Jana Wagemaker, Nate Foster, Tobia Kappe, Dexter Kozen, and Jurriaan Rot.

Please contact the office team for link information,

We present fully automated approaches to safety and termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions over random variables and parametrised distributions. We combine methods from symbolic summation and statistics to derive invariants as valid properties over higher-order moments, such as expected values or variances, of program variables, synthesizing this way quantitative invariants of probabilistic program loops. We further extend our moments-based analysis to prove termination of considered probabilistic while-programs. This is a joint work with Ezio Bartocci, Joost-Pieter Katoen, Marcel Moosbrugger and Miroslav Stankovic.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

Microarchitectural security is one of the most challenging and exciting problems in system security today. With the discovery of transient execution attacks, it has become clear that microarchitectural attacks have significant impact on the security properties of software running on a processor that runs code from various stakeholders (such as, for instance, in the cloud). This talk will first provide an overview of the current understanding of microarchitectural security, with a focus on how the research community has built formal models for processors that support proving that software is resilient to specific classes of microarchitectural attacks. Next, we turn to the problem of validating these proposed formal models: how can we convince ourselves and others that a given formal model is an adequate model for a given real-world processor, and that we can justifiably trust the security properties proven based on the model. This is an instance of the more general problem of empirically validating whether a real-world system satisfies the assumptions on which a formal model relies. We will discuss a small case study where we empirically validated a formally proven security property of a simple processor by systematically attacking the corresponding real-world implementation of the processor. We end with some conclusions and reflections on how our experiences from this case study might help us build more adequate formal models.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

Rigorous approaches based on controller synthesis can generate correct-by-construction controllers that guarantee that the system under control meets some higher-level tasks. By reducing designing and testing cycles, synthesis can help create safe autonomous systems that involve complex interactions of dynamics and decision logic. In general, however, synthesis problems are known to have high computational complexity for high dimensional and nonlinear systems. In this talk, I will present a series of new synthesis algorithms that suggest that these challenges can be overcome and that rigorous approaches are indeed promising. I will talk about how to synthesize controllers for linear systems, nonlinear systems, hybrid systems with both discrete and continuous control variables, and multi-agent systems, with guarantees on the safety and optimality of the solutions.

Please contact the office team for link information.

Max Planck Distinguished Speaker Talk in Quantum Computing and Quantum Information

Speaker: Andrew Childs (University of Maryland), https://www.cs.umd.edu/~amchilds/

Title: Efficient quantum algorithm for dissipative nonlinear differential equations

Time: Thursday, July 22nd, 4pm.

Location: https://zoom.us/j/94577321297?pwd=N3l5K1ZtZ3E1aytnWlBkL1FUazNXZz09 Meeting ID: 945 7732 1297 Passcode: 205903

Hosts: Ignacio Cirac (MPQ) and Kurt Mehlhorn (MPI-INF).

Abstract: While there has been extensive previous work on efficient quantum algorithms for linear differential equations, analogous progress for nonlinear differential equations has been severely limited due to the linearity of quantum mechanics. Despite this obstacle, we develop a quantum algorithm for initial value problems described by dissipative quadratic n-dimensional ordinary differential equations. Assuming R<1, where R is a parameter characterizing the ratio of the nonlinearity to the linear dissipation, this algorithm has complexity T^2 poly(log T, log n, log(1/ϵ))/ϵ, where T is the evolution time and ϵ is the allowed error in the output quantum state. This is an exponential improvement over the best previous quantum algorithms, whose complexity is exponential in T. We achieve this improvement using the method of Carleman linearization, for which we give a novel convergence theorem. This method maps a system of nonlinear differential equations to an infinite-dimensional system of linear differential equations, which we discretize, truncate, and solve using the forward Euler method and the quantum linear system algorithm. We also provide a lower bound on the worst-case complexity of quantum algorithms for general quadratic differential equations, showing that the problem is intractable for R≥sqrt(2). Finally, we discuss potential applications of this approach to problems arising in biology as well as in fluid and plasma dynamics.

Based on joint work with Jin-Peng Liu, Herman Kolden, Hari Krovi, Nuno Loureiro, and Konstantina Trivisa.

When using distributed machine learning (ML) systems to train models on a cluster of worker machines, users must configure a large number of parameters: hyper-parameters (e.g. the batch size and the learning rate) affect model convergence; system parameters (e.g. the number of workers and their communication topology) impact training performance. Some of these parameters, such as the number of workers, may also change in elastic machine learning scenarios. In current systems, adapting such parameters during training is ill-supported. In this talk, I will describe our recent work on KungFu, a distributed deep learning library for TensorFlow and PyTorch that is designed to enable adaptive and elastic training. KungFu allows users to express high-level Adaptation Policies (APs) that describe how to change hyper-and system parameters during training. APs take real-time monitored metrics (e.g. signal-to-noise ratios) as input and trigger control actions (e.g. cluster rescaling or synchronisation strategy updates). For execution, APs are translated into monitoring and control operators that are embedded in the dataflow graph. APs exploit an efficient asynchronous collective communication layer, which ensures concurrency and consistency of monitoring and adaptation operations.

--

Please contact the MPI-SWS Office Team for the ZOOM link information.

Within a span of just a few years, we have gone from completely trusting our hardware to realising that everything is broken and all our security guarantees are built on sand. Memory chips have fundamental (Rowhammer) flaws that allow attackers to modify data without accessing it and CPUs are full of side channels and transient execution problems that lead to information leakage across pretty much all security boundaries. Combined, these issues have led to a string of high-profile attacks. In this talk, I will discuss some of the developments in such attacks, mostly by means of the attacks in which our group was involved. Although the research was exciting, I will argue that the way we conduct security research on hardware is broken. The problem is that the interests of hardware manufacturers and academics do not align and this is bad for everyone.

--

Please contact MPI-SWS Office Team for Zoom link information.

Domain-specific hardware accelerators for graphics, deep learning, image processing, and other tasks have become pervasive to meet the performance and energy-efficiency needs of emerging applications. However, such specializations are inherently at odds with the programmability long enjoyed by software developers from general-purpose processors. In this talk, I will explore the feasibility of programmable, domain-agnostic accelerators that can be morphed and instantiated to specialized accelerators at runtime through software. In particular, I will present Coarse-Grained Reconfigurable Array (CGRA) as a promising approach to offer high accelerator efficiency while supporting diverse tasks through compile-time configurability. The central challenge is efficient spatio-temporal mapping of the applications expressed in high-level programming languages with complex data dependencies, control flow, and memory accesses to the accelerator. We approach this challenge through a synergistic hardware-software co-designed approach with (a) innovations at the architecture level to improve the efficiency of the application execution as well as ease the burden on the compilation, and (b) innovations at the compiler level to fully exploit the architectural optimizations for quality and fast mapping. Finally, I will share systems-level considerations for real-world deployment of domain-agnostic accelerators in the context of edge computing.

Please contact the office team for link information

Algorithms are increasingly used to aid decision-making in high-stakes settings including employment, lending, healthcare, and the legal system. This development has led to an ecosystem of growing complexity in which algorithms and people interact around consequential decisions, often mediated by organizations and firms that may be in competition with one another.

We consider two related sets of issues that arise in this setting. First, concerns have been raised about the effects of algorithmic monoculture, in which multiple decision-makers all rely on the same algorithm. In a set of models drawing on minimal assumptions, we show that when competing decision-makers converge on the use of the same algorithm as part of a decision pipeline, the result can potentially be harmful for social welfare even when the algorithm is more accurate than any decision-maker acting on their own. Second, we consider some of the canonical ways in which data is simplified over the course of these decision-making pipelines, showing how this process of simplification can introduce sources of bias in ways that connect to principles from the psychology of stereotype formation.

The talk will be based on joint work with Sendhil Mullainathan and Manish Raghavan.

Please contact the office team for link information.

Financial applications such as Landing and Payment protocols, and their realization in decentralized financial (DeFi) applications in Blockchains, comprise a unique domain where bugs in the code may be exploited by anyone to steal assets. This situation provides unique opportunities for formal verification to enable "move fast and break nothing". Formal verification can be used to detect errors early in the development process and guarantee correctness when a new version of the code is deployed.

I will describe an attempt to automatically verify DeFis and identify potential bugs. The approach is based on breaking the verification of DeFis into decidable verification tasks. Each of these tasks is solved via a decision procedure which automatically generates a formal proof or a test input showing a violation of the specification. In order to overcome undecidability, high level properties are expressed as ghost states and static analysis used to infer how low level programs update ghost states.

--

Please contact MPI-SWS Office Team for Zoom link information

Want to speed up data access? Add a cache! Data caching, as the solution to performance woes, is as old as our field. However, we have been less aggressive at caching computation. While memoization is a widely known technique, it is rarely employed as pervasively as data caching. In this talk, I'll present examples of how we've used computational caching in areas ranging from interpretable machine learning to program synthesis to automatic parallelization.

--

Please contact the MPI-SWS office team for Zoom link details.

In the synthesis problem, we are given a specification over input and output signals, and we synthesize a system that realizes the specification: with every sequence of input signals, the system associates a sequence of output signals so that the generated computation satisfies the specification. The above classical formulation of the problem is Boolean. The talk surveys recent efforts to automatically synthesize reactive systems that are not only correct, but also of high quality. Indeed, designers would be willing to give up manual design only after being convinced that the automatic procedure that replaces it generates systems of comparable quality. We distinguish between behavioral quality, which refers to the way the specification is satisfied, and costs, which refer to resources that the system consumes. We argue that both are crucial for synthesis to become appealing in practice. __________________________________________________________________________

Please contact MPI-SWS Office Team for Zoom link information

Distributional reinforcement learning (RL) is a new approach to RL with the emphasis on the distribution of the rewards obtained rather than just the expected reward as in traditional RL. In this work we take the distributional point of view and analyse a number of sampling-based algorithms such as value iteration, TD(0) and policy iteration. These algorithms have been shown to converge under various assumptions but usually with completely different proofs. We have developed a new viewpoint which allows us to prove convergence using a uniform approach. The idea is based on couplings and on viewing the approximation algorithms as Markov processes in their own right. It originated from work on bisimulation metrics in which I have been working for the last quarter century. This is joint work with Philip Amortila (U. Illinois), Marc Bellemare (Google Brain) and Doina Precup (McGill, Mila and DeepMind).

Please contact MPI-SWS office for the Zoom links

Computational social choice is an interdisciplinary field that studies collective decision making from an algorithmic perspective. Determining the winners under various voting rules is a mainstream area of research in computational social choice. Many such rules assume that the voters provide complete information about their preferences, an assumption that is often unrealistic because typically only partial preference information is available.  This state of affairs has motivated the study of the notions of the necessary winners and the possible winners with respect to a variety of voting rules.

The main aim of this talk is to present an overview of winner determination under incomplete information and to highlight some recent advances in this area, including the development of a framework that aims to create bridges between computational social choice and data management. This framework infuses relational database context into social choice and allows for the formulation of sophisticated queries about voting rules, candidates, winners, issues, and positions on issues. We will introduce the necessary answer semantics and the possible answer semantics to queries and will explore the computational complexity of query evaluation under these semantics.

------------------------------------------------------------

Please contact MPI-SWS Office Team for Zoom link information

Program termination is a key question in program verification. This talk considers the termination of probabilistic programs, programs that can describe e.g., randomized algorithms, security algorithms and Bayesian learning.

Probabilistic termination has several nuances. Diverging program runs may occur with probability zero. Such programs are almost surely terminating (AST). If the expected duration until termination is finite, they are positive AST.

This talk presents a simple though powerful proof rule for deciding AST, reports on recent approaches towards automation, and sketches a Dijkstra-like weakest precondition calculus for proving positive AST in a compositional way.

-------------

Please contact MPI-SWS Office Team for Zoom link information

Cyber-physical systems (CPSs) combine cyber capabilities, such as computation or communication, with physical capabilities, such as motion or other physical processes. Cars, aircraft, and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms is challenging due to their tight coupling with physical behavior, while it is vital that these algorithms be correct because we rely on them for safety-critical tasks.

This talk highlights some of the most fascinating aspects of the logical foundations for developing cyber-physical systems with the mathematical rigor that their safety-critical nature demands. The underlying logic, differential dynamic logic, provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations.

In addition to providing a strong theoretical foundation for CPS, differential dynamic logics have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. Logic is the foundation to provably transfer safety guarantees about models to CPS implementations. This technology is also the key ingredient behind Safe AI for CPS.

-------

Please contact MPI-SWS office team for zoom link information

The Internet was meant to be neutral: treat all traffic the same, without discriminating in favor of specific apps, sites, or services. As commercial interests threaten this ideal, many countries have introduced neutrality regulations. Unfortunately, none of them are actually enforceable. In this talk, I will first discuss the challenge of inferring whether a network is neutral or not using solely external observations. Then, I will show that we can go beyond neutrality inference and reach network transparency, in which networks provide explicit hints that enable their users to reliably assess network behavior, including neutrality. Network transparency, however, requires exposing information about what traffic is seen where and when, which can hurt user privacy. I will close by looking at the important question of whether network transparency indeed must come at the cost of reduced anonymity for Internet users.

--

Please contact MPI-SWS Office Team for Zoom link information

Don't we all dream of the perfect assistant whom we can just tell what to do and the assistant can figure out how to accomplish the tasks? Formally, given a specification F(X,Y) over the set of input variables X and output variables Y, we want the assistant, aka functional synthesis engine, to design a function G such that (X,Y=G(X)) satisfies F. Functional synthesis has been studied for over 150 years, dating back Boole in 1850's and yet scalability remains a core challenge. Motivated by progress in machine learning, we design a new algorithmic framework Manthan, which views functional synthesis as a classification problem, relying on advances in constrained sampling for data generation, and advances in automated reasoning for a novel proof-guided refinement and provable verification. On an extensive and rigorous evaluation over 609 benchmarks, we demonstrate that Manthan significantly improves upon the current state of the art, solving 356 benchmarks in comparison to 280, which is the most solved by a state of the art technique; thereby, we demonstrate an increase of 76 benchmarks over the current state of the art. The significant performance improvements, along with our detailed analysis, highlights several interesting avenues of future work at the intersection of machine learning, constrained sampling, and automated reasoning.

Please contact MPI-SWS office team for link information

LLVM is an industrial-strength compiler that's used for everything from day-to-day iOS development (in Swift) to pie-in-the-sky academic research projects. This makes the LLVM framework a sweet spot for bug-finding and verification technologies--any improvements to it are amplified across its many applications.

This talk asks the question: what does LLVM code _mean_, and, how can we ensure that LLVM-based tools (compilers, optimizers, code instrumentation passes, etc.) do what they're supposed to -- especially for safety- or security-critical applications? The Verified LLVM project (Vellvm) is our attempt to provide an answer. Vellvm gives a semantics to LLVM IR programs in the Coq interactive theorem prover, which can be used for developing machine-checkable formal properties about LLVM IR programs and transformation passes.

Our approach to modeling LLVM IR semantics uses _interaction trees_, a data structure that is suitable for representing impure, possibly nonterminating programs in dependent type theory. Interaction trees support compositional and modular reasoning about program semantics but are also executable, and hence useful for implementation and testing. We'll see how interaction trees are used in Vellvm and, along the way, we'll get a taste of what LLVM code looks like including some of its trickier semantic aspects. We'll also see (at a high level) how modern interactive theorem provers--in this case, Coq--can be used to verify compiler transformations.

No experience with LLVM or formal verification technologies will be assumed.

--

Please contact office for the Zoom details.

This talk will be a survey of instances of the synthesis problem in distributed models with rendez-vous synchronization. I will talk about synthesis for distributed automata within the theory of Mazurkiewicz traces and about the simpler model of negotiation diagrams (aka as workflow nets). 

---

Please contact Office for Zoom details. 

Human Behavior Modeling and Understanding is a key challenge in the development of intelligent systems. In my talk I will describe a few of the projects that I have carried out over the course of the past 25 years to address this challenge. In particular, I will give an overview of my work on Smart Rooms (real-time facial expression recognition and visual surveillance), Smart Cars (driver maneuver recognition), Smart Offices (multi-modal office activity recognition), Smart Mobile Phones (boredom inference) and finally a Smart World (pandemics and specifically COVID-19). On this last area, I will share the lessons learned during the past 8 months as Commissioner to the President of the Valencian Government in Spain on AI and Data Science against COVID-19. It is a very special initiative of collaboration between the civil society at large (through the survey), the scientific community and a public administration (at the President level)

--

Please contact office for Zoom link details

People who use modern technologies are inundated with content and information from many sources, including advertisements on the web, posts on social media, and (looking to the future) content in augmented or virtual reality. While these technologies are transforming our lives and communications in many positive ways, they also come with serious risks to users’ security, privacy, and the trustworthiness of content they see: the online advertising ecosystem tracks individual users and may serve misleading or deceptive ads, social media feeds are full of potential mis/disinformation, and emerging augmented reality technologies can directly modify users’ perceptions of the physical world in undesirable ways. In this talk, I will discuss several lines of research from our lab that explore these issues from a broad computer security and privacy perspective, leveraging methodologies ranging from qualitative user studies to systematic measurement studies to system design and evaluation. What unites these efforts is a key question: what can (or do) users believe about the content they receive through our existing and emerging technologies, and how can we design platforms and ecosystems more robust to these risks?

--

Contact SWS Office for Zoom link details

People play a central role in the machine learning life cycle. Consequently, building machine learning systems that are reliable, trustworthy, and fair requires that relevant stakeholders—including developers, users, and the people affected by these systems—have at least a basic understanding of how they work. Yet what makes a system "intelligible" is difficult to pin down. Intelligibility is a fundamentally human-centered concept that lacks a one-size-fits-all solution. I will explore the importance of evaluating methods for achieving intelligibility in context with relevant stakeholders, ways of empirically testing whether intelligibility techniques achieve their goals, and why we should expand our concept of intelligibility beyond machine learning models to other aspects of machine learning systems, such as datasets and performance metrics.

--

Please contact Office for the Zoom details.

Human cooperation is fundamental to the success of our species. But emerging machine intelligence poses new challenges to human cooperation. This talk explores two interrelated problems: How can we humans cooperate *through* machines--that is, agree among ourselves on how machines should behave? And how can we cooperate *with* machines--that is, convince self-interested machines to cooperate with us. The talk will then propose an interdisciplinary agenda for understanding and improving our human-machine ecology.

--

Please contact SWS Office for Zoom details

On-demand ride-hailing platforms like Uber and Lyft are helping reshape urban transportation, by enabling car owners to become drivers for hire with minimal overhead. Such platforms are a multi-sided market and offer a rich space for studies with socio-economic implications. In this talk I am going to address two questions:

1. In the absence of coordination, what is the best course of action for a self-interested driver that wants to optimize his earnings?

2. In the presence of coordination, is it possible to maximize social welfare objectives in an environment where the objectives of the participants (drivers, customers and the platform) are (often) misaligned?

We will discuss the computational problems behind these problems and describe simple algorithmic solutions that work extremely well in practice. We will demonstrate the practical strength of our approaches with well-designed experiments on novel datasets we collected from such platforms. --- Please contact Office for the Zoom details.

In this talk, we'll look together at some of the problems of today's data ecosystem, including issues of privacy, control, fairness, surveillance, and manipulation. We'll explore the ways in which various recent technologies can provide (partial) solutions to some of these woes, and we'll confront some of the limitations of technology. The discussion will expose a rich array of interesting research problems that bridge between computer science, law, economics, and beyond. -- Please contact Office for the Zoom details.

The generalization gap of a learning algorithm is the expected difference between its performance on the training data and its performance on fresh unseen test samples. Modern deep learning algorithms typically have large generalization gaps, as they use more parameters than the size of their training set. Moreover the best known rigorous bounds on their generalization gap are often vacuous.

In this talk we will see a new upper bound on the generalization gap of classifiers that are obtained by first using self-supervision to learn a complex representation of the (label free) training data, and then fitting a simple (e.g., linear) classifier to the labels. Such classifiers have become increasingly popular in recent years, as they offer several practical advantages and have been shown to approach state-of-art results.

We show that (under the assumptions described below) the generalization gap of such classifiers tends to zero as long as the complexity of the simple classifier is asymptotically smaller than the number of training samples. We stress that our bound is independent of the complexity of the representation that can use an arbitrarily large number of parameters. Our bound holds assuming that the learning algorithm satisfies certain noise-robustness (adding small amount of label noise causes small degradation in performance) and rationality (getting the wrong label is not better than getting no label at all) properties.  These conditions widely (and sometimes provably) hold across many standard architectures. We complement this result with an empirical study, demonstrating that our bound is non-vacuous for many popular representation-learning based classifiers on CIFAR-10 and ImageNet, including SimCLR, AMDIM and BigBiGAN.

The talk will not assume any specific background in machine learning, and should be accessible to a general mathematical audience. Joint work with Yamini Bansal and Gal Kaplun.

Abstract: Machine learning (ML) is driving many of our applications and life-changing decisions. Yet, it is often brittle and unstable, making decisions that are hard to understand or can be exploited. Tiny changes to an input can cause dramatic changes in predictions; this results in decisions that surprise, appear unfair, or enable attack vectors such as adversarial examples. Moreover, models trained on users' data can encode not only general trends from large datasets but also very specific, personal information from these datasets; this threatens to expose users' secrets through ML models or predictions. This talk positions differential privacy (DP) -- a rigorous privacy theory -- as a versatile foundation for building into ML much-needed guarantees of security, stability, and privacy. I first present PixelDP (S&P'19), a scalable certified defense against adversarial example attacks that leverages DP theory to guarantee a level of robustness against these attacks. I then present Sage (SOSP'19), a DP ML platform that bounds the cumulative leakage of secrets through models while addressing some of the most pressing challenges of DP, such as running out of privacy budget and the privacy-accuracy tradeoff. PixelDP and Sage are designed from a pragmatic, systems perspective and illustrate that DP theory is powerful but requires adaptation to achieve practical guarantees for ML workloads.

In this talk I will describe how formal methods such as synthesis – automatically creating a system from a formal specification – can be leveraged to design robots, explain and provide guarantees for their behavior, and even identify skills they might be missing. I will discuss the benefits and challenges of synthesis techniques and will give examples of different robotic systems including modular robots, swarms and robots interacting with people.

In this talk, I will discuss an ambitious research program towards graph algorithms that work efficiently across many computational models. I will provide an overview of new results and techniques coming out of this research program. Results that will be discussed include edge connectivity (global minimum cut), vertex connectivity, and maximum matching. No background is required, except for some very basic graph algorithms.

Non-convex and discrete optimization problems are at the heart of many algorithmic tasks that arise in machine learning and other computing applications. A promising approach to solve such problems with provable guarantees is the sum-of-squares (SOS) meta-algorithm, which has been discovered multiple times across different disciplines including control theory, proof complexity, and quantum information.

My collaborators and I show in a sequence of recent works that for a wide range of optimization and estimation problems, this meta-algorithm achieves the best known provable guarantees, often improving significantly over all previous methods. For example, for mixtures of spherical Gaussians, we obtain guarantees that improve exponentially over the previous best ones and approach, for the first time, the information-theoretic limits. Remarkably, the SOS meta-algorithm achieves these guarantees without being tailored to this specific problem.

Moreover, we prove that for a rich class of problems, the guarantees that SOS achieves are best possible with respect to a restricted but very powerful model of computation. This result leads to the strongest known concrete lower bounds for NP-complete problems.

Taken together these results point toward a unified theory for efficient optimization and estimation centered around SOS that could change how we think about efficient computation in general.

Physical-layer programmability enables the network topology to be changed dynamically. In this talk, the speaker will make a case that cloud data center networks can be significantly easier to manage with physical-layer programmability. Three example network architectures will be shown as different use cases of this approach. ShareBackup enhances reliability through sharing backup switches efficiently network-wide, where a backup switch can be brought online instantaneously to recover from failures. Flat-tree solves the problem of choosing the right network topology for different cloud services by dynamically changing topological clustering characteristics of the network. OmniSwitch is a universal building block of data center networks that supports automatic device wiring and easy device maintenance. At the end of the talk, the speaker will briefly introduce an ongoing follow-up research that extends physical-layer programmability from data center networks to backbone networks.

Two important challenges in image and video understanding are designing more efficient deep Convolutional Neural Networks and learning models that are able to achieve higher-level understanding. In this talk, I will present some of my recent works towards tackling these challenges. Specifically, I will introduce the Octave Convolution [ICCV 2019], a plug-and-play replacement for the convolution operator that exploits the spatial redundancy of CNN activations and can be used without any adjustments to the network architecture. I will also present the Global Reasoning Networks [CVPR 2019], a new approach for reasoning over arbitrary sets of features of the input, by projecting them from a coordinate space into an interaction space where relational reasoning can be efficiently computed.  The two methods presented are complementary and achieve state-of-the-art performance on both image and video tasks. Aiming for higher-level understanding, I will also present our recent works on vision and language modeling, specifically our work on learning state-of-the-art image and video captioning models that are also able to better visually ground the generated sentences with [CVPR 2019] or without [arXiv 2019] explicit localization supervision. The talk will conclude with current research and a brief vision for the future.

Machine learning increasingly supports consequential decisions  in health, lending, criminal justice or employment that affect the wellbeing of individual members or entire groups of our society. Such applications raise concerns about fairness, privacy violations and the long-term consequences of automated decisions in a social context. After a brief introduction to fairness in machine learning, I will highlight concrete settings with specific fairness or privacy ramifications and outline approaches to address them. I will conclude by embedding these examples into a broader context of socioalgorithmic systems and the complex interactions therein.

We live in a world where errors in computation are becoming ubiquitous and come from a wide variety of sources -- from unintentional soft errors in shrinking transistors to deliberate errors introduced by approximation or malicious attacks. Guaranteeing perfect functionality across a wide range of future systems will be prohibitively expensive. Error-Efficient computing offers a promising solution by allowing the system to make controlled errors. Such systems can be considered as being error-efficient: they only prevent as many errors as they need to for an acceptable user experience. Allowing the system to make errors can lead to significant resource (time, energy, bandwidth, etc.) savings. Error-efficient computing can transform the way we design hardware and software to exploit new sources of compute efficiency; however, excessive programmer burden and a lack of principled design methodologies have thwarted its adoption. My research addresses these limitations through foundational contributions that enable the adoption of error-efficiency as a first-class design principle by a variety of users and application domains. In this talk, I will show how my work (1) enables an understanding of how errors affect program execution by providing a suite of automated and scalable error analysis tools, (2) demonstrates how such an understanding can be exploited to build customized error-efficiency solutions targeted to low-cost hardware resiliency and approximate computing and (3) develops methodologies for principled integration of error-efficiency into the software design workflow.Finally, I will discuss future research avenues in error-efficient computing with multi-disciplinary implications in core disciplines (programming languages, software engineering, hardware design, systems) and emerging application areas (AI, VR, robotics, edge computing).

Software testing remains the key technique for detection of functionality errors and vulnerabilities. Automated test generation typically involves searching in a huge input domain. Similarly many other software engineering activities such as software debugging and automated repair can be seen as large search problems. Despite advances in constraint solving and symbolic reasoning, major practical challenges in the use of automated testing and automated program repair, as opposed to manual testing and manual repair include (a) the lack of specifications, leading to problems such as overfitting patches and test-suite bias, and (b) learning curve in using these automated tools, leading to the lack of deployment. In this talk, I will present pragmatic solutions to address these challenges. Lack of specifications can be alleviated by implicitly exploiting lightweight specifications from comment-code inconsistencies, past program versions, or other program artifacts. Lack of deployment can be alleviated via systematic approaches towards collaborative bug finding. Such a collaborative approach can contribute to automated program repair as well as testing.

Learning is a predominant theme for any intelligent system, humans or machines. Moving beyond the classical paradigm of learning from past experience, e.g., supervised learning from given labels, a learner needs to actively collect exploratory feedback to learn the unknowns. Considerable challenges arise in such a setting, including sample complexity, costly and even outdated feedback.

In this talk, I will introduce our themed efforts on developing solutions to efficiently explore the unknowns and dynamically adjust to the changes through exploratory feedback. Specifically, I will first present our studies in leveraging special problem structures for efficient exploration. Then I will present our work on empowering the learner to detect and adjust to potential changes in the environment adaptively. Besides, I will also highlight the impact our research has generated in top-valued industry applications, including online learning to rank and interactive recommendation.

The communication complexity of secure protocols is a fundamental question of the theory of computation and has important repercussions in the development of real-life systems. As an example, the recent surge in popularity of cryptocurrencies has been enabled and accompanied by advancements in the construction of more compact cryptographic machinery. In this talk we discuss how to meet the boundaries of compactness in cryptography and how to exploit succinct communication to construct systems with new surprising properties. Specifically, we consider the problem of computing functions on encrypted data: We show how to construct a fully-homomorphic encryption scheme with message-to-ciphertext ratio (i.e. rate) of 1 – o(1), which is optimal. Along the way, we survey the implication of cryptographic compactness in different contexts, such as proof systems, scalable blockchains, and fair algorithms.

A fundamental challenge of software testing is the statistically well-grounded extrapolation from program behaviors observed during testing. For instance, a security researcher who has run the fuzzer for a week has currently no means (i) to estimate the total number of feasible program branches, given that only a fraction has been covered so far, (ii) to estimate the additional time required to cover 10% more branches (or to estimate the coverage achieved in one more day, resp.), or (iii) to assess the residual risk that a vulnerability exists when no vulnerability has been discovered. Failing to discover a vulnerability, does not mean that none exists—even if the fuzzer was run for a week (or a year). Hence, testing provides no formal correctness guarantees.

In this talk, I establish an unexpected connection with the otherwise unrelated scientific field of ecology, and introduce a statistical framework that models Software Testing and Analysis as Discovery of Species (STADS). For instance, in order to study the species diversity of arthropods in a tropical rain forest, ecologists would first sample a large number of individuals from that forest, determine their species, and extrapolate from the properties observed in the sample to properties of the whole forest. The estimation (i) of the total number of species, (ii) of the additional sampling effort required to discover 10% more species, or (iii) of the probability to discover a new species are classical problems in ecology. The STADS framework draws from over three decades of research in ecological biostatistics to address the fundamental extrapolation challenge for automated test generation. Our preliminary empirical study demonstrates a good estimator performance even for a fuzzer with adaptive sampling bias—AFL, a state-of-the-art vulnerability detection tool. The STADS framework provides statistical correctness guarantees with quantifiable accuracy.

In a cyber-physical system (CPS), a physical process is controlled by software running on a cyber platform. And there exists a strong interaction between the physical dynamics, the control software, the sensors and actuators, and the cyber resources (i.e., computation, communication, and memory resources). These systems are common in domains such as automotive, avionics, health-care, smart manufacturing, smart grid, among others. The state-of-practice is to design CPSs using a disjoint set of tools handling different design domains. Such a design methodology has proved to be inefficient with respect to resource usage and performance. In this talk, I will discuss how models from different engineering disciplines can be integrated to design efficient cyber-physical systems. In particular, I will show two use-cases. First, I will talk about a multi-resource platform consisting of high- and low-quality resources. Correspondingly, I will show that a cost-efficient switching control strategy can be designed exploiting heterogeneous resources and by effectively managing the interplay between control theory, scheduling and formal verification. Second, I will talk about the cyber-physical battery management systems (BMS) for high-power battery packs. I will specifically discuss the problem of cell balancing which is an important task of BMS. I will show how integrated modeling of the individual cells, battery architecture, control circuits, and cyber architecture, can lead to energy- and time-efficient scheduling for active cell balancing.

Information systems have the potential to enhance or limit opportunities when mediating user interactions. They also have the potential to violate privacy by accumulating observational data into detailed user profiles or by exposing people in sensitive contexts. This talk will cover measures and mechanisms we have proposed for mitigating various threats to user well-being in online information ecosystems. In particular, I am going to focus on two contributions in the areas of algorithmic fairness and privacy. The first contribution demonstrates how to operationalize the notion of equity in the context of search systems and how to design optimization models that achieve equity while accounting for human cognitive biases. The second ties our empirical work on profiling privacy and data collection to concepts in data protection laws. Finally, I will discuss the necessity for a holistic approach to responsible technology, from studying different types of harms, through development of different types of interventions, up to taking a step back and refusing technologies that cannot be fixed by technical tweaks.

Recent progress in systems verification have shown that verification techniques can scale to thousands of lines. It is time to ask whether verification can displace testing as an effective path to software correctness. The veribetrfs project is developing a verified high-performance storage system. A primary goal of the project is to reduce verification methodology to engineering practice. Veribetrfs is developed using the Iron★ methodology, a descendent of the Ironclad and IronFleet projects. So far, we have a key-value store with 100k iops performance and strong guarantees against data loss. This talk will give an overview of the methodology and describe how we have enhanced it in veribetrfs. 

Program synthesis techniques aim to generate executable programs from some high-level of expression on user intent, such as logical specifications, examples, or naive reference implementation. This talk will survey different flavors of program synthesis and their applications across the entire software stack, ranging from computer end-users all the way to systems programmers. We will also illustrate how program synthesis is useful for addressing different concerns in software development, including functionality, correctness, performance, and security.

WebAssembly is the first new language to be introduced to the Web ecosystem in over 20 years. Its official specification is given as a formal semantics, making the language a perfect target for further applications of formal methods. This talk highlights recent work which builds on this formal semantics, and discusses the ongoing development of WebAssembly's relaxed memory model, which is complicated by the language's inter-operation with JavaScript.

Producing reliable systems software is a major challenge, plagued by the ubiquitous problems of shared mutable state, pointer aliasing, dynamic memory management, and subtle concurrency issues such as race conditions; even expert programmers struggle to tame the wide variety of reasons why their programs may not behave as they intended. Formal verification offers potential solutions to many of these problems, but typically at a very high price: the mathematical techniques employed are highly-complex, and difficult for even expert researchers to understand and apply.

The relatively-new Rust programming language is designed to help with the former problem: a powerful ownership type system requires programmers to specify and restrict their discipline for referencing heap locations, providing in return the strong guarantee (almost – the talk, and Rustbelt!) that code type-checked by this system will be free from dangling pointers, unexpected aliasing, race conditions and the like. While this rules out a number of common errors, the question of whether a program behaves as intended remains.

In this talk, I’ll give an overview of the Prusti project, which leverages Rust’s type system and compiler analyses for formal verification. By combining the rich information available about a type-checked Rust program with separate user-specification of intended behaviour, Prusti enables a user to verify functional correctness of their code without interacting with a complex program logic; in particular, specifications and all interactions with our implemented tool are at the level of abstraction of Rust expressions.

Epidemic processes can model anything that spreads. As such, they are a useful tool for studying not only human diseases, but also network attacks, chains of activation in the brain, the propagation of real or fake news, the spread of viral tweets, and other processes. In this talk, we investigate epidemics spreading on a graph in the presence of various forms of uncertainty. We present in particular a result about controlling the spread of an epidemic when there is uncertainty about who exactly is infected. We show first that neither algorithms nor results are robust to uncertainty. In other words, uncertainty fundamentally changes how we must approach epidemics on graphs. We also present two related results about learning the graph underlying an epidemic process when there is uncertainty about when people were infected or what infected them.

Cloud providers are nervous about recent research showing how Rowhammer attacks affect many types of DRAM including DDR4 and ECC-equipped DRAM.  Unfortunately, cloud providers lack a systematic way to test the DRAM present in their servers for the threat of a Rowhammer attack. Building such a methodology needs to overcome two difficult challenges: (1) devising a CPU instruction sequence that maximizes the rate of DRAM row activations on a given system, and (2) determining the adjacency of rows internal to DRAM. This talk will present an end-to-end methodology that overcomes these challenges to determine if cloud servers are susceptible to Rowhammer attacks. With our methodology, a cloud provider can construct worst-case testing conditions for DRAM.

We used our methodology to create worst-case DRAM testing conditions on the hardware used by a major cloud provider for a recent generation of its servers. Our findings show that none of the instruction sequences used in prior work to mount Rowhammer attacks create worst-case DRAM testing conditions. Instead, we construct an instruction sequence that issues non-explicit load and store instructions. Our new sequence leverages microarchitectural side-effects to ``hammer'' DRAM at a near-optimal rate on modern Skylake platforms. We also designed a DDR4 fault injector capable of reverse engineering row adjacency inside a DRAM device. When applied to our cloud provider's DIMMs, we find that rows inside DDR4 DRAM devices do not always follow a linear map.

Joint work with Lucian Cojocar (VU Amsterdam), Jeremie Kim, Minesh Patel, Onur Mutlu (ETH Zurich), Lily Tsai (MIT), and Alec Wolman (MSR)

Online services, devices or secret services are constantly collecting data and meta-data from users. This data collection is mostly  used to target users or customise their services. However, as illustrated by the Cambridge Analytica case, data and technologies are more and  more used to manipulate, influence or shape people's opinions online, i.e. to "hack" our brains. In this context, it is urgent to develop the field of  "Cognitive security" in order to better comprehend these attacks and provide counter-measures.  This talk will introduce the concept of "Cognitive security". We will explore the different types of cognitive attacks and discuss possible research directions.

How can we make better applications for social impact issues? For example, the combination of Human-Centered Design (HCD) and Data Science (DS) can be the answer to avoid biases in the collection of data with online-experiments and the analysis of small data. This presentation shows how we combine HCD and DS to design applications and analyze the collected data for Good.  We will focus mainly on the project: "Early screening of dyslexia using a language-independent content game and machine learning". With our two designed games (MusVis and DGames), we collected data sets (313 and 137 participants) in different languages (mainly Spanish and German) and evaluated them with machine learning classifiers. For MusVis, we mainly use content that refers to one single acoustic or visual indicator, while DGames content refers to generic content related to various indicators. Our results open the possibility of low-cost and early screening of dyslexia through the Web. In this talk, we will further address the techniques used from HCD and DS to reach these results. 

The performance of modern key-value servers or layer-7 load balancers often heavily depends on the efficiency of the underlying TCP stack. Despite numerous optimizations such as kernel-bypassing and zero-copying, performance improvement for TCP applications is fundamentally limited due to the protocol conformance overhead for compatible TCP operations.

In this talk, I will introduce AccelTCP, a hardware-assisted TCP stack architecture that harnesses programmable network interface cards (NICs) as a TCP protocol accelerator. AccelTCP can offload complex TCP operations such as connection setup and teardown completely to NIC, which frees a significant amount of host CPU cycles for application processing. In addition, for layer-7 proxies, it supports running connection splicing on NIC so that the NIC relays all packets of the spliced connections with zero DMA overhead. We showcase the effectiveness of AccelTCP with two real-world applications: (1) Redis, a popular in-memory key-value store, and (2) HAProxy, a widely-used layer-7 load balancer. Our evaluation shows that AccelTCP improves their performance by 2.3x and 11.9x, respectively.

Recent research in automated software synthesis from specifications or observations has leveraged the power of SMT solvers in order to explore the space of synthesis conjectures efficiently. In most of this work, synthesis techniques are built around a backend SMT solver which is used as a black-box reasoning engine. In this talk, I will describe a successful multiyear research effort by the developers of the SMT solver CVC4 that instead incorporates synthesis capabilities directly within the solver, and the discuss the advances in performance and scope made possible by this approach.

Learning technologies are becoming increasingly important in today's education. This includes game-based learning and simulations, which produce high volume output, and MOOCs (massive open online courses), which reach a broad and diverse audience at scale. The users of such systems often are of very different backgrounds, for example in terms of age, prior knowledge, and learning speed. Adaptation to the specific needs of the individual user is therefore essential. In this talk, I will present two of my contributions on modeling and predicting student learning in computer-based environments with the goal to enable individualization. The first contribution introduces a new model and algorithm for representing and predicting student knowledge. The new approach is efficient and has been demonstrated to outperform previous work regarding prediction accuracy. The second contribution introduces models, which are able to not only take into account the accuracy of the user, but also the inquiry strategies of the user, improving prediction of future learning. Furthermore, students can be clustered into groups with different strategies and targeted interventions can be designed based on these strategies. Finally, I will also describe lines of future research.

Since introduction of the IEEE 754 floating point standard in 1985, numerical methods have become ubiquitous --- and increasingly sophisticated. With growing code complexity of numerical libraries grows the need for rigorous Software Engineering methodology: as provided by Computer Science and state of the art regarding digital processing of discrete data, but lacking in the continuous realm. We apply, adapt, and extend the classical concepts --- specification, algorithmics, analysis, complexity, verification --- from discrete bit strings, integers, graphs etc. to real numbers, converging sequences, smooth/integrable functions, bounded operators, and compact subsets: A new paradigm formalizes mathematical structures as continuous Abstract Data Types with rigorous Turing-computable semantics but without the hassle of actual Turing machines.

A growing number of domestic spaces incorporate products that collect data from cameras, microphones and other sensors, leading to privacy concerns. In this talk I report on two user studies performed to learn about perceptions of privacy and trust for sensor-enabled, connected devices such as smart home assistants. The study results suggest that users are more likely to trust devices with materially representative privacy status indicators. This means that the indicators themselves are part of what determines what sensing can take place. I will describe how we have applied the study results to the design of current devices and what the implications are for the physical design of future smart devices.

Time permitting, I will also talk about my other current passion -- design for additive manufacturing – and what researchers can do to ensure we reach the vastly exciting potential of this method of production. I will bring exotic 3D printed parts to help demonstrate my points.

Automated program repair is an emerging and exciting field of research, which allows for automated rectification of errors and vulnerabilities. The use of automated program repair can be myriad, such as (a) improving programmer productivity (b) automated fixing of security vulnerabilities as they are detected, (c) self-healing software for autonomous devices such as drones, as well as (d) use of repair in introductory programming education by grading and providing hints for programming assignments. One of the key technical challenges in achieving automated program repair, is the lack of formal specifications of intended program behavior. In this talk, we will conceptualize the use of symbolic execution approaches and tools for extracting such specifications. This is done by analyzing a buggy program against selected tests, or against reference implementations. Such specification inference capability can be combined with program synthesis techniques to automatically repair programs. The capability of specification inference also serves a novel use of symbolic execution beyond verification and navigation of large search spaces. Automated program repair via symbolic execution goes beyond search-based approaches which attempt to lift patches from elsewhere in the program. Such an approach can construct "imaginative" patches, serves as a test-bed for the grand- challenge of automated programming, and contributes to the vision of trustworthy self-healing software. Towards the end of the talk, we can put the research on automated repair in light of the overall practice of software security, by sharing some experiences gained at the Singapore Cyber-security Consortium.

The spread of fake news was one of the most discussed characteristics of the 2016 U.S. Presidential Election. The concerns regarding fake news have garnered significant attention in both media and policy circles, with some journalists even going as far as claiming that results of the 2016 election were a consequence of the spread of fake news. Yet, little is known about the prevalence and focus of such content, how its prevalence changed over time, and how this prevalence related to important election dynamics. In this talk, I will address these questions by examining social media, news media, and interview data. These datasets allow examining the interplay between news media production and consumption, social media behavior, and the information the electorate retained about the presidential candidates leading up to the election.

In the last two decades, automation has had a significant impact on software testing and analysis. Automated testing techniques, such as symbolic execution, concolic testing, and feedback-directed fuzzing, have found numerous critical faults, security vulnerabilities, and performance bottlenecks in mature and well-tested software systems. The key strength of automated techniques is their ability to quickly search state spaces by performing repetitive and expensive computational tasks at a rate far beyond the human attention span and computation speed. In this talk, I will give a brief overview of our past and recent research contributions in automated test generation using symbolic execution, program analysis, constraint solving, and fuzzing. I will also describe a new technique, called constraint-directed fuzzing, where given a pre-condition on a program as a logical formula, we can efficiently generate millions of test inputs satisfying the pre-condition.

The ongoing shift of enterprise computing to the cloud provides an opportunity to rethink operating systems for this new setting. I will discuss two specific technologies, kernel bypass for high performance networking and low latency non-volatile storage, and their implications for operating system design. In each case, delivering the performance of the underlying hardware requires novel approaches to the division of labor between hardware, the operating system kernel, and the application library.

Software-defined Networks and programmable data-planes represent a shift in networking paradigm, which enables novel applications. Despite the growing interest and adoption of SDNs, SDNs remain plagued with availability and performance problems. In this talk, I discuss recent and ongoing work by my group to analyze these paradigms and create systematic abstractions that provide control over performance and availability. First, I will discuss Tardis a system that improves fault tolerance by leveraging the novel programmability provided by SDNs to identify and transform the failure-inducing event(s). Second, I will discuss a pair of projects, Hermes and SCC, that revisits traditional storage principles and applies them to network updates. Through this work, I will demonstrate how the centralization and programmability offered by SDNs enables us to more systematically reason about traditional networking issues such as availability and performance.

Multiprocessor Systems-on-Chip (MPSoC) integrating hard processing cores with programmable logic (PL) are becoming increasingly common. While these platforms have been originally designed for high performance computing applications, their rich feature set can be exploited to efficiently implement mixed criticality domains serving both critical hard real-time tasks, as well as soft real-time tasks.

In this talk, we show how one can tailor these MPSoCs to support a mixed criticality system, where cores are strictly isolated to avoid contention on shared resources such as Last-Level Cache (LLC) and main memory. We present and discuss a set of software and hardware techniques to improve the predictability using a modern MPSoC platform. We evaluate our techniques using an image processing application and show the maximum supported processing frequency.

As deep learning research pushes towards using larger and more sophisticated models, system infrastructure must use many GPUs efficiently. Analyzing the dataflow graph that represents the DNN computation is a promising avenue for optimization. By specializing execution for a given dataflow graph, we can accelerate DNN computation in ways that are transparent to programmers. In this talk, I show the benefits of dataflow graph analysis by discussing two recent systems that we've built to support large model training and low-latency inference. To train very large DNN models, Tofu automatically re-writes a dataflow graph of tensor operators into an equivalent parallel graph in which each original operator can be executed in parallel across multiple GPUs.  To achieve low-latency inference, Batchmaker discovers identical sub-graph computation among different requests to enable batched execution of requests arriving at different times. 

Recent AI advances have been driven by high-quality input data, often labeled by human annotators. A fundamental challenge in eliciting high-quality information from humans is that there is often no way to directly verify the quality of the information they provide. Consider, for example, product reviews and marketing surveys where data is inherently subjective, environmental community sensing where data is highly localized, and geopolitical forecasting where the ground truth is revealed in the distant future. In these settings, data elicitation has to rely on peer-consistency mechanisms, which incentivize high-quality reporting by examining the consistency between the reports of different data providers. In this talk, I will discuss some of the recent advances in peer-consistency designs. Furthermore, I will outline some thoughts on an agenda around the design of human-AI collaborative systems.

Secure Multi-Party Computation (MPC) allows mutually distrusting parties to run joint computations without revealing private data. Current MPC algorithms scale poorly with data size, which makes MPC on "big data" prohibitively slow and inhibits its practical use. Many relational analytics queries can maintain MPC’s end-to-end security guarantee without using cryptographic MPC techniques for all operations. Conclave is a query compiler that accelerates such queries by transforming them into a combination of data-parallel, local cleartext processing and small MPC steps. When parties trust others with specific subsets of the data, Conclave applies new hybrid MPC-cleartext protocols to run additional steps outside of MPC and improve scalability further. Our Conclave prototype generates code for cleartext processing in Python and Spark, and for secure MPC using the Sharemind and Obliv-C frameworks. Conclave scales to data sets between three and six orders of magnitude larger than state-of-the-art MPC frameworks support on their own. Thanks to its hybrid protocols and additional optimizations, Conclave also substantially outperforms SMCQL, the most similar existing system.

In 2012, Herbelin developed a calculus (dPAω) in which constructive proofs for the axioms of countable and dependent choices can be derived via the memoization of choice functions However, the property of normalization (and therefore the one of soundness) was only conjectured. The difficulty for the proof of normalization is due to the simultaneous presence of dependent dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type ℕ→A into streams (a₀,a₁,…)) and of lazy evaluation with sharing (for these coinductive objects). Building on previous works, we introduce a variant of dPAω presented as a sequent calculus. On the one hand, we take advantage of a variant of Krivine classical realizability we developed to prove the normalization of classical call-by-need. On the other hand, we benefit of dLtp, a classical sequent calculus with dependent types in which type safety is ensured using delimited continuations together with a syntactic restriction. By combining the techniques developed in these papers, we manage to define a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness. This talk will go over the whole process, starting from Herbelin’s calculus dPAω until the introduction of its sequent calculus counterpart dLPAω that we prove to be sound.

Recognizing that applications (whether in mobile, desktop, or server environments) are rarely executed in isolation today, I will discuss some practical challenges in making best use of available hardware and our approach to addressing these challenges. I will describe two independent and complementary control mechanisms using low-overhead hardware performance counters that we have developed: a sharing- and resource-aware mapper (SAM) to effect task placement with the goal of localizing shared data communication and minimizing resource contention based on the offered load; and an application parallelism manager (MAPPER) that controls the offered load with the goal of improving system parallel efficiency. If time permits, I will also outline our work on streamlining instruction memory management and address translation to eliminate redundancy and improve efficiency, especially in mobile environments. Our results emphasize the need for low-overhead monitoring of application behavior under changing environmental conditions in order to adapt to environment and application behavior changes.

The notion of edge computing introduces new computing functions away from centralized locations and closer to the network edge and thus facilitating new applications and services. This enhanced computing paradigm is provides new opportunities to applications developers, not available otherwise. In this talk, I will discuss why placing computation functions at the extreme edge of our network infrastructure, i.e., in wireless Access Points and home set-top boxes, is particularly beneficial for a large class of emerging applications. I will discuss a specific approach, called ParaDrop, to implement such edge computing functionalities, and use examples from different domains -- smarter homes, sustainability, and intelligent transportation -- to illustrate the new opportunities around this concept.

A sliding window algorithm for a language L receives a stream of symbols and has to decide at each time step whether the suffix of length n belongs to L or not. The window size n is either a fixed number (in the fixed-size model) or can be controlled online by an adversary (in the variable-size model). In this talk we give a survey on recent results for deterministic and randomized sliding window algorithms for regular languages.

The last few years have seen a surge of decision problems with an astronomical, non primitive-recursive complexity, in logic, verification, and games. While the existence of such uncontrived problems is known since the early 1980s, the field has matured with techniques for proving complexity lower and upper bounds and the definition of suitable complexity classes. This framework has been especially successful for analysing so-called `well-structured systems'---i.e., transition systems endowed with a well-quasi-order, which underly most of these astronomical problems---, but it turns out to be applicable to other decision problems that resisted analysis, including two famous problems: reachability in vector addition systems and bisimilarity of pushdown automata. In this talk, I will explain how some of these techniques apply to reachability in vector addition systems, yielding tight Ackermannian upper bounds for the decomposition algorithm initially invented by Mayr, Kosaraju, and Lambert; this will be based on joint work with Jérôme Leroux.

Real-time embedded systems need to be analyzable for execution time guarantees. Despite significant scientific advances, however, timing analysis lags years behind current microarchitectures with out-of-order scheduling pipelines, several hardware threads and multiple (shared)cache layers. To satisfy the increasing demand for predictable performance, analyzable performance features are required. We introduce runtime-reconfigurable instruction set processors as one way to escape the scarcity of analyzable performance features while preserving the flexibility of the system. To this end, we first present a reconfiguration controller for guaranteed reconfiguration delays of accelerators onto an FPGA. We propose a novel timing analysis approach to obtain worst-case execution time (WCET) guarantees for applications that utilize runtime-reconfigurable custom instructions (CIs), which each utilize one or more accelerators. Given the constrained reconfigurable area of an FPGA, we solve the problem of selecting CIs for each computational kernel of an application to optimize its worst-case execution time. Finally, we show that runtime reconfiguration provides the unique feature of optimized static WCET guarantees and optimization of the average-case execution time (maintaining statically-given WCET guarantees) by repurposing reconfigurable area for different selections of CIs at runtime.

Algorithms and decision making based on Big Data have become pervasive in all aspects of our daily (offline and online) lives. Social media, e-commerce, professional, political, educational, and dating sites, to mention just a few, shape our possibilities as individuals, consumers, employees, voters, students, and lovers. In this process, vast amounts of personal data are collected and used to train machine-learning based systems. These systems are used to classify and rank people, and can discriminate us on grounds such as gender, age, or ethnicity, even without intention, and even if legally protected attributes, such as race, are not explicit in the data. Algorithmic bias exists even when there is no discrimination intention in the developer of the algorithm. Sometimes it may be inherent to the data sources used (software making decisions based on data can reflect, or even amplify, the results of historical discrimination), but even when the sensitive attributes have been suppressed from the input, a well trained machine learning algorithm may still discriminate on the basis of such sensitive attributes because of correlations existing in the data.

Cloud computing gives the illusion of infinite computational capacity and allows for on-demand resource provisioning. As a result, over the last few years, the cloud computing model has experienced widespread industrial adoption and companies like Netflix offloaded their entire infrastructure to the cloud. However, with even the largest datacenter being of a finite size, cloud infrastructures have experienced overload due to overbooking or transient failures. In essence, this is an excellent opportunity for the design of control solutions, that tackle the problem of mitigating overload peaks, using feedback from the infrastructure. These solutions can then exploit control-theoretical principles and take advantage of the knowledge and the analysis capabilities of control tools to provide formal guarantees on the predictability of the infrastructure behavior. This talk introduces recent research advances on feedback control in the cloud computing domain, together with my research agenda for enhancing predictability and formal guarantees for cloud computing.

Internet applications rely on large-scale networked environments such as the cloud for their backend support. In these multi-tenanted environments, various stakeholders have diverse goals. The objective of the infrastructure provider is to increase revenue by utilizing the resources efficiently. Applications, on the other hand, want to meet their performance requirements at minimal cost. However, estimating the exact amount of resources required to meet the application needs is a difficult task, even for expert users. Easy workarounds employed for tackling this problem, such as resource over-provisioning, negatively impact the goals of the provider, applications, or both. In this talk, I will discuss the design of application-aware self-optimizing systems through automated resource management that helps meet the varied goals of the provider and applications in large-scale networked environments. The key steps in closed-loop resource management include learning of application resource needs, efficient scheduling of resources, and adaptation to variations in real time. I will describe how I apply this high-level approach in two distinct environments using (a) Morpheus in enterprise clusters, and (b) Patronus in cellular provider networks with geo-distributed micro data centers. I will also touch upon my related work in application-specific context at the intersection of network scheduling and deep learning. I will conclude with my vision for self-optimizing systems including fully automated clouds and an elastic geo-distributed platform for thousands of micro data centers.

Nowadays, innovation in many industrial areas is software driven, where existing software functions become more complex and new software functions are constantly introduced. The rapid increase in functionality comes along with a steep increase in software complexity. To cope with this transition, current trends shift away from today’s distributed architectures towards integrated architectures. Here, previously distributed functionality is consolidated on fewer, more powerful, computers. Such a trend can for example be observed in the automotive or avionics domain. This can ease the integration process, reduce the hardware complexity, and ultimately save costs. One promising hardware platform for these powerful embedded computers is the many-core processor. A many-core processor hosts a vast number of compute cores, that are partitioned on clusters which are connected by a Network-on-Chip. However, ensuring that real-time requirements are satisfied in the presence of contention in shared resources, such as memories, remains an open issue. In addition, industrial applications are often subject to timing constraints on the data propagation through a chain of semantically related tasks. Such requirements pose challenges to the system designer as they are only able to verify them after the system synthesis (i.e. very late in the design process). In this talk, we present methods that transform timing constraints on the data propagation delay into precedence constraints between individual task instances. An execution framework for the cluster of the many-core is proposed that allows access to cluster external memory while it avoids contention on shared resources by design. Spatial and temporal isolation between different clusters is provided by a partitioning and configuration of the Network-on-Chip that further reduces the worst-case access times to external memory.

The rise of user-centric Internet systems such as Facebook or Twitter brought security and privacy threats that became out of control in recent years. To make such systems more dependable, my research focuses on three key aspects: (1) privacy: ensure users understand and can control the information that is disclosed about them; (2) transparency: ensure users understand how their data is being used and how it affects the services they receive; and (3) trust: ensure users can evaluate the trustworthiness of content consumed from these systems. 

In this talk, I will share my research efforts in understanding and tackling security and privacy threats in social media targeted advertising. Despite a number of recent controversies regarding privacy violations, lack of transparency, or vulnerability to discrimination or propaganda by dishonest actors; users still have little understanding of what data targeted advertising platforms have about them and why they are shown the ads they see. To address such concerns, Facebook recently introduced the "Why am I seeing this?" button that provides users with an explanation of why they were shown a particular ad. I first investigate the level of transparency provided by this mechanism by empirically measuring whether it satisfies a number of key properties and what are the consequences of the current design choices. To provide a better understanding of the Facebook advertising ecosystem, we developed a tool called AdAnalyst that collects the ads users receive and provides aggregate statistics. I will then share our findings from analyzing data from over 600 real-world AdAnalyst users; in particular on who is advertising on Facebook and how these advertisers are targeting users and customizing ads via the platform. 

Over the past decade, the field of artificial intelligence (AI) has seen striking developments. Yet, today’s AI systems sorely lack the essence of human intelligence i.e.  our ability to (a) understand language and grasp its meaning, (b) assimilate common-sense background knowledge of the world, and (c) draw inferences and perform reasoning. Before we even begin to build AI systems that possess the aforementioned human abilities, we must ask an even more fundamental question: How would we even evaluate an AI system on the aforementioned abilities? In this talk, I will argue that we can evaluate AI systems in the same way as we evaluate our children - by giving them standardized tests. Standardized tests are administered to students to measure the knowledge and skills gained by them. Thus, it is natural to use these tests to measure the intelligence of our AI systems. Then, I will describe Parsing to Programs (P2P), a framework that combines ideas from semantic parsing and probabilistic programming for situated question answering. We used P2P to build systems that can solve pre-university level Euclidean geometry and Newtonian physics examinations. P2P achieves a performance at least as well as the average student on questions from textbooks, geometry questions from previous SAT exams, and mechanics questions from Advanced Placement (AP) exams. I will conclude by describing implications of this research and some ideas for future work.

Modern applications must collect and store massive amounts of data. Cloud storage offers these applications simplicity: the abstraction of a failure-free, perfectly scalable black-box. While appealing, offloading data to the cloud is not without challenges. Cloud storage systems often favour weaker levels of isolation and consistency. These weaker guarantees introduce behaviours that, without care, can break application logic. Offloading data to an untrusted third party like the cloud also raises questions of security and privacy.

This talk summarises my efforts to improve the performance, the semantics and the security of transactional cloud storage systems. It centers around a simple idea: defining consistency guarantees from the perspective of the applications that observe these guarantees, rather than from the perspective of the systems that implement them. I will discuss how this new perspective brings forth several benefits. First, it offers simpler and cleaner definitions of weak isolation and consistency guarantees. Second, it enables more scalable implementations of existing guarantees like causal consistency. Finally, I will discuss its applications to security: our client-centric perspective allows us to add obliviousness guarantees to transactional cloud storage systems.

Developing high-performance datacenter applications is complex and time-consuming today, as developers must understand and correctly implement subtle interactions between different backend systems. I describe a new approach that redesigns core datacenter systems around new abstractions: the right abstractions substantially reduce complexity while maintaining the same performance. This saves expensive developer time, uses datacenter servers more efficiently, and can enable new, previously impossible systems and applications. I illustrate the impact of such redesigns with Noria, which recasts web application backends-i.e., databases and caches-as a streaming dataflow computation based on a new abstraction of partial state. Noria's partially-stateful dataflow brings classic databases' familiar query flexibility to scalable dataflow systems, simplifying applications and improving the backend's efficiency. For example, Noria increases the request load handled by a single server by 5-70x compared to state-of-the-art backends. Additional new abstractions from my research increase the efficiency of other datacenter systems (e.g., cluster schedulers), or enable new kinds of systems that, for example, may help protect user data against exposure through application bugs.

Symbolic execution is a program analysis technique that can automatically explore and analyse paths through a program. While symbolic execution was initially introduced in the seventies, it has only received significant attention during the last decade, due to tremendous advances in constraint solving technology and effective blending of symbolic and concrete execution into what is often called dynamic symbolic execution. Dynamic symbolic execution is now a key ingredient in many computer science areas, such as software engineering, computer security, and software systems, to name just a few. In this talk, I will discuss recent advances and ongoing challenges in the area of dynamic symbolic execution, drawing upon our experience developing several symbolic execution tools for many different scenarios, such as high-coverage test input generation, bug and security vulnerability detection, patch testing and bounded verification, among many others.

First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows. Desirable properties of these systems such as functional correctness or non-interference have conveniently been formulated as safety properties. Here, we go one step further. Our goal is to verify safety, and also to develop techniques for automatically synthesizing strategies to enforce safety. For that reason, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is equivalent to second-order quantifier elimination. For monadic games, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal invariants only. We identify a non-trivial sub-class where safety is decidable. For the general case, we provide meaningful abstraction and refinement techniques for realizing a CEGAR based synthesis loop. Joint work with: Christian Müller, TUM Bernd Finkbeiner, Universität des Saarlandes

Many approaches to analyze the complexity of programs automatically are based on transformations into integer or term rewrite systems. However, state-of-the-art tools that analyze the worst-case complexity of rewrite systems are restricted to the inference of upper bounds. In this talk, the first techniques for the inference of lower bounds on the worst-case complexity of integer and term rewrite systems are introduced. While upper bounds can prove the absence of performance-critical bugs, lower bounds can be used to find them.

For term rewriting, the power of the presented technique gives rise to the question whether the existence of a non-constant lower bound is decidable. Thus, the corresponding decidability results are also discussed in this talk.

Finally, to see the practical value of complexity analysis techniques for rewrite systems, we will have a glimpse at the transformation from Java programs to integer rewrite systems that is implemented in the tool AProVE.

In this talk I shall outline a summary of our five year long initiative studying the temporal dynamics of various human language-like entities over the social media. Some of the topics that I plan to cover are (a)  how opinion conflicts could be effectively used for incivility detection in Twitter [CSCW 2018], (b) how word borrowings can be automatically identified from social signals [EMNLP 2017] and (c)  how hashtags in Twitter form compounds like natural language words (e.g., #Wikipedia+#Blackout=#WikipediaBlackout) that become way more popular than the individual constituent hashtags [CSCW 2016, Honorable Mention].

Many classification tasks have no objective ground truth. Examples include: which content or explanation is "better" according to some community? is this comment toxic? what is the political leaning of this news article? The traditional modeling approach assumes each item has an objective true state that is perceived by humans with some random error. It fails to account for the fact that people have greater agreement on some items than others. I will describe an alternative model where the true state is a distribution over labels that raters from a specified population would assign to an item. This leads to information gain (mutual information) as a theoretically justified and computationally tractable measure of a classifier's quality, and an intuitive interpretation of information gain in terms of the sample size for a survey that would yield the same expected error rate.

I will present a recent non-elementary lower bound for the complexity of reachability problem for Vector Addition Systems. I plan to show the main insights of the proof. In particular I will present a surprising equation on fractions, which is the core of the new source of hardness found in VASes.

In real-time embedded systems, for each task the compliance to timing constraints has to be guaranteed in addition to the functional correctness. The first part of the talk considers the theoretical comparison of scheduling algorithms and schedulability tests by evaluating speedup factors for non-preemptive scheduling, which leads to a discussion about general problems of resource augmentation bounds. In addition, it is explained how utilization bounds can be parametrized, resulting in better bounds for specific scenarios, i.e., when analyzing non-preemptive Rate-Monotonic scheduling as well as task sets inspired by automotive applications.

In the second part, a setting similar to mixed-criticality systems is considered and the criticism on previous work in this area is detailed. Hence, a new system model that allows a better applicability to realistic scenarios, namely Systems with Dynamic Real-Time Guarantees, is explained. This model is extended to a multiprocessor scenario, considering CPU overheating as a possible cause for mixed-criticality behaviour. Finally, a way to determine the deadline-miss probability for such systems is described that drastically reduces the runtime of such calculations.

The third part discusses tasks with self-suspension behaviour, explains a fixed-relative-deadline strategy for segmented self-suspension tasks with one suspension interval, and details how this approach can be exploited in a resource-oriented partitioned scheduling. Furthermore, it is explained how the gap between the dynamic and the segmented self-suspension model can be bridged by hybrid models.

SCION is a new Internet architecture that addresses many of the security vulnerabilities of today’s Internet. Its clean-slate design provides, among other properties, route control, failure isolation, and multi-path communication. The verifiedSCION project is an effort to formally verify the correctness and security of SCION. It aims to provide strong guarantees for the entire architecture, from the protocol design to its concrete implementation. The project uses stepwise refinement to prove that the protocol withstands increasingly strong attackers. The refinement proofs assume that all network components such as routers satisfy their specifications. This property is then verified separately using deductive program verification in separation logic. This talk will give an overview of the verifiedSCION project and explain, in particular, how we verify code-level properties such as memory safety, I/O behavior, and information flow security.

Cloud computing gives the illusion of infinite computational capacity and allows for on-demand resource provisioning. As a result, over the last few years, the cloud computing model has experienced widespread industrial adoption and companies like Netflix offloaded their entire infrastructure to the cloud. However, with even the largest datacenter being of a finite size, cloud infrastructures have experienced overload due to overbooking or transient failures. In essence, this is an excellent opportunity for the design of control solutions, that tackle the problem of mitigating overload peaks, using feedback from the computing infrastructure. Exploiting control-theoretical principles and taking advantage of the knowledge and the analysis capabilities of control tools, it is possible to provide formal guarantees on the predictability of the cloud platform. This talk introduces recent research advances on feedback control in the cloud computing domain. This talk discusses control solutions and future research for both cloud application development, and infrastructure management. In particular, it covers application brownout, control-based load-balancing, and autoscaling.

A variety of experts -- computer scientists, policy makers, judges -- constantly make decisions about best practices for computational systems. They decide which features are fair to use in a machine learning classifier predicting whether someone will commit a crime, and which security behaviors to recommend and require from end-users. Yet, the best decision is not always clear. Studies have shown that experts often disagree with each other and, perhaps more importantly, with the people for whom they are making these decisions: the users.

This raises a question: Is it possible to learn best practices directly from the users? The field of moral philosophy suggests yes, through the process of descriptive decision-making, in which we observe people’s preferences and then infer best practice rather than using experts’ normative (prescriptive) determinations to define best practice. In this talk, I will explore the benefits and challenges of applying such a descriptive approach to making computationally relevant decisions regarding: (i) selecting security prompts for an online system; (ii) determining which features to include in a classifier for jail sentencing; (iii) defining standards for ethical virtual reality content.

Fairness considerations in settings where decisions are made by supervised learning algorithms (e.g. criminal risk assessment) has received considerable attention, recently. As the fairness literature continues to expand mostly around this canonical learning task, it is important to recognize that many real-world applications of ML fall outside the category of supervised, one-shot learning. In this presentation, I will talk about two scenarios in which algorithmic decisions are made in a sequential manner and over time. I will argue that in such settings, being fair---at a minimum---requires decisions to be "consistent" across individuals who arrive at different time steps, that is, similar individuals must be treated similarly. I will then talk about how such consistency constraints affect learning. 

In the first part of the talk, I will introduce a generic sequential decision making framework, in which at each time step the learning algorithm receives data corresponding to a new individual (e.g. a new job application) and must make an irrevocable decision about him/her (e.g. whether to hire the applicant) based on observations it has made so far. I propose a general framework for post-processing predictions made by a black-box learning model, so that the resulting sequence of outcomes is guaranteed to be consistent. I show, both theoretically and via simulations, that imposing consistency constraints will not significantly slow down learning.

In the second part of the talk, I will focus on fairness considerations in a particular type of market---namely, combinatorial prediction markets---where traders can submit limit orders on various security bundles, and the market maker is tasked with executing these orders in a fair manner. The main challenge in running such market is that executing one order can potentially change the price of every other order in the book. I define the notion of a "fair trading path", which at a high level guarantees similar orders are executed similarly: no order executes at a price above its limit, and every order executes when its market price falls below its limit price. I present a market algorithm that respects these fairness conditions, and evaluate it using real combinatorial predictions made during the 2008 U.S. Presidential election. 

I will conclude by comparing my work with previous papers on fairness for online learning, and a list of directions for future work.

Parameterized complexity analyzes the computational complexity of NP-hard combinatorial problems in finer detail than classical complexity: instead of expressing the running time as a univariate function of the size $n$ of the input, one or more relevant parameters are defined and the running time is analyzed as a function depending on both the input size and these parameters. The goal is to obtain algorithms whose running time depends polynomially on the input size, but may have arbitrary (possibly exponential) dependence on the parameters. Moreover, we would like the dependence on the parameters to be as slowly growing as possible, to make it more likely that the algorithm is efficient in practice for small values of the parameters. In recent years, advances in parameterized algorithms and complexity have given us a tight understanding of how the parameter has to influence the running time for various problems. The talk will survey results of this form, showing that seemingly similar NP-hard problems can behave in very different ways if they are analyzed in the parameterized setting.

Programmable analog devices are a powerful new computing substrate that are especially appropriate for performing computationally intensive simulations of dynamical systems. Until recently, the de-facto standard for programming these devices required hardware specialists to manually program the analog device to model the dynamical system of interest. In this talk, I will present Arco, a compiler that automatically configures analog devices to perform dynamical system simulation, and Jaunt, a compilation technique that that scales dynamical system parameters to change the speed of the simulation and render the resulting simulation physically realizable given the operating constraints of the analog hardware platform. These techniques capture the domain knowledge required to fully exploit the capabilities of reconfigurable analog devices, eliminating a key obstacle to the widespread adoption of these devices.

Suppose that a group of voters wants to select k \ge 1 alternatives from a given set, and each voter indicates which of the alternatives are acceptable to her: the alternatives could be conference submissions, applicants for a scholarship or locations for a fast food chain. In this setting it is natural to require that the winning set represents the voters fairly, in the sense that large groups of voters with similar preferences have at least some of their approved alternatives in the winning set. We describe several ways to formalize this idea, and show how to use it to classify voting rules. For one of our axioms, the only known voting rule that satisfies it is not polynomial-time computable, and it was conjectured that no voting rule that satisfies this axiom can be polynomial-time computable; however, we will show that this is not the case.

In this talk, I will present AI2, a sound and scalable analyzer for deep neural networks. Based on overapproximation, AI2 can automatically prove safety properties (e.g., robustness) of realistic neural networks (e.g., convolutional neural networks). The key insight behind AI2 is to phrase reasoning about safety and robustness of neural networks in terms of classic abstract interpretation, enabling to leverage decades of advances in that area. To this end, I will introduce abstract transformers that capture the behavior of fully connected and convolutional neural network layers with rectified linear unit activations (ReLU), as well as max pooling layers. This allows to handle real-world neural networks, which are often built out of these types of layers. I will also empirically demonstrate that (i) AI2 is precise enough to prove useful specifications (e.g., robustness), (ii) AI2 can be used to certify the effectiveness of state-of-the-art defenses for neural networks, and (iii) AI2 is significantly faster than existing analyzers based on symbolic analysis, which often take hours to verify simple fully connected networks.

Energy consumption is an important concern for cloud datacenters. Its cost represents about 80% of the total cost of ownership and it is estimated that in 2020, the US datacenters alone will spend about $13 billion on energy bills. Generally, the servers are manufactured in such a way that they achieve high energy efficiency at high utilizations. Thereby for a low cost per computation all datacenter servers should push the utilization as high as possible. In order to fight the historically low utilization, cloud computing adopted server virtualization. This technology enables a cloud provider to pack (consolidate) the entire set of virtual machines (VMs) on a small set of physical servers and thereby, reduce the number of active servers. Even so, the datacenter servers rarely reach utilizations higher than 50% which means that they operate with a set of long-term unused resources (called 'holes'). Our first contribution is a cloud management system that dynamically splits/fusions VMs such that they can better fill the holes. However the datacenter resource fragmentation has a more fundamental problem. Over time, cloud applications demand more and more memory but the physical servers provide more an more CPU. In nowadays datacenters, the two resources are strongly coupled since they are bounded to a physical sever. Our second contribution is a practical way to decouple the CPU-memory tuple that can simply be applied to a commodity server. The underutilization observed on physical servers is also true for virtual machines. It has been shown that VMs consume only a small fraction of the allocated resources because the cloud customers are not able to correctly estimate the resource amount necessary for their applications. Our third contribution is a system that estimates the memory consumption (i.e. the working set size) of a VM, with low overhead and high accuracy. Thereby, we can now consolidate the VMs on based on their working set size (not the booked memory). However, the drawback of this approach is the risk of memory starvation. If one or multiple VMs have an sharp increase in memory demand, the physical server may run out of memory. This event is undesirable because the cloud platform is unable to provide the client with the memory he paid for. Our fourth contribution is a system that allows a VM to use remote memory provided by a different rack server. Thereby, in the case of a peak memory demand, our system allows the VM to allocate memory on a remote physical server.

Embedding a domain-specific language (DSL) in a general purpose host language is an efficient way to develop a new DSL. Various kinds of languages and paradigms can be used as host languages, including object-oriented, functional, statically typed, and dynamically typed variants, all having their pros and cons. For deep embedding, statically typed languages enable early checking and potentially good DSL error messages, instead of reporting runtime errors. Dynamically typed languages, on the other hand, enable flexible transformations, thus avoiding extensive boilerplate code. In this talk, I will discuss the concept of gradually typed symbolic expressions that mix static and dynamic typing for symbolic data. The key idea is to combine the strengths of dynamic and static typing in the context of deep embedding of DSLs. Moreover, I will briefly outline an ongoing research effort of developing a new framework for developing heterogenous domain-specific languages.

The design and implementation of real-time systems require that both the logical and the temporal behaviour are correct. There exist several specialized languages and tools that use the notion of logical time, as well as industrial strength languages such as Ada and RTJS that incorporate direct handling of real time. Although these languages and tools have shown to be good alternatives for safety-critical systems, most commodity real-time and embedded systems are today implemented in the standard C programming language. Such systems are typically targeting proprietary bare-metal platforms, standard POSIX compliant platforms, or open-source operating systems. It is, however, error prone to develop large, reliable, and portable systems based on these APIs. In this talk, I will talk about an extension to the C programming language, called Timed C, with a minimal set of language primitives, and show how a retargetable source-to-source compiler can be used to compile and execute simple, expressive, and portable programs

Road safety is a major public health issue, with road accidents accounting for an estimated 1.25 million fatalities, and many more injuries, the world over, each year. The problem is particularly acute in India, with nearly a quarter of a million fatalities every year, i.e., 20% of the world’s total. Besides the heavy human cost, road accidents also impose a significant economic cost. The crux of the problem is that the major factors impacting safety — vehicles, roads, and people — have virtually no ongoing monitoring today. In the HAMS project at Microsoft Research India, we employ a dashboard-mounted smartphone, and the array of sensors it includes, as a virtual harness, with a view to monitoring drivers and their driving. We focus primarily on the camera sensors of the smartphone, both the front camera, which faces the driver, and the back camera, which looks out to the front of the vehicle. We address the challenges arising from our choice of low-cost generic sensors instead of more expensive specialized sensors, the need for efficient processing on a smartphone, and demands of robust operation in uncontrolled environments. HAMS has been piloted as part of a driver training program, with promising early results.

Materials and manufacturing processes can be made to adapt to the way in which their end-products are used, by imbuing raw materials with sensing and computation elements. By making the algorithms that run on these computing elements aware of the physics of the objects in which they are embedded, computation-and-sensing augmented materials could change the way we think about the border between inanimate objects and computing systems. One way to exploit knowledge about the physical world in the programs running on (or in) these objects is to exploit the fact that these programs can often tolerate noise and other deviations from correctness in their input data. This talk will highlight research that builds on these observations.

Is perfect matching in NC? That is, is there a deterministic fast parallel algorithm for it? This has been an outstanding open question in theoretical computer science for over three decades, ever since the discovery of RNC matching algorithms. Within this question, the case of planar graphs has remained an enigma: On the one hand, counting the number of perfect matchings is far harder than finding one (the former is #P-complete and the latter is in P), and on the other, for planar graphs, counting has long been known to be in NC whereas finding one has resisted a solution. In this paper, we give an NC algorithm for finding a perfect matching in a planar graph. Our algorithm uses the above-stated fact about counting matchings in a crucial way. Our main new idea is an NC algorithm for finding a face of the perfect matching polytope at which W(n) new conditions, involving constraints of the polytope, are simultaneously satisfied. Several other ideas are also needed, such as finding a point in the interior of the minimum weight face of this polytope and finding a balanced tight odd set in NC.

We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar’s effect handlers, Filinski’s monadic reflection, and delimited control. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.

We present each notion as an extension of a simply-typed core lambda-calculus with an effect type system. Using Felleisen’s notion of a macro translation, we show that these abstractions can macro-express each other, providing we disregard types. Alas, not all of the translations are type-preserving; moreover, no alternative type-preserving macro translations exist. We show that if we add suitable notions of polymorphism to the core calculus and its extensions then all of the translations can be adapted to preserve typing.

(based on joint work with Yannick Forster, Ohad Kammar, and Matija Pretnar)

Automated invariant generation is a fundamental challenge in program analysis and verification, going back many decades, and remains a topic of active research. In this talk I'll present a select overview and survey of work on this problem, and discuss unexpected connections to other fields including algebraic geometry, group theory, and quantum computing. (No previous knowledge of these fields will be assumed.) This is joint work with Ehud Hrushovski, Amaury Pouly, and James Worrell.

The ongoing trend to more heterogeneity forces us to rethink the design of systems. In this talk, I will present a new system design that considers heterogeneous compute units (general-purpose cores with different instruction sets, DSPs, FPGAs, fixed-function accelerators, etc.) from the beginning instead of as an afterthought. The goal is to treat all compute units (CUs) as first-class citizens, enabling 1) isolation and secure communication between all types of CUs, 2) a direct interaction of all CUs to remove the conventional CPU from the critical path, and 3) access to OS services such as file systems and network stacks for all CUs. To study this system design, I am using a hardware/software co-design based on two key ideas: 1) introduce a new hardware component next to each CU used by the OS as the CUs' common interface and 2) let the OS kernel control applications remotely from a different CU. In my talk, I will show how this approach allows to support arbitrary CUs as aforementioned first-class citizens, ranging from fixed-function accelerators to complex general-purpose cores.

We are developing methods to improve human learning and performance on challenging perceptual categorization tasks, e.g., bird species identification, diagnostic dermatology. Our approach involves inferring psychological embeddings -- internal representations that individuals use to reason about a domain. Using predictive cognitive models that operate on an embedding, we perform surrogate-based optimization to determine efficient and effective means of training domain novices as well as amplifying an individual's capabilities at any stage of training. Our cognitive models leverage psychological theories of: similarity judgement and generalization, contextual and sequential effects in choice, attention shifts among embedding dimensions.  Rather than searching over all possible training policies, we focus our search on policy spaces motivated by the training literature, including manipulation of exemplar difficulty and the sequencing of category labels. We show that our models predict human behavior not only in the aggregate but at the level of individual learners and individual exemplars, and preliminary experiments show the benefits of surrogate-based optimization on learning and perform ance.

This work was performed in close collaboration with Brett Roads at University College London.

Next to performance, early power and energy estimation is a key challenge in the design of computer systems. Traditional simulation-based methods are often too slow while existing analytical models are often not sufficiently accurate. In this talk, I will present our work on bridging this gap by providing fast yet accurate alternatives for power and performance modeling of software and hardware. In the past, we have pioneered so-called source-level and host-compiled simulation techniques that are based on back-annotation of source code with semi-analytically estimated target metrics. More recently, we have studied alternative approaches in which we employ advanced machine learning techniques to synthesize analytical proxy models that can extract latent correlations and accurately predict time-varying power and performance of an application running on a target platform purely from data obtained while executing the application natively on a completely different host machine. We have developed such learning-based approaches for both hardware and software. On the hardware side, learning-based models for white-box and black-box hardware accelerators reach simulation speeds of 1 Mcycles/s at 97% accuracy. On the software side, depending on the granularity at which prediction is performed, cross-platform prediction can achieve more than 95% accuracy at more than 3 GIPS ofequivalent simulation throughput.

One of the fundamental NP-hard problems in combinatorial optimization is Bin Packing. In terms of the best polynomial time approximation algorithm, we show how to improve over the previous best algorithm by Karmarkar and Karp from 1981 by a quadratic factor. The crucial techniques come from recent developments in discrepancy theory, a sub-field of combinatorics.

Then we will consider the special case that the number of different item sizes is a constant. It had been open for at least 15 years, whether or not this case is solvable in polynomial time. We provide an affirmative answer to that.

The talk includes joint work with Michel X. Goemans and Rebecca Hoberg.

As software systems, especially those based on machine learning and data analysis, become ever more deeply engrained in modern society and take on increasingly powerful roles in shaping people's lives, concerns have been raised about the fairness, equity, and other embedded values of these systems. Many definitions of "fairness" have been proposed, and the technical definitions capture a variety of desirable statistical invariants. However, such invariants may not address fairness for all stakeholders, may be in tension with each other or other desirable properties, and may not be recognized by people as capturing the correct notion of fairness. In addition, requirements that serve fairness, in practice, often are enacted by prohibiting a set of practices considered unfair rather than fully modeling a particular definition of fairness.

For these reasons, we attack the goal of producing fair systems from a different starting point. We argue that a focus on accountability and transparency in the design of a computer system is a stronger basis for reasoning about fairness. We outline a research agenda in responsible system design based on this approach, attacking both technical and non-technical open questions. Technology can help realize human values - including fairness - in computer systems, but only if it is supported by appropriate organizational best practices and a new approach to the system design life cycle.

As a first step toward realizing this agenda, we present a cryptographic protocol for accountable algorithms, which uses a combination of commitments and zero-knowledge proofs to construct audit logs for automated decision-making systems that are publicly verifiable for integrity. Such logs comprise an integral record of the behavior of a computer system, providing evidence for future interrogation, oversight, and review while also providing immediate public assurance of important procedural regularity properties, such as the guarantee that all decisions were made under the same policy. Further, the existence of such evidence provides a strong incentive for the system's designers to capture the right human values by making deviations from those values apparent and undeniable. Finally, we describe how such logs can be extended to demonstrate the existence of key fairness and transparency properties in machine-learning settings. For example, we consider how to demonstrate that a model was trained on particular data, that it operates without considering particular sensitive inputs, or that it satisfies particular fairness invariants of the type considered in the machine-learning fairness literature. This approach leads to a better, more complete, and more flexible outcome from the perspective of preventing unfairness.

Serious concerns have been raised about the role of `socialbots' in manipulating public opinion and influencing the outcome of elections by retweeting partisan content to increase its reach. Here we analyze the role and influence of socialbots on Twitter by determining how they contribute to retweet diffusions. We collect a large dataset of tweets during the 1st U.S. presidential debate in 2016 and we analyze its 1.5 million users from three perspectives: user influence, political behavior (partisanship and engagement) and botness. First, we define a measure of user influence based on the user's active contributions to information diffusions, i.e. their tweets and retweets. Given that Twitter does not expose the retweet structure -- it associates all retweets with the original tweet -- we model the latent diffusion structure using only tweet time and user features, and we implement a scalable novel approach to estimate influence over all possible unfoldings. Next, we use partisan hashtag analysis to quantify user political polarization and engagement. Finally, we use the BotOrNot API to measure user botness (the likelihood of being a bot). We build a two-dimensional "polarization map" that allows for a nuanced analysis of the interplay between botness, partisanship and influence. We find that not only are socialbots more active on Twitter -- starting more retweet cascades and retweeting more -- but they are 2.5 times more influential than humans, and more politically engaged. Moreover, pro-Republican bots are both more influential and more politically engaged than their pro-Democrat counterparts. However we caution against blanket statements that software designed to appear human dominates politics-related activity on Twitter. Firstly, it is known that accounts controlled by teams of humans (e.g. organizational accounts) are often identified as bots. Secondly, we find that many highly influential Twitter users are in fact pro-Democrat and that most pro-Republican users are mid-influential and likely to be human (low botness).

To create a truly sustainable world, we need to generate ample resources and allocate them appropriately.  In traditional economics, these goals are achieved using money.  However, in many settings of particular social significance, monetary transactions are infeasible, be it due to ethical considerations or technological constraints.  In this talk, we will discuss alternatives to money, including risk, social status, and scarcity, and show how to use them to achieve socially-optimal outcomes.  Risk helps determine a person's value for a resource: the more someone is willing to risk for something, the more they value it.  Using this insight, we propose an algorithm to find a good assignment of students in school choice programs.  Social status helps motivate people to contribute to a public project.  Using this insight, we design badges to maximize contributions to user-generated content websites.  Scarcity forces people to evaluate trade-offs, allowing algorithms to infer the relative strength of their preference for different options.  Using this insight, we design voting schemes that select the most highly-valued alternative.

We tackle the problem of deciding whether two probabilistic programs are equivalent in the context of Probabilistic NetKAT, a formal language for reasoning about the behavior of packet-switched networks. The main challenge lies in reasoning about iteration, which we address by a reduction to finite-state absorbing Markov chains. Building on this approach, we develop an effective decision procedure based on stochastic matrices. Through an extended case study with a real-world data center network, we show how to use these techniques to automatically verify various properties of interests, including resilience in the presence of failures. This is joint work with Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, and Dexter Kozen.

What are the odds that you will get hacked tomorrow? To answer this question, it is not enough to reason about the state of your host -- we must also understand how easy it is for adversaries to exploit software vulnerabilities and what helps them distribute malware around the world. Moreover, the machine learning techniques that drive the success of such prediction tasks in non-adversarial domains, like computer vision or autonomous driving, face new challenges in security. 

In this talk I will discuss my work, combining machine learning with global-scale measurements, that has exposed critical security threats and has guided industrial practices. First, I will present the Worldwide Intelligence Network Environment (WINE), an analytics platform that has enabled systematic security measurements across more than 10 million hosts from around the world. Second, I will use WINE as a vehicle for exploring open research questions, such as the duration and impact of zero-day attacks, the weaknesses in public key infrastructures (PKIs) that allow malware to masquerade as reputable software, and how we can use machine learning to predict certain security incidents. I will conclude by discussing the impact of these predictions on the emerging cyber insurance industry and the lessons we learned about using machine learning in the security domain.

I will speak about an unexpected correspondence between a beautiful theory, due to Lovasz, about homomorphisms and graph limits and a popular heuristic for the graph isomorphism problem known as the Weisfeiler-Leman algorithm. I will also relate this to graph kernels in machine learning. Indeed, the context of this work is to desgin and understand similarity measures between graphs and discrete structures.

The popularity of wearable and mobile devices, including smartphones and smartwatches, has generated an explosion of detailed behavioral data. These massive digital traces provide us with an unparalleled opportunity to realize new types of scientific approaches that provide novel insights about our lives, health, and happiness. However, gaining valuable insights from these data requires new computational approaches that turn observational, scientifically "weak" data into strong scientific results and can computationally test domain theories at scale. In this talk, I will describe novel computational methods that leverage digital activity traces at the scale of billions of actions taken by millions of people. These methods combine insights from data mining, social network analysis, and natural language processing to generate actionable insights about our physical and mental well-being. Specifically, I will describe how massive digital activity traces reveal unknown health inequality around the world, and how personalized predictive models can target personalized interventions to combat this inequality. I will demonstrate that modelling how fast we are using search engines enables new types of insights into sleep and cognitive performance. Further, I will describe how natural language processing methods can help improve counseling services for millions of people in crisis. I will conclude the talk by sketching interesting future directions for computational approaches that leverage digital activity traces to better understand and improve human well-being.

There is growing recognition that machine learning (ML) exposes new security and privacy vulnerabilities in software systems, yet the technical community's understanding of the nature and extent of these vulnerabilities remains limited but expanding. In this talk, I explore the threat model space of ML algorithms, and systematically explore the vulnerabilities resulting from the poor generalization of ML models when they are presented with inputs manipulated by adversaries. This characterization of the threat space prompts an investigation of defenses that exploit the lack of reliable confidence estimates for predictions made. In particular, we introduce a promising new approach to defensive measures tailored to the structure of deep learning. Through this research, we expose connections between the resilience of ML to adversaries, model interpretability, and training data privacy.

The datacenters behind popular cloud services are extremely resource-dense. A typical deployment has thousands of cores, terabytes of memory, gigabits of bandwidth, and petabytes of storage available per-rack. Datacenter economics require that providers share these resources across multiple customers for efficient utilization and as a means of providing price-competitive offerings. Shared infrastructure, however, risks cross-client interference and can result in degraded performance or data leaks, leading to outages and breaches. My work explores this tension with systems that provide security and performance isolation on shared hardware, while enabling efficient utilization and preserving the underlying performance of the devices.

This talk describes two such systems dealing with different resources: the first, Plastic, transparently mitigates poor scalability on multi-core systems caused by insufficient cache line isolation, which results in unnecessary memory contention and wasted compute cycles. Another one, Decibel, provides isolation in shared non-volatile storage and allows clients to remotely access high-speed devices at latencies comparable to local devices while guaranteeing throughput, even in the face of competing workloads.

As we rely more and more on computer software for automating processes and making decisions, the range of software that is considered critical goes well beyond the avionics and nuclear power industries: nowadays software plays an increasingly important role in convicting criminals, trading on the financial markets, autonomously driving cars, and performing medical diagnoses, to name a few applications. It is now paramount to ensure the reliability and security of such software, and expectations about software fairness and transparency are rapidly rising. To meet these needs, we need new mathematical models of software behavior that capture the aspects relevant for a particular dependability property, and new algorithmic approaches to effectively navigate this mathematical space and decide whether the software behaves as desired. This talk gives an overview of the steps I have taken towards addressing these challenges. Starting from a series of works on deciding software termination, I show that the insights from this domain are transferable to other formal methods and properties. These results pave the way for a unified framework for deciding increasingly advanced software dependability properties. I discuss the first results that I obtained in this more general direction, which in particular bring new conceptual clarity to the synergies with deciding security properties of software. Finally, I conclude with an outlook to the future and discuss the potential impact of this research on our personal, civic, and economic life.

Recent years have seen a rise in distributed systems for interactive, large-scale data processing. Cutting-edge systems focus on reducing latency and increasing expressiveness in order to provide an interactive and rich experience to more and varied users coming from emerging fields such as data science. Meanwhile, the languages and runtimes underlying such systems face numerous challenges in the context of the severely demanding needs of these new distributed systems; popular languages and runtimes like Scala and the JVM (a) limit the customizability of fundamental operations like serialization, and (b) expose low-level distribution-related errors to application developers and end users when trying to distribute core language features, such as functions. This talk presents three systems that (a) give more control over these primitives to distributed systems builders thereby enabling important optimizations, and (b) increase the reliability of distributing functions and objects. Theoretical, experimental, and empirical results are used in the validation of our work.

Distributed systems represent some of the most interesting and successful computing applications in use today, from modern web applications and social networks, to data analytics and large-scale machine learning.  However, it is notoriously difficult to understand, troubleshoot, and enforce distributed systems behaviors, because unlike standalone programs, they lack a central point of visibility and control.  This impacts important tasks like resource management, performance, security, accounting, and more.  In this talk I will outline techniques and abstractions for re-establishing cross-component visibility and control.  I will demonstrate with two cross-cutting tools that I have developed in my research: Retro, which measures resource usage and co-ordinates scheduler parameters to achieve end-to-end performance goals; and Pivot Tracing, which dynamically monitors and correlates metrics across component boundaries.  Together, these tools illustrate some of the common challenges and potential solutions when developing and deploying tools for distributed systems.

A popular approach to automatic program verification is to come up with an abstraction that reflects pertinent properties of the program. This abstraction is drawn from a class of formal models that is amenable to analysis. In the plethora of existing formal models, the aspects of programs that can be represented faithfully are typically determined by the infinite dimension of its state space, its storage mechanism. A central theme of my recent research is to obtain general insights into how the structure of the storage mechanism affects the analysis of a formal model. In the first part of my talk, I will survey results on an overarching framework of storage mechanisms developed in my doctoral work. It encompasses a range of infinite-state models and permits meaningful characterizations of when a particular method of analysis is applicable. Another current focus of my work concerns finite-state abstractions of infinite-state models. On one hand, these can be over- or under-approximations that are more efficient to analyze than infinite-state systems. On the other hand, they can serve as easy-to-check correctness certificates that are produced instead of yes-or-no answers to a verification task. Thus, the second part of my talk will be concerned with results on computing downward closures and related finite-state abstractions.

The widespread access to the Internet and the ubiquity of web-based services make it easy to communicate and interact globally. Unfortunately, the software implementing the functionality of these services is often vulnerable to attacks. In turn, an attacker can exploit them to compromise and abuse the services for nefarious purposes. In my research, I aim to better understand, detect, and prevent these attacks.

In this talk, we first look at detecting website defacements, which can inflict significant harm on a website's owner or operator through the loss of sales, the loss in reputation, or because of legal ramifications. Then, we dive into how to automatically identify malware distribution campaigns, which has become a major challenge in today's Internet. Next, we look at how to mitigate the dangers of domain takeover attacks, which give attackers the same capabilities to spread misinformation or malware as vulnerabilities do, but without the actual need for a vulnerability in the affected service. Last, I will conclude by sketching interesting future directions on how to better understand, detect, and prevent Internet abuse.

TCP is widely used for client-server communication in modern data centers. But TCP packet handling is notoriously CPU intensive, accounting for an increasing fraction of data center processing time. Techniques such as TCP segment offload, kernel bypass, and RDMA are of limited benefit for the typical small, frequent RPCs. These techniques can also compromise protocol agility, resource isolation, overall system reliability, and complicate multi-tenancy.

I propose a unique refactoring of TCP functionality that splits processing between a streamlined fast path for common operations, and an out-of-band slow path. Protocol processing executes in the kernel on dedicated cores that enforce correctness and resource isolation. Applications asynchronously communicate with the kernel through event queues, improving parallelism and cache utilization. I show that my approach can increase RPC throughput by up to 4.1x compared to Linux. The fast-path can be offloaded to a programmable NIC to further improve performance and minimize CPU time for network processing. With hardware offload, data packets are delivered directly from application to application, while the NIC and kernel cooperate to enforce correctness and resource isolation. I show that hardware offload can increase per-core packet throughput by 10.7x compared to the Linux kernel TCP implementation.

A large portion of computation is now carried out in datacenter. A single datacenter hosts several 100s or 1000s of applications which share common compute and network resources in a datacenter. Isolating each application's performance, i.e., ensuring that its performance is predictable regardless of the behavior of other applications is essential to developing and deploying data center applications, since otherwise developers need to account for co-located applications, which increases development and deployment complexity. Despite its importance current approaches to performance isolation are incomplete, and focus mostly on isolating computational resources. In this talk I present two schemes for isolation network performance. The first, Silo, takes a resource allocation based approach and implements mechanisms for guaranteeing an application's network latency and throughput. The second, Express Pass, takes a congestion control based approach and fairly partitions network resources across applications.  Both approaches require no hardware (ASIC) changes, and can be deployed in today's datacenter. This shows that full application performance isolation is achievable today.

Whether or not a distributed optimization problem, such as MST, shortest path, or min-cut, can be solved fast in a given network depends in a highly non-trivial manner on the network's topology. While there are pathological worst-case n-node topologies on which any of these optimization problems require Omega(sqrt(n)) rounds to compute, despite a small diameter D, most networks allow for fast O(D polylog n) round distributed algorithms. This talk will introduce the low-congestion shortcuts framework which allows to study these dependencies and makes it easy to design algorithms that, on networks of interest, are provably fast and often near instance optimal.

This is joint work with Mohsen Ghaffari, Goran Zuzic, Taisuke Izumi, Ellis Hershkowitz, David Wajc, and Jason Li.

Formal verification has been gaining the attention and resources of both the academic and the industrial world since it prevents critical software bugs that cost money, energy, time, and even lives. Yet, software development and formal verification are decoupled, requiring verification experts to prove properties of a template – instead of the actual – implementation ported into verification specific languages. My goal is to bridge formal verification and software development for the programming language Haskell. Haskell is a unique programming language in that it is a general purpose, functional language used for industrial development, but simultaneously it stands at the leading edge of research and teaching welcoming new, experimental, yet useful features.

In this talk I am presenting Liquid Haskell, a refinement type checker in which formal specifications are expressed as a combination of Haskell’s types and expressions and are automatically checked against real Haskell code. This natural integration of specifications in the language, combined with automatic checking, established Liquid Haskell as a usable verifier, enthusiastically accepted by both industrial and academic Haskell users. Recently, I turned Liquid Haskell into a theorem prover, in which arbitrary theorems about Haskell functions would be proved within the language. As a consequence, Liquid Haskell can be used in Haskell courses to teach the principles of mechanized theorem proving.   

Turning a general purpose language into a theorem prover opens up new research questions – e.g., can theorems be used for runtime optimizations of existing real-world applications? – that I plan to explore in the future.

In the era of Big Data, datacenter and cloud architectures decouple compute and storage resources from each other for better scalability. While this design choice enables elastic scale-out, it also causes unnecessary data movements. One solution is to push parts of the computation down to storage where data can be filtered more efficiently. Systems that do this are already in use and rely either on regular server machines as storage nodes or on network attached storage devices. Even though the former provide complex computation and rich functionality since there are plenty of conventional cores available to run the offloaded computation, this solution is quite inefficient because of the over-provisioning of computing capacity and the bandwidth mismatches between storage, CPU, and network.  Networked storage devices, on the other hand, are better balanced in terms of bandwidth but at the price of offering very limited options for offloading data processing.

With Caribou, we explore an alternative design that offers rich offloading functionality while matching the available line-rate processing performance of either storage or network. It also does this in a much more efficient package (size, energy consumption) than regular servers. Our FPGA-based prototype system has been designed such that the internal data management logic can saturate the network for most operation mixes, without being over-provisioned. As a result, it can extract and process data from storage at multi-GB/s rate before sending it to the computing nodes, while at the same time offering features such as replication for fault-tolerance.

Caribou has been released as open source. Its modular design and extensible processing pipeline make it a convenient platform for exploring domain-specific processing inside storage nodes.

Formal reasoning about computational complexity turns out to be quite cumbersome as it often requires to manipulate explicit time bounds for a specific machine model. Implicit Computational Complexity is a research area which provides techniques and complexity classes characterisations to avoid this. We have formally verified the soundness (and part of the completeness) of such a technique − called quasi-interpretations − using the Coq proof assistant. In particular, we turned this into a tool to help guarantee the polynomial complexity of programs (here, term rewriting systems).

An educational program of study can be viewed as a knowledge graph consisting of learning units and relationships between them. Such a knowledge graph provides the core data structure for organizing and navigating learning experiences. We address three issues in this talk. First, how can we synthesize the knowledge graph, given a set of concepts to be covered in the study program. Next, how can we use data mining to identify and correct deficiencies in a knowledge graph. Finally, how can we use data mining to form study groups with the goal of maximizing overall learning. We conclude by pointing out some open research problems.

Static verification techniques are used to analyse and prove properties about programs before they are deployed. In particular, deductive verification techniques often work directly on the source code and are used to verify data-oriented properties of all possible executions. In contrast, runtime verification techniques have been extensively used for control-oriented properties, and analyse concrete executions that occur in the deployed program. I present an approach in which data-oriented and control-oriented properties may be stated in a single formalism amenable to both static and dynamic verification techniques. The specification language enhances a control-oriented property language with data-oriented pre/postconditions. We show how such specifications can be analysed using a combination of the deductive verification system KeY and the runtime verification tool LARVA. Verification is performed in two steps: KeY performs fully automated proof attempts, the resulting partial proofs are analysed, and used to optimize the specification for efficient runtime checking.

Complex statistical models are increasingly being used or considered for use in high-stakes decision-making pipelines in domains such as financial services, health care, criminal justice and human services. These models are often investigated as possible improvements over more classical tools such as regression models or human judgement. While the modeling approach may be new, the practice of using some form of risk assessment to inform decisions is not. When determining whether a new model should be adopted, it is essential to be able to compare the proposed model to the existing approach across a range of task-relevant accuracy and fairness metrics. In this talk I will describe a subgroup analysis approach for characterizing how models differ in terms of fairness-related quantities such as racial or gender disparities. I will also talk about an ongoing collaboration with the Allegheny County Department of Health and Human Services on developing and implementing a risk assessment tool for use in child welfare referral screening.

https://arxiv.org/abs/1707.00046

http://www.post-gazette.com/local/region/2017/04/09/Allegheny-County-using-algor ithm-to-assist-in-child-welfare-screening/stories/201701290002

Much of the policy and legal debate about algorithmic decision-making has focused on issues of accuracy and bias. Equally important, however, is the question of whether algorithmic decisions are understandable by human observers: whether the relationship between algorithmic inputs and outputs can be explained. Explanation has long been deemed a crucial aspect of accountability, particularly in legal contexts. By requiring that powerful actors explain the bases of their decisions — the logic goes — we reduce the risks of error, abuse, and arbitrariness, thus producing more socially desirable decisions. Decision-making processes employing machine learning algorithms complicate this equation. Such approaches promise to refine and improve the accuracy and efficiency of decision-making processes, but the logic and rationale behind each decision often remains opaque to human understanding. Indeed, at a technical level, it is not clear that all algorithms can be made explainable and, at a normative level, it is an open question when and if the costs of making algorithms explainable outweigh the benefits. This presentation will begin to map out some of the issues that must be addressed in determining in what contexts, and under what constraints, machine learning approaches to governmental decision-making are appropriate.

Two-thirds of all American adults access the news through social media. But social networks and social media recommendations lead to information bubbles, and personalization and recommendations, by maximizing the click-through rate, lead to ideological polarization. Consequently, rumors, false news, conspiracy theories, and now even fake news sites are an increasingly worrisome phenomena. While media organizations (Snopes.com, PolitiFact, FactCheck.org, et al.) have stepped up their efforts to verify news, political scientists tell us that fact-checking efforts may be ineffective or even counterproductive. To address some of these challenges, researchers at Indiana University are working on an open platform for the automatic tracking of both online fake news and fact-checking on social media. The goal of the platform, named Hoaxy, is to reconstruct the diffusion networks induced by hoaxes and their corrections as they are shared online and spread from person to person.

This talk will introduce synchronization strings, which provide a novel way to efficiently deal with synchronization errors, i.e., insertions and deletions. Synchronization errors are strictly more general and much harder to cope with than more commonly considered Hamming errors, i.e., symbol corruptions and erasures. For every eps > 0, synchronization strings allow to index a sequence with an eps^{-O(1)} size alphabet such that one can efficiently transform k synchronization errors into (1 + eps) k Hamming errors. This powerful new technique has many applications. This talk will focus on designing insdel codes, i.e., error correcting block codes (ECCs) for insertion deletion channels.

While ECCs for both half-errors and synchronization errors have been intensely studied, the later has largely resisted progress. As Mitzenmacher puts it in his 2009 survey: "Channels with synchronization errors . . . are simply not adequately understood by current theory. Given the near-complete knowledge we have for channels with erasures and errors ... our lack of under- standing about channels with synchronization errors is truly remarkable."

A straight forward application of our synchronization strings based indexing method gives a simple black-box construction which transforms any ECC into an equally efficient insdel code with only a small increase in the alphabet size. This instantly transfers much of the highly developed understanding for regular ECCs into the realm of insdel codes. Most notably, for the complete noise spectrum we obtain efficient insdel codes which get arbitrarily close to the optimal rate-distance tradeoff, i.e., for any delta < 1 and eps > 0 we give insdel codes achieving a rate of 1 - delta that efficiently correct a delta - eps fraction of insertions or deletions.

This is joint work with Amirbehshad Shahrasbi.

Social media has brought a revolution on how people get exposed to information and how they are consuming news. Beyond the undoubtedly large number of advantages and capabilities brought by social-media platforms, a point of criticism has been the creation of filter bubbles or echo chambers, caused by social homophily as well as by algorithmic personalisation and recommendation in content delivery. In this talk, I will present the methods we developed to (i) detect and quantify the existence of polarization on social media, (ii) monitor the evolution of polarisation over time, and finally, (iii) devise methods to overcome the effects caused by increased polarization. We build on top of existing studies and ideas from social science with principles from graph theory to design algorithms which are language independent, domain agnostic and scalable to large number of users.

We define a syntactic monadic translation of type theory, called the weaning translation, that allows for a large range of effects in dependent type theory, such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions with a restricted version of dependent elimination, dubbed Baclofen Type Theory, which we conjecture is the proper generic way to mix effects and dependence. This provides the first effectful version of CIC, which can be implemented as a Coq plugin.

Due to modern computer and data technology, we can today collect, store, process, and share more data than every before. This data revolution opens fundamentally new ways to think about the classical concept of feedback control as a basis for building future (artificial) intelligent systems, which interact with the physical world. In this talk, I will provide an overview of our recent research on intelligent control systems, which leverages machine learning and modern communication networks for control. I will present algorithms that enable systems to (i) autonomously learn from data, (ii) interconnect in cooperative networks, and (iii) use their resources efficiently. Throughout the talk, the developed algorithms and theory are highlighted with experiments on humanoid robots and a self-balancing dynamic sculpture.

The nonnegative rank of a nonnegative m x n matrix M is the smallest number d such that M can be written as the product M = WH of a nonnegative m x d matrix W and a nonnegative d x n matrix H.  The notions of nonnegative rank and nonnegative matrix factorization have a wide variety of applications, including bioinformatics, computer vision, communication complexity, document clustering, and recommender systems. A longstanding open problem is whether, when M is a rational matrix, the factors W and H in a rank decomposition M=WH can always be chosen to be rational.  In this talk we resolve this problem negatively and discuss consequences of this result for the computational complexity of computing nonnegative rank.

This is joint work with Dmitry Chistikov, Stefan Kiefer, Ines Marusic, and Mahsa Shirmohammadi.

Moore's Law may be slowing, but, perhaps as a result, other measures of processor complexity are only accelerating. In recent years, Intel's architects have turned to an alphabet soup of instruction set extensions such as MPX, SGX, MPK, and CET as a way to sell CPUs through new security features. SGX in particular promises powerful security: user-mode "enclaves" protected against both physical attacks and privileged software adversaries. To achieve this, SGX's designers implemented an isolation mechanism approaching the complexity of an OS microkernel in the ISA, using an inscrutable mix of silicon and microcode. However, while CPU-based security mechanisms are harder to attack, they are also harder to deploy and update, and already a number of significant flaws have been identified. Worse, the availability of new SGX features is dependent on the slowing deployment of new CPUs.

In this talk, I'll describe an alternative approach to providing SGX-like enclaves: decoupling the underlying hardware mechanisms such as memory encryption, address-space isolation and attestation from a privileged software monitor which implements enclaves. The monitor's trustworthiness is guaranteed by a machine-checked proof of both functional correctness and high-level security properties. The ultimate goal is to achieve security that is equivalent or better than SGX while decoupling enclave features from the underlying hardware.

Web deep links are instrumental to many fundamental user experiences such as navigating to one web page from another, bookmarking a page, or sharing it with others. Such experiences are not possible with individual pages inside mobile apps, since historically mobile apps did not have links equivalent to web deep links. Mobile deep links, introduced in recent years, still lack many important properties of web deep links. Unlike web links, mobile deep links must be explicitly built into apps by developers, cover a small number of predefined pages, and are defined statically to navigate to a page for a given link, but not to dynamically generate a link for a given page. Another problem with state-of-the-art deep links is that, once exposed, they are hard to discover, thus limiting their usage in both first and third-party experiences.

In this talk, I'll give an overview of two new deep linking mechanisms that address these problems. First, we implemented an application library that transparently tracks data- and UI-event-dependencies of app pages and encodes the information in links to the pages; when a link is invoked, the information is utilized to recreate the target page quickly and accurately. Second, using static and dynamic analysis we prototyped a tool that can automatically discover links that are exposed by an app; in addition, it can discover many links that are not explicitly exposed. The goal is to obtain links to every page in an app automatically and precisely.

In this talk I will present my research in developing local reasoning techniques in both concurrent and sequential settings.

On the concurrency side, I’ll present my work on the program logic of CoLoSL (Concurrent Local Subjective Logic) and its application to various fine-grained concurrent algorithms. A key difficulty in verifying concurrent programs is reasoning compositionally about each thread in isolation. CoLoSL is the first program logic to introduce the general composition and framing of interference relations (describing how shared resources may be manipulated by each thread) in the spirit of resource composition and framing in separation logic. This in turn enables local reasoning and allows for more concise specifications and proofs.

I will then present preliminary work on extending CoLoSL to reason about distributed database applications running under the snapshot isolation (SI) consistency model. SI is a commonly used consistency model for transaction processing, implemented by most distributed databases. The existing work focuses on the SI semantics and verification techniques for client-side applications remain unexplored. To fill this gap, I look into extending CoLoSL towards a program logic for client-side reasoning under SI.

On the sequential side, I’ll briefly discuss my work on specification and verification of web programs. My research in this area include: a compositional specification of the DOM (Document Object Model) library in separation logic; integrating this DOM specification with the JaVerT (JavaScript Verification Toolchain) framework for automated DOM/JavaScript client verification; as well as ongoing work towards extending JaVerT to reason about higher-order JavaScript programs.

Flight critical subsystems in aerospace vehicles must achieve probability of failure rates of less than 1 failure in 10^9 flight hours (i.e. less than 1 failure per 100,000 years of operation).  Systems that achieve this level of reliability are hard to design, hard to verify, and hard to validate, especially if software is involved.  In this talk, I will talk about some of the challenges that the aerospace community faces in designing systems with this level of reliability and how tools from formal methods and control theory might help.  I will also describe some of the my group’s work in synthesis of reactive protocols for hybrid systems and its applications to design of safety critical systems.

Configuration errors are among the dominant causes of service-wide, catastrophic failures in today's cloud and datacenter systems. Despite the wide adoption of fault-tolerance and recovery techniques, these large-scale software systems still fail to effectively deal with configuration errors. In fact, even tolerance/recovery mechanisms are often misconfigured and thus crippled in reality.

In this talk, I will present our research efforts towards hardening cloud and datacenter systems against configuration errors. I will start with work that seeks for understanding the fundamental causes of misconfigurations. I will then focus on two of my approaches, PCheck and Spex, that enable software systems to anticipate and defend against configuration errors. PCheck generates checking code to help systems detect configuration errors early, and Spex exposes bad system reactions to configuration errors based on constraints inferred from source code.

Modern networks do far more than  just deliver packets, and provide network functions -- including  firewalls, caches, and WAN optimizers — that are crucial for scaling networks, ensuring security and enabling new applications. Network functions were traditionally implemented using dedicated hardware middleboxes, but in recent years they are increasingly being deployed as VMs on commodity servers. While many herald this move towards network function virtualization (NFV) as a great step forward, I argue that accepted virtualization techniques are ill-suited to network functions. In this talk I describe NetBricks — a new approach to building and running virtualized network functions that speeds development and increases performance. I end the talk by discussing the implications of being able to easily create and insert new network functions. 

We first present an approach for analyzing the event time series, namely, the times of event occurrences. Interestingly, the event time series appears in various fields, including neuroscience (action potentials of a neuron), social media analysis (Twitter, Facebook), and so on. Then, we develop a framework for forecastingretweet activity through the analysis of Twitter dataset(Kobayashi & Lambiotte, ICWSM, 2016). This work is joint work with Renaud Lambiotte.

Current cloud services are vulnerable to hacks and surveillance programs that undermine user privacy and personal liberties. In this talk, I present how we can build practical systems for protecting user privacy from powerful persistent threats. I will discuss Talek, a private publish-subscribe protocol. With Talek, application developers can send and synchronize data through the cloud without revealing any information about data contents or communication patterns of application users. The protocol is designed with provable security guarantees and practical performance, 3-4 orders of magnitude better throughput than other systems with comparable security goals. I will also discuss Radiatus, a security-focused web framework to protect web apps against external intrusions, and uProxy, a Internet censorship circumvention tool in deployment today.

Algorithms and formal verification are two classical areas of computer science. The two fields apply rigorous mathematical proof to seemingly disparate ends---on the one hand, analyzing computational efficiency of algorithms; on the other, designing techniques to mechanically show that programs are correct.

In this talk, I will present a surprising confluence of ideas from these two areas. First, I will show how coupling proofs, used to analyze random walks and Markov chains, correspond to proofs in the program logic pRHL (probabilistic Relational Hoare Logic). This connection enables formal verification of novel probabilistic properties, and provides an structured understanding of proofs by coupling. Then, I will show how an approximate version of pRHL, called apRHL, points to a new, approximate version of couplings closely related to differential privacy. The corresponding proof technique---proof by approximate coupling---enables cleaner proofs of differential privacy, both for humans and for formal verification. Finally, I will share some directions towards a possible "Theory AB", blending ideas from both worlds.

Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications, including network reliability, privacy, probabilistic reasoning, and constrained-random verification. In constrained counting, the task is to compute the total weight, subject to a given weighting function, of the set of solutions of the given constraints. In constrained sampling, the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. In this talk, I will introduce a novel algorithmic framework for constrained sampling and counting that combines the classical algorithmic technique of universal hashing with the dramatic progress made in Boolean reasoning over the past two decades. This has allowed us to obtain breakthrough results in constrained sampling and counting, providing a new algorithmic toolbox in machine learning, probabilistic reasoning, privacy, and design verification. I will demonstrate the utility of the above techniques on various real applications including probabilistic inference, design verification and our ongoing collaboration in estimating the reliability of critical infrastructure networks during natural disasters.

Bayesian methods are frequently used for analysing privacy-sensitive datasets, including medical records, emails, and educational data, and there is a growing need for practical Bayesian inference algorithms that protect the privacy of individuals' data. To this end, we provide a general framework for privacy-preserving variational Bayes (VB) for a large class of probabilistic models, called the conjugate exponential (CE) family. Our primary observation is that when models are in the CE family, we can privatise the variational posterior distributions simply by perturbing the expected sufficient statistics of the complete-data likelihood. For widely used non-CE models with binomial likelihoods (e.g., logistic regression), we exploit the Polya-Gamma data augmentation scheme to bring such models into the CE family, such that inferences in the modified model resemble the original (private) variational Bayes algorithm as closely as possible. The iterative nature of variational Bayes presents a further challenge for privacy preservation, as each iteration increases the amount of noise needed. We overcome this challenge by combining: (1) a relaxed notion of differential privacy, called concentrated differential privacy, which provides a tight bound on the privacy cost of multiple VB iterations and thus significantly decreases the amount of additive noise; and (2) the privacy amplification effect of subsampling mini-batches from large-scale data in stochastic learning. We empirically demonstrate the effectiveness of our method in CE and non-CE models including latent Dirichlet allocation (LDA), Bayesian logistic regression, and Sigmoid Belief Networks (SBNs), evaluated on real-world datasets. >

People are becoming an integral part of computational systems, fueled primarily by recent technological advancements as well as deep-seated economic and societal changes. Consequently, there is a pressing need to design new data science and machine learning frameworks that can tackle challenges arising from human participation (e.g. questions about incentives and users’ privacy) and can leverage people’s capabilities (e.g. ability to learn).

In this talk, I will share my research efforts at the confluence of people and computing to address real-world problems. Specifically, I will focus on collaborative consumption systems (e.g. shared mobility systems and sharing economy marketplaces like Airbnb) and showcase the need to actively engage users for shaping the demand who would otherwise act primarily in their own interest. The main idea of engaging users is to incentivize them to switch to alternate choices that would improve the system’s effectiveness. To offer optimized incentives, I will present novel multi-armed bandit algorithms and online learning methods in structured spaces for learning users’ costs for switching between different pairs of available choices. Furthermore, to tackle the challenges of data sparsity and to speed up learning, I will introduce hemimetrics as a structural constraint over users’ preferences. I will show experimental results of applying the proposed algorithms on two real-world applications: incentivizing users to explore unreviewed hosts on services like Airbnb and tackling the imbalance problem in bike sharing systems. In collaboration with an ETH Zurich spinoff and a public transport operator in the city of Mainz, Germany, we deployed these algorithms via a smartphone app among users of a bike sharing system. I will share the findings from this deployment.

The CakeML project has recently produced a verified compiler which we believe to be the most realistic verified compiler for a functional programming language to date. In this talk I'll give an overview of the CakeML project with focus on the new compiler, in particular how the compiler is structured, how the intermediate languages are designed and how the proofs are carried out. The talk will stay at a fairly high-level, but I am happy to dive into details for any of the parts that I know well.

The CakeML project is currently a collaboration between six sites across three continents. The new compiler is due to: Anthony Fox (Cambridge, UK), Ramana Kumar (Data61, Sydney Australia), Magnus Myreen (Chalmers, Sweden), Michael Norrish (Data61, Canberra Australia), Scott Owens (Kent, UK), and Yong Kiam Tan (CMU, USA).

There has been an uptrend in the demand and need for complex Cyber-Physical Systems (CPS), such as self-driving cars, unmanned aerial vehicles (UAVs), and smart manufacturing systems for Industry 4.0. CPS  often need to accurately sense the surrounding environment by using high-bandwidth acoustic, imaging and other types of sensors; and to take coordinated decisions and issue time critical actuation commands. Hence, temporal predictability in sensing, communication, computation, and actuation is a fundamental attribute. Additionally, CPS must operate safely even in spite of software and hardware misbehavior to avoid catastrophic failures. To satisfy the increasing demand for performance, modern computing platforms have substantially increased in complexity; for instance, multi-core systems are now mainstream, and partially re-programmable system-on-chip (SoC) have just entered production. Unfortunately, extensive and unregulated sharing of hardware resources directly undermines the ability of guaranteeing strong temporal determinism in modern computing platforms. Novel software architectures are needed to restore temporal correctness of complex CPS when using these platforms. My research vision is to design and implement software architectures that can serve as a reference for the development of high-performance CPS, and that embody two main requirements: temporal predictability and robustness. In this talk, I will address the following questions concerning modern multi-core systems: Why application timing can be highly unpredictable? What techniques can be used to enforce safe temporal behaviors on multi-core platforms? I will also illustrate possible approaches for time-aware fault tolerance to maximize CPS functional safety. Finally, I will review the challenges faced by the embedded industry when trying to adopt emerging computing platforms, and I will highlight some novel directions that can be followed to accomplish my research vision.

The emergence of online platforms has brought about a fundamental shift in economic thinking: the design of economic systems is now a problem that computer science can tackle. For the first time we are able to move from the study of economic systems as natural systems to carefully designing and executing them on a computer. Prominent examples of digital market mechanisms include auctions for ads (run by companies such as Google) and electromagnetic spectrum (used by the US government). I will discuss several recent developments in fair division and mechanism design. I will start with a dictatorship theorem for fair division (cake cutting), showing that requiring truthfulness gives rise to a dictator. Afterwards, I will discuss the theme of simplicity and complexity in mechanism design, and more generally the interplay between economics and computation and learning.

The past decade has seen a rapid acceleration in the development of new and transformative applications in many areas including transportation, medicine, finance, and communication. Most of these applications are made possible by the increasing diversity and scale of hardware and software systems.

While this brings unprecedented opportunity, it also increases the probability of failures and the difficulty of diagnosing them. Increased scale and transience has also made management increasingly challenging. Devices can come and go for a variety of reasons including mobility, failure and recovery, and scaling capacity to meet demand.

In this talk, I will be presenting several systems that I built to address the resulting challenges to reliability, management, and security.

Ori is a reliable distributed file system for devices at the network edge. Ori automates many of the tasks of storage reliability and recovery through replication, taking advantage of fast LANs and low cost local storage in edge networks.

Castor is record/replay system for multi-core applications with predictable and consistently low overheads. This makes it practical to leave record/replay on in production systems, to reproduce difficult bugs when they occur, and to support recovering from hardware failures through fault tolerance.

Cryptographic CFI (CCFI) is a dynamic approach to control flow integrity. Unlike previous CFI systems that rely purely on static analysis, CCFI can classify pointers based on dynamic and runtime characteristics. This limits the attacks to only actively used code paths, resulting in a substantially smaller attack surface.

Modern programming languages safeguard developers from many typical errors, yet more subtle errors—such as violations of security policies—still plague software. Program synthesis has the potential to eliminate such errors, by generating executable code from concise and intuitive high-level specifications. Traditionally, program synthesis failed to scale to specifications that encode complex behavioral properties of software: these properties are notoriously hard to check even for a given program, and so it’s not surprising that finding the right program within a large space of candidates has been considered very challenging. My work tackles this challenge through the design of synthesis-friendly program verification mechanisms, which are able to check a large set of candidate programs against a complex specification at once, whereby efficiently pruning the search space.

Based on this principle, I developed Synquid, a program synthesizer that accepts specifications in the form of expressive types and uses a specialized type checker as its underlying verification mechanism. Synquid is the first synthesizer powerful enough to automatically discover provably correct implementations of complex data structure manipulations, such as insertion into Red-Black Trees and AVL Trees, and normal-form transformations on propositional formulas. Each of these programs is synthesized in under a minute. Going beyond textbook algorithms, I created a language called Lifty, which uses type-driven synthesis to automatically rewrite programs that violate information flow policies. In our case study, Lifty was able to enforce all required policies in a prototype conference management system.

The security properties of blockchain technology allow for the shifting of trust assumptions, e.g., to remove trusted third parties; they, however, create new challenges for security and scalability, which have not yet been fully understood and that we investigate in this talk. The blockchain’s security, for example, affects the ability of participants to exchange monetary value or to participate in the network communication and the consensus process. Our first contribution provides a quantitative framework to objectively compare the security and performance characteristics of Proof of Work-based blockchains under adversaries with optimal strategies. Our work allows us to increase Bitcoin’s transaction throughput by a factor of ten, given only one parameter change and without deteriorating the security of the underlying blockchain. In our second contribution, we highlight previously unconsidered impacts of the PoW blockchain’s scalability on its security and propose design modifications that are now implemented in the primary Bitcoin client. Because blockchain technology is still in its infancy, we conclude the talk with an outline of future work towards an open, scalable, privacy-preserving and decentralized blockchain.

Most static program analysis techniques do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties, fail to verify properties, or check properties under certain unsound assumptions, such as the absence of arithmetic overflow. In the first part of the talk, I will present a technique to complement partial verification results by automatic test case generation. In contrast to existing work, our technique supports the common case that the verification results are based on unsound assumptions. We annotate programs to reflect which executions have been verified, and under which assumptions. These annotations are then used to guide dynamic symbolic execution toward unverified program executions, leading to smaller and more effective test suites.

In the second part of the talk, I will describe a new program simplification technique, called program trimming. Program trimming is a program pre-processing step to remove execution paths while retaining equi-safety (that is, the generated program has a bug if and only if the original program has a bug). Since many program analyzers are sensitive to the number of execution paths, program trimming has the potential to improve their effectiveness. I will show that program trimming has a considerable positive impact on the effectiveness of two program analysis techniques, abstract interpretation and dynamic symbolic execution.

Static verification of performance properties of programs is an important problem that has attracted great deal of research. However, most existing tools infer best-effort upper bounds and hope that they match users expectations. In this talk, I will present a system for specifying and verifying bounds on resources such as the number of evaluation steps and heap-allocated objects, for functional Scala programs that may rely on lazy evaluation and memoization. In our system, users can specify the desired resource bound as a template with numerical holes in the contracts of functions e.g. as "steps <= ? * size(list) + ?", along with other functional properties necessary for establishing the bounds. The system automatically infers values for the holes that will make the templates hold for all executions of the functions. For example, the property that a function converting a propositional formula f into negation-normal form (NNF) takes time linear in the size of f can be expressed in the post-condition of the function using the predicate "steps <= ? * size(f) + ?", where size is a user-defined function counting the number of nodes in the syntax tree of the formula. Using our tool, we have verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions and memoization. Our benchmarks include balanced search trees like red-black trees and AVL trees, Okasaki’s constant-time queues, deques, lazy data structures based on numerical representations such as lazy binomial heaps, cyclic streams, and dynamic programming algorithms. Some of the benchmarks have posed serious challenges to automatic as well as manual reasoning. The system is a part of the Leon verifier and can be tried online at "http://leondev.epfl.ch" ("Resource bounds" section).

Static verification of performance properties of programs is an important problem that has attracted great deal of research. However, most existing tools infer best-effort upper bounds and hope that they match users expectations. In this talk, I will present a system for specifying and verifying bounds on resources such as the number of evaluation steps and heap-allocated objects, for functional Scala programs that may rely on lazy evaluation and memoization. In our system, users can specify the desired resource bound as a template with numerical holes in the contracts of functions e.g. as "steps <= ? * size(list) + ?", along with other functional properties necessary for establishing the bounds. The system automatically infers values for the holes that will make the templates hold for all executions of the functions.  For example, the property that a function converting a propositional formula f into negation-normal form (NNF)  takes time linear in the size of f can be expressed in the post-condition of the function using the predicate "steps <= ? * size(f) + ?",  where size is a user-defined function counting the number of nodes in the syntax tree of the formula. Using our tool, we have verified asymptotically precise bounds of several algorithms and data structures that rely on complex sharing of higher-order functions and memoization. Our benchmarks include balanced search trees like red-black trees and AVL trees, Okasaki’s constant-time queues, deques, lazy data structures based on numerical representations such as lazy binomial heaps, cyclic streams, and dynamic programming algorithms. Some of the benchmarks have posed serious challenges to automatic as well as manual reasoning. The system is a part of the Leon verifier and can be tried online at "http://leondev.epfl.ch" ("Resource bounds" section).

References:   (a) Symbolic Resource Bound Inference For Functional Programs. Ravichandhran Madhavan and Viktor Kuncak. Computer Aided Verification, CAV 2014 (b) Contract-based Resource Verification for Higher-order Functions with Memoization. Ravichandhran Madhavan, Sumith Kulal and Viktor Kuncak. To appear in POPL 2017

The energy sector is in the midst of an exciting transition. Driven by new generation technologies and by infrastructure digitalization, the traditional way of transmitting, distributing and using energy is transforming a centralized hierarchical system into a multi-directional open infrastructure. While the vision of Intelligent Energy Networks is appealing and desirable---especially from a sustainability perspective---a number of major challenges remain to be tackled. The loss of centralized control, the intermittent nature of renewable energy sources and the scale of the future digital energy systems are novel situations for power systems infrastructures and consumers that pose reliability and availability threats.

In this talk, I show examples of how Computer Science techniques are having and will have an important role in future energy systems. I focus on electricity as energy vector, and techniques from Service-Oriented Computing and AI Planning. I also present Complex Network theory as a design tool for energy distribution systems. To make things concrete, I will review almost ten years of personal research that include making office buildings energy efficient, homes smarter, and futuristic models for the evolution of power distribution grids to accommodate for multi-directional energy flows with distributed generation and local control.

Attribute-based Encryption(ABE) is a form of asymmetric cryptography that allows encryption over labels named "attributes". In an ABE scheme, an "authority" generates public parameters and secrets and assigns attributes (and associated secrets) to users. Data can be encrypted using formulas over attributes; users can decrypt if they have attribute secrets that satisfy the encryption formula.

In this talk, I will discuss an extension to ABE that allows encryption over attributes provided by multiple authorities. Such a scheme enables secure data sharing between otherwise distrusting organizations. I will discuss example scenarios where multi-authority ABE is useful, and describe one new construction of multi-authority ABE scheme named DMA.

In DMA, a data owner is a first class principal: users in the system get attributes in cooperation with the data owner and various authorities. Compared to previous work, DMA does not require a global identity for users, or require the multiple authorities to trust a single central authority. DMA is also immune to collusion attacks mounted by users and authorities.

The controller synthesis problem for CPS is often reduced to solving omega-regular games with an optional optimization criterion. The criteria commonly used in the literature on omega-regular games are however frequently unsuitable for obtaining high-quality CPS controllers as they are unable to capture many, if not most, real-world optimization objectives. We survey a few such cases and show that such problems can be overcome with more sophisticated optimization criteria. The synthesis problem for them gives rise to ugly games, i.e. games that have complicated definitions but relatively simple solutions.

In this talk, I will show how we can harness the synergy between programming languages and verification methods to help programmers build reliable software, prove complex properties about them, and scale verification to industrial projects. First, I will describe P a domain-specific language to write asynchronous event driven code. P isolates the control-structure, or protocol, from the data-processing. This allows us not only to generate efficient code, but also to test it using model checking techniques. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8 and later versions. The language abstractions and verification helped building a driver which is both reliable and fast. Then, I will introduce PSync a domain specific language for fault-tolerant distributed algorithms that simplifies the implementation of these algorithms enables automated formal verification, and can be executed efficiently. Fault-tolerant algorithms are notoriously difficult to implement correctly, due to asynchronous communication and faults. PSync provides an high-level abstraction by viewing an asynchronous faulty system as synchronous one with an adversarial environment that simulates faults. We have implemented in PSync several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSync against implementations in other languages.

The existing gap between the processor and main memory operating speeds motivated the introduction of intermediate cache memories to accelerate the average access time to instructions and data accessed by programs running on the processor. The introduction of cache memories in modern computing platforms is the cause of important variations in the execution time of each task, depending on whether the instruction and data it requires are already loaded in the cache or not. Many works have focused on analyzing the impact of preemptions on the worst-case execution time (WCET) and worst-case response time (WCRT) of tasks in preemptive systems. Indeed, the preempted tasks may suffer additional cache misses if its memory blocks are evicted from the cache during the execution of preempting tasks. These evictions cause extra accesses to the main memory, which result in additional delays in the task execution. This extra cost is usually referred to as cache-related preemption delays (CRPDs).

Several approaches use information about the tasks' memory access patterns to bound and incorporate preemption costs into the WCRT analysis. These approaches all result in pessimistic WCRT bounds due to the fact that they do not consider the variation in memory demand for successive instances of a same task. They usually assume that the useful cache content for the task is completely erased between two of its executions. However, in actual systems, successive instances of a task may re-use most of the data and instructions that were already loaded in the cache during previous executions. During this talk, we will discuss the concept of persistent cache blocks from a task WCRT perspective, and will present how it can be used to reduce the pessimism of the WCRT analysis for fixed priority preemptive systems. Then, we will introduce techniques exploiting this notion of cache persistence to pre-configure systems so as to improve their runtime behavior.

Laci will report about this breakthrough result on graph isomorphism.

The presentation will be in two parts of 45 minutes each.

The first part will be for a general audience.

This talk will briefly cover the overall research agenda of the MSR Lab in Bangalore. We work in many broad areas that of CS including Algorithms, Crypto, Systems, ML, and ICT4D among others.  The talk will cover three ongoing projects to give you a sense of the breadth of our work: The Trusted Cloud, Green Spaces, and 99DOTS. The goal of the Trusted Cloud project is to explore the challenges of keeping client data stored in the Cloud secure without trusting the Cloud operator, and involves research in the disciplines of computer security, programming languages and verification, and hardware.

The Green Spaces project attempts to understand the implications of using TV spectrum to provide ubiquitous internet access in countries like India or Brazil where, unlike the US, there is plenty of unused spectrum that can be tapped. This project involves both questions in CS research as well as policy issues at the national level on spectrum allocation.

The 99DOTS project address the problem that arises when patients do not adhere to medications as prescribed by the doctors. Such non-adherence has severe health consequences to large population of patients in all parts of the world. 99DOTS proposes a novel solution to ensure medication adherence in a very cost way, and is used by the Indian Government for Tuberculosis in all its treatment centers in the country.

Synthesis, the automatic construction of objects related to hard- and software, is one of the great challenges of computer science. Although synthesis problems are impossible to solve in general, learning-based approaches, in which the synthesis of an object is based on learning from examples, have recently been used to build elegant and extremely effective solutions for a large number of difficult problems. Such examples include automatically fixing bugs, translating programs from one language into another, program verification, as well as the generation of high-level code from given specifications.

This talk gives an introduction to learning-based synthesis. First, we develop a generic view on learning-based synthesis, called abstract learning frameworks for synthesis, which introduces a common terminology to compare and contrast learning-based synthesis techniques found in the literature. Then, we present a learning-based program verifier, which can prove the correctness of numeric programs (nearly) automatically, and show how this technique can be modeled as an abstract learning framework for synthesis. During the talk, we present various examples that highlight the power of the learning-based approach to synthesis.

Machine learning has taken over our world, in more ways than we realize. You might get book recommendations, or an efficient route to your destination, or even a winning strategy for a game of Go. But you might also be admitted to college, granted a loan, or hired for a job based on algorithmically enhanced decision-making. We believe machines are neutral arbiters: cold, calculating entities that always make the right decision, that can see patterns that our human minds can't or won't. But are they? Or is decision-making-by-algorithm a way to amplify, extend and make inscrutable the biases and discrimination that is prevalent in society? To answer these questions, we need to go back — all the way to the original ideas of justice and fairness in society. We also need to go forward — towards a mathematical framework for talking about justice and fairness in machine learning.

Internet crime has become increasingly dependent on the underground economy: a loose federation of specialists selling capabilities, services, and resources explicitly tailored to the abuse ecosystem. Through these emerging markets, modern criminal entrepreneurs piece together dozens of à la carte components into entirely new criminal endeavors. In this talk, I'll discuss parts of this ecosystem and show that criminal reliance on this black market introduces fragile dependencies that, if disrupted, undermine entire operations that as a composite appear intractable to protect against.

Discrepancy theory is widely studied area in combinatorics, and has various applications in computer science to areas such as approximation algorithms, space-time lower bounds, geometric algorithms, numerical integration and so on. In the last few years there has been remarkable progress in our understanding of algorithmic aspects of discrepancy. In addition to leading to efficient algorithms for various problems where only non-constructive proofs were known before, these methods have also led to improved results and various new connections between discrepancy and convex geometry, optimization and probability. In this talk, we will give an overview of some of these developments.

Counter automata are an appealing formal model of systems and programs with an unbounded number of states that find a plethora of applications, for instance in the verification of concurrent shared-memory programs. A counter automaton comprises a finite-state controller with a finite number of counters ranging over the natural numbers that can be incremented, decremented and tested for zero when a transition is taken. Despite having been studied since the early days of computer science, many important problems about decidable subclasses of counter automata have remained unsolved. This talk will give an overview over the history and some of the progress on both theoretical and practical aspects of counter automata that has been made over the last two years, focusing on new results concerning reachability, stochastic extensions, practical decision procedures, and the challenges that lie ahead.

This talk is based on joint work with M. Blondin (Montreal), A. Finkel (Cachan), S. Haddad (Cachan), P. Hofman (Cachan), S. Kiefer (Oxford) and M. Lohrey (Siegen).

YouTube competes with Hollywood as an entertainment channel, and also supplements Hollywood by acting as a distribution mechanism.  Twitter has a similar relationship to news media, and Coursera to Universities. But there are no online alternatives for making democratic decisions at large scale as a society. In this talk, we will describe two algorithmic approaches towards large scale decision making that we are exploring.

a) Knapsack voting and participatory budgeting: All budget problems are knapsack problems at their heart, since the goal is to pack the largest amount of societal value into a budget. This naturally leads to "knapsack voting" where each voter solves a knapsack problem, or comparison-based voting where each voter compares pairs of projects in terms of benefit-per-dollar. We analyze natural aggregation algorithms for these mechanisms, and show that knapsack voting is strategy-proof. We will also describe our experience with helping implement participatory budgeting in close to two dozen cities and municipalities, and briefly comment on issues of fairness.

b) Triadic consensus: Here, we divide individuals into small groups (say groups of three) and ask them to come to consensus; the results of the triadic deliberations in each round form the input to the next round. We show that this method is efficient and strategy-proof in fairly general settings, whereas no pair-wise deliberation process can have the same properties.

This is joint work with Tanja Aitamurto, Brandon Fain, Anilesh Krishnaswamy, David Lee, Kamesh Munagala, and Sukolsak Sakshuwong.

In this talk I will introduce first  my general research interests which span from mobility modelling and geo-social network analysis to mobile sensing and mobile systems. I will then describe our work in the area of understanding patterns of mobility through sensing using microphone, accelerometer and gyroscope, primarily. I will then describe techniques which help make this energy efficient to achieve continuous sensing on smartphones and wearables. Examples will be drawn from our studies in mental health monitoring, vehicular mobility monitoring and organization analytics.

With the success of machine learning, we increasingly see learning algorithms ma ke decisions in the real world. Often, however, this is in stark contrast to the  classical train- test paradigm, since the learning algorithm affects the very data it must operat e on.  I will explain how predictive confidence bounds can guide data acquisition in a principled way to make effecti ve decisions in a variety of complex settings.  I will present algorithms with performance guarantees relying on the notion of submodularity, a natural notion of diminishing returns.  I will also discuss several applications, ranging from autonomously guiding wetlab experimen ts in protein structure optimization, to safe automatic parameter tuning on a ro botic platform.

For computer software, our security models, policies, mechanisms, and means of assurance were primarily conceived and developed before the end of the 1970's. However, since that time, software has changed radically: it is thousands of times larger, comprises countless libraries, layers, and services, and is used for more purposes, in far more complex ways. This suggests that we should revisit some of our core computer security concepts. For example, what does the Principle of Least Privilege mean when all software contains libraries that can express arbitrary functionality? And, what security policy should be enforced when software is too complex for either its developers or its users to explain its intended behavior in detail? One possibility is to take an empirical, data-driven approach to modern software, and determine its exact, concrete behavior via comprehensive, online monitoring. Such an approach can be a practical, effective basis for security— as demonstrated by its success in spam and abuse fighting—but its use to constrain software behavior raises many questions. In particular, two questions seem critical. First, is it possible to learn the details of how software *is* behaving, without intruding on the privacy of its users?  Second, are those details a good foundation for deriving security policies that constrain how software *should* behave?  This talk answers both these questions in the affirmative, as part of an overall approach to data-driven security. Specifically, the talk describes techniques for learning detailed software statistics while providing differential privacy for its users, and how deep learning can help derive useful security policies that match users' expectations with intended software behavior. Those techniques are both practical and easy to adopt, and have already been used at scale for billions of users.

Connectivity services have been the focus of tremendous innovation in the recent past. The majority of such innovation, however, has primarily targeted mobile devices, despite the ever growing interest around home services. In this talk I am going to describe different types of innovation that I consider interesting for residential users and why they have or have not succeeded. The fundamental question is "What does it actually take to create interesting, novel user experiences for residential users?". In the talk I am going to focus on constraints, but also opportunities that could create meaningful value added services for the place that we love to call our home.

Reliability is a first-order concern in modern distributed systems. Even large, well-provisioned systems such as Gmail and Amazon Web Services can be brought down by failures, incurring millions of dollars of cost and hurting company reputation. Such service outages are typically caused by either hardware failures or software bugs. The systems community has developed various techniques for dealing with both kinds of failures (e.g. replication, software testing), but those techniques come at a significant cost. For example, our replication techniques for handling hardware failures are incompatible with multithreaded execution, forcing a stark choice between reliability and performance. As for guarding against software failures, our only real option today is to test our system as best we can and hope we have not missed any subtle bugs. In principle there exists another option, formal verification, that fully addresses this problem, but its overhead in both raw performance and programming effort is considered way too impractical to adopt in real developments.

In this talk, I make the case for Sustainable Reliability, i.e. reliability techniques that provide strong guarantees without imposing unnecessary overhead that limits their practicality. My talk covers the challenges faced by both hardware and software failures and proposes novel techniques in each area. In particular, I will describe how we can reconcile replication and multithreaded execution by rethinking the architecture of replicated systems. The resulting system, Eve, offers an unprecedented combination of strong guarantees and high performance. I will also describe IronFleet, a new methodology that brings formal verification of distributed systems within the realm of practicality. Despite its strong guarantees, IronFleet incurs a very reasonable overhead in both performance and programming effort.

Many of our everyday activities are now performed online - whether it is banking, shopping, or chatting with friends. Behind the scenes, these activities are implemented by large distributed systems that often contain machines from several different organizations. Usually, these machines do what we expect them to, but occasionally they 'misbehave' - sometimes by mistake, sometimes to gain an advantage, and sometimes because of a deliberate attack.

In society, accountability is widely used to counter such threats. Accountability incentivizes good performance, exposes problems, and builds trust between competing individuals and organizations. In this talk, I will argue that accountability is also a powerful tool for designing distributed systems. An accountable distributed system ensures that 'misbehavior' can be detected, and that it can be linked to a specific machine via some form of digital evidence. The evidence can then be used just like in the 'offline' world, e.g., to correct the problem and/or to take action against the responsible organizations.

I will give an overview of our progress towards accountable distributed systems, ranging from theoretical foundations and efficient algorithms to practical applications. I will also present one result in detail: a technique that can detect information leaks through covert timing channels.

Application developers lack tools to profile and compare the energy consumption of different software designs. This energy-optimization task is challenging because of unpredictable interactions between the application and increasingly complex power management logic. Yet, having accurate power information would allow application developers to both avoid inefficient designs and discover opportunities for new optimizations.

In this talk, I will show that it is possible to accurately measure system-level power and attribute it to application activities. I will present BattOr, a portable, easy-to-use power monitor that provides developers with a profile of the energy consumption of their designs-without modifications to hardware or software. I will show how Google developers are using BattOr to improve Chrome's energy efficiency. I will also show how fine-grained understanding of cellular power at different signal strengths enables novel energy optimizations. Finally, I will describe my future plans to attribute system-level power to individual hardware components and to investigate opportunities presented by instrumenting every server in a data center with fine-grained power monitoring.

Understanding the complex defender-adversary interaction in any adversarial interaction allows for the design of intelligent and adaptive defense.  Game theory is a natural model for such multi-agent interaction. However, significant challenges need to be overcome in order to apply game theory in practice. In this talk, I will present my work on addressing two such challenges: scalability and learning adversary behavior. First, I will present a game model of screening of passengers at airports and a novel optimization approach based on randomized allocation and disjunctive programming techniques to solve large instances of the problem. Next, I will present an approach that learns adversary behavior and then plans optimal defensive actions, thereby bypassing standard game-theoretic assumptions such as rationality. However, a formal Probably Approximately Correct (PAC) model analysis of the learning module in such an approach reveals possible conditions under which learning followed by optimization can produce sub-optimal results. This emphasizes the need of formal compositional reasoning when using learning in large systems. 

The airport screening work was done in collaboration with the Transport Security Administration in USA. The approach of learning adversary behavior was applied for predictive policing in collaboration with University of Southern California (USC) police, and is being tested on the USC campus.

We present a recent line of work on automated synthesis of synchronization constructs for concurrent programs. Our techniques are inspired by a study of the most common types of concurrency bugs and bugs-fixes in Linux device-drivers.  As opposed to classical techniques which tend to use expensive synchronization constructs, our technique attempts to use inexpensive program transformations, such as reordering independent statements, to improve the performance of generated fixes.

Our techniques are based on the observation that a large fraction of concurrency bugs are data-independent. This observations allow us to characterize and fix concurrency bugs based only on the order of execution of the statements involved. We evaluated our techniques on several real concurrency bugs that occurred in Linux device drivers, and showed that our synthesis procedure is able to produce more efficient and "programmer-like" bug-fixes.

We finish by talk with a brief note on the general theme of soft specifications, such as performance and energy consumption, in program synthesis. Specifically, we will discuss the use of quantitative specifications and their applications to resource management in embedded and cyber-physical systems.

Online social interactions have become an integral part of people's lives, e.g., presidential candidates use Facebook and Twitter to engage with the public, programmers rely on Stackoverflow to write code, and various communities have been forming online. This unprecedented amount of social interaction offers tremendous opportunities to understand human behavior. Such an understanding can induce significant social impact, ranging from influencing election outcomes to better communication for everyone. 

My research leverages newly available massive datasets of social interactions to understand human behavior and predict human decisions. These results can be used to build or improve socio-technical systems. In this talk, I will explain my research at both micro and macro levels. At the micro level, I investigate the effect of wording in message sharing via natural experiments. I develop a classifier that outperforms humans in predicting which tweet will be retweeted more. At the macro level, I examine how users engage with multiple communities and find that, surprisingly, users continually explore new communities on Reddit. Moreover, their exploration patterns in their early ``life'' can be used to predict whether they will eventually abandon Reddit. I will finish with some discussion of future research directions in understanding human behavior.

The state of Internet security today is largely reactive, continually raising the defensive bar in response to increasingly sophisticated attackers. In this talk, I will present an alternate approach to building Internet systems that underlies much of my work: instead of reactively working around some attacks, what if we were to make them impossible in the first place?

 I will discuss two primitives my collaborators and I have created that provide small proofs of impossibility, and I will demonstrate   how they can be applied to solve large-scale problems, including censorship resistance, digital currency, and online voting.     First, I will present TrInc, a small piece of trusted hardware that provides proof that an attacker could not have sent conflicting   messages to others.  Second, I will present Alibi Routing, a peer-to-peer system that provides proof that a user's packets could   not have gone through a region of the world the user requested them to forbid. Finally, I will describe some of my ongoing   and future efforts, including securing the Web's public key infrastructure.

The shift to multi-core architectures in the past ten years pushed developers to write concurrent software to leverage hardware parallelism. The transition to multi-core hardware happened at a more rapid pace than the evolution of associated programming techniques and tools, which made it difficult to write concurrent programs that are both efficient and correct. Failures due to concurrency bugs are often hard to reproduce and fix, and can cause significant losses.

In this talk, I will first give an overview of the techniques we developed for the detection, root cause diagnosis, and classification of concurrency bugs. Then, I will discuss how the techniques we developed have been adopted at Microsoft and Intel. I will then discuss in detail Gist, a technique for the root cause diagnosis of failures. Gist uses hybrid static-dynamic program analysis and gathers information from real user executions to isolate root causes of failures. Gist is highly accurate and efficient, even for failures that rarely occur in production. Finally, I will close by describing future work I plan to do toward solving the challenges posed to software systems by emerging technology trends.

Humans as well as information are organized in networks. Interacting with these networks is part of our daily lives: we talk to friends in our social network; we find information by navigating the Web; and we form opinions by listening to others and to the media. Thus, understanding, predicting, and enhancing human behavior in networks poses important research problems for computer and data science with practical applications of high impact. In this talk I will present some of my work in this area, focusing on (1) human navigation of information networks and (2) person-to-person opinions in social networks.

Network navigation constitutes a fundamental human behavior: in order to make use of the information and resources around us, we constantly explore, disentangle, and navigate networks such as the Web. Studying navigation patterns lets us understand better how humans reason about complex networks and lets us build more human-friendly information systems. As an example, I will present an algorithm for improving website hyperlink structure by mining raw web server logs. The resulting system is being deployed on Wikipedia's full server logs at terabyte scale, producing links that are clicked 10 times as frequently as the average link added by human Wikipedia editors.

Communication and coordination through natural language is another prominent human network behavior. Studying the interplay of social network structure and language has the potential to benefit both sociolinguistics and natural language processing. Intriguing opportunities and challenges have arisen recently with the advent of online social media, which produce large amounts of both network and natural language data. As an example, I will discuss my work on person-to-person sentiment analysis in social networks, which combines the sociological theory of structural balance with techniques from natural language processing, resulting in a machine learning model for sentiment prediction that clearly outperforms both text-only and network-only versions.

I will conclude the talk by sketching interesting future directions for computational approaches to studying and enhancing human behavior in networks.

Severe low-level vulnerabilities abound in today's computer systems, allowing cyber-attackers to remotely gain full control. This happens in big part because our programming languages, compilers, and architectures were designed in an era of scarce hardware resources and too often trade off security for efficiency. The semantics of mainstream low-level languages like C is inherently insecure, and even for safer languages, establishing security with respect to a high-level semantics does not guarantee the absence of low-level attacks. Secure compilation using the coarse-grained protection mechanisms provided by mainstream hardware architectures would be too inefficient for most practical scenarios.

In this talk I will present a new project that is aimed at leveraging emerging hardware capabilities for fine-grained protection to build the first, efficient secure compilers for realistic programming languages, both low-level (the C language) and high-level (ML and F*, a dependently-typed variant). These compilers will provide a secure semantics for all programs and will ensure that high-level abstractions cannot be violated even when interacting with untrusted low-level code. To achieve this level of security without sacrificing efficiency, our secure compilers target a novel tagged architecture, which associates a metadata tag to each word and efficiently propagates and checks tags according to software-defined rules. Formally, our goal is full abstraction with respect to a secure high-level semantics. This property is much stronger than just compiler correctness and ensures that no machine-code attacker can do more harm to securely compiled components than a component in the secure source language already could.

Cyber-physical systems -- such as cars, pacemakers, and power plants -- need to interact with the physical world in a timely manner to ensure safety. It is important to have a way to analyze these systems and to prove that they can meet their timing requirements. However, modern cyber-physical systems are increasingly complex: they can involve thousands of tasks running on dozens of processors, many of which can have multiple cores or shared caches. Existing techniques for ensuring timing guarantees cannot handle this level of complexity. In this talk, I will present some of my recent work that can help to bridge this gap, such as overhead-aware compositional scheduling and analysis. I will also discuss some potential applications, such as real-time cloud platforms and intrusion-resistant cyber-physical systems.

This talk will present the design and soundness proof of Verasco, a formally verified static analyzer for most of the ISO C99 language (excluding recursion and dynamic allocation), developed using the Coq proof assistant. Verasco aims at establishing the absence of run-time errors in the analyzed programs. It enjoys a modular architecture that supports the extensible combination of multiple abstract domains, both relational and non-relational. It include a memory abstract domain, an abstract domain of arithmetical symbolic equalities, an abstract domain of intervals, an abstract domain of arithmetical congruences and an octagonal abstract domain.

Verasco integrates with the CompCert formally-verified C compiler so that not only the soundness of the analysis results is guaranteed with mathematical certitude, but also the fact that these guarantees carry over to the compiled code.

Today, many embedded and cyber-physical systems, e.g., automotive, comprise several control applications. Guaranteeing the stability of these control applications is perhaps the most fundamental requirement while implementing such applications. Often, however, the design of such systems is done without considering the implementation impacts. In this case, the guarantees provided at design time might not be preserved for the final implementation. In this talk, we discuss the implementation- aware design of embedded control systems.

CakeML is a new ML dialect aimed at supporting formally verified programs. The CakeML project has several aspects including formal semantics and metatheory, a verified compiler, a formal connection between its semantics and higher-order logic (in the HOL4 interactive theorem prover), and example verified applications written in CakeML and HOL4. The project is an active collaboration between Ramana Kumar at NICTA, Magnus Myreen at Chalmers, Michael Norrish at NICTA, Yong Kiam Tan at (A*STAR, Singapore), and myself.

In this talk, I will explain the architecture of CakeML's verified compiler, focussing on a new optimising backend that we are currently developing.

CakeML's web site is https://cakeml.org, and development is hosted on GitHub at https://github.com/CakeML/cakeml.

Processor architectures are critical interfaces in computing, but they are typically defined only by prose and pseudocode documentation. This is especially problematic for the subtle concurrency behaviour of weakly consistent multiprocessors such as ARM and IBM POWER: the traditional documentation does not define precisely what programmer-observable behaviour is (and is not) allowed for concurrent code; it is not executable as a test oracle for pre-Silicon or post-Silicon hardware testing; it is not executable as an emulator for software testing; and it is not mathematically rigorous enough to serve as a foundation for software verification.

In this talk, I will present a rigorous architectural envelope model for IBM POWER and ARM multiprocessors, that aims to support all of these for small-but-intricate test cases, integrating an operational concurrency model with an ISA model for the sequential behaviour of a substantial fragment of the user-mode instruction set (expressed in a new ISA description language). I will present the interface between the two, whose requirements drove the development of our new language Sail. I will also present the interesting aspects of Sail's dependent type system, which is a light-weight system balancing the benefits of static bounds and effects checking with the usability of the language for engineers. Futher, our models can be automatically translated into executable code, which, combined with front-ends for concurrency litmus tests and ELF executables, can interactively or exhaustively explore all the allowed behaviours of small test cases.

Joint work with: S. Flur, G. Kerneis*, L. Maranget**, D. Mulligan, C. Pulte, S. Sarkar***, and P. Sewell, University of Cambridge (* Google, ** Inria, *** St Andrews)

In my PhD thesis I have developed a formal semantics of a significant part of the C programming language as described by the C11 standard. In this talk I will give a brief overview of the main parts of my formalized semantics.

* A structured memory model based on trees to capture subtleties of C11 that have not been addressed by others.

* A core C language with a small step operational semantics. The operational semantics is non-deterministic due to unspecified expression evaluation order.

* An explicit type system for the core language that enjoys type preservation and progress.

* A type sound translation of actual C programs into the core language.

* An executable semantics that has been proven sound and complete with respect to the operational semantics.

* Extensions of separation logic to reason about subtle constructs in C like non-determinism in expressions, and gotos in the presence of block scope variables.

Software is susceptible to malformed data originating from untrusted sources. Occasionally the programming logic or constructs used are inappropriate to handle the varied constraints imposed by legal and well-formed data. Consequently, software may produce unexpected results or even crash. In this paper, we present \tool, a novel hybrid approach that saves such software from crashing when failures originate from malformed strings or inappropriate handling of strings. Clotho statically analyzes a program to identify statements that are vulnerable to failures related to associated string data. Clotho then generates patches that are likely to satisfy constraints on the data, and in case of failures produces program behavior which would be close to the expected. The precision of the patches is improved with the help of a dynamic analysis. 

We have implemented Clotho for the Java String API, and our evaluation based on several popular open-source libraries shows that Clotho generates patches that are semantically similar to the patches generated by the programmers in the later versions. Additionally, these patches are activated only when a failure is detected, and thus Clotho incurs no runtime overhead during normal execution, and negligible overhead in case of failures.

The benefits of adopting emerging multicore processors include reductions in space, weight, power, and cooling, while increasing CPU bandwidth per processor. However, the existing real-time software engineering process is based on the constant worst case execution time (WCET) assumption, which states that the measured worst case execution time of a software task when executed alone is the same as when that task is running together with other tasks. While this assumption is correct for single-core chips, it is NOT true for multicore chips. As it is now, the interference between cores can cause delay spikes as high as 600% in industry benchmarks. This presentation reviews main challenges faced by the embedded industry today when adopting multicore in safety critical embedded systems. A discussion on the notion of Single Core Equivalence follows.

n geo-replicated distributed data stores, the need to ensure responsiveness in the face of network partitions and processor failures results in implementations that provide only weak (so-called eventually consistent) guarantees on when data updated by one process becomes visible to another. Applications must be carefully constructed to be aware of unwanted inconsistencies permitted by such implementations (e.g., having negative balances in a bank account, or having an item appear in a shopping cart after it has been removed), but must balance correctness concerns with performance and scalability needs. Because understanding these tradeoffs requires subtle reasoning and detailed knowledge about the underlying data store, implementing robust distributed applications in such environments is often an error-prone and expensive task.

The collection and analysis of observational and experimental data represent the main tools for assessing the presence, the extent, the nature, and the trend of discrimination phenomena. Data analysis techniques have been proposed in the last fifty years in the economic, legal, statistical, and, recently, in the data mining literature. This is not surprising, since discrimination analysis is a multi-disciplinary problem, involving sociological causes, legal argumentations, economic models, statistical techniques, computational issues. The objective of the talk is to provide first an introduction on concepts, problems, application areas, datasets, methods and approaches from a multidisciplinary perspective; and then to deep in the data-driven approach based on data mining for discrimination discovery and prevention. Reference: · A. Romei, S. Ruggieri. A multidisciplinary survey on discrimination analysis. The Knowledge Engineering Review. Vol. 29, Issue 5, November 2014, 582-638.

In real-time scheduling theory we are interested in finding out whether a set of repeatedly activated computational tasks can be co-executed on a shared computer platform, such that all of their deadlines are met. The periodic and sporadic task models are among the most basic formalisms used for modeling computational tasks. Among computer platforms considered, the preemptive uniprocessor is one of the simplest. To decide whether a given set of periodic or sporadic tasks can be scheduled on a preemptive uniprocessor so that all deadlines are met is therefore a core problem in real-time scheduling theory. Still, the complexity of this decision problem has long been open. In this talk, which is targeted to a general audience, I will outline some recent results pinpointing this complexity.   

In this talk, I will present an approach to ease the verification of file-system code using a domain-specific language, currently called CoGent, supported by a self-certifying compiler that produces C code, a high-level specification, and translation correctness proofs.

CoGent is a restricted, polymorphic, higher-order, and purely functional language with linear types and without the need for a trusted runtime or garbage collector. It compiles to efficient C code that is designed to interoperate with existing C functions.

For a well-typed CoGent program, the compiler produces C code, a high-level shallow embedding of its semantics in Isabelle/HOL, and a proof that the C code correctly implements this embedding. The aim is for proof engineers to reason about the full semantics of real-world systems code productively and equationally, while retaining the interoperability and leanness of C.

I will give a high-level overview of the formal verification stages of the compiler, which include automated formal refinement calculi, a switch from imperative update semantics to functional value semantics formally justified by the linear type system, and a number of standard compiler phases such as type checking and monomorphisation. The compiler certificate is a series of language-level meta proofs and per-program translation validation phases, combined into one coherent top-level theorem in Isabelle/HOL.

Octagonal constraints expressing weakly relational numerical properties of the form ($l \le \pm x \pm y \leq h$) have been found useful and effective in static analysis of numerical programs. Their analysis serves as a key component of the tool ASTREE based on abstract interpretation framework proposed by Patrick Cousot and his group, which has been successfully used to analyze commercial software consisting of hundreds of thousand of lines of code. This talk will discuss a heuristic based on the quantifier-elimination (QE) approach presented by Kapur (2005) that can be used to automatically derive loop invariants expressed as a conjunction of octagonal constraints in $O(n^2)$, where $n$ is the number of program variables over which these constraints are expressed. This is in contrast to the algorithms developed in Mine's thesis which have the complexity at least $O(n^3)$. The restricted QE heuristic usually generates invariants stronger than those obtained by the freely available Interproc tool. Extensions of the proposed approach to generating disjunctive invariants will be presented.

The underlying theories of both control engineering and real-time systems engineering assume idealized system abstractions that mutually neglect central aspects of the other discipline. Control engineering theory, on the one hand, usually assumes jitter free sampling and constant input-output latencies disregarding complex real-world timing effects. Real-time engineering theory, on the other hand, uses abstract performance models that neglect the functional behavior, and derives worst-case situations that have little expressiveness for control functionalities in physically dominated automotive systems. As a consequence, there is a lot of potential for a systematic co-engineering between both disciplines, increasing design efficiency and confidence. In this talk, possible approaches for such a co-engineering and their current applicability to real world problems are discussed. In particular, simulation-based and formal verification techniques are compared for different construction principles of automotive real-time control software.

Data centers run a range of important applications with ever increasing performance demands, from cloud and server computing to Big Data and eScience. However, the scaling of CPU frequency has stalled in recent years, leading to hardware architectures that no longer transparently scale software performance. Two trends stand out: 1) Instead of frequency, hardware architectures increase the number of CPU cores, leaving complex memory system performance and CPU scheduling tradeoffs exposed to software. 2) Network and storage I/O performance continues to improve, but without matching improvements in CPU frequency. Software thus faces ever increasing I/O efficiency demands.

In my research, I address how operating systems (OSes) can handle these growing complexity and performance pressures to avoid becoming the limiting factor to performance. I first explain how current OS architecture is already inadequate to address these trends, limiting application performance. I then present how the OS can be redesigned to eliminate the performance limitations without compromising on existing features or application compatibility. I finish with an outlook on how these hardware trends affect software in the future and present ideas to address them.

As the most serious cyber-attack threats rapidly shift from untargeted toward increasingly targeted methods, it is becoming more crucial for organizations to protect the identity and location of their members against malicious tracking and surveillance. The common approach by organizations to use encryption is not enough, as metadata, such as the sender and receiver, has recently been shown to be as valuable and hence as dangerous as data. Employing existing anonymous communication tools, such as Tor, only deter but do not prevent tracking and targeting attacks. This talk describes three major challenges to protecting users: network-based traffic analysis attacks, intersection attacks against identities and traffic flows, and application / environment exploits. The talk then introduces practical approaches that address these challenges as implemented and evaluated in the Dissent project.

Abstract: Large Internet services, "big science", and increasingly, industrial R&D, are all powered by warehouse scale computing — tens of thousands of servers connected over a network. Increasing parallelism and big data analytics require that the network provide high throughput connectivity. In this talk, I will describe Jellyfish, our proposed design for such a network. Jellyfish uses a random graph topology, allowing construction at arbitrary sizes, easier network growth over time, and integration of newer and more powerful network equipment as it becomes available — practical problems that rigidly structured traditional networks fail to address. Surprisingly, Jellyfish also beats state-of-the-art real-world designs on throughput, by as much as 40%. In fact, we show that Jellyfish networks achieve near optimal throughput, i.e., one cannot build, using the same networking equipment, *any* network that provides much higher throughput.

Large-scale private user data theft has become a common occurrence on the web. A huge factor in these privacy breaches we hear so much about is that developers specify and enforce data security policies by strewing checks throughout their application code. Overlooking even a single check can lead to vulnerabilities.

In this talk, I will describe a new approach to protecting sensitive data even when application code is buggy or malicious. The key ideas behind my approach are to separate the security and privacy concerns of an application from its functionality, and to use language-level information flow control (IFC) to enforce policies throughout the code. The main challenge of this approach is at once to design practical systems that can be easily adopted by average developers, and simultaneously to leverage formal semantics that rule out large classes of design error. The talk will cover a server-side web framework (Hails), a language-level IFC system (LIO), and a browser security architecture (COWL), which, together, provide end-to-end security against the privacy leaks that plague today's web applications.

Trusted hardware modules are becoming prevalent in computing devices of all kinds. A broad trusted hardware assumption purports to solve almost all security problems in a trivial and uninteresting manner. However, relying entirely on hardware assumptions to achieve security goals of a system can be impractical given the limited memory, bandwidth and CPU capabilities of available hardware modules, and makes the designed system vulnerable to even a tiny overlooked or undiscovered flaw/side-channel in the employed module. Thus, the key challenge to me while designing a trusted hardware-based system is to determine a minimal hardware assumption required to achieve the system's goals, and justify the assumption for an available hardware module.

In this talk, I will present my recent work on developing privacy-preserving systems based on the above insight. In particular, I will introduce a privacy-preserving transaction protocol for credit networks (PrivPay), an architecture for privacy-preserving online behavioral advertising (ObliviAd), and an asynchronous multiparty computation protocol with only an honest majority (NeqAMPC).

Online privacy and security decision making is complex, because it is affected both by objective risks and benefits from disclosure or protection of personal information, and by factors that do not directly affect economic trade-offs. For instance, design features - such as default visibility settings, look & feel of a website, granularity of privacy controls, or framing of privacy policies - as well as cognitive and behavioral biases affect risk perception. Behavioral sciences provide useful insights on how people respond to risks and threats. Of particular interest to my research is whether individuals detect, recognize, and react differently to "offline" and "online" threats. I will present a series of laboratory experiments, that combine findings from HCI and behavioral sciences, showing how to help users of online sharing technologies detect online privacy and security threats, and thus make better informed decisions. The experiments demonstrate how sensorial, visceral stimuli from the offline, physical world can affect online privacy concern and online disclosures. The results show the importance of going beyond privacy and security usability research, and provide suggestions on how to improve interfaces to help users make sound privacy and security decisions.

Numerical software, common in scientific computing or embedded systems, inevitably uses an approximation of the real arithmetic in which most algorithms are designed. Finite-precision arithmetic, such as fixed-point or floating-point, is a common and efficient choice, but introduces an uncertainty on the computed result that is often very hard to quantify. We need adequate tools to estimate the errors introduced in order to choose suitable approximations which satisfy the accuracy requirements. I will present a new programming model where the scientist writes his or her numerical program in a real-valued specification language with explicit error annotations. It is then the task of our verifying compiler to select a suitable floating-point or fixed-point data type which guarantees the needed accuracy. I will show how a combination of SMT theorem proving, interval and affine arithmetic and function derivatives yields an accurate, sound and automated error estimation which can handle nonlinearity, discontinuities and certain classes of loops. We have further combined our error computation with genetic programming to not only verify but also improve accuracy. Finally, together with techniques from validated numerics we developed a runtime technique to certify solutions of nonlinear systems of equations, quantifying truncation in addition to roundoff errors.

Abstract: In recent years, we have witnessed the emergence of many sophisticated web services that allow people to interact on an unprecedented scale. The wealth of data produced by these new ways of communication can be used, in principle, to increase our understanding of human social behaviour, but a fundamental hurdle is posed by the sensitivity of these data. Access must of necessity be severely constrained in order to protect the privacy of the users and the confidentiality of the data. A very broad question arises naturally: can non-trivial conclusions about various social processes be inferred based only on such limited information? We give a few specific examples taken from our own research of what can, and cannot, be learned from digital traces. The talk describes joint work with several people: B.Abrahao, P.Brach, F.Chierichetti, R.Kleinberg, A.Epasto, P.Sankowski

Dynamic graph algorithms are data structures that maintain properties of graphs while they are modified by edge deletions and insertions. These data structures can be used, for example, to efficiently detect deadlocks in operating systems, compute shortest-paths in navigation systems, or to speed up static algorithms, such as algorithms used in computer-aided verification or certain multi-commodity flow algorithms, that solve multiple graph propblems on very similar graphs.

While basic properties, such as connectivity, in undirected graphs can be maintained in time polylogarithmic in the size of the graph per edge update, no such bounds are known for basic properties, such as reachability, in directed graphs or more sophisticated graph properties, such as shortest paths, in undirected graphs. We will present the state of the art for these problems, giving both upper and (conditional) lower bounds. Conditional lower bounds result from a relatively new research direction, where similar to hardness reductions in complexity theory, we show that based on the assumption that some well-known problems, such as Boolean matrix multiplication, cannot be solved fast, certain dynamic problems cannot be solved in polylogarithmic time per operation.

Shared memory parallel machines have existed since the 1960s and, with the proliferation of multi-core processors, shared memory parallel programming has become increasingly important. Unfortunately, some fairly basic questions about parallel program semantics have not been addressed until quite recently. Multi-threaded programming languages are on much more solid ground than they were as recently as a decade ago. Nonetheless a number of foundational issues have turned out to be surprisingly subtle and resistant to easy solutions. We briefly survey three such issues:

1) All major programming languages support atomic operations that enforce only very weak memory ordering properties. These implicitly rely on enforcement of dependencies to preclude certain "nonsensical" outcomes. Unfortunately, we do not know how to define a suitable notion of dependency.

2) Garbage collected programming languages such as Java, rely on finalization, most commonly to interact correctly with non-garbage-collected parts of the system. But finalization raises largely unsolved concurrency issues. As a result, almost all interesting uses of finalization uses are subtly, but seriously, incorrect.

3) It can be difficult to avoid object destruction or memory deallocation races in-garbage-collected languages like C++. As a result, async(), the basic C++11 thread spawning facility has surprisingly complex semantics, with unintended consequences.

In this talk we'll consider two problems in which users must select from a set of alternatives. In the first scenario, a user consumes a class of item repeatedly, such as listening to a sequence of songs, or visiting a sequence of restaurants over time. Our goal is to understand the dynamics of repeated consumption of the same item. We present a model related to Herbert Simon's 1955 copying model, and analyze its effectiveness. In the second scenario, a user traverses a directed graph whose nodes represent items, and whose arcs represent related items recommended by the system. In this setting, we develop a model and algorithm for determining the underlying quality of each node based on traversal data. Our result provides a well-motivated unique solution to the problem of "reverse engineering" a markov chain by finding a transition matrix given the graph and the steady state

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

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.

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.

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

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)

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

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.

What can be computed, and how efficiently, is a core question in computer science. Not surprisingly, in distributed systems and networking research, a fundamental question is what can be computed how efficiently in a distributed fashion, in a network. More precisely, if nodes of a network must solve a problem by locally communicating with their neighbors, how fast can they compute (or approximate) a global (optimization) problem? Throughout the years, we studied different aspects and problems of this "network complexity" theory. In my talk I will discuss a few facets, e.g., how to compute the network diameter, or the role of randomness. Towards the end of the talk I will present some nuggets regarding "complex networks", in particular updates in Software Defined Networks, and attacks on the Bitcoin network.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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.

I am going to talk about two approaches to the verification of probabilistic systems: (1) equivalence analysis; and (2) termination analysis.

Deciding equivalence of probabilistic automata is a key problem for establishing various behavioural and anonymity properties of probabilistic systems. In particular, it is at the heart of the tool APEX, an analyser for probabilistic programs. APEX is based on game semantics and analyses a broad range of anonymity and termination properties of randomised protocols and other open programs.

Proving programs terminating is a fundamental computer science challenge. Recent research has produced powerful tools that can check a wide range of programs for termination. The analogue for probabilistic programs, namely termination with probability one (``almost-sure termination''), is an equally important property for randomised algorithms and probabilistic protocols. We have developed a novel algorithm for proving almost-sure termination of probabilistic programs. Our algorithm exploits the power of state-of-the-art model checkers and termination provers for nonprobabilistic programs.

The Internet is at once an immense engineering artifact, a pervasive social force, and a fascinating object of study. Unfortunately many natural questions about the Internet cannot be answered by direct measurement, requiring us to turn instead to the tools of statistical inference. As a detailed example I'll describe a current project in traffic measurement. We are asking the question: using traffic measurements taken at one location in the Internet, can we estimate how much traffic is flowing in a different part of the Internet? Surprisingly, the answer is yes. I'll explain why this is possible (with a connection to problems like the Netflix Prize), how it can be done, and how this result could be used to give a network operator an edge over its competitors.

EasyCrypt is a tool supported framework that supports the machine-checked construction and verification of security proofs of cryptographic systems, and that has been used to verify emblematic examples of public-key encryption schemes, digital signature schemes, hash function designs, and block cipher modes of operation. The lecture will motivate the role of computer-aided proofs in the broader context of provable security, explore the connections between provable security and programming language methods, and speculate on potential applications of computer tools in security analysis and design of cryptographic constructions.

Internet measurement and experimentation platforms, such as PlanetLab, have become essential for network studies and distributed systems evaluation. Despite their many benefits and strengths, a by now well-known problem with existing platforms is their inability to capture the geographic and network diversity of the wider, commercial Internet. Lack of diversity and poor visibility into the network hamper progress in a number of important research areas, from network troubleshooting to broadband characterization and Internet topology mapping, and complicate our attempts to generalize from test-bed evaluations of networked systems. The issue has served as motivation for several efforts to build new experimentation platforms and expand existing ones. However, capturing the edge of the network remains an elusive goal. I argue that at its root, the problem is one of incentives. Today's platforms build on the assumption that the goals of experimenters and those hosting the platform are the same. As much of the Internet growth occur in residential broadband and mobile networks, this no longer holds. In this talk, I will present Dasu, a measurement experimentation platform for the Internet's edge that explicitly aligns the objectives of the experimenters with those of the users hosting the platform. Dasu is designed to support both network measurement experimentation and broadband characterization. Dasu has been publicly available since mid 2010 and has been adopted by over 95,000 users, across 150 countries. I will then illustrate the value of Dasu's unique perspective with some of the ongoing projects and collaboration already taking advantage of it.

Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce an affine bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This is a very useful type-theoretic and denotational framework for many applications to resource-sensitive compilation, and it represents a generalization of several existing type systems. As a non-trivial instance, motivated by our ongoing work on hardware compilation, we present a complex new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.

Dan R. Ghica, Alex Smith

Cluster management is the term that Google uses to describe how we control the computing infrastructure in our datacenters that supports almost all of our external services. It includes allocating resources to different applications on our fleet of computers, looking after software installations and hardware, monitoring, and many other things. My goal is to present an overview of some of these systems, introduce Omega, the new cluster-manager tool we are building, and present some of the challenges that we're facing along the way. Many of these challenges represent research opportunities, so I'll spend the majority of the time discussing those.

-

Let F:K×M→∑ be a functionality, where K is the key space and M is the message space and Σ is the output space.Then a functional encryption (FE) scheme for F is a special encryption scheme in which, for every key k∈K, the owner of the master secret key Msk associated with the public key Pk can generate a special key or "token" Tok that allows the computation of F(k,m) from a ciphertext of m computed under public key Pk. In other words, whereas in traditional encryption schemes decryption is an all-or-nothing affair, in FE it is possible to finely control thea mount of information that is revealed by a ciphertext. Unlike traditional encryption, for FE indistinguishability-security is not equivalent to simulation-based security. This work attempts to clarify to what extent simulation-based security (SIM-security) is achievable for functional encryption and its relation to the weaker indistinguishability-based security (IND-security). Our main result is a compiler that transforms any FE scheme for the general circuit functionality (which we denote by circuit-FE) meeting IND-security to a circuit-FE scheme meeting SIM-security, where: In the random oracle model, the resulting scheme is secure for an unbounded number of encryption and key queries, which is the strongest security level one can ask for. In the standard model, the resulting scheme is secure for a bounded number of encryption and non-adaptive key queries, but an unbounded number of adaptive key queries. This matches known impossibility results and improves upon Gorbunov et al. [CRYPTO'12] (which is only secure for non-adaptive key queries). Our compiler is inspired by the celebrated Fiat-Lapidot-Shamir paradigm [FOCS'90] for obtaining zero-knowledge proof systems from witness-indistinguishable proof systems. We also give a tailored construction of SIM-secure hidden vector encryption (HVE) in composite-order bilinear groups. Finally, we revisit the known negative results for SIM-secure FE, extending them to natural weakenings of the security definition and thus providing essentially a full picture of the achievability of FE. We conclude with open problems and future challenges in the area.

Finite blocking is an important correctness property of multi-threaded programs. It requires that each blocking operation such as acquiring a lock or joining a thread executes eventually. In addition to deadlock freedom, finite blocking in the presence of non-terminating threads requires one to prove that no thread holds a lock indefinitely or attempts to join a non-terminating thread. In this talk, I will present a verification technique for finite blocking of possibly non-terminating programs. The key idea is to track explicitly whether a thread has an obligation to perform an operation that releases another thread from being blocked, for instance, an obligation to release a lock or to terminate. Each obligation is associated with a lifetime to ensure that it is fulfilled within finitely many steps. Our technique guarantees finite blocking for programs with a finite number of threads and fair scheduling. We have implemented our technique in the automatic program verifier Chalice.

Type refinements, introduced by Freeman and Pfenning and explored by Davies and Dunfield, unify the ontological and epistemic views of typing. Types tell us what programming language constructs exist, whereas refinements express properties of the values of a type.  Here we show that refinements are very useful in compiler correctness proofs, wherein it often arises that two expressions that are inequivalent in general are equivalent in the particular context in which they occur.  Refinements serve to restrict the contexts sufficiently so that the desired equivalence holds.  For example, an expression might be replaced by a more efficient one, even though it is not generally equivalent to the original, but is interchangeable in any context satisfying a specified refinement of the type of those expressions.

We study here in detail a particular problem of compiler correctness, namely the correctness of compiling polymorphism (generics) to dynamic types by treating values of variable type as values of a universal dynamic type. Although this technique is widely used (for example, to compile Java generics), no proof of its correctness has been given to date.  Surprisingly, standard arguments based on logical relations do not suffice, precisely because it is necessary to record deeper invariants about the compiled code than is expressible in their types alone.  We show that refinements provide an elegant solution to this problem by capturing the required invariants so that a critical invertibility property that is false is general can be proved to hold in the contexts that arise in the translated code.  This proof not only establishes the correctness of this compilation method, but also exemplifies the importance of refinements for compiler correctness proofs more generally

Determinism of applications is required in the domains of testing, debugging, and fault-tolerant replication. Literature has presented various ways to render application execution deterministic in either transparent or non-transparent manner. Existing approaches operate on the layers of hardware, operating system, rutime environments, or even inside the application logic. Other systems operate in-between two layers: hypervisors between hardware and operating system; and supervisors between operating systems and applications. In this talk, I focus on the combination of replication and determinism: Applying replication techniques and replication protocols to business applications requires that the logic of the business application behave deterministic, while the other parts of the system such as the replication logic does not. This talk gives a brief introduction to the Java-based Virtual Nodes Replication Framework (VNF). VNF allows a transparent replication of business logic. It enables a late configuration of multiple aspects of a replica group including the particular replication protocol. Deciding late which replication protocol to apply, however, is only possible when the application logic satisfies contraints imposed by the replication protocol. Many replication protocols can only be applied when it is ensured that the application logic behaves deterministically. The Deterministic Java suite (Dj suite) is capable of rendering Java applications fully deterministic. In contrast to other approaches, it is pure Java and hence, portable across JVMs, operating systems, and hardware platforms. Furthermore, it can be selectively applied to only parts of entire Java programmes what makes it suited for replicated scenarios. In addition, the Dj suite comprises a deterministic version of the Java runtime libraries which makes it the only comprehensive, Java-based approach in literature. The capability for a flexible configuration ensures adaptability to many different use cases. In this talk, I give an overview on mechanisms and techniques for making Java applications deterministic. In addition, I sketch how to build a determinitic Java-only runtime system from an existing open source Java implementation. The talk concludes with evaluation results, a discussion of future work, and an outlook on the integration of Dj with VNF as well as the possibility of virtualised Java platforms.

Eff is a programming language in which computational effects and handlers are first-class, so we can define new computational effects and handle existing ones in flexible ways. This allows us to express naturally not only the traditional computational effects, but also control operators, such as delimited continuations, I/O redirection, transactions, backtracking and other search strategies, and cooperative multi-threading.

In the talk I shall first introduce Eff from a practical point of view through examples, and then focus on a more precise treatment of a core Eff. I shall also present an effect system for Eff.

We present the first analysis of the popular Tor anonymity network that indicates the security of typical users against reasonably realistic adversaries in the Tor network or in the underlying Internet. Our results show that Tor users are far more susceptible to compromise than indicated by prior work. Specific contributions include (1) a model of various typical kinds of users, (2) an adversary model that includes Tor network relays, autonomous systems (ASes), Internet exchange points (IXPs), and groups of IXPs drawn from empirical study (3) metrics that indicate how secure users are over a period of time, (4) the most accurate topological model to date of ASes and IXPs as they relate to Tor usage and network configuration, (5) a novel realistic Tor path simulator (TorPS), and (6) analyses of security making use of all the above. To show that our approach is useful to explore alternatives and not just Tor as currently deployed, we also analyze a published alternative path selection algorithm, Congestion-Aware Tor. We create an empirical model of Tor congestion, identify novel attack vectors, and show that it too is more vulnerable than previously indicated.

An increasing number of today's social interactions occurs using online social media as communication channels. Some online social networks have become extremely popular in the last decade. They differ among themselves in the character of the service they provide to online users. For instance, Facebook can be seen mainly as a platform for keeping in touch with close friends and relatives, Twitter is used to propagate and receive news, LinkedIn facilitates the maintenance of professional contacts, Flickr gathers amateurs and professionals of photography, etc. Albeit different, all these online platforms share an ingredient that pervades all their applications. There exists an underlying social network that allows their users to keep in touch with each other and helps to engage them in common activities or interactions leading to a better fulfillment of the service's purposes. This is the reason why these platforms share a good number of functionalities, e.g., broadcasted status updates, personal communication channels, easy one-step information sharing, groups created and maintained by the users, organized user-generated content etc. As a result, online social networks are an interesting field to study social behavior that seems to be generic among the different online services. Since at the bottom of these services lays a network of declared relations and the basic interactions in these platforms tend to be pairwise, a natural methodology for studying these systems is provided by network science. In this presentation I describe some of the results of my studies about community structure, interaction dynamics and browsing patterns in online social networks. I present them in an interdisciplinary context of network science, sociology and computer science.

The presentation is divided into three main parts, here are the links to our publications related to each of the sections:

Part I: Interaction patterns in the context of social groups http://www.plosone.org/article/info%3Adoi%2F10.1371%2Fjournal.pone.0029358

Part II: Social and topical groups http://dl.acm.org/citation.cfm?id=2433475

Part III: User browsing patterns and photo recommendation https://docs.google.com/file/d/0B0_e6k3kQKEubEZfZnQwckNjQXM/edit

In this talk I'll describe the Naiad system, based on a new model for low-latency incremental and iterative dataflow. Naiad is designed to provide three properties we do not think yet exist in a single system: the expressive power of loops, concurrent vertex execution, and fine-grained edge completion. Removing any one of these requirements yields an existing class of solutions (respectively: streaming systems like StreamInsight, iterative incremental systems like Nephele, and callback systems like Percolator), but all three together appear to require a new system design. We will describe Naiad's structured cyclic dataflow model and protocol for tracking and coordinating outstanding work, more closely resembling memory fences than traditional distributed systems barriers. We give several examples of how Naiad can be used to efficiently implement many of the currently popular "big data" programming patterns, as well as several new ones, and experimental results indicating that Naiad's relative performance ranges from "as good as" to "much better than" existing systems.

This is joint work with Derek G. Murray, Rebecca Isaacs, Michael Isard, Paul Barham, and Martin Abadi.

Cloud computing in general and Infrastructure-as-a-Service (IaaS) in particular, are becoming ever more popular. However, effective resource management of virtualized resource is a challenging task. Moreover, performance interference (and the resulting unpredictability in the delivered performance) across virtual machines co-located on the same physical machine threatens to make cloud computing inadequate for performance-sensitive customers and more expensive than necessary for all customer.

In this talk, I will describe two frameworks - DejaVu and DeepDive - for dealing with the resource management and performance interference issues in virtualized environments. The key idea behind DejaVu is to cache and reuse the results of previous resource allocation decisions at runtime. By doing so, it speeds up adaptation to workload changes by 18X relative to the state-of-the-art. DeepDive transparently diagnoses and manages performance interference in the cloud by leveraging easily-obtainable low level metrics to discern when interference is occurring and what resource is causing it. DeepDive also mitigates interference using a low-overhead approach to identifying a VM placement that alleviates interference.

Verification technology has proved useful for increasing software reliability and productivity. Its great asset lies in concepts and algorithms for the mechanical construction of formally precise, conservative abstractions of behavioral aspects of systems. Its applicability extends to other problems in Computer Science. A recent example is our uses of abstraction algorithms for automated debugging of programs. In my talk, I will present techniques for computing and analyzing abstractions of systems whose behavior depends on complex data and control, such as heap-allocated data structures and distributed message passing concurrency. Our techniques are based on decision procedures for specific logical theories. The resulting logical abstractions give rise to a new generation of verification tools.

We introduce a novel variant of logical relations that maps types not merely to partial equivalence relations on values, as is commonly done, but rather to a proof-relevant generalisation thereof, namely setoids.

A setoid is like a category all of whose morphisms are isomorphisms (a groupoid) with the exception that no equations between these morphisms are required to hold.

The objects of a setoid establish that values inhabit semantic types, whilst its morphisms are understood as evidence for semantic equivalence.

The transition to proof-relevance solves two well-known problems caused by the use of existential quantification over future worlds in traditional Kripke logical relations: failure of admissibility, and spurious functional dependencies.

We illustrate the novel format with two applications: a direct-style validation of Pitts and Stark's equivalences for ``new'' and a denotational semantics for a region-based effect system that supports type abstraction in the sense that only externally visible effects need to be tracked; non-observable internal modifications, such as the reorganisation of a search tree or lazy initialisation, can count as `pure' or `read only'. This `fictional purity' allows clients of a module soundly to validate more effect-based program equivalences than would be possible with traditional effect systems.

This is joint work with Nick Benton and Vivek Nigam

Modern Massively Multiplayer Online Role-Playing Games (MMORPGs) provide lifelike virtual environments in which players can conduct a variety of activities including combat, trade, and chat with other players. While the game world and the available actions therein are inspired by their offline counterparts, the games’ popularity and dedicated fan base are testament to the allure of novel social interactions granted to people by granting them an alternative life as new characters and personae. In this paper we investigate the phenomenon of "gender swapping," which refers to players choosing avatars of genders opposite to their natural ones. We report the behavioral patterns observed in players of Fairyland Online, a globally serviced MMORPG, during social interactions when playing as in-game avatars of their own real gender or gender-swapped, and discuss the effect of gender role and self-image in virtual social situations and the potential of our study for improving MMORPG qualities and detection of fake online identities.

(To appear at WWW2013, Joint work with Jing-Kai Lou, Kunwoo Park,Juyong Park, Chin-Laung Lei, and Kuan-Ta Chen)

Big data processing frameworks (MapReduce, Hadoop, Dryad) are hugely popular today. A strong selling point is their ability to provide failure resilience guarantees. They can run computations to completion despite occasional failures in the system. However, an overlooked point has been the efficiency of the failure resilience provided. The vision of this work is that big data frameworks should not only finish computations under failures but minimize the impact of the failures on the computation time.

The first part of the talk presents the first in-depth analysis of the efficiency of the failure resilience provided by the popular Hadoop framework at the level of a single job. The results show that compute node failures can lead to variable and unpredictable job running times. The causes behind these results are detailed in the talk. The second part of the talk focuses on providing failure resilience at the level of multi-job computations. It presents the design, implementation and evaluation of RCMP, a MapReduce system based on the fundamental insight that using replication as the main failure resilience strategy oftentimes leads to significant and unnecessary increases in computation running time. In contrast, RCMP is designed to use job re-computation as a first-order failure resilience strategy. RCMP enables re-computations that perform the minimum amount of work and also maximizes the efficiency of the re-computation work that still needs to be performed.

Industrial-scale control systems are often developed in the model-based design paradigm. This typically involves capturing a plant model that describes the dynamical characteristics of the physical processes within the system, and a controller model, which is a block-diagram-based representation of the software used to regulate the plant behavior. In practice, plant models and controller models are highly complex as they can contain highly nonlinear hybrid dynamics, look-up tables storing pre-computed values, several levels of design-hierarchy, design-blocks that operate at different frequencies, and so on. Moreover, the biggest challenge is that system requirements are often imprecise, non-modular, evolving, or even simply unknown. As a result, formal techniques have been unable to digest the scale and format of industrial-scale control systems. On the other hand, the Simulink modeling language -- a popular language for describing such models -- is widely used as a high-fidelity simulation tool in the industry, and is routinely used by control designers to experimentally validate their controller designs. This raises the question: "What can we accomplish if all we have is a very complex Simulink model of a control system?" In this talk, we give an example of a simulation-guided formal technique that can help characterize temporal properties of the system, or guide the search for design behaviors that do not conform to "good behavior". Specifically, we present a way to algorithmically mine temporal assertions from a Simulink model. The input to our algorithm is a requirement template expressed in Parametric Signal Temporal Logic -- a formalism to express temporal formulas in which concrete signal or time values are replaced by parameters. Our algorithm is an instance of counterexample-guided inductive synthesis: an intermediate candidate requirement is synthesized from simulation traces of the system, which is refined using counterexamples to the candidate obtained with the help of a falsification tool. The algorithm terminates when no counterexample is found. Mining has many usage scenarios: mined requirements can be used to validate future modifications of the model, they can be used to enhance understanding of legacy models, and can also guide the process of bug-finding through simulations.

Precise flow- and context-sensitive pointer analysis (FCPA) is generally considered prohibitively expensive for arge programs; most tools relax one or both of the requirements for scalability. We argue that precise FCPA has been over-harshly judged---the vast majority of points-to pairs calculated by existing algorithms are never used by any client analysis or transformation because they involve dead variables. We therefore formulate a FCPA in terms of a joint points-to and liveness analysis which we call L-FCPA.

Our analysis computes points-to information only for live pointers and its propagation is sparse (restricted to live ranges of respective pointers). Further, our analysis uses strong liveness, effectively including dead code elimination. It calculates must-points-to information from may-points-to information afterwards instead of using a mutual fixed-point, and uses value-based termination of call strings during interprocedural analysis (which reduces the number of call strings significantly).

We implemented a naive L-FCPA in GCC-4.6.0 using linked lists. Evaluation on SPEC2006 showed significant increase in the precision of points-to pairs compared to GCC's analysis. Interestingly, our naive implementation turned out to be faster than GCC's analysis for all programs under 30kLoC. Further, L-FCPA showed that fewer than 4% of basic blocks had more than 8 points-to pairs. We conclude that the usable points-to information and the required context information is small and sparse and argue that approximations (e.g. weakening flow or context sensitivity) are not only undesirable but also unnecessary for performance.

Synthesis methods automatically construct a system, or an individual component within a system, such that the result satisfies a given specification. The synthesis procedure must take into account the component's interface and deliver implementations that comply with its limitations. For example, what a component can observe about its environment may be restricted by imprecise sensors or inaccessible communication channels. In addition, sufficiently precise models of a component's environment are typically infinite-state, for example due to modeling real time or unbounded communication buffers. In this talk I will present synthesis methods for infinite-state systems with partial observability. First, I will describe a technique for automatic generation of observation predicates (clock constraints) for timed control with safety requirements. Finding the right observations is the main challenge in timed control with partial observability. Our approach follows the Counterexample-Guided Abstraction Refinement scheme, i.e., it uses counterexamples to guide the search. It employs novel refinement techniques based on interpolation and model generation. Our approach yields encouraging results, demonstrating better performance than brute-force enumeration of observation sets, in particular for systems where a fine granularity of the observations is necessary. Second, I will outline a synthesis algorithm for Lossy Channel Systems (LCSs) with partial observability and safety specifications. The algorithm uses an extension of the symbolic representation common for backward analysis of LCSs. Its termination relies on the fact that LCSs are better-quasi ordered systems.

Computer systems sometimes need to release some confidential information. However, they must also prevent inadvertent release of information that should remain confidential. These requirements significantly complicate reasoning about system security, and are not addressed by conventional security mechanisms. To provide assurance for such systems we need to develop principled approaches for specifying and enforcing secure information release. In this talk, I will describe how this can be achieved using systems and programming languages techniques.

The first part of the talk will focus on controlling inadvertent leaks in complex systems. I will discuss the leaks that happen when an adversary can measure the time at which a system performs an observable action, also known as timing channels. I will explain how timing channels present a serious threat in computer security, and introduce predictive mitigation---a general technique for mitigating timing channels that works by predicting timing from past behavior and public information. Rather than eliminating timing channels entirely, predictive mitigation bounds the amount of information that an adversary can learn via timing channels with a trade-off in system performance. Under reasonable assumptions, the bounds are logarithmic in the running time of the system.

The second part of the talk will present insights into the formalization of practical security specifications for the intentional release of confidential information. I will introduce a programming language-based framework that provides a formal vocabulary for expressing such specifications. Example specifications include what information may be released, when a release may happen, and whether an adversary has any control over a release. These specifications are soundly enforceable using a variety of static and dynamic program analyses.

I will first outline a series of research results on verifying shared-variable concurrent programs, including techniques for predicate abstraction for such programs, and how to check the resulting concurrent Boolean programs. I will then elaborate on two recent results on supporting weak memory consistency (ESOP and CAV 2013, respectively).

We increasingly depend on Internet connectivity and performance for services ranging from telephony and video streaming to home monitoring and remote health care. However, hardware failures, misconfigurations, and software bugs frequently cause outages and other performance problems that disrupt these services. Existing tools provide network operators with only limited visibility into these problems and few options to address them. The result is that debugging Internet problems is often a slow, manual process. In this talk, I discuss how we can improve Internet reliability by enabling better tools for detecting, isolating, and repairing network problems as they occur. First, I discuss a system for crowdsourcing network monitoring to end. By leveraging the network view from applications running on a large number of hosts, we can efficiently detect network problems that impact end-to-end performance. Second, I describe a system for isolating the network responsible for a problem. To address this, we develop new tools that allow an ISP to identify the root cause even when portions of the Internet are unreachable. Third, I present an approach for automatically repairing isolated network problems. This allows an ISP to use existing routing protocols in novel ways to cause other networks to avoid problems, thus restoring normal connectivity.

With the advent of multiprocessor systems, it is now the role of the programmers to explicitly expose parallelism and take advantage of parallel computing resources. However, parallel programming is inherently complex as programmers have to reason about all possible thread interleavings. A deterministic replay system that records and reproduces the execution of parallel programs can serve as a foundation for building many useful tools (e.g., time-travel debugger, fault tolerance system, etc.) by overcoming the inherent non-determinism in multiprocessor systems. While it is well known how to replay uniprocessor systems, it is much harder to provide deterministic replay of shared memory multithreaded programs on multiprocessors because shared memory accesses add a high-frequency source of non-determinism. I introduce a new insight to deterministic replay that it is sufficient for many replay uses to guarantee only the same output and the final states between the recorded and replayed executions, and thus it is possible to support replay without logging precise shared-memory dependencies. I call this relaxed but sufficient replay guarantee "external determinism" and leverage this observation to build efficient multiprocessor replay systems. In this talk, I will introduce two replay systems: Respec and Chimera. Respec enables software-only deterministic replay at low overhead with operating system support. Chimera leverages static data-race analysis to build an efficient software-only replay solution.

User authentication is a critical part of many systems.  As strong cryptography has become widespread and vulnerabilities in systems become harder to find and exploit, attackers are turning toward user authentication as a potential avenue for compromising users.  Unfortunately, user authentication on the web has remained virtually unchanged since the invention of the Internet.  I will present three systems that attempt to strengthen user authentication, and its close cousin authorization, on the web while being practical for developers, usable for users, and secure against attackers.  First, I will discuss Origin Bound Certificates -- a mechanism for tweaking Transport Layer Security (TLS) that can then be used to strongly strengthen the authentication of HTTP requests by binding cookies (or other tokens) to a client certificate.  This renders stolen cookies unusable by attackers. Second, I will present PhoneAuth, a system for protecting password-based login by opportunistically providing cryptographic identity assertions from a user's mobile phone while maintaining a simple and usable authentication experience.  Third, I will describe ongoing research into how a class of web vulnerabilities called Cross-Site Request Forgeries (CSRFs) can be fundamentally prevented using Allowed Referrer Lists.  I'll discuss the next big challenges in user authentication and conclude with several examples of where authentication matters beyond the web.

I will cover a couple of my recent contributions to secure localization and distance bounding. Distance bounding protocols have been proposed for many security critical applications as a means of getting an upper bound on the physical distance to a communication partner. I will show some practical examples of problems where distance bounding can provide a unique solution to problems which are otherwise difficult to solve. One such example is in the context of implantable medical devices.

One of the main obstacles for the wider deployment of distance bounding using electromagnetic (radio) waves, is the lack of hardware platforms that implement and support these protocols. I will show the first prototype system that demonstrates that radio distance bounding protocols can be implemented to match the strict requirements on processing time, that these protocols require. Our system implements a radio that is able to receive, process and transmit signals in less than 1ns.

Finally I will present an area where I see a great potential for future work. In both sensing and actuation applications there is a semantic gap between the electrical system and the physical world. In an adversarial setting this gap can be exploited to make a system believe that, e.g., a switch was activated, when in fact it wasn't. there is a plethora application domains that share this problem, from bio-medical sensors and implantable medical devices to factory control systems and security critical infrastructures. Some of these challenges can be solved using a traditional cryptographic approach, and some are highly interdisciplinary, and will best be handled in collaboration with experts from other fields.

Some cloud storage services, like Windows Azure, replicate data while providing strong consistency to their clients while others, like Amazon, have chosen eventual consistency in order to obtain better performance and availability. A broader class of consistency guarantees can, and perhaps should, be offered to clients that read shared data. During a baseball game, for example, different participants (the scorekeeper, umpire, sportswriter, and so on) benefit from six different consistency guarantees when reading the current score. Eventual consistency is insufficient for most of the participants, but strong consistency is not needed either.

We rely on a computational infrastructure that is a densely intertwined mass of software and hardware: programming languages, network protocols, operating systems, and processors. It has accumulated great complexity, from a combination of engineering design decisions, contingent historical choices, and sheer scale, yet it is defined at best by prose specifications, or, all too often, just by the common implementations. Can we do better? More specifically, can we apply rigorous methods to this mainstream infrastructure, taking the accumulated complexity seriously, and if we do, does it help? My colleagues and I have looked at these questions in several contexts: the TCP/IP network protocols with their Sockets API; programming language design, including the Java module system, the C11/C++11 concurrency model, and the C programming language; the hardware concurrency behaviour of x86, IBM POWER, and ARM multiprocessors; and compilation of concurrent code.

In this talk I will draw some lessons from what did and did not succeed, looking especially at the empirical nature of some of the work, at the social process of engagement with the various different communities, and at the mathematical and software tools we used. Domain-specific modelling languages (based on functional programming ideas) and proof assistants were invaluable for working with the large and loose specifications involved: idioms within HOL4 for TCP, our Ott tool for programming language specification, and Owens's Lem tool for portable semantic definitions, with HOL4, Isabelle, and Coq, for the relaxed-memory concurrency semantics work. Our experience with these suggests something of what is needed to make mathematically rigorous engineering of mainstream computer systems (and in systems research) a commonplace reality.

In this talk I present our recent results on data-aware static verification, in which we select the artifact-centric model as a natural vehicle for our investigation. Artifact-centric systems are models for business process systems in which the dynamics and the manipulation of data are equally central. Given the family of variations on this model found in the literature, for the sake of a uniform terminology we introduce our own pristine formalization, which captures existing artifact-centric dialects, and which is semantically equivalent to the most expressive ones. We call our business process formalism ``Data-Centric Dynamic Systems'' (DCDS). The process is described in terms of atomic actions that evolve the system. Action execution may involve calls to external services, thus inserting fresh data into the system. As a result such systems are infinite-state. We show that verification is undecidable in general, and we isolate notable cases where decidability is achieved. More specifically, we show that in a first-order $\mu$-calculus variant that preserves knowledge of objects appeared along a run, we get decidability under the assumption that the fresh data introduced along a run are bounded, though they might not be bounded in the overall system. Then, we investigate decidability under the assumption that knowledge of objects is preserved only if they are continuously present. We show that if infinitely many values occur in a run but do not accumulate in the same state, then we get again decidability. We give syntactic conditions to avoid this accumulation through the novel notion of ``generate-recall acyclicity'', which ensures that every service call activation generates new values that cannot be accumulated indefinitely. We believe that DCDSs are natural and expressive models for systems powered by an underlying database (i.e., so called data-centric systems), and thus are an ideal vehicle for foundational research with potential to transfer to alternative models.

When constructing complex concurrent and distributed systems, abstraction is vital: programmers should be able to reason about system components in terms of abstract specifications that hide the implementation details. Nowadays such components often provide only weak consistency guarantees about the data they manage: in shared-memory systems because of the effects of relaxed memory models, and in distributed systems because of the effects of replication. This makes existing notions of component abstraction inapplicable. In this talk I will describe our ongoing effort to specify consistency guarantees provided by modern shared-memory and distributed systems in a uniform framework and to propose notions of abstraction for components of such systems. I will illustrate our results using the examples of the C/C++ memory model and eventually consistent distributed systems. This is joint work with Mark Batty (University of Cambridge), Sebastian Burckhardt (Microsoft Research), Mike Dodds (University of York) and Hongseok Yang (University of Oxford).

The Deep Web has enabled the availability of a huge amount of useful information and people have come to rely on it to fulfill their information needs in a variety of domains. We present a recent study on the accuracy of data and the quality of Deep Web sources in two domains where quality is important to people's lives: Stock and Flight. We observe that, even in these domains, the quality of the data is less than ideal, with sources providing conflicting, out-of-date and incomplete data. Sources also copy, reformat and modify data from other sources, making it difficult to discover the truth. We describe techniques proposed in the literature to solve these problems, evaluate their strengths on our data, and identify directions for future work in this area.

Most caching DNS resolvers still rely for their security, against poisoning, on validating that the DNS responses contain some ‘unpredictable’ values, copied from the request. These values include the 16 bit identifier field, and other fields, randomised and validated by different ‘patches’ to DNS. We investigate the prominent patches, and show how off-path attackers can circumvent all of them, exposing the resolvers to cache poisoning attacks. We present countermeasures preventing our attacks; however, we believe that our attacks provide additional motivation for adoption of DNSSEC (or other MitM-secure defenses). We then investigate vulnerabilities in DNSSEC configuration among resolvers and zones, which reduce or even nullify the protection offered by DNSSEC. Finally we provide our recommendations and countermeasures to prevent the vulnerabilities.

Modern computer networks perform a bewildering array of tasks, from routing and traffic monitoring, to access control and server load balancing. Moreover, historically, managing these networks has been hideously complicated and error-prone, due to a heterogeneous mix of devices (e.g., routers, switches, firewalls, and middleboxes) and their ad hoc, closed and proprietary configuration interfaces. Software-Defined Networking (SDN) is poised to change this state of affairs by offering a clean, simple and open interface between network devices and the software that controls them. In particular, many commercial switches now support the OpenFlow protocol, and a number of campus, data-center, and backbone networks have deployed the new technology.

However, while SDN makes it possible to program the network, it does not make it easy: The first generation of SDN controllers offered application developers the "assembly language" of network programming platforms. To reach SDN’s full potential, research in programming languages and compilers is desperately needed. In this talk, I discuss our work to date in this area, which revolves around the design of a language, compiler and run-time system for SDN programming. The language, called Frenetic, allows programmers to work declaratively, specifying the behavior of a network at a high level of abstraction. The compiler and run-time system take care of the tedious details of compiling and implementing these high-level policies using the OpenFlow protocol.

A key strength of the Frenetic design is its support for modular programming: Complex network applications can be decomposed in to logical subcomponents --- an access control policy, a load balancer, a traffic monitor --- and coded independently. Frenetic's rich combinator library makes it possible to stitch such components back together to form a fully functioning whole. Frenetic also contains carefully designed operators that help users transition from one global, high-level network policy to the next while preserving key network invariants. Overall, Frenetic's abstractions make it dramatically easier for programmers to write and reason about SDN applications.

Today's scientific processes heavily depend on fast and accurate analysis of experimental data. Scientists are routinely overwhelmed by the effort needed to manage the volumes of data produced either by observing phenomena or by sophisticated simulations. As database systems have proven inefficient, inadequate, or insufficient to meet the needs of scientific applications, the scientific community typically uses special-purpose legacy software. When compared to a general-purpose data management system, however, application-specific systems require more resources to maintain, and in order to achieve acceptable performance they often sacrifice data independence and hinder the reuse of knowledge. With the exponential growth of dataset sizes, data management technology are no longer luxury; they are the sole solution for scientific applications.

I will discuss some of the work from teams around the world and the requirements of their applications, as well as how these translate to challenges for the data management community. As an example I will describe a challenging application on brain simulation data, and its needs; I will then present how we were able to simulate a meaningful percentage of the human brain as well as access arbitrary brain regions fast, independently of increasing data size or density. Finally I will present some of the data management challenges that lie ahead in domain sciences, and will introduce NoDB, a new query processor which explores raw, never-before-seen data in-situ, using full querying power.

Every time you touch a computer, you leave a trace. Sensitive information about you can be found in the remnants of visited websites and voice-over-IP conversations on your machine; in the allegedly "de-identified" data about your purchases, preferences, and social relationships collected by advertisers and marketers; and, in the not-too-distant future, in the video and audio feeds gathered by sensor-based applications on mobile phones, gaming devices, and household robots.

This talk will describe several research systems developed at UT Austin that aim to provide precise privacy guarantees for individual users. These include (1) the Airavat system for differentially private data analysis, (2) the "Eternal Sunshine of the Spotless Machine" system that runs full-system applications in private sessions and then erases all memories of their execution from the host, and (3) "A Scanner Darkly" system that adds a privacy protection layer to popular vision and image processing libraries, preserving the functionality of sensor-based applications but preventing them from collecting raw images of their users.

SecGuru is a tool for automatically validating network connectivity restriction policies in large-scale data centers. The problem solved by SecGuru is acute in data centers offering public cloud services where multiple tenants are hosted in customized isolation boundaries. Our tool supports the following interactions: (1) given a policy and a contract verify that the policy satisfies the contract (2) provide a semantic difference between policies. The former facilitates property checking and the latter facilitates identifying configuration drifts. We identify bit-vector logic as a suitable basis for policy analysis and use the Z3 theorem prover to solve these constraints. We furthermore develop algorithms for compact enumeration of differences for bit-vector constraints. Finally, we evaluate SecGuru on large scale production services where it has been used to identify and fix numerous configuration errors.

In this talk, I'll argue for sophisticated automated reasoning capabilities as a first-class OS service. With such a service, one can delegate many OS policy decisions and calculations to a component which is highly flexible, expressive, and dynamic, providing considerable advantages of hard-coding such functionality in C or scripts. Modern operating systems face several engineering challenges: hardware is increasingly complex, increasingly diverse, and evolving rapidly. This, combined with parallel workloads having complex performance interactions with hardware make it hard to build a simple OS kernel which delivers good performance for a variety of platforms and workloads.

As a first step, we decided to tackle this head-on by building a reasoning engine as a first class service (the "System Knowledge Base") in the Barrelfish OS, borrowing ideas from such fields as knowledge representation, constraint satisfaction, logic programming, and optimization. Doing so was not without problems, but we found it highly convenient in a number of widely different application areas - for example PCI programming, process coordination, spatial scheduling, and message routing. I'll discuss several of these, and how the structure of the OS as a whole changes when a facility like the SKB is available Finally, I'll talk about some future directions, in particularly with embedded devices such as SoCs.

We present Expositor, a new debugging environment that combines scripting and time-travel debugging to allow developers to automate complex debugging tasks. The fundamental abstraction provided by Expositor is the execution trace, which is a time-indexed sequence of program state snapshots. Developers can manipulate traces as if they were simple lists with operations such as map and filter. Under the hood, Expositor efficiently implements traces as lazy, sparse interval trees, whose contents are materialized on demand. Expositor also provides a novel data structure, the edit hash array mapped trie, which is a lazy implementation of sets, maps, multisets, and multimaps that enables developers to maximize the efficiency of their debugging scripts. We have used Expositor to debug a stack overflow and to unravel a subtle data race in Firefox. We believe that Expositor represents an important step forward in improving the technology for diagnosing complex, hard-to-understand bugs. This is joint work with Yit Phang Khoo and Jeff Foster, both at Maryland

Software systems should be robust, reliable, and predictable. Today, we routinely reason about the runtime behavior of software using formal systems such as type systems or logics for access control or information flow to establish safety and liveness properties.

In this talk, I will survey Beluga, a dependently typed programming and proof environment. It supports specifying formal systems in the logical framework LF and directly supports common and tricky routines dealing with variables, such as capture-avoiding substitution and renaming. Moreover, Beluga allows embedding LF objects together with their context in programs and types supporting inductive and coinductive definitions. I will discuss how to write inductive and coinductive proofs about LF specifications using three different examples: type uniqueness, normalization by evaluation, and the fact that evaluating a lambda-term cannot yield a value and diverge at the same time. Taken together these examples demonstrate the elegance and conciseness of Beluga for specifying, verifying and validating safety properties.

Software-Defined Networking (SDN) promises to enable vigorous innovation, through separation of the control plane from the data plane, and to enable novel forms of network management, through a controller that uses a global view to make globally-valid decisions. The design of SDN controllers creates novel challenges; much previous work has focussed on making them scalable, reliable, and efficient.

We argue that, to control a realistic network, we do not want one monolithic SDN controller. Instead, we want to compose the effects of many controller modules managing different aspects of the network, which may be competing for resources. Each module will try to optimize one or more objectives; we address the challenge of how to coordinate between these modules to optimize an overall objective function. Our framework design, Corybantic, focusses on achieving both modular decomposition and maximizing the overall value delivered by the controller's decisions.

Decentralized approaches spanning multiple administrative domains (MAD) are an increasingly effective way to deploy services. Popular examples include peer-to-peer (p2p) applications, content distribution networks, and mesh routing protocols. Cooperation lies at the heart of these services. Yet, when working together is crucial, a natural question is: "What if users stop cooperating?" After all, users in a MAD system are vulnerable not only to the failure of some of the equipment in the system, or to the possibility that some users may behave maliciously, but also to the possibility that users may selfishly refrain from sharing their resources as the protocol would require. In this setting, it is hard to put a bound on the number of components in the systems that deviate from their correct specification. Is it still possible under such circumstances to build systems that not only provide provable guarantees in terms of their safety and liveness properties but also yield practical performance?

Malicious software (malware) is an important threat and root cause of many security problems on the Internet. In this talk, I will discuss our recent efforts on malware analysis, detection, and mitigation. First, I will introduce our infrastructure to collect and analyze malicious code samples. Then, I will present techniques to improve the quality of the results produced by automated, dynamic malware analysis systems. Finally, I will discuss ways in which these results can be leveraged for the detection and mitigation of malicious code.

A fundamental belief underlying forty years of programming languages research, aptly captured by the slogan "Well-typed programs can't go wrong", is that programs augmented with machine-checked annotations are more likely to be free of bugs. But of course, real programs do wrong and programmers are voting with their feet. Dynamic languages such as Ruby, Python, Lua, JavaScript and R are unencumbered by redundant type annotations and are increasingly popular. JavaScript, the lingua franca of the web, is moving to the server with the success of Node.js. R, another dynamic language, is being used in statistics, biology and finance for data analysis and visualization. Not only are these languages devoid of types, but they utterly lack any static structure that could be used for program verification. This talk will draw examples from recent results on JavaScript and R to illustrate the extent of the problem and propose some directions for research.

Embedded systems are increasingly used in circumstances where people's lives or valuable assets are at stake, hence they should be trustworthy - safe, secure, reliable. True trustworthiness can only be achieved through mathematical proof of the relevant properties. Yet, real-world software systems are far too complex to make their formal verification tractable in the foreseeable future. The Trustworthy Systems project at NICTA has formally proved the functional correctness as well as other security-relevant properties of the seL4 microkernel. This talk will provide an overview of the principles underlying seL4, and the approach taken in its design, implementation and formal verification. It will also discuss on-going activities and our strategy for achieving the ultimate goal of system-wide security guarantees.

Opportunistic networks exploit human mobility and consequent device-to-device ad hoc contacts to disseminate content in a "store-carry-forward" fashion. In opportunistic networks, disconnections and highly variable delays caused by human mobility are the norm. Another major challenge in opportunistic communications arises from the small form factor of mobile devices which introduces resource limitations compared to static computing systems. Lastly, human mobility and social interactions have a large impact on the structure and performance of opportunistic networks, hence, understanding these phenomena is crucial for the design of efficient algorithms and applications.

In this work, we take an experimental approach to better understand opportunistic mobile social networks. We design and implement of MobiClique, a communication middleware for opportunistic mobile social networking. MobiClique takes advantage of user mobility and social relationships to forward messages in an opportunistic manner. We perform a large-scale MobiClique experiment with 76 people, where we collect social network information (i.e. their Facebook profiles), and ad hoc contact and communication traces. We use the collected data with three other data sets to analyse in detail the time-varying structure and epidemic content dissemination in opportunistic networks. Most of the related works have focused on the pairwise contact history among users in conference or campus environments. We claim that given the density of these networks, this approach leads to a biased understanding of the content dissemination process. We design a methodology to break the contact traces down into "temporal communities", i.e., groups of people who meet periodically during an experiment. We show that these communities correlate with people's social communities. As in previous works, we observe that efficient content dissemination is mostly due to high contact rate users. However, we show that high contact rate users that are more frequently involved in temporal communities contribute less to the dissemination process, leading us to conjecture that social communities tend to limit the efficiency of content dissemination in opportunistic mobile social networks.

Digital signatures can be seen as the digital equivalent of handwritten signatures, and are considered one of the most important cryptographic primitives. At a high level, they allow a user Alice to authenticate a digital document by generating a piece of information, that is the signature, using a secret key which is known only by her. Any other user who gets a matching public verification key can check the validity of such signature and thus be convinced that it was generated by Alice. Digital signatures are required to satisfy the most natural security property one could expect: no one, except who knows the secret key, should be able to generate valid signatures. In the quest of mimicking in the digital world what we are used to do in the real world, an interesting question naturally arises: can Alice delegate the signing process (on a restricted set of messages) to third parties without having to reveal to them her secret key? A positive answer to this question has been recently given by Boneh et al. (PKC 2009) by means of homomorphic signatures.

In the first part of my talk, I will present the notion of homomorphic signatures: I will describe important applications which motivate the study of this primitive, and I will survey recent results of mine that propose efficient constructions.

In the second part of the talk I will move the focus to a related, but more general and intriguing question: can we sign computation? Are there means to certify that a program has been run correctly and/or on the correct inputs? These and similar questions are nowadays arising in the context of cloud computing applications in which users want to delegate computation and memory to third parties that are called cloud providers. I will describe relevant security issues emerging from these applications, and will discuss how cryptography can help to solve such problems.

During my presentation I will also mention the usual approaches underlying the process of designing cryptographic protocols, with a particular emphasis on how theory and practice can interact in a significant way.

The talk is mainly based on the following works joint with Dario Catalano, Rosario Gennaro and Bogdan Warinschi. - D. Catalano, D. Fiore and B. Warinschi. Adaptive Pseudo-Free Groups and Applications. EUROCRYPT 2011 - D. Catalano, D. Fiore and B. Warinschi. Efficient Network Coding Signatures in the Standard Model. PKC 2012 - D. Fiore and R. Gennaro. Publicly Verifiable Delegation of Large Polynomials and Matrix Computations, with Applications. Pre-print (May 2012): http://eprint.iacr.org/2012/281

This paper presents the first real-time multiprocessor locking protocol that supports fine-grained nested resource requests. This locking protocol relies on a novel technique for ordering the satisfaction of resource requests to ensure a bounded duration of priority inversions for nested requests. This technique can be applied on partitioned, clustered, and globally scheduled systems in which waiting is realized by either spinning or suspending. Furthermore, this technique can be used to construct fine-grained nested locking protocols that are efficient under spin-based, suspension-oblivious or suspension-aware analysis of priority inversions. Locking protocols built upon this technique perform no worse than coarse-grained locking mechanisms, while allowing for increased parallelism in the average case (and, depending upon the task set, better worst-case performance).

Database transformations (queries, views, mappings) take apart, filter,and recombine source data in order to populate warehouses, materialize views,and provide inputs to analysis tools. As they do so, applications often need to track the relationship between parts and pieces of the sources and parts and pieces of the transformations' output. This relationship is what we call database provenance.

This talk presents an approach to database provenance that relies on two observations. First, provenance is a kind of annotation, and we can develop a general approach to annotation propagation that also covers other applications, for example to uncertainty and access control. In fact, provenance turns out to be the most general kind of such annotation,in a precise and practically useful sense. Second, the propagation of annotation through a broad class of transformations relies on just two operations: one when annotations are jointly used and one when they are used alternatively.This leads to annotations forming a specific algebraic structure, a commutative semiring.

The semiring approach works for annotating tuples, field values and attributes in standard relations, in nested relations (complex values), and for annotating nodes in(unordered) XML. It works for transformations expressed in the positive fragment of relational algebra, nested relational calculus, unordered XQuery, as well as for Datalog, GLAV schema mappings, and tgd constraints. Finally, when properly extended to semimodules it works for queries with aggregates. Specific semirings correspond to earlier approaches to provenance, while others correspond to forms of uncertainty, trust, cost, and access control.

This is joint work with Y. Amsterdamer, D. Deutch, J.N. Foster, T.J. Green, Z. Ives, and G. Karvounarakis, done in part within the frameworks of the Orchestra and pPOD projects.

Being a personal device that is constantly online, the mobile device will revolutionize social computing. We will be able to share multimedia and interact freely with any of our different circles of friends, colleagues, and families, without being confined to closed proprietary social networks and without having our communication intermediated by third-parties. We believe this openness will lead to an explosion of social apps in new categories including health, finance, and corporate.

We have started the revolution with the first of such a system called Musubi. Musubi is a real-time, multimedia group chat app that allows users to control all their data. It is also an open app platform that lets apps be easily created and spread virally among friends. Musubi is built on top of an egocentric social platform where identity-based cryptography is used to allow individuals communicate securely with each other without the friction of key exchange. It provides an innovative identity firewall that supports social apps without users giving up friends' data to the app creators.

Musubi Beta and a number of social apps are already available in the Google Play Store. We invite you to give us feedback on the apps and to join us in creating an open mobile social internet.

Unique Identification Authority of India (UIDAI) has been setup by the Govt. of India with a mandate to issue a unique identification number to all the residents in the country. UIDAI proposes to create a platform to first collect the identity details and then to perform authentication that can be used by several government and commercial services providers. A key requirement of the UID system is to minimize/eliminate duplicate identity in order to improve the efficacy of the service delivery. UIDAI has selected biometrics feature set as the primary method to check for duplicate identity. In order to ensure that an individual is uniquely identified in an easy and cost-effective manner, it is necessary to ensure that the captured biometric information is capable of carrying out the de-duplication at the time of collection of information. For government and commercial providers to authenticate the identity at the time of service delivery, it is necessary that the biometric information capture and transmission are standardized across all the partners and users of the UID system.

UID provides, online, cost-effective, ubiquitous authentication services across the country and establishes identity. Authentication is transactional and to be done at the time of availing a benefit.

The objective of the UIDAI is to provide a robust, reusable ID to those who do not have any ID proof, cleaning up existing databases of multiple and fake entries through Uniqueness and to improve targeting and delivery of services. It will also reduce the cost of delivery of services.

Scalable content personalization and profiling is a key tool for the internet. In this talk I will illustrate based on three problems how this can be achieved. More specifically I will show how hashing can be used to deal with compactly representing enormous amounts of parameters, how distributed latent variable inference can be used for user profiling, and how session modeling provides an attractive alternative to ranking.

Credit networks represent a way of modeling trust between entities in a network. Nodes in the network print their own currency and trust each other for a certain amount of each other's currency. This allows the network to serve as a decentralized payment infrastructure---arbitrary payments can be routed through the network by passing IOUs along a chain of trusting nodes in their respective currencies---and obviates the need for a common currency. Thus, credit networks are a decentralized approach based on trust to enable interactions between untrusting individuals in internet based networks and markets.

We will first analyze the liquidity, i.e. the ability to route transactions, in credit networks in terms of the long term failure probability of transactions for various network topologies and credit values. We will show that under symmetric transaction rates, the transaction failure probability in a number of credit network topologies is comparable to that in equivalent centralized currency systems; thus we do not lose much liquidity in return for their robustness and decentralized properties. This is based on joint work with Ashish Goel, Ramesh Govindan and Ian Post which appeared in EC'11.

Next we will analyze the formation of credit networks when agents strategically decide how much credit to extend each other under different models of risk. When each agent trusts a fixed set of other agents, and transacts directly only with those it trusts, the formation game is a potential game and all Nash equilibria are social optima. Moreover, the Nash equilibria of this game are equivalent in a very strong sense: the sequences of transactions that can be supported from each equilibrium credit network are identical. However, when we allow transactions over longer paths, the game may not admit a Nash equilibrium, and the price of anarchy is unbounded. When agents have a shared belief about the trustworthiness of each agent, the networks formed in equilibrium have a star-like structure. Though the price of anarchy is unbounded, myopic best response quickly converges to a social optimum. This is based on joint work with Ashish Goel, Michael Wellman and Bryce Wiedenbeck to be presented at WWW'12.

Despite the incredible market penetration of smartphones and exponential growth of the app market, utility of smartphones has been and will remain severely limited by the battery life. As such, energy has increasingly become the scarcest resource on smartphones that critically affects user experience. In this talk, I will start with a first study that characterizes smartphone energy bugs, or ebugs, broadly defined as errors in the system (apps, OS, hardware, firmware, or external conditions) that result in unexpected smartphone battery drainage and leads to significant user frustrations.

As a first step towards taming ebugs, we built the first fine-grained energy profiler, eprof, that performs energy accounting and hence answers the very question "where was the energy spent in the app?" at the per-routine, per-thread, and per-process granularity. Building eprof in turn requires a fine-grained, online power model which we have developed that captures the unique asynchronous power behavior of modern smartphones. Using eprof, we dissected the energy drain of some of the most popular apps in Android Market and discovered ebugs in popular apps like Facebook.

While essential, eprof only provides a semi-automatic tool for energy debugging. The "holy grail" in energy debugging in smartphones is to develop fully automatic debugging techniques and tools, which can draw synergies from many areas of computer science including OS, PL, compilers, machine learning, HCI, etc. I will present the first automatic ebug detection technique based on static compiler analysis for detecting "no-sleep" energy bugs, the most notorious category of energy bugs found in smartphone apps.

We present the first Internet architecture designed to provide route control, failure isolation, and explicit trust information for end-to-end communications. SCION separates ASes into groups of independent routing sub-planes, called trust domains, which then interconnect to form complete routes. Trust domains provide natural isolation of routing failures and human misconfiguration, give endpoints strong control for both inbound and outbound traffic, provide meaningful and enforceable trust, and enable scalable routing updates with high path freshness. As a result, our architecture provides strong resilience and security properties as an intrinsic consequence of good design principles, avoiding piecemeal add-on protocols as security patches. Meanwhile, SCION only assumes that a few top-tier ISPs in the trust domain are trusted for providing reliable end-to-end communications, thus achieving a small Trusted Computing Base. Both our security analysis and evaluation results show that SCION naturally prevents numerous attacks and provides a high level of resilience, scalability, control, and isolation.

Cloud computing promises virtually unlimited scalability and high availability at low cost. However, it is commonly believed that a system's consistency must be relaxed in order to achieve these properties. We evaluated existing commercial cloud offerings for transactional workloads and found that consistency is indeed expensive and limits scalability in these systems.  Because of these costs, many systems designers have chosen to provide only relaxed consistency guarantees, if any, making such systems inappropriate for many mission-critical applications. This dichotomy is based on unrealistically pessimistic assumptions about Big Data environments. First, it assumes that consistency is an all or nothing decision that must be applied uniformly to all data in a system. Secondly, even in situations where strong consistency is required, previous transaction commit protocols were based on worst-case assumptions regarding the likelihood of conflicts.  In this talk, I will describe two techniques that build on a more nuanced view of consistency requirements and the costs of maintaining them.

I will first describe Consistency Rationing, which builds on inventory holding models used in Operations Research to help classify and manage data based on their consistency requirements. Consistency Rationing exploits the fact that for some data the cost of maintaining consistency outweighs the benefit obtained by avoiding inconsistencies. In the second part of the talk, I will present a new optimistic commit protocol for the wide-area network. For a long time, synchronized wide-area replication was considered to be infeasible with strong consistency. With MDCC, I will show how we can achieve strong consistency with similar response-time guarantees as eventual consistency in the normal operational case. This work was done as part of a larger project around Big Data management. At the end of the talk, I will provide an overview of some of my other projects and give an outline for future work.

It seems to be generally accepted that designing correct and efficient concurrent software is a sophisticated task that can only be held by experts. A crucial challenge then is to convert sequential code produced by a ``mainstream'' programmer into concurrent one. Various synchronization techniques may be used for this, e.g., locks or transactional memory, but what does it mean for the resulting concurrent implementation to be correct? And which synchronization primitives provide more efficiency at the end?

We introduce a correctness criterion for a transformation that enables the use of a sequential data structure in a concurrent system. We then evaluate the performance of resulting concurrent implementations in terms of the sets of concurrent schedules (interleavings of steps of the sequential code) they accept. Intuitively, this captures the amount of concurrency that a given implementation can stand. This allows us to analyze relative power of seemingly different synchronization techniques, such as various forms of locking and transactional memory

What effect does language have on people, and what effect do people have on language? The answers to these questions can help shape the future of social-media systems by bringing a new understanding of communication and collaboration between users.

I will describe two of my efforts to address these fundamental problems computationally, exploiting very large-scale textual and social data. The first project uncovers previously unexamined contextual biases that people have when determining which opinions to focus on, using Amazon.com helpfulness votes on reviews as a case study to evaluate competing theories from sociology and social psychology. The second project leverages insights from psycho- and socio-linguistics and embeds them into a novel computational framework in order to provide a new understanding of how key aspects of social relations between individuals are embedded in (and can be inferred from) their conversational behavior. In particular, I will discuss how power differentials between interlocutors are subtly revealed by how much one individual immediately echoes the linguistic style of the person they are responding to.

This talk includes joint work with Susan Dumais, Michael Gamon, Jon Kleinberg, Gueorgi Kossinets, Lillian Lee and Bo Pang.

The focus of my research is on enabling novel kinds of interaction between the user and the information in a variety of digital environments, ranging from social content sites, to digital libraries, to the Web. In this talk, I will give an overview of my research, and will then present two recent lines of work that focus on information discovery in two important application domains.

In the first part of this talk, I will present an approach for tracking and querying fine-grained provenance in data-intensive workflows. A workflow is an encoding of a sequence of steps that progressively transform data products. Workflows help make experiments reproducible, and may be used to answer questions about data provenance -- the dependencies between input, intermediate, and output data. I will describe a declarative framework that captures fine-grained dependencies, enabling novel kinds of analytic queries, and will demonstrate that careful design and leveraging distributed processing make tracking and querying fine-grained provenance feasible.

In the second part of this talk, I will discuss personalized search and ranking on the Social Web. Social Web users provide information about themselves in stored profiles, register their relationships with other users, and express their preferences with respect to information and products. I will argue that information discovery should account for a user's social context, and will present network-aware search – a novel search paradigm in which result relevance is computed with respect to a user's social network. I will describe efficient algorithms appropriate for this setting, and will show how social similarities between users may be leveraged to make processing more efficient.

Current trends have seen data grow larger, more intertwined, and more diverse, as more and more users contribute to and use it. This trend has given rise to the need to support richer data analysis tasks. Such tasks involve determining the causes of observations, finding and correcting the sources of error in query results, as well as modifying the data in order to make it conform to complex desirable properties.

In this talk I will discuss three challenges: (a) providing explanations through support for causal queries ("Why"), (b) tracing and correcting errors at their source (post-factum data cleaning), and (c) integrating database systems with constrained optimization capabilities ("How"). First, I will show how to apply causal reasoning to tuple provenance in order to determine the causes of query results, and their responsibility. I will present extensive analysis of the data complexity for the case of conjunctive queries, and focus on a complete dichotomy between NP-hard and PTIME cases for the problem of computing responsibility. This concrete characterization of PTIME cases is crucial in scaling up to the challenges of Big Data. Second, I will demonstrate the applicability of the causality framework in a practical setting. I will use a mobile sensing application to show that ranking provenance tuples by their degrees of responsibility identifies errors more effectively than other schemes. Finally, I will present the Tiresias system, the first how-to query engine, which seamlessly integrates database systems with constrained problem solving capabilities. The contributions of the system are threefold: (a) a declarative interface for defining how-to queries over a database, (b) translation rules from the declarative statements to the constrained problem specification, and (c) a suite of data-specific optimizations that allow scaling to large data sizes. Initial results of our prototype system implementation show order-of-magnitude speedups to state-of-the-art solver runtimes, which indicates that there are significant gains in pushing this functionality within the database engine. I will conclude with a summary of my contributions, and discuss my future steps with the Tiresias system, and the bigger vision of reverse data management.

Tremendous amounts of personal data about individuals are being collected and shared online. Legal requirements and an increase in public awareness due to egregious breaches of individual privacy have made data privacy an important field of research. Recent research, culminating in the development of a powerful notion called differential privacy, have transformed this field from a black art into a rigorous mathematical discipline. 

This talk critically analyzes the trade-off between accuracy and privacy in the context of social advertising – recommending people, products or services to users based on their social neighborhood. I will present a theoretical upper bound on the accuracy of performing recommendations that are solely based on a user's social network, for a given level of (differential) privacy of sensitive links in the social graph. I will show using real networks that good private social recommendations are feasible only for a small subset of the users in the social network or for a lenient setting of privacy parameters.

I will also describe some exciting new research about a no free lunch theorem, which argues that privacy tools (including differential privacy) cannot simultaneously guarantee utility as well as privacy for all types of data, and conclude with directions for future research in data privacy and big-data management.

The choice between Byzantine and crash fault tolerance is viewed as a fundamental design decision when building fault tolerant systems. We show that this dichotomy is not fundamental, and present a unified model of fault tolerance in which the number of tolerated faults of each type is a configuration choice. Additionally, we observe that a single fault is capable of devastating the performance of existing Byzantine fault tolerant replication systems. We argue that fault tolerant systems should, and can, be designed to perform well even when failures occur. In this talk I will expand on these two insights and describe our experience leveraging them to build a generic fault tolerant replication library that provides flexible fault tolerance and robust performance. We use the library to build a fault tolerant version of the Hadoop Distributed File system.

Today, the large-scale compromise of Internet hosts serves as a platform for supporting a range of criminal activity in the so-called Internet underground economy. In this talk I will quickly survey work that our group has performed over the past decade on the problems posed by these threats, and how our research directions have evolved over time. In the remainder of the talk, I will describe recent work that our group has performed, including the ecosystem of CAPTCHA-solving service providers and an end-to-end analysis of the spam value chain. Using extensive measurements over months of diverse spam data, broad crawling of naming and hosting infrastructures, and product purchases from a wide variety of spam-advertised sites, I'll characterize the relative prospects for anti-spam interventions at multiple levels.

This work is part of a larger effort of the Collaborative Center for Internet Epidemiology and Defenses (CCIED), a joint NSF Cybertrust Center with UCSD and ICSI (http://www.ccied.org), and an ONR MURI collaboration (http://www.sysnet.ucsd.edu/botnets).

The ability to participate anonymously in online communities is widely valued, but existing anonymous communication protocols offer limited security against anonymous abuse, traffic analysis, or denial-of-service attacks. Dissent is a general-purpose anonymous messaging protocol that addresses these limitations in the context of group communication applications, where members of a well-defined group wish to "post" messages anonymously to each other or onto a common "bulletin board" without a message being linkable to a particular group member. Unlike most existing anonymous communication schemes, the Dissent protocol provides anonymity while also holding its members accountable: if a group member deviates from the protocol in attempt to block communication or attack other members anonymously, the protocol ensures that the group can identify and expel the misbehaving member. The key technical idea enabling this combination of anonymity and accountability is to use a verifiable cryptographic shuffle scheme as a setup phase for a dining cryptographers (DC-nets) communication channel. The verifiable shuffle enables the group to create and agree on a random permutation of user identities to pseudonyms, then use that permutation as a logical schedule for subsequent DC-nets communication. The group can use this agreed-upon schedule to identify any member attempting to disrupt communication by deviating from the schedule or jamming the DC-nets channel. Currently working prototypes of Dissent support small groups, but ongoing efforts are extending the protocol to scale to large groups, handle node failure and network churn gracefully, and address intersection attacks against users who maintain long-term pseudonyms

In this talk, I present a new model of class-based Algol-like programming languages inspired by automata-theoretic concepts.  The model may be seen as a variant of the "object-based" model previously developed in 1993, where objects are described by their observable behaviour in terms of events, and "state-based" models studied by Reynolds, Oles, Tennent and O'Hearn where objects are not explicitly represented.  The idea is to view objects as automata which are described from the outside through their observable behaviour while, internally, their operations are represented as state transformations.  This allows us to to combine both the state-based and event-based views of objects.  I illustrate the efficacy of the model by proving several test equivalences and discuss its connections to the previous models.

Internet availability-the ability for any two nodes in the Internet to communicate-is essential to being able to use the Internet for delivery critical applications such as real-time health monitoring and response. Despite massive investment by ISPs worldwide, Internet availability remains poor, with literally hundreds of outages occurring daily, even in North America and Europe. Some have suggested that addressing this problem requires a complete redesign of the Internet, but in this talk I will argue that considerable progress can be made with a small set of backwardly compatible changes to the existing Internet protocols. We take a two-pronged approach. Many outages occur on a fine-grained time scale due to the convergence properties of BGP, the Internet's interdomain routing system. We describe a novel set of additions to BGP that retains its structural properties, but applies lessons from fault tolerant distributed systems research to radically improve its availability. Other outages are longer-lasting and occur due to complex interactions between router failures and router misconfiguration. I will describe some ongoing work to build an automated system to quickly localize and repair these types of problems.

JavaScript arguably is the most widely-used "lambda language": first-class functions play a central role in the language, and they form the basis for its object system. Not only that: every JavaScript programmer uses concepts like higher-order functions or continuation-passing on a daily basis, without ever having heard those terms.

In this talk, I first give a quick intro into the good, the bad, and the unfathomable of JavaScript, for the language geeks. Then I present some of the technology that V8, Google's high-performance JavaScript VM, is using to get performance out of this mess, namely just-in-time compilation, inline caching, type feedback, dynamic optimization and deoptimization.

In this talk, I'm going to tell the story of how a group of european researchers arrived at a design for communications software that seems rather well suited to the new "Data Center Networking" paradigm. The tale starts with moving from UCL Cambridge and choosing to learn about ad hoc networks, and then with Intel research lablet trying out a few disruptive ideas and stumbled on the notion for Haggle ("Haggle" comes from the phrase Ad Hoc Google, now really known as Opportunistic Networking) combining results from Grossglauser & Tse's work on capacity of multi-hop networks with Kevin Fall's work on Delay Tolerant Networks. In the process of building various testbeds in the Haggle project (and three complete versions for native Java phones, C# on Windows Mobile, and native Android&iPhone versions), as well as measuring various aspects of human society, we ended up with a system that appears to be rather more general than expected. Most recently, for example, it was used to build a P2P secure, disconnect tolerant version of Dropbox, as well as to track a Flu epidemic.

Today's datacenters need to support a variety of applications, and an even higher variety of dynamically changing workloads. In this talk, I will present Mesos, a platform for sharing commodity clusters between diverse computing frameworks, such as Hadoop and MPI.  Sharing improves cluster utilization and avoids per-framework data replication. To support the diverse requirements of these frameworks, Mesos employs a two-level scheduling mechanism, called resource offers. Mesos decides how many resources to offer each framework, while frameworks decide which resources to accept and which computations to schedule on these resources. To allocate resources across frameworks, Mesos uses Dominant Resource Fairness (DRF). DRF generalizes fair sharing to multiple-resources, provides sharing incentives, and is strategy proof. Our experimental results show that Mesos can achieve near-optimal locality when sharing the cluster among diverse frameworks, can scale up to 50,000 nodes, and is resilient to node failures.

This talk presents the design of a novel distributed, database system that was designed to give query response time guarantees, independent of the query and update workload. The system makes use of aggressive sharing of operations (e.g., scans and joins) between concurrent queries and updates. Specifically, this talk gives details of the storage manager (called Crescando) and of the query processor (called SharedDB), both of which can be deployed in a distributed and scalable infrastructure. Furthermore, the talk presents the results of performance experiments with workloads from an airline reservation system.

There are many web applications that require users to coordinate. Friends want to coordinate travel plans, students want to jointly enroll in the same set of courses, and busy researchers want to coordinate their schedules. These tasks are difficult to program using existing abstractions provided by database systems because they all require some type of coordination between users. This is fundamentally incompatible with isolation in the classical properties of ACID database transactions. In this talk, I will argue that it is time to look beyond isolation, and I will describe ideas that allow users to perform declarative data-driven coordination through entangled queries and transactions. This talk describes joint work with Gabriel Bender, Nitin Gupta, Christoph Koch, Lucja Kot, Milos Nikolic, and Sudip Roy.

Nominal datatypes are a simple extension of the usual notion of algebraic datatypes with facilities for declaring constructors involving names and name-binding. In this talk I want to revisit the topic of higher-order functional programming with nominal datatypes. Destructing name-bindings seems to inevitably involve the use of locally scoped names in one form or another. The original work on this topic (such as Shinwell's Fresh patch for OCaml) used state-based implementations of local scoping. In this talk I will discuss this and two other possible implementations, that have greater degrees of purity.

As far as I am concerned, the goal of this work is to arrive at a language design that (1) can express common patterns of use of bound names in informal algorithms that manipulate syntax with binders, but (2) has good logical properties---for example, that can co-exist with Constructive Type Theory. That goal has yet to be attained.

I will present the WebBlaze project, aiming at designing and developing new techniques and tools to improve web security. WebBlaze's new technologies cover a broad range including new architectural solutions for defending against cross-site scripting attacks, tools for detecting and defending against cross-origin JavaScript capability leaks which lead to universal cross-site scripting attacks, and new approaches for secure browser extensions and web advertisements.

I will also give an overview of the BitBlaze project, describing how we build a unified binary program analysis platform and use it to provide novel solutions to computer security problems including automatic vulnerability discovery, automatic generation of vulnerability signatures for defense, and automatic extraction of security models for analysis and verification. I will also describe some ongoing efforts in mobile security. More information about WebBlaze and BitBlaze is available at http://webblaze.cs.berkeley.edu and http://bitblaze.cs.berkeley.edu.

In this talk, I describe a denotational model of higher-order functional reactive programming using ultrametric spaces and nonexpansive maps, which provides a natural Cartesian closed generalization of causal stream functions and uarded recursive defnitions. To write programs, I also show how to define a normalizing type theory corresponding to this semantics.

I show how reactive programs written in this language can be implemented efficiently using an imperatively updated dataflow graph (with correctness proof, but not in this talk!), and demonstrate how GUI (graphical user interface) programs look when written in this style.

We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. We define compositional techniques for computing procedure summaries concerning various aspects such as shapes, sizes, and data. Relations between program configurations are represented by graphs where vertices represent list segments without sharing. The data in the these list segments are characterized by constraints in new complex abstract domains. We define an abstract domain whose elements correspond to an expressive class of first order universally quantified formulas and an abstract domain of multisets. Our analysis computes the effect of each procedure in a local manner, by considering only the reachable parts of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domains. The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post- condition reasoning.

Asynchronous Weak Secret Sharing (AWSS) is a well known primitive for the design of statistical Asynchronous Verifiable Secret Sharing (AVSS) schemes involving n parties. The existing efficient AWSS schemes are based on the idea of sharing a secret using bivariate polynomial and invokes n^2 instances of another well known asynchronous primitive, namely Asynchronous Information Checking Protocol (AICP). In this paper, we propose a substitute for AWSS called asynchronous weak commitment scheme (AWCS) that has weaker requirements in comparison to AWSS. Due to its weaker requirements, AWCS is conceptually much simpler to construct compared to AWSS. In fact, we can design AWCS using simple Shamir secret sharing scheme (based on univariate polynomial), instead of using bivariate polynomials. Moreover, our AWCS invokes only n instances of AICP. Therefore, the existing best known AVSS schemes call for only n^2 instances of AICP when they incorporate our AWCS, as compared to n^3 instances required earlier. This matches the number of instances of ICP (synchronous version of AICP) invoked in the best known statistical VSS schemes in the synchronous settings. We observe that we gain a factor of \Theta(n) in the communication complexity when our AWCS is used in the existing AVSS schemes in place of AWSS. This further saves a factor of \Theta(n) in the communication complexity of the best known existing asynchronous Byzantine agreement (ABA) and asynchronous multiparty computation (AMPC) protocols where AVSS is used as an important stepping stone.

Virtually all chips today are built with an increasing number of processor cores. To leverage these hardware trends, all future software will have to be concurrent.

The main challenge in developing reliable concurrent software is that a programmer is forced to coordinate a fantastic number of possible interactions. Manual coordination of these interactions (e.g., via locks) has proven to be extremely time consuming, and brittle, often resulting in programs that are incorrect, do not fully utilize the underlying computational resources, or both.

In this talk, I will present new techniques that harness the growing power of modern hardware and the increasing maturity of formal methods to simplify the process of program construction: in essence, given a concurrent program that violates a desired property, the techniques will analyze the (possibly infinite-state) program and attempt to automatically repair it by synthesizing the necessary synchronization.

A tool implementing these techniques has been successfully applied to a variety of challenging problems: from discovering tricky synchronization under weak memory models, to enforcing general atomicity properties, to obtaining new concurrent data structures and memory management algorithms.

Understanding the dynamics in large scale networks is a major challenge in front of the network research community. Traditional graph theoretic approaches have their own limitations and are not applicable due to the large size and dynamic nature of the network. In this background, my talk primarily addresses two different issues in technological and social networks. The first half of my talk is directed towards understanding the resilience and emergence of technological networks, specifically superpeer networks. We propose an analytical framework in order to measure the resilience of superpeer networks in face peer churn and attacks. Other side, it is not obvious why bootstrapping of peer nodes and other local dynamics results in the appearance of bimodal degree distribution in superpeer networks like Gnutella. We develop a formalism which enables us to explain the emergence of bimodal network in face of dynamics like peer bootstrapping, churn, link rewiring etc. Further analysis leads us in formulating interesting bootstrapping protocols such that superpeer network evolves with desired topological properties. The second half of my talk mostly focuses towards the detection and analysis of dynamical communities in social networks, specifically in citation network. Most of the recent methods aim at exhibiting community partitions from successive graph snapshots and thereafter connecting or smoothing these partitions using clever time-dependent features and sampling techniques. These approaches are nonetheless achieving "longitudinal" rather than 'dynamic' community detection. Assuming that communities are fundamentally defined by a certain amount of interaction recurrence among a possibly disparate set of nodes over time, we suggest that the loss of information induced by considering successive snapshots makes it difficult to appraise essentially dynamic phenomena. We propose a methodology which aims at tackling this issue in the context of citation datasets, and present several illustrations on both empirical and synthetic dynamic network datasets.

Sensitive data in many organizations such as intelligence, healthcare and finance corporations, is often protected by complex access policies that rely on a mix of signed credentials, clock time and system state. Enforcement of such policies through conventional mechanisms like access control lists is administratively infeasible. Motivated by this disparity, this talk presents the theoretical and practical aspects of a logic-based access control subsystem for representing, interpreting, and enforcing access policies. The theoretical underpinning of the subsystem is a new logic to represent access policies, and its proof theory to determine their consequences. By carefully separating policy interpretation, policy decision, and policy enforcement, the subsystem leverages (conventionally inefficient) logical tools to attain very high throughput. The subsystem is evaluated in its implementation in a local file system, and its expressiveness is validated through a case study of policies used in the U.S. intelligence community.

With wireless networks slated to become the dominant method of internet access of the future, the radio spectrum is fast becoming a scarce and expensive resource. Despite the significant growing pressures on the demand for spectrum, there are large portions of the overall spectrum that are severely under-utilized ultimately leading to inefficient use of available capacity. To address these problems we build opportunistic wireless networks, which work by continually seeking and using portions of the spectrum that are unused by the spectrum owners (incumbents) while ensuring non-interference with the incumbents. A prominent emerging system where opportunistic wireless networking can work well is in the so-called white spaces. Enabled by two historic rulings (in 2008 and 2010) by the Federal Communications Commission (FCC) in the United States, white spaces are those television channels that, in an instant in time, are not used by the incumbents: television stations or wireless microphones.

In this talk I will present the challenges encountered when building the next generation of wireless networks that operate opportunistically over these white spaces., I will first present WhiteFi, which consists of new algorithms and protocols for networking over the white spaces. I will then present SenseLess, a white spaces network that obviates the need for white space devices to sense the presence of incumbents. I will present results and evaluations from prototype implementations and deployments of the two systems.

A major challenge in data management is how to manage uncertain data. Many reasons for the uncertainty exists: the data may be extracted automatically from text, it may be derived from the physical world such as RFID data, it may be integrated using fuzzy matches, or may be the result of complex stochastic models. Whatever the reason for the uncertainty, a data management system needs to offer predictable performance to queries over such data.

In this talk I will address a fundamental problem in probabilistic databases: given a query, what is the computational complexity of evaluating it over probabilistic databases? Probabilistic inference is known to be hard in general, but once we fix a query, it becomes a specialized problem. I will show that Unions of Conjunctive Queries (also known as non-recursive datalog rules) admit a dichotomy: every query is either provably #P hard, or can be evaluated in PTIME. For practicaly purposes, the most interesting part of this dichotomy is the PTIME algorithm. It uses in a fundamental way the Mobius' inversion formula on finite lattices (which is the inclusion-exclusion formula plus term cancellation), and, because of that, it can perform probabilistic inference in PTIME on classes of Boolean expressions where other established methods fail, including OBDDs, FBDDs, inference based on bounded tree widths, or d-DNNF's.

With the recent advent of multicore chips, real-time applications are now increasingly being deployed on multiprocessors. The underlying real-time operating systems (RTOSs) must hence adapt to become "multicore-ready". This poses a challenge: which scheduling and synchronization algorithms should be used to maximize RTOS flexibility and efficiency on multicore platforms?

This talk focusses on two relevant results. In the first part, I present an overhead-aware scheduler evaluation methodology and a case study, which highlights that the traditional choice of fixed-priority scheduling is indeed not the best choice for multicore systems. In the second part, I present the first provably optimal multiprocessor real-time locking protocol, which answers a long-open question pertaining to blocking optimality in multiprocessor real-time systems.

Modern society is increasingly dependent on (and fearful of) massive amounts and availability of electronic information. There are numerous everyday scenarios where sensitive data must be -- sometimes reluctantly or suspiciously -- shared between two or more entities without mutual trust. This prompts the need for mechanisms to enable limited (privacy-preserving) sharing of sensitive information. Among them, Private Set Intersection (PSI) techniques are particularly appealing whenever two parties wish to compute an intersection of their respective sets of items without revealing to each other any other information, beyond the intersection. This talk motivates the need for PSI techniques with various features and illustrates several concrete PSI variants that offer appreciably better efficiency than prior work and guarantee stronger privacy properties. Finally, motivated by proliferation of smartphones, and increasing amount of personal information shared ubiquitously, we identify some privacy issues specific to smartphone environments. We present several solutions geared for privacy-enhanced smartphone applications, such as: scheduling, location/interest sharing, and participatory sensing.

The game-based approach is an established methodology for structuring security proofs of cryptographic schemes. Its essence lies in giving precise mathematical descriptions of the interaction between an adversary and an oracle system---such descriptions are referred to as games---and to organize proofs as sequences of games, starting from a game that represents a security goal, and proceeding by successive transformations to games that represent security assumptions. Game-based proofs can be rigorously formalized by representing games as probabilistic programs and relying on programming language techniques to justify proof steps. In this talk I will describe two tools that follow this approach: CertiCrypt and EasyCrypt.

* CertiCrypt is built upon the general-purpose proof assistant Coq and provides certified mechanisms to reason about probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, verified program transformations, and ad-hoc techniques, such as reasoning about failure events. CertiCrypt has been notably applied to verify security proofs of OAEP and FDH.

* EasyCrypt is an automated tool written in OCaml that builds upon SMT solvers to synthesize machine-checked proofs from proof sketches, which include the full sequence of games, relational logic judgments and claims relating the probability of events in successive games. Relational judgments are proved using a verification condition generator that yields proof obligations that can be discharged by SMT solvers. To verify claims about probability, we implement a mechanism that combines some elementary rules to directly compute bounds on the probability of events with rules to derive probability (in)equalities from relational judgments. Most components of EasyCrypt are proof-producing, so that proofs built by EasyCrypt can be exported to CertiCrypt and verified using Coq, assuming proof obligations discharged by SMT solvers are valid. EasyCrypt has been notably used to verify the security of the Cramer-Shoup cryptosystem.

If time permits, the talk will feature a demo of the use of EasyCrypt to build a proof, export it to CertiCrypt and verify it using Coq.

Online production communities are increasingly important, creating commercially valuable software (e.g., Linux), generating scientific data (e.g., galaxyzoo.org) and building history's largest encyclopedia (Wikipedia). Motivating and coordinating the volunteers who do this work is a serious problem for many communities. This talk will review empirical research, primarily based on data from Wikipedia, that examines some of the interpersonal and managerial tactics that online production communities use to socialize new community members, to coordinate the work of volunteers and to motivate them. Our research indicates, for example, that broad-based participation is primarily valuable when a subset of the volunteers does the lion's share of the work, but is less valuable when work is distributed more evenly among them. It suggests that group goals help both motivate and socialize participants. It identifies the types of interactions between new community members and old-timers that foster commitment and continued participation. The talk will also review the CrowdForge system for coordinating the micro-contributions of Amazon Mechanical Turk workers, so that they can accomplish complex and highly interdependent projects.

Software synthesis is a technique for automatically generating code from a given specification. The goal of software synthesis is to make software development easier while increasing both the productivity of the programmer and the correctness of the produced code. In this talk I will present an approach to synthesis that relies on the use of automated reasoning and decision procedures. First I will describe how to generalize decision procedures into predictable and complete synthesis procedures. Here completeness means that the procedure is guaranteed to find code that satisfies the given specification. I will illustrate the process of turning a decision procedure into a synthesis procedure using linear integer arithmetic as an example. Next I will outline a synthesis procedure for specifications given in the form of type constraints. The procedure takes into account polymorphic type constraints as well as code behavior. The procedure derives code snippets that use given library functions. I will conclude with an outlook on possible future research directions and applications of synthesis procedures. I believe that in the future we can make programming easier and more reliable by combining program analysis, software synthesis, and automated reasoning.