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.

This thesis proposes and evaluates new system designs to support two emerging Internet workloads: (a) bulk content, such as downloads of large media and scientific libraries, and (b) user-generated content (UGC), such as photos and videos that users share online, typically on online social networks (OSNs).

Bulk content accounts for a large and growing fraction of today's Internet traffic. Due to the high cost of bandwidth, delivering bulk content in the Internet is expensive. To reduce the cost of bulk transfers, I proposed traffic shaping and scheduling designs that exploit the delay-tolerant nature of bulk transfers to allow ISPs to deliver bulk content opportunistically. I evaluated my proposals through software prototypes and simulations driven by real-world traces from commercial and academic ISPs and found that they result in considerable reductions in transit costs or increased link utilization.

The amount of user-generated content (UGC) that people share online has been rapidly growing in the past few years. Most users share UGC using online social networking websites (OSNs), which can impose arbitrary terms of use, privacy policies, and limitations on the content shared on their websites. To solve this problem, I evaluated the feasibility of a system that allows users to share UGC directly from the home, thus enabling them to regain control of the content that they share online. Using data from popular OSN websites and a testbed deployed in 10 households, I showed that current trends bode well for the delivery of personal UGC from users' homes. I also designed and deployed Stratus, a prototype system that uses home gateways to share UGC directly from the home.

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.

Abstract: Older adults are quickly becoming diverse and savvy users of a broad range of technologies. Of adults age 65 and over, 38% are currently online, and of these, one in four has adopted social media. Though uptake remains low compared to that of younger generations, it is growing dramatically; for example, social networking use among internet users 65 and older doubled over the past year. These trends are encouraging because computer technologies offer immense potential to support individuals as they age - by compensating for cognitive and sensory impairments, by supporting independent living, and by promoting social interaction.

In this talk, I will first give an overview of my dissertation work on increasing the accessibility of pen-based interaction for older adults. Pen-based devices are an appealing platform for older adults because they allow users to take full advantage of their hand-eye coordination skills in a familiar form of interaction. However, research has chiefly focused on the accessibility limitations of the mouse as it has historically garnered more wide-spread adoption. As we move beyond accessibility, we can begin to explore the ways in which technology can be designed to further enrich lives and fulfill unmet needs. Within that theme, I will present ongoing projects aimed at better understanding the technological needs of older adults, and at envisioning new technologies specifically targeted to those needs.

The number of systems and services that people interact with has increased rapidly over the past 20 years. Most of those systems and services have security controls, but until recently, the usability of those mechanims was not considered. Research over the past 15 years has provide ample evidence that systems that are not usable are not secure, either, because users make mistakes or devise workarounds that create vulnerabilities. In this talk, I will present an overview of the most pressing problems, and what research on usable security (HCISec) has produced in response to this challenge. I will argue that past attempts have been focussed on improving user interfaces to security mechanisms, but that delivering systems with usable and effective security controls requires a change in how we design and implement security in systems and services. The talk will present examples of new approaches to requirements capture and system design, and new approaches to 'security thinking' in organisations.