Institute colloquium
06 September 2010, 11:00 AM
Periklis Akritidis
University of Cambridge
Kaiserslautern, Building MPI-SWS, Room 206 (simultaneous videocast to Saarbrücken, Building MPI-SWS, Room 5th floor)
Title: Practical memory safety for C
Abstract:
C facilitates high performance execution and low-level systems programming, but the lack of memory safety undermines security and reliability; for example, memory corruption bugs can breach security, and faults in kernel extensions can bring down the entire operating system. Memory safe languages, however, are unlikely to displace C in the near future, and solutions currently in use offer inadequate protection. Comprehensive proposals, on the other hand, are either too slow for practical use, or break backwards compatibility by requiring source code porting or generating incompatible binary code. My talk will present backwards-compatible solutions to prevent dangerous memory corruption in C programs at a low cost.
17 August 2010, 11:00 AM
Mike Rainey
University of Chicago
Kaiserslautern, Building MPI-SWS, Room 206 (simultaneous videocast to Saarbrücken, Building MPI-SWS, Room 5th floor)
Title: Effective scheduling techniques for high-level parallel-programming languages
Abstract:
In the not-so-distant past, parallel programming was mostly the concern of programmers specializing in high-performance computing. Nowadays, on the other hand, many of today's desktop and laptop computers come equipped with a species of shared-memory multiprocessor called a multicore processor, making parallel programming a concern for a much broader range of programmers. High-level parallel languages, such as Parallel ML (PML) and Haskell, seek to reduce the complexity of programming multicore processors by giving programmers abstract execution models, such as implicit threading, where programmers annotate their programs to suggest the parallel decomposition. Implicitly-threaded programs, however, do not specify the actual decomposition of computations or mapping from computations to processors. The annotations act simply as hints that can be ignored and safely replaced with sequential counterparts. The parallel decomposition itself is the responsibility of the language implementation and, more specifically, of the scheduling system. Threads can take arbitrarily different amounts of time to execute, and these times are difficult to predict. Implicit threading encourages the programmer to divide the program into threads that are as small as possible because doing so increases the flexibility the scheduler in its duty to distribute work evenly across processors. The downside of such fine-grain parallelism is that if the total scheduling cost is too large, then parallelism is not worthwhile. This problem is the focus of this talk. The starting point of this talk is work stealing, a scheduling policy well known for its scalable parallel performance, and the work-first principle, which serves as a guide for building efficient implementations of work stealing. In this talk, I present two techniques, Lazy Promotion and Lazy Tree Splitting, for implementing work stealing. Both techniques derive their efficiency from adhering to the work-first principle. Lazy Promotion is a strategy that improves the performance, in terms of execution time, of a work-stealing scheduler by reducing the amount of load the scheduler places on the garbage collector. Lazy Tree Splitting is a technique for automatically scheduling the execution of parallel operations over trees to yield scalable performance and eliminate the need for per-application tuning. I use Manticore, PML's compiler and runtime system, and a sixteen-core NUMA machine as a testbed for these techniques. In addition, I present two empirical studies. In the first study, I evaluate Lazy Promotion over six PML benchmarks. The results demonstrate that Lazy Promotion either outperforms or performs the same as an alternative scheme based on Eager Promotion. This study also evaluates the design of the Manticore runtime system, in particular, the split-heap memory manager, by comparing the system to an alternative system based on a unified-heap memory manager, and showing that the unified version has limited scalability due to poor locality. In the second study, I evaluate Lazy Tree Splitting over seven PML benchmarks by comparing Lazy Tree Splitting to its alternative, Eager Tree Splitting. The results show that, although the two techniques offer similar scalability, only Lazy Tree Splitting is suitable for building an effective language implementation.
22 July 2010, 1:00 PM
Vijay Ganesh
MIT
Kaiserslautern, Building MPI-SWS, Room 206 (simultaneous videocast to Saarbrücken, Building MPI-SWS, Room 5th floor)
Title: Solvers for Software Reliability and Security
Abstract:
The task of building reliable and secure software remains one of the most important and challenging issues in computer science. In recent years, there has been rapid progress in the scalability and effectiveness of software reliability tools. A key reason for this success is the dramatic improvement in the speed of constraint solvers over the last decade. Constraint solvers are essential components of most software reliability tools, whether they are based on formal methods, program analysis, testing or synthesis. My research on constraint solvers has directly contributed to this trend of increasing solver efficiency and expressive power, thus advancing the state-of-the-art in software reliability research. In this talk, I will present two solvers that I have designed and implemented, namely, STP and HAMPI. I will talk about the techniques that enable STP and HAMPI to scale, and also some theoretical results. I will also talk about the contexts and applications where each solver is best suited. STP is a solver for the theory of bit-vectors and arrays. STP was one of the first constraint solvers to enable an exciting new testing technique called Dynamic Systematic Testing (aka Concolic Testing). STP-enabled concolic testers have been used to find hundreds of previously unknown bugs in Unix utilities, OS kernels, media players, and commercial software, some with approximately a million lines of code. Next, I will describe HAMPI, a solver for a rich theory of equality over bounded string variables, bounded regular expressions, and context-free grammars. Constraints in this theory are generated by analysis of string-manipulating programs. HAMPI has been used to find many unknown SQL injection vulnerabilities in applications with more than 100,000 lines of PHP code using static and dynamic analysis. Finally, I will conclude my talk with two future research programs. First, I will discuss how faster solvers can enable qualitatively novel approaches to software reliability. Second, I will discuss how we can go from specific solver techniques to solver design paradigms for rich logics.
19 July 2010, 11:00 AM
Kyomin Jung
KAIST
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Approximate Inference Algorithms in Markov Random Field with Their Applications
Abstract:
Markov Random Field (MRF) provides an elegant and succinct abstraction to capture inter-dependency between a large number of random variables - applications abound in communication networks, signal processing, statistical physics, combinatorics, biology, etc. In most of these applications, the key task pertains inferring the most likely assignment (aka MAP). This problem is computationally hard in general. Therefore, various approximations have been developed that utilize graph structure of the MRF for efficient computation. Popular approaches like Belief Propagation (and its variants) work well when the underlying graph has large girth, eg. sparse graphical codes like LDPC codes. In many applications of interest, graphs do have lots of short cycles, but they naturally posses some ``geometry''. We develop a new class of approximation algorithms that utilize geometry, which is called polynomially growing, of the underlying graph to obtain efficient approximation with provable guarantee for the inference problem. In this talk, I will describe the main idea of the Belief Propagation, and our new algorithm based on simple local updates. I will describe their applications to wireless network and image processing.
19 July 2010, 1:00 PM
Linh Phan
University of Pensylvania
Kaiserslautern, Building MPI-SWS, Room 206 (simultaneous videocast to Saarbrücken, Building MPI-SWS, Room 5th floor)
Title: Timing Analysis of Mixed Time / Event-Triggered Multi-Mode Systems
Abstract:
Many embedded systems operate in multiple modes, where mode switches can be both time- as well as event-triggered. While timing and schedulability analysis of the system while it is operating in a single mode has been well studied, it is always difficult to piece together the results from different modes in order to deduce the timing properties of a multi-mode system. In this talk, I will present a model and associated analysis techniques to describe embedded systems that process multiple bursty/complex event/data streams and in which mode changes are both time- and event-triggered. Compared to previous studies, our model is very general and can capture a wide variety of real-life systems. Our analysis techniques can be used to determine different performance metrics, such as the maximum fill-levels of different buffers and the delays suffered by the streams being processed by the system. The main novelty in our analysis lies in how we piece together results from the different modes in order to obtain performance metrics for the full system.
25 June 2010, 1:30 PM
Tanzeem Choudhury
Dartmouth College
Kaiserslautern, Building MPI-SWS, Room 206
Title: Spoken Networks: Analyzing face-to-face conversations and how they shape our social connections
Abstract:
With the proliferation of sensor-rich mobile devices, it is now possible to collect data that continuously capture the real-world social interactions of entire groups of people. These new data sets provide opportunities to study the social networks of people as they are observed "in the wild." However, traditional methods often model social networks as static and binary, which are inadequate for continuous behavioral data. Networks derived from behavioral data are almost always temporal, are often non-stationary, and have finer grained observations about interactions as opposed to simple binary indicators. Thus, new techniques are needed that can take into account the variable tie intensities and the dynamics of a network as it evolves in time. In this talk, I will provide an overview of the computational framework we have developed for modeling the micro-level dynamics of human interactions as well as the macro-level network structure and its dynamics from local, noisy sensor observations. Furthermore, by studying the micro and macro levels simultaneously we are able to link dyad-level interaction dynamics (local behavior) to network-level prominence (a global property). I will conclude by providing some specific examples of how the methods we have developed can be applied more broadly to better understand and enhance the lives and health of people. Based on joint work with Danny Wyatt (University of Washington), James Kitts (Columbia), Jeff Bilmes (University of Washington), Andrew Campbell (Dartmouth), and Ethan Berke (Dartmouth Medical School)
15 June 2010, 11:00 AM
Andreas Haeberlen
University of Pennsylvania
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Privacy and forensics in federated distributed systems
Abstract:
In this talk, I will describe two of my ongoing projects, one on collaborative security and the other on secure network provenance. Collaborative security is an approach to fighting security threats that span many different administrative domains. For example, it is often difficult for Internet service providers to detect botnets because each domain can locally observe only a small part of the botnet; however, exchanging information across domains is challenging because of privacy concerns. We are working on a system that enables domains to share information in a controlled fashion. Each domain establishes a 'privacy budget' and allows other domains to ask queries in a special language; the 'privacy cost' of each query is inferred automatically and deducted from the budget. This is accomplished through a combination of type systems and differential privacy. Secure network provenance (SNP) is a technique for answering forensic questions about distributed systems in which some nodes have been compromised by an adversary. Each node maintains a record of past states and the (local or remote) causes of state transitions. Thus, if the symptoms of an intrusion are observed, it is possible to trace them back to their root causes or, conversely, to determine how an intrusion on one node has affected other nodes.
14 June 2010, 10:15 AM
Arvind Krishnamurthy
University of Washington
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Reverse Traceroute
Abstract:
Traceroute is the most widely used Internet diagnostic tool today. Network operators use it to help identify routing failures, poor performance, and router misconfigurations. Researchers use it to map the Internet, predict performance, geolocate routers, and classify the performance of ISPs. However, traceroute has a fundamental limitation that affects all these applications: it does not provide reverse path information. Although various public traceroute servers across the Internet provide some visibility, no general method exists for determining a reverse path from an arbitrary destination. We address this longstanding limitation by building a reverse traceroute tool. Our tool provides the same information as traceroute, but for the reverse path, and it works in the same case as traceroute, when the user may lack control of the destination. Our approach combines a number of ideas: source spoofing, IP timestamp and record route options, and multiple vantage points. In the median case our tool finds 87% of the hops seen in a directly measured traceroute along the same path, versus only 38% if one simply assumes the path is symmetric, a common fallback given the lack of available tools. We then use our reverse traceroute tool to study previously unmeasurable aspects of the Internet: we uncover more than a thousand peer-to-peer AS links invisible to current topology mapping efforts, we examine a case study of how a content provider could use our tool to troubleshoot poor path performance, and we measure the latency of individual backbone links with, on average, sub-millisecond precision
12 May 2010, 2:00 PM
Jennifer B. Sartor
University of Texas, Austin
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Exploiting Language Abstraction to Optimize Memory Efficiency
Abstract:
Memory continues to be a bottleneck in modern systems as application complexity and the number of cores have increased, generating more traffic. These complex applications are written largely in high-level managed languages, which offer an opportunity to dynamically optimize memory performance because they virtualize memory management. We explored memory inefficiencies in a Java virtual machine, performing a study of data compression techniques. I will present the results of that study, showing arrays are a dominant source of heap bloat. Focusing on arrays, we found the traditional contiguous layout precludes space optimizations and does not offer memory management time and space bounds. I show how to exploit the opportunities afforded by managed languages to implement an efficient discontiguous array layout with tunable optimization parameters that improve space usage. Having attacked memory performance on the software side, I will then describe new work that takes a cooperative software-hardware approach. I show how a memory manager can communicate regions of dead data to the architecture, allowing it to eliminate useless writes, substantially reducing memory write traffic. My research combines the flexibility and productivity of high-level managed languages with improved memory efficiency that is critical to current and future hardware.
27 April 2010, 2:00 PM
Ruy Ley-Wild
Carnegie Mellon University
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Programmable Self-Adjusting Computation
Abstract:
In the self-adjusting computation model, programs can respond automatically and efficiently to input changes by tracking the dynamic data dependencies of the computation and incrementally updating the output as needed. After a run from scratch, the input can be changed and the output can be updated via change-propagation, a mechanism for re-executing the portions of the computation affected by the changes while reusing the unaffected parts. Previous research shows that self-adjusting computation can be effective at achieving near-optimal update bounds for various applications. We address the question of how to write and reason about self-adjusting programs. We propose a language-based technique for annotating ordinary programs and compiling them into equivalent self-adjusting versions. We also provide a cost semantics and a concept of trace distance that enables reasoning about the effectiveness of self-adjusting computation at the source level. To facilitate asymptotic analysis, we propose techniques for composing and generalizing concrete distances via trace contexts (traces with holes). The translation preserves the extensional semantics of the source programs, the intensional cost of from-scratch runs, and ensures that change-propagation between two evaluations takes time bounded by their relative distance.
15 April 2010, 10:00 AM
Vibhor Rastogi
University of Washington
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Accurate Analysis of Large Private Datasets
Abstract:
Today, no individual has full control over access to his personal information. Private data collected by various hospitals and universities, and also by websites like Google and Facebook, contain valuable statistical facts that can be mined for research and analysis, e.g., analyze outbreak of diseases, detect traffic patterns on the road, or understand browsing trends on the web, but concerns about individual privacy severely restricts its use, e.g., privacy attacks led AOL to recently pull-off its published search-log data. To remedy this, much recent work focuses on data analysis with formal privacy guarantees. This has given rise to differential privacy considered by many as the golden standard of privacy. However, few practical techniques satisfying differential privacy exist for complex analysis tasks (e.g., analysis involving complex query operators), or new data models (e.g., data having temporal correlations or uncertainty). In this talk, I will discuss techniques that fill this void. I will first discuss a query answering algorithm that can handle joins (previously, no private technique could accurately answer join queries arising in many analysis tasks). This algorithm makes several privacy-preserving analyses over social network graphs possible for the first time. Then I will discuss a query-answering technique over time-series data, which enables private analysis of GPS traces and other temporally-correlated data. Third, I will discuss an access control mechanism for uncertain data, which enables enforcing security policies on RFID-based location data. Finally, I will conclude by discussing some privacy and security problems in building next-generation computing systems based on new models for data (e.g., uncertain data), computing (e.g., cloud computing), and human computer interaction (e.g., ubiquitous systems).
01 April 2010, 11:00 AM
Juan Caballero
Carnegie Mellon University
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Binary Program Analysis and Model Extraction for Security Applications
Abstract:
In this talk I present a platform to extract models of security-relevant functionality from program binaries, enabling multiple security applications such as active botnet infiltration, finding deviations between implementations of the same functionality, vulnerability signature generation, and finding content-sniffing cross-site scripting (XSS) attacks. In this talk, I present two applications: active botnet infiltration and finding content-sniffing XSS attacks. Botnets, large networks of infected computers under control of an attacker, are one of the dominant threats in the Internet, enabling fraudulent activities such as spamming, phishing, and distributed denial-of-service attacks. To build strong botnet defenses, defenders need information about the botnet's capabilities and the attacker's actions. One effective way to obtain that information is through active botnet infiltration, but such infiltration is challenging due to the encrypted and proprietary protocols that botnets use to communicate. In this talk, I describe techniques for reverse-engineering such protocols and present how we use this information to infiltrate a prevalent, previously not analyzed, spam botnet. Cross-site scripting attacks are the most prevalent class of attacks nowadays. One subtle class of overlooked XSS attacks are content-sniffing XSS attacks. In this talk, I present model extraction techniques and how they enable finding content-sniffing XSS attacks. We use those models to find attacks against popular web sites and browsers such as Wikipedia when accessed using Internet Explorer 7. I describe our defenses for these attacks and how our proposals have been adopted by widely used browsers such as Google Chrome and IE8, as well as standardization groups.
29 March 2010, 11:00 AM
Marco Cova
University of California, Santa Barbara
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Taming the Malicious Web: Avoiding and Detecting Web-based Attacks
Abstract:
The world wide web is an essential part of our infrastructure and a predominant mean for people to interact, do business, and participate to democratic processes. Unfortunately, in recent years, the web has also become a more dangerous place. In fact, web-based attacks are now a prevalent and serious threat. These attacks target both web applications, which store sensitive data (such as financial and personal records) and are trusted by large user bases, and web clients, which, after a compromise, can be mined for private data or used as drones of a botnet. In this talk, we will present an overview of our techniques to detect, analyze, and mitigate malicious activity on the web. In particular, I will present a system, called Wepawet, which targets the problem of detecting web pages that launch drive-by-download attacks against their visitors. Wepawet visits web pages with an instrumented browser and records events that occur during the interpretation of their HTML and JavaScript code. This observed activity is analyzed using anomaly detection techniques to classify web pages as benign or malicious. We made our tool available as an online service, which is currently used by several thousands of users every month. We will also discuss techniques to automatically detect vulnerabilities and attacks against web applications. In particular, we will focus on static analysis techniques to identify ineffective sanitization routines and to detect vulnerabilities stemming from the interaction of multiple modules of a web application. These techniques found tens of vulnerabilities in several real-world web applications.
25 March 2010, 11:00 AM
Arthur Chargueraud
INRIA
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Formal Program Verification Through Characteristic Formulae
Abstract:
The characteristic formula of a program is a logical formula that implies any valid post-condition for that program. In this talk, I will explain how to build, in a systematic manner, the characteristic formula of a given purely functional Caml program, and then explain how one can use this formula to verify the program interactively, using the Coq proof assistant. This new, sound and complete approach to the verification of total correctness properties has been applied to the formalization of a number of data structures taken from Chris Okasaki's reference book. My presentation will include demos based on those case studies.
22 March 2010, 11:00 AM
Chung-Kil Hur
Laboratoire PPS
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Program equivalence and compositional compiler correctness
Abstract:
We introduce a notion of program equivalence between different languages and talk about what kind of mathematical techniques are used, how it gives a compositional notion of compiler correctness and more ambitiously how it may be seen as a technique to prove the correctness of programs. We also briefly discuss how these ideas can be formalized and verified in the formal proof assistant Coq.
18 March 2010, 11:00 AM
Viktor Vafeiadis
University of Cambridge
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Towards full verification of concurrent libraries
Abstract:
Modern programming platforms, such as Microsoft's .NET, provide libraries of efficient concurrent data structures, which are used in a wide range of applications. In this talk, I will discuss some of the pitfalls in implementing such concurrent data structures, what correctness of these libraries means, how one can formally prove that a given library is correct, and the extent to which these proofs can be carried out automatically.
15 March 2010, 11:00 AM
Michael Bond
University of Texas, Austin
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Achieving Reliability in Deployed Software Systems
Abstract:
Software is becoming more complex and concurrent due to demand for features and hardware trends that are leading to more instead of faster cores. In the face of these challenges, developers have trouble writing large, correct, scalable programs. Deployed software inevitably contains bugs, even if it has been thoroughly tested, because it is infeasible to analyze and test all possible inputs, environments, and thread schedules. My research focuses on improving reliability while production software runs, to help prevent, diagnose, and tolerate errors that actually manifest in deployment. This talk first presents Pacer, a deployable, scalable approach for detecting data races, which are a common and serious type of concurrency bug. Second, I describe techniques for efficiently reporting the calling context (stack trace) of concurrency and other bugs -- essential information for understanding the behavior of complex, modern programs. I conclude with my future plans for developing new analyses and frameworks that make concurrent software reliable.
11 March 2010, 11:00 AM
Thomas Ristenpart
UC San Diego
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Improving the Interface between Systems and Cryptography
Abstract:
Modern cryptography provides a rigorous mathematical framework for proving the security of cryptographic algorithms. To be effective, however, these mathematical models must accurately reflect the realities of cryptography's use in systems. In this talk, I will address mismatches between theory and use, giving several examples from my work: the problem of credit card number encryption, dealing with bad (cryptographic) randomness, the increasingly diverse applications of cryptographic hash functions, and privacy-preserving device tracking. In each example, problems arise because of gaps between what cryptography offers and what security and privacy demands. To fix these issues, I take an application-oriented approach. This involves modifying cryptography in a theoretically-sound to work better for systems, as well as understanding cryptography's role in broader system security mechanisms. Looking forward, I will discuss my recent work on new attacks in the setting of cloud computing and my future plans for securing next-generation cloud computing services.
10 March 2010, 4:00 PM
Allen Clement
University of Texas
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Byzantine fault tolerance for cluster services
Abstract:
Experiences with computers and computer systems indicate an inconvenient truth: computers fail, and they fail for a wide range of reasons including power outage, disc and memory corruption, misconfiguration, NIC malfunction, user error, and many others. The impact of computer failures can be dramatic, ranging from unavailability of email to canceled flights and stranded airline passengers to closed companies. Byzantine fault tolerant (BFT) state machine replication is posited as an approach for masking individual computer faults and deploying robust services that continue to function despite failures. However, the lack of deployed systems that utilize BFT techniques is indicates that the current state of the art falls short of the needs of practical deployments. In this talk I will discuss our efforts to make BFT a practical and attractive option for practitioners. These efforts are centered around developing BFT techniques that (a) are fast and efficient, (b) tolerate Byzantine faults, and (c) can be easily incorporated into legacy applications. This work is in collaboration with Amit Aiyer, Lorenzo Alvisi, Mike Dahlin, Manos Kapritsos, Yang Wang, and Edmund Wong (UT-Austin), Rama Kotla (currently MSR-SVC), and Mirco Marchetti (currently University of Modena and Reggio Emilia).
08 March 2010, 11:00 AM
Cristiano Calcagno
Imperial College, London
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Compositional Shape Analysis by means of Bi-Abduction
Abstract:
We describe a compositional shape analysis, where each procedure is analyzed independently of its callers. The analysis uses an abstract domain based on a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Compositionality brings its usual benefits - increased potential to scale, ability to deal with unknown calling contexts, graceful way to deal with imprecision - to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses) which we call bi-abduction. Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new interprocedural analysis algorithm. We have implemented our analysis algorithm and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger programs (e.g., an entire Linux distribution) to test scalability and graceful imprecision.
05 March 2010, 3:00 PM
Guy Blelloch
Carnegie Mellon University
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Saarbrücken, Building E1 4 - MPI-INF, Room 24)
Title: Algorithms for Parallel Cache Hierarchies
Abstract:
Cache hierarchies in multicore computers are quite complex consisting of many levels of both shared and private caches. Designing algorithms and applications for such caches can be very complicated although often necessary to get good performance. We discuss approaches of capturing the locality of a parallel algorithm at a high-level requiring little work by the algorithm designer or programmer and then using this along with an appropriate thread scheduler to get good cache performance on a variety of parallel cache configurations. I will describe results for private caches, shared caches and some new results on multiple level cache hierarchies. In all cases the same algorithms can be used, but the scheduler needs to be changed. The approach makes use of ideas on cache oblivious algorithms.
03 March 2010, 2:00 PM
Joshua Dunfield
McGill University
Saarbrücken, Building MPI SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Verifying Functional Programs with Type Refinements
Abstract:
Types express properties of programs; typechecking is specification checking. But the specifications expressed by conventional type systems are imprecise. Type refinements enable programmers to express more precise properties, while keeping typechecking decidable. I present a system that unifies and extends past work on datasort and index refinements. Intersection and union types permit a powerful type system that requires no user input besides type annotations. Instead of seeing type annotations as a burden or just as a shield against undecidability, I see them as a desirable form of machine-checked documentation. Accordingly, I embrace the technique of bidirectional typechecking for everything from dimension types to first-class polymorphism. My implementation of this type system, for a subset of Standard ML, found several bugs in the SML/NJ data structure libraries.
16 February 2010, 2:00 PM
Nicolas Schiper
University of Lugano
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Partial Replication in Large Networks
Abstract:
The popularity of Internet applications such as e-banking, on-line stores, and social networks has tremendously increased in the past years. As a consequence, our daily lives depend on computers more and more each day. These applications typically run on many machines spread across several geographical sites, or groups, to provide low response times to clients. In these complex systems, hardware and software failures are common. Providing high availability without sacrificing performance is thus of a prime importance. In this talk, we present protocols to achieve high availability through data replication. We proceed in two steps. We first devise fault-tolerant atomic multicast algorithms that offer message ordering guarantees, and allow messages to be addressed to any subset of groups. We then build a partial replication protocol that relies on this multicast service. The four atomic protocols presented differ in which properties they ensure, namely disastertolerance and genuineness. With the former property, entire groups may contain faulty computers; with the latter, to deliver a message m, protocols only involve the groups addressed by m. Performance at the multicast layer is obtained by minimizing the latency to deliver multicast messages. At the replication layer, data is partitioned among groups. This allows for more scalability than found in traditional replicated systems since sites only handle a fraction of the workload. We show how convoy effects can appear in partially replicated systems and propose techniques to reduce these effects. Experimental evaluations compare the proposed solutions.
08 February 2010, 2:00 PM
Jade Alglave
Inria
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Fences in Weak Memory Models
Abstract:
We present an axiomatic framework, implemented in Coq, to define weak memory models w.r.t. several parameters: local reorderings of reads and writes, and visibility of inter and intra processor communications through memory, including full store atomicity relaxation. Thereby, we give a formal hierarchy of weak memory models, in which we provide a formal study of what should be the action and placement of fences to restore a given model such as Sequential Consistency from a weaker one. Finally, we provide a tool, diy, that tests a given machine to determine the architecture it exhibits. We detail the results of our experiments on Power and the model we extract from it. This identified an implementation error in Power 5 memory barriers (for which IBM is providing a software workaround); our results also suggest that Power 6 does not suffer from this problem.
03 February 2010, 2:00 PM
Aniket Kate
University of Waterloo
Saarbrücken, Building MPI-SWS, Room 5th floor
Title: Distributed Key Generation and its Applications
Abstract:
Although distributed key generation (DKG) has been studied for some time, it has never been examined outside of the synchronous communication setting. In this talk, I will present the first practical and provably secure asynchronous DKG protocol and its implementation for use over the Internet. I will also discuss cryptographic properties such as uniform randomness of the shared secret, and will provide proactive security and group modification primitives. Notably, this asynchronous DKG protocol requires a set agreement protocol, and implements it using a leader-based Byzantine agreement scheme. In the second half of the talk, I will describe applications of the DKG protocol in designing distributed private-key generators (PKGs) for identity-based cryptography (IBC), a pairing-based onion routing (PB-OR) circuit construction and two robust communication protocols in distributed hash tables. Looking in detail at PB-OR, I will describe a provably secure privacy-preserving key agreement scheme in the IBC setting with distributed PKG and use it to design an efficient and compact onion routing circuit construction that is secure in the universal composability framework.
02 February 2010, 2:00 PM
Sorelle Friedler
University of Maryland
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: A Sensor-Based Framework for Kinetic Data
Abstract:
We introduce a framework for storing and processing kinetic data observed by sensor networks, such as highway traffic or migratory birds. These sensor networks generate vast quantities of data, which motivates a significant need for data compression. We are given a set of sensors, each of which continuously monitors some region of space. We are interested in the kinetic data generated by a finite set of objects moving through space, as observed by these sensors. Our model relies purely on sensor observations; it allows points to move freely and requires no advance notification of motion plans. Sensor outputs are represented as random processes, where nearby sensors may be statistically dependent. We model the local nature of sensor networks by assuming that two sensor outputs are statistically dependent only if the two sensors are among the k nearest neighbors of each other. We present an algorithm for the lossless compression of the data produced by the network. We show that, under the statistical dependence and locality assumptions of our framework, asymptotically this compression algorithm encodes the data to within a constant factor of the information-theoretic lower bound optimum dictated by the joint entropy of the system. We also present an efficient algorithm for answering spatio-temporal range queries. Our algorithm operates on a compressed representation of the data, without the need to decompress it. We analyze the efficiency of our algorithm in terms of two natural measures of information content, the statistical and empirical joint entropies of the sensor outputs. We show that with space roughly equal to entropy, queries can be answered in time that is roughly logarithmic in entropy. These results represent the first solution to range searching problems over compressed kinetic sensor data and set the stage for future statistical analysis. This is joint work with David Mount.
11 January 2010, 3:00 PM
Marco Shapiro and Pierre Sutra
LIP6
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Fault-tolerant partial replication at large-scale
Abstract:
Experience with many applications (e.g., web caching, P2P sharing, and grid and cloud computing) shows that data replication is a fundamental feature of large systems. Replication improves performance, availability and dependability. Replication algorithms based on state machine replication are attractive because they maintain a simple sequential semantics. However, we believe they will not scale to massive cloud and peer-to-peer systems. To be successful, future algorithms must: (1) support multi-object transactions across distant data centres, (2) leverage the semantics of data accesses, and (3) support partial replication. In the first part of this talk, we describe two variants of Generalized Paxos, a solution to consensus that leverages the commutativity semantics. Our algorithms reduce message delay when a collision occurs between non-commuting operations. In the second part, we present a new approach to partial replication of database systems at large scale. Previous protocols either reexecute transactions entirely and/or compute a total order of transactions. In contrast, ours applies update values, and generate a partial order between mutually conflicting transactions only.
15 December 2009, 2:00 PM
Brad Chen
Google Inc.
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Saarbrücken, Building E1 4 - MPI-INF, Room 007)
Title: Reinventing The Desktop
Abstract:
Desktop software, in the form of web browsers, browser features, and OS distributions, are a growing area of engineering activity at Google. This talk will give an overview of this work, looking in detail at Native Client as an example project in the space. Native Client is an open-source technology for running untrusted native code in web applications, with the goal of maintaining the browser neutrality, OS portability, and safety that people expect from web apps. It supports performance-oriented features generally absent from web application programming environments, such as thread support, instruction set extensions such as SSE, and use of compiler intrinsics and hand-coded assembler. We combine these properties in an open architecture designed to leverage existing web standards, and to encourage community review and 3rd-party tools. Overall, Google's desktop efforts seek to enable new Web applications, improve end-user experience, and enable a more flexible balance between client and server computing. Google has open sourced many of our desktop efforts, in part to encourage collaboration and independent innovation.
07 December 2009, 2:00 PM
Anirban Mahanti
NICTA
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Characterization of an Online Social Aggregation Service
Abstract:
Many Web users have accounts with multiple different social networking services. This has prompted development of services that aggregate information available through various services. This talk will consider one such aggregation service, FriendFeed. The first part of the talk will consider questions such as what types of services users aggregate content from, the relative popularity of services, who follows the aggregated feeds, and why. The second part of the talk will focus on factors such as proximity, common interests, time spent in the system, and combinations thereof, and their influence in link formation. Results based on data collected from FriendFeed between September 2008 and May 2009 will be presented. This talk is based on joint work with Martin Arlitt (HP Labs/University of Calgary), Niklas Carlsson (University of Calgary), Sanchit Garg (IIT Delhi), and Trinabh Gupta (IIT Delhi).
04 December 2009, 2:00 PM
Stefan Saroiu
Microsoft Research
Saarbrücken, Building MPI-SWS, Room 5th floor
Title: Improving the Privacy of Online Social Networks and Cloud Computing
Abstract:
This talk has two parts. In the first part, I will present Lockr, a system that improves the privacy of online social networks (OSNs). Lockr offers three significant privacy benefits to OSN users. First, it separates social networking content from all other functionality that OSNs provide. This decoupling puts users in control of their own social information: they decide which OSN providers should store it, which third parties should have access to it, or they can even choose to manage it themselves. Second, Lockr ensures that digitally signed social relationships needed to access social data cannot be re-used by an OSN site for unintended purposes. This feature drastically reduces the value of the social content that users entrust to their OSN providers. Finally, Lockr enables message encryption using a social relationship key. This key lets two strangers with a common friend verify their relationship without exposing it to others, a common privacy threat when sharing data in a decentralized scenario. In the second part, I will present our ongoing work in improving privacy when users run their code in the infrastructure. This is becoming an increasingly common scenario as cloud computing and mobile computing are becoming more popular. I will start by discussing these scenarios, after which I will present our current work in minimizing the attack surface exposed to malicious users and operators in VM-based cloud environments. Lockr is joint work with Alec Wolman (MSR), Amin Tootoonchian, and Yashar Ganjali (U. of Toronto). For more information or to download our Lockr implementations for Flickr and for BitTorrent, please visit http://www.lockr.org. The second part is work-in-progress that is jointly done with Alec Wolman (MSR) and Shravan Rayanchu (U. of Wisconsin).
02 December 2009, 11:00 AM
Eno Thereska
Microsoft Research
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Sierra: a power-proportional, distributed storage system
Abstract:
I'll present the design, implementation, and evaluation of Sierra: a power-proportional, distributed storage system. I/O workloads in data centers show significant diurnal variation, with peak and trough periods. Sierra powers down storage servers during the troughs. The challenge is to ensure that data is available for reads and writes at all times, including power-down periods. Consistency and fault-tolerance of the data, as well as good performance, must also be maintained. Sierra achieves all these through a set of techniques including power-aware layout, predictive gear scheduling, and a replicated short-term versioned store. Replaying live server traces from a large e-mail service (Hotmail) shows power savings of at least 23%, and analysis of load from a small enterprise shows that power savings of up to 60% are possible.
30 November 2009, 11:00 AM
Ant Rowstron
Microsoft Research
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: BorgCube: Rethinking the data center
Abstract:
The BorgCube project explores how to combine ideas from high performance computing, networking and distributed systems to create future data centers. A BorgCube has a tight integration between servers, networking and services, achieved by not using any switches or routers. Instead, servers are directly connected to a small set of other servers. The BorgCube uses a k-ary 3-cube (or 3D Torus) physical topology, providing good failure resilience with reduced cost. More importantly, we believe this also creates a platform on which it is easier to build the large-scale core distributed services, e.g. GFS, BigTable and Dynamo, which underpin many of the applications that run in large-scale data centers. Each server has a coordinate creating a namespace, similar to the namespace provided by a structured overlay. However, unusually for an overlay, the physical network topology and virtual topology are the same. This namespace can be exploited by the services, and all functionality is implemented on top of a link-orientated low-level API. We have implemented many services on our prototype BorgCube, including a bootstrap service, several multi-hop routing protocols, and a service supporting unmodified TCP/IP applications allowing them to run on the BorgCube. In this talk I will describe the ideas behind BorgCube, and explain some of our early experiences with writing services for the BorgCube. This is joint work with Paolo Costa and Greg O'Shea.
08 October 2009, 11:00 AM
Graham Steel
ENS-Cachan
Saarbrücken, Building MPI-SWS, Room 5th floor
Title: Differential attacks on PIN Processing APIs
Abstract:
International standards dictate that all processing of customer Personal Identification Numbers (PINs) in the international cash machine network must take place inside special tamper resistant Hardware Security Modules (HSMs). These HSMs have a restricted API designed so that even if an attacker is able to make arbitrary command calls to the device, no customer PINs can be obtained. However, in recent years, a number of attacks have been found on these APIs. Some of them are so-called differential attacks, whereby an attacker makes repeated calls to the API with slightly different parameters, and from the pattern of error messages received, he is able to deduce the value of a PIN. In this talk, I will present some of these attacks, and talk about efforts to analyse them formally. This will include techniques for proving the absence of such attacks in patched APIs, and a practical proposal for improving the security of the network without making large-scale changes to the current infrastructure.
18 September 2009, 11:00 AM
Bruce Maggs
Duke University
Saarbrücken, Building MPI-SWS, Room 5th floor
Title: "Cutting the Electrical Bill for Internet-Scale Systems"
Abstract:
This talk shows how operators of Internet-scale distributed systems, such as Google, Microsoft, and Akamai can reduce electricity costs (but not necessarily energy consumption) by dynamically allocating work among data centers in response to fluctuating energy prices. The approach applies to systems consisting of fully replicated clusters of servers installed in diverse geographical locations where energy can be purchased through spot markets. Using historical energy prices for major energy markets in the United States, as well as usage data from Akamai's content delivery network, we should how much can be saved now, and what might be saved in the future given server technology trends. Joint work with Asfandyar Quershi, Rick Weber, Hari Balakrishnan, and John Guttag.
10 September 2009, 2:00 PM
Eijiro Sumii
Tohoku University, Sendai, Japan
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Saarbrücken, Building E1 4 - MPI-INF, Room 019)
Title: A complete characterization of observational equivalence in polymorphic lambda-Calculus with general references
Abstract:
We give the first sound and complete proof method for observational equivalence in full polymorphic lambda-calculus with existential types and first-class, higher-order references. Our method is syntactic and elementary in the sense that it only employs simple structures such as relations on terms. It is nevertheless powerful enough to prove many interesting equivalences that can and cannot be proved by previous approaches such as logical relations.
04 September 2009, 11:00 AM
Virgilio Almeida
Federal University of Minas Gerais, Brazil
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: *Looking over the evolution of Internet workloads*
Abstract:
The Internet has a number of popular applications and services experiencing workloads with very different, non-trivial and unique properties. The emergence of new applications and computing models (e.g., online social networking, streaming video, games and cloud computing), and the explosive growth in popularity of others (e.g., search, peer-to-peer, e-business, malware), most of which with workloads with not fully understood fundamental properties, make this a research topic of timely relevance. Real workload characterization and modeling provide key insights into the cost-effective design, operation, and management of Internet-based services and systems. This talk looks over the evolution of Internet workloads, by presenting an overview of a variety of real Internet workloads and how they have evolved through the years; from system workload to social workload. It shows the main properties of these workloads and discusses the invariants across different types of workloads. It outlines methodologies and techniques used in workload characterization and modeling. Constructing a model involves tradeoffs between usefulness and accuracy. The talk shows how characterization techniques have been used to capture the most relevant aspects of Internet workloads while keeping the model as simple as possible. The talk concludes showing some examples of how workload models have been used to design efficient Web systems and services.
13 July 2009, 2:00 PM
Ratul Mahajan
Microsoft Research, Redmond
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: "Using Redundancy to Enable Interactive Communication for Moving Vehicles"
Abstract:
Through extensive measurements of wireless connectivity from moving vehicles, I find that packet loss creates significant performance issues for interactive applications. This poor performance exists for both WLAN technologies (e.g., WiFi) and WWAN technologies (e.g., 3G and WiMax). Unlike wired networks, in wireless networks priority-based queuing is not sufficient to reduce packet loss for loss-sensitive applications. I propose that losses should instead be masked through aggressive but controlled use of available redundancy, and I describe two such systems. The first system, called ViFi, targets the use of WiFi from moving vehicles. Current WiFi handoff methods, in which clients communicate with one base station at a time, lead to frequent disruptions in connectivity. ViFi leverages the presence of redundant in-range base stations to reduce disruptions and improve application performance. The second system, called PluriBus, targets the use of 3G or WiMax from moving vehicles. PluriBus leverages the spare capacity in the wireless channel using a novel erasure coding method. In my experiments, each system improves the performance of interactive applications by at least a factor of 2.
08 June 2009, 4:00 PM
Ali R. But
Virginia Tech
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Rethinking Storage Space Management in High-Performance Computing Centers
Abstract:
Modern scientific applications, such as computer models for analyzing data from particle colliders or space observatories, process data that is exponentially growing in size. High-performance computing (HPC) centers that support such applications are now faced with a data deluge, which can no longer be managed using ad hoc approaches in use today. Consequently, a fundamental reevaluation of the data management tools and techniques is required. In this talk, I will describe a fresh approach to HPC storage space management, especially for the center scratch space --- a high speed storage used for servicing currently running and soon to run applications --- which effectively treats the storage as a tiered cache and provide comprehensive integrated storage management. I will discuss how the caching model is achieved, and how its mechanisms are supported through just-in-time staging and timely offloading of data. Finally, I will show how this approach can also mitigate the effects of center storage failures. The overall goal is to improve HPC center serviceability and resource utilization.
28 May 2009, 1:00 PM
Ben Y. Zhao
UC Santa Barbara
Saarbrücken, Building MPI-SWS, Room 5th floor
Title: Online Social Networks and Applications: a Measurement Perspective
Abstract:
With more than half a billion users worldwide, online social networks such as Facebook are popular platforms for interaction, communication and collaboration between friends. Researchers have recently proposed an emerging class of Internet applications that integrate relationships from social networks to improve security and performance. But can these applications be effective in real life? And if so, how can we predict their effectiveness when they are deployed on real social networks? In this talk, we will describe recent research that tries to answer these questions using measurement-based studies of online social networks and applications. Using measurements of a socially-enhanced web auction site, we show how social networks can actually reduce fraud in online transactions. We then discuss the evaluation of social network applications, and argue that existing methods using social graphs can produce to misleading results. We use results from a large-scale study of the Facebook network to show that social graphs are insufficient models of user activity, and propose the use of "interaction graphs" as a more accurate model. We construct interaction graphs from our Facebook datasets, and use both types of graphs to validate two well-known social-based applications (Reliable Email and SybilGuard). Our results reveal new insights into both systems and confirm our hypothesis that choosing the right graph model significantly impacts predictions of application performance.
20 May 2009, 3:00 PM
Olga Brukman
Ben-Gurion University
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Saarbrücken, Building E1 4 - MPI-INF, Room 019)
Title: Self-Stabilizing Autonomic Recoverers
Abstract:
In this talk I will cover research conducted towards my PhD dissertation. This dissertation introduces theoretical foundations for system architectures and algorithms for creating truly robust autonomic systems -- systems that are able to recover automatically from unexpected failures. Our approaches complement each other starting with the case of given black-box systems, continuing with the process of developing new systems, and concluding with the case of automatic creation of recovery-oriented software. In the first part we consider software packages to be black boxes. We propose modeling software package flaws (bugs) by assuming eventual Byzantine behavior of the package. A general, yet practical, framework and paradigm for the monitoring and recovery of systems called autonomic recoverer is proposed. The framework receives task specific requirements in the form of safety and liveness predicates and recovery actions. The autonomic recoverer uses a new scheme for liveness assurance via on-line monitoring that complements known schemes for on-line safety assurance. In the second part we consider a software package to be a transparent box and introduce the recovery oriented programming: programs will include important safety and liveness properties and recovery actions as an integral part of the program. We design a pre-compiler that produces augmented code for monitoring the properties and executing the recovery actions upon a property violation. Assuming the restartability property of a given program, the resulting code is able to overcome safety and liveness violations. We provide a correctness proof scheme for proving that the code produced by the pre-compiler from the program code combined with the important properties and recovery actions fulfills its specifications when started in an arbitrary state. Finally, in the third part we consider a highly dynamic environment, which typically implies that there are no realizable specifications for the environment, i.e., there does not exist a program that respects the specifications for every given environment. In such cases the predefined recovery action may not suffice and a dramatic change in the program is required. We suggest to search for a program in run time by trying all possible programs on plant replicas in parallel, where the plant is the relevant part of the environment. We present control search algorithms for various settings plant state settings (reflection and ability to set plant to a certain state).
15 May 2009, 11:00 AM
Balachander Krishnamurthy
AT&T Labs - Research
Saarbrücken, Building MPI-SWS, Room Wartburg, 5th floor
Title: "Internet Privacy Diffusion: A longitudinal perspective"
Abstract:
For the last few years we have been examining the leakage of privacy on the Internet from one specific angle: how information related to individual users is aggregated as they browse seemingly unrelated Web sites. Thousands of Web sites across numerous categories, countries, and languages were studied to generate a privacy "footprint". This talk reports on our longitudinal study consisting of multiple snapshots of our examination of such diffusion over four years. We examine the various technical ways by which third-party aggregators acquire data and the depth of user-related information acquired. We study techniques for protecting privacy diffusion as well as limitations of such techniques. We introduce the concept of secondary privacy damage. Our results show increasing aggregation of user-related data by a steadily decreasing number of entities. A handful of companies are able to track users' movement across almost all of the popular Web sites. Virtually all the protection techniques have significant limitations highlighting the seriousness of the problem and the need for alternate solutions. I will also talk about a recent discovery of large-scale leakage of personally identifiable information (PII) via Online Social Networks (OSN). Third-parties can link PII with user actions both within OSN sites and elsewhere on non-OSN sites.
15 May 2009, 3:00 PM
John Wilkes
Google, Mountain View California
Saarbrücken, Building MPI-SWS, Room Wartburg, 5th floor
Title: Traveling to Rome: a retrospective on the journey
Abstract:
Starting in 1994/5, the Storage Systems Program at HP Labs embarked on a decade-long journey to automate the management of enterprise storage systems by means of a technique we initially called attribute-managed storage. The key idea was to provide declarative specifications of workloads and their needs, and of storage devices and their capabilities, and to automate the mapping of one to the other. One of many outcomes of the project was a specification language we called Rome – hence the title of this talk, which offers a retrospective on the overall approach and some of the lessons we learned along the way.
13 May 2009, 3:00 PM
Zaynah Dargaye
ENSIIE, Evry
Saarbrücken, Building MPI-SWS, Room Wartburg, 5th floor (simultaneous videocast to Saarbrücken, Building E1 4 - MPI-INF, Room 019)
Title: Formal Verification of Realistic Compilers
Abstract:
It is generally expected that the compiler is semantically transparent, that is, produces executable code that behaves as prescribed by the semantics of the source code. However, compilers -- and especially optimizing compilers, which attempt to increase the efficiency of generated code through program analyses and transformations -- are highly complex software systems that perform delicate symbolic computations. Bugs in the compiler are therefore unavoidable : they can cause wrong code to be produced from a correct source code The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs. This talk describes the formal verification of compilers and focuses on two experimentation : the C CompCert compiler and the MLCompCert compiler. MLCompCert is the mechanically verified compiler for the purely functional fragment of ML that I have developed and verified in Coq in my Ph. D. thesis.
11 May 2009, 4:00 PM
Moises Goldszmidt
Microsoft Research, Silicon Valley
Saarbrücken, Building MPI-SWS, Room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Fingerprinting performance crises in the datacenter
Abstract:
We propose a method for significantly reducing troubleshooting and diagnosis time in the datacenter by automatically generating fingerprints of performance crises, enabling fast classification and recognition of recurring instances. We evaluated the approach on data from a production datacenter with hundreds of machines running a 24x7 enterprise-class user-facing application, verifying each identification result with the operators of the datacenter (and the corresponding troubleshooting tickets). The approach has 80% identification accuracy in the operations-online setting with time to identification below 15 minutes (on average) after the start of the crises (operators stipulated a deadline of 60 minutes). In an offline setting, where some parameters can be fitted optimally, the accuracy is on the 95%-98% range. After explaining the fingerprinting method and the results, I will end the talk with a discussion on the possibility of predicting the crises, and on extending this work to model the operator’s repair actions for learning models of automated decision making. Joint work with Peter Bodik and Armando Fox from UC Berkeley, and Hans Andersen from Microsoft.
04 May 2009, 4:00 PM
John C. Mitchell
Stanford University
Saarbrücken, Building E1 4 - MPI-INF, Room 019
Title: JavaScript Isolation and Web Security
Abstract:
Web sites that incorporate untrusted content may use browser-or language-based methods to keep such content from maliciously altering pages, stealing sensitive information, or causing other harm. We use accepted methods from the study of programming languages to investigate language-based methods for filtering and rewriting JavaScript code, using Facebook's FBJS as a motivating example. We explain the core problems by describing previously unknown vulnerabilities and shortcomings, provide JavaScript code that enforces provable isolation properties at run-time, and develop a foundation for improved solutions based on an operational semantics of the full ECMA262 language. We also compare our results with the techniques used in FBJS. Joint work with Sergio Maffeis and Ankur Taly
29 April 2009, 4:00 PM
David Molnar
Univeristy of California at Berkeley
Saarbrücken, Building E1 4 - MPI-INF, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Theory Plus Practice in Computer Security : Radio FrequencyIdentification and Whitebox Fuzzing
Abstract:
I will describe two areas in computer security that demonstrate the wide range of techniques, from both theory and practice, we need to make impact. First, I treat privacy and security in Radio Frequency Identification (RFID). RFID refers to a range of technologies where a small device with an antenna, or "tag" is attached to an item and can be queried later wirelessly by a reader. While proponents of RFID promise security and efficiency benefits, the technology also raises serious security concerns. I will describe my work on practical security analysis of RFID in library books and the United States e-passport deployments. These deployments in turn uncover a new theoretical problem, that of "scalable private authentication." I will describe the first solution to this problem that scales sub-linearly in the number of RFID tags. Second, I describe recent work in "whitebox fuzz testing," a new approach to finding security bugs. Security bugs cost millions of dollars to patch after the fact, so we want to find and fix them as early in the deployment cycle as possible. I review previous fuzz testing work, how fuzzing has been responsible for serious security bugs, and classic fuzz testing's inability to deal with "unlikely" code paths. I then show how marrying the idea of dynamic test generation with fuzz testing overcomes these shortcomings, but raises significant scaling problems. Two recent tools, SAGE at Microsoft Research, and SmartFuzz at Berkeley, overcome these scaling problems; I present results on the effectiveness of these tools on commodity Windows and Linux media playing software. Finally, I close with directions for leveraging cloud computing to improve developers' testing and debugging experience. The talk describes joint work with Ari Juels and David Wagner (RFID), and with Patrice Godefroid, Michael Y. Levin, and Xue Cong Li and David Wagner (Whitebox Fuzzing).
27 April 2009, 4:00 PM
Sachin Katti
University of California at Berkeley
Kaiserslautern, Building MPI-SWS, Room 204 (simultaneous videocast to Saarbrücken, Building MPI-SWS, Room Wartburg OG 5)
Title: "Network Coded Wireless Architecture"
Abstract:
Wireless is becoming the preferred mode of network access. The performance of wireless networks in practice, however, is hampered due to the harsh characteristics of the wireless medium: its shared broadcast nature, interference, and high error rate. Traditionally, network designers have viewed these characteristics as problematic, and tried to work around them. In this talk, I will show how we can turn these challenges into opportunities that we exploit to significantly improve performance. To do so, we use a simple yet fundamental shift in network design. We allow routers to "mix" (i.e., code) packets' content before forwarding them. We built three systems, COPE, ANC and MIXIT, which exploit this network coding functionality via novel algorithms to provide large practical gains. In this talk, I will discuss COPE and ANC; COPE exploits wireless broadcast, while ANC exploits strategic interference to improve throughput. This work bridges and contributes to two unrelated areas: network coding and wireless mesh network design. It lays down the algorithmic framework for using network coding in modern wireless networks, by designing algorithms which work with the common case of unicast flows in dynamic and unknown environments. It also provides the first implementation, deployment and experimental evaluation of network coding. For wireless mesh networks, it shows how the framework of network coding allows us to profitably harness the inherent wireless characteristics. This union ultimately allows us to deliver a several-fold increase in wireless throughput.
20 April 2009, 1:30 PM
Neelakantan R. Krishnaswami
CMU Computer Science Department at Pittsburgh
Saarbrücken, Building MPI-SWS, Room Wartburg OG 5 (simultaneous videocast to Saarbrücken, Building E1 4 - MPI-INF, Room 019)
Title: "Proving GUIs Correct: Verifying Higher-Order Imperative Programs withHigher-Order Separation Logic"
Abstract:
O'Hearn and Reynolds' separation logic has proven to be a very successful attempt at taming many of the difficulties associated with reasoning about aliased, mutable data structures. Using it, researchers have given correctness proofs of even quite intricate low-level imperative programs such as garbage collectors and device drivers. However, high level languages such as ML and Haskell also give programmers access to mutable, aliased data, and when those features are used, programmers are still prone to all the troubles state is heir to. In fact, many problems become more complex, since these languages encourage the use of an abstract, higher-order style, and support the design of libraries that rely on higher-order functions as well as callbacks (ie, references to functions in the heap). In this talk, I'll describe work I've done (in collaboration with my PhD supervisors) designing a version of separation logic suitable for use in languages such as ML, and describe an application of this logic to formally verifying the correctness of a small library for writing event-driven programs in a lazy dataflow style. This then allows an efficient imperative implementation of a functional reactive programming library.
16 April 2009, 4:00 PM
Umut A. Acar
Toyota Technological Institute at Chicago
Saarbrücken, Building E1 4 - MPI-INF, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 204/206)
Title: Self - Ajusting Computation
Abstract:
Many application domains require computations to interact with data sets that change slowly or incrementally over time. For example, software systems that interact with the physically changing world, e.g., databases, graphical systems, robotic software systems, program-development environments, scientific-computing applications, must respond efficiently and correctly to changes as they occur in the world. Since incremental modifications to data are often small, they can be processed asymptotically faster than re-computing from scratch, often generating orders of magnitude speedups in practice. Realizing this potential using traditional techniques, however, often requires complex algorithmic and software design and implementation, ultimately limiting the range of problems that can effectively be addressed in practice. In this talk, I present an overview of advances on self-adjusting computation: an approach to developing software systems that interact with changing data. I start by presenting the principle ideas behind a mechanism for propagating a change through a computation, and then describe the design of programming-language constructs for enabling computations to respond automatically and efficiently to modifications to their data. I show that these language constructs are realistic by describing how to extend existing languages with them and how to compile the extended languages into provably efficient executables, whose performance properties can be analyzed via cost semantics. To evaluate the effectiveness of the approach, I consider a number of benchmarks as well as more sophisticated applications from diverse areas such as computational geometry, scientific computing, machine learning, and computational biology. Our results show that self-adjusting computation can be broadly effective in achieving efficient implementations, solving open problems, and pointing to new research directions. In practice, our measurements show that self-adjusting programs often respond to incremental modifications by a linear factor faster than recomputing from scratch, resulting in orders of magnitude speedups.
14 April 2009, 4:00 PM
Aleksandar Nanevski
Microsoft Research, Cambridge, UK
Saarbrücken, Building E1 4 - MPI-INF, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 204/206)
Title: Programming with Hoare Type Theory
Abstract:
Two main properties make type systems an effective and scalable formal method. First, important classes of programming errors are eliminated by statically enforcing the correct use of values. Second, types facilitate modular software development by serving as specifications of program components, while hiding the component's actual implementation. Implementations with the same type can be interchanged, thus facilitating software reuse and evolution. Mainstream type systems focus on specifying relatively simple properties that admit type inference and checking with little or no input from the programmer. Unfortunately, this leaves a number of properties, including data structure invariants and API protocols outside of their reach, and also restricts the practical programming features that can be safely supported. For example, most simply-typed languages cannot safely allow low-level operations such as pointer arithmetic or explicit memory management. In this talk, I will describe Hoare Type Theory (HTT) which combines dependent types of a system like Coq with features for specification and verification of low-level stateful operations in the style of Hoare and Separation Logic. Such a combination is desirable for several reasons. On the type-theoretic side, it makes it possible to integrate stateful behaviour into dependent type theories that have so far been purely functional. On the Hoare Logic side, it makes is possible to use the higher-order data abstraction and information hiding mechanisms of type theory, which are essential for scaling the verification effort. I will discuss the implementation of HTT, verification of various examples that I have carried out, as well as the possibilities for extending HTT to support further programming features such as concurrency.
23 March 2009, 4:00 PM
Matthew Fluet
Toyota Technological Institute at Chicago
Saarbrücken, Building E1 4 - MPI-INF, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Functional Programming Perspectives on Concurrency and Parallelis
Abstract:
The trend in microprocessor design toward multicore processors has sparked renewed interest in programming languages and language features for harnessing concurrency and parallelism in commodity applications. Past research efforts demonstrated that functional programming provides a good semantic base for concurrent- and parallel-language designs, but slowed in the absence of widely available multiprocessor machines. I will describe new functional programming approaches towards concurrency and parallelism, grounded in more recent functional programming research. To frame the discussion, I will introduce the Manticore project, an effort to design and implement a new functional language for parallel programming. Unlike some earlier parallel language proposals, Manticore is a heterogenous language that supports parallelism at multiple levels. In this talk, I will describe a number of Manticore's notable features, including implicitly-parallel programming constructs (inspired by common functional programming idioms) and a flexible runtime model that supports multiple scheduling disciplines. I will also take a deeper and more technical look at transactional events, a novel concurrency abstraction that combines first-class synchronous message-passing events with all-or-nothing transactions. This combination enables elegant solutions to interesting problems in concurrent programming. Transactional events have a rich compositional structure, inspired by the use of monads for describing effectful computations in functional programming. I will conclude with future research directions in the Manticore project, aiming to combine static and dynamic information for the implementation and optimization of parallel constructs.
19 March 2009, 4:00 PM
Serge Egelman
Carnegie Mellon
Saarbrücken, Building MPI-SWS, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: "Usable Security Lessons for Creating Effective Browser Warnings"
Abstract:
In a world where making an incorrect online trust decision can mean the difference between checking your account balance and transferring it to criminals, Internet users need effective security warnings to help them identify risky situations. In a perfect world, software could automatically detect all security threats and then block access to high risk websites. Because there are many threats that we cannot detect with 100% accuracy and false positives are all too frequent, web browser vendors generally opt to warn users about security threats. In this talk I cover the common pitfalls of web browser security warnings and draw parallels with literature in the warning sciences. I describe the results of two laboratory phishing studies I performed in order to examine users' mental models, risk perceptions, and comprehension of current security warnings. Finally, I show how I used these findings to iteratively design and test a more usable SSL warning that clearly conveys risk and uses context to minimize habituation effects.
10 March 2009, 4:00 PM
Amal Ahmed
Toyota Technological Institute Chicago
Saarbrücken, Building E1 4 - MPI-INF, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Logical Relations: A Step Towards More Secure and Reliable Software
Abstract:
Logical relations are a powerful proof technique for establishing many important properties of programs, programming languages, and language implementations. In particular, they provide a convenient method for proving behavioral equivalence of programs. Hence, they may be used to show that one implementation of an abstract data type (ADT) can be replaced by another without affecting the behavior of the rest of the program; to prove that security-typed languages satisfy noninterference, which requires that confidential data not affect the publicly observable behavior of a program; and to establish the correctness of compiler optimizations. Yet, despite three decades of research and much agreement about their potential benefits, logical relations are still primarily used to reason about languages that are not even Turing complete. The method has not scaled well to many features found in practical programming languages: support for recursive types (lists, objects) and mutable memory (as in Java or ML) requires sophisticated mathematical machinery (e.g., domain theory, category theory), which makes the resulting logical relations cumbersome to use and hard to extend. Mutable memory is particularly problematic, especially in combination with features like generics (parametric polymorphism) and ADTs. In this talk, I will describe *step-indexed* logical relations which support all of the language features mentioned above and yet permit simple proofs based on operational reasoning, without the need for complicated mathematics. To illustrate the effectiveness of step-indexed logical relations, I will discuss three applications. The first is a secure multi-language system where we show that code written in different languages may interoperate without sacrificing the abstraction guarantees provided by each language in isolation. The second is imperative self-adjusting computation, a system for efficiently updating the results of a computation in response to changes to some of its inputs; we show that our update mechanism is consistent with a from-scratch run. The third is security-preserving compilation, which ensures that compiled code is no more vulnerable to attacks launched at the level of the target language than the original code is to attacks launched at the level of the source language; we show that the typed closure conversion phase of a compiler has this property.
25 February 2009, 11:00 AM
Bruce Allen
Max-Planck-Institut fuer Gravitationsphyik
Saarbrücken, Building MPI-SWS, Room conf.room 5th floor (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 204/206)
Title: "A distributed file system wish-list"
Abstract:
My research group at the MPI for Gravitational Physics, Hannover, operates a large computer cluster used for data analysis. In principle, the most cost-effective and highest-bandwidth data storage available is the disks local to the compute nodes. In the case of Atlas, there are 1680 disks with an aggregate capacity of 840 TB. With a suitable file system the array of these disks could form a highly reliable storage system, however at the moment there appears to be no open-source distributed file system with the necessary RAID-like properties. In this talk I present a list and description of the properties that such a file-system should have, and arguments to support the case that it should be possible to achieve this in the real world. If such a file system were available, I believe that thousands of large computer clusters around the world would employ and benefit from it.
24 February 2009, 4:00 PM
Krishnendu Chatterjee
Univeristy of California at Berkeley
Saarbrücken, Building E1 4 - MPI-INF, Room 019 (simultaneous videocast to Kaiserslautern, Building MPI-SWS, Room 206)
Title: Stochastic Games in Synthesis and Verification
Abstract:
Dynamic games played on game graphs with winning conditions specified as automata provide the theoretical framework for the study of controller synthesis and many problems related to formal verification. Besides synthesis and verification, these games have been used in several other contexts such as checking interface compatibility, modular reasoning, checking receptiveness. In this talk we first present different game models, that are suited to different applications, and the canonical winning conditions that can be specified as automata. We first consider the strictly competitive (zero-sum) game formulation that is appropriate for controller synthesis. We present a brief overview of the field, summarizing the classical results, and then present our results that significantly improve the complexity for several classes of games. We also present practical algorithms for analysis of several classes of such games. We then consider the problem of multi-process verification and argue that the zero-sum formulation is too strong for multi-process verification. This is because the environment for a process is typically other processes with their own specifications. On the other hand, the notion of Nash equilibria, that captures the notion of rational behavior in absence of external criteria, is too weak for multi-process verification. We will present a new notion of equilibrium, which we call secure equilibrium. We will show how the new notion of equilibrium is more appropriate for multi-process verification, discuss the existence and computation of such equilibrium for graph games.
21 November 2008, 2:00 PM
Dejan Kostic
EPFL
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: "CrystalBall: Predicting and Preventing Inconsistencies in Deployed Distributed Systems"
Abstract:
Distributed systems form the foundation of our society's infrastructure. Complex distributed protocols and algorithms are used in enterprise storage systems, distributed databases, large-scale planetary systems, and sensor networks. Errors in these protocols translate to denial of service to some clients, potential loss of data, and even monetary losses. Unfortunately, it is notoriously difficult to develop reliable high-performance distributed systems that run over asynchronous networks, such as the Internet. Even if a distributed system is based on a well-understood distributed algorithm, its implementation can contain coding bugs and errors arising from complexities of realistic distributed environments. This talk describes CrystalBall, a new approach for developing and deploying distributed systems. In CrystalBall, nodes predict distributed consequences of their actions, and use this information to detect and avoid errors. Each node continuously runs a state exploration algorithm on a recent consistent snapshot of its neighborhood and predicts possible future violations of specified safety properties. We describe a new state exploration algorithm, consequence prediction, which explores causally related chains of events that lead to property violation. Using CrystalBall, we identified new bugs in mature Mace implementations of a random overlay tree, BulletPrime content distribution system, and the Chord distributed hash table. Furthermore, we show that if the bug is not corrected during system development, CrystalBall is effective in steering the execution away from inconsistent states at run-time, with low false negative rates.
14 November 2008, 2:00 PM
Michael Walfish
University of Texas and University College London
Saarbrücken, Building MPI-SWS, Room Rotunda 6th floor
Title: Defending Networked Resources Against Floods of Unwelcome Requests
Abstract:
The Internet is afflicted by unwelcome "requests", defined broadly as claims on a scarce resource, such as a server's CPU (in the case of spurious traffic whose purpose is to deny service) or a human's attention (in the case of spam). Traditional responses to these problems apply heuristics: they try to identify "bad" requests based on their content (e.g., in the way that spam filters analyze an email's text). This talk argues that heuristics are inherently gameable and that defenses should instead aim to allocate resources proportionally to all clients (so if, say, 10% of the requesters of some scarce resource are "bad", those clients should be limited to 10% of the resources). To meet this goal, this talk presents two systems. The first is a denial-of-service mitigation in which clients are encouraged to automatically send *more* traffic to a besieged server. The "good" clients can thereby compete equally with the "bad" ones. The second is a distributed system for enforcing per-sender email quotas to control spam. This system scales to a workload of millions of requests per second, tolerates arbitrary faults in its constituent hosts, and resists a variety of attacks. It achieves this fault-tolerance despite storing only one copy (roughly) of any given datum and, ultimately, does a fairly large job with fairly little mechanism.
13 November 2008, 2:00 PM
Ricardo Jimenez-Peris
TU Madrid
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: "Boosting Database Replication through Snapshot Isolation"
Abstract:
Database replication has received a lot of attention during the last decade. This wave of research has concentrated on how to obtain scalable database replication. This talk will be devoted to the most recent advances on how to attain scalable database replication contributed by the Distributed Systems Lab (LSD) at Universidad Politenica de Madrid. It will address the most important bottlenecks that limit scalability such as isolation level, degree of replication, recovery, and engineering issues. The talk will cover techniques to overcome these bottlenecks. Special emphasis will be put on the role of snapshot isolation as enabling factor of large scalability to overcome the scalability limit of serializability. The talk will also cover other techniques building upon snapshot isolation to overcome other scalability bottlenecks such as partial replication.
18 September 2008, 3:30 PM
Dalibor Topic
Sun Microsystems
Saarbrücken, Building MPI-SWS, Room Rotunda, 6th floor
Title: The Evolution of Java(TM) software on GNU/Li
Abstract:
The inclusion of OpenJDK 6 into the core of Fedora, Debian, OpenSuse and Ubuntu has enabled millions of GNU/Linux users to easily obtain the latest version of the Java SE platform. This has changed the packaging landscape for Java software, since ISVs and distro builders can now rely on the Java platform being available out of the box. Planned enhancements to the Java programming language aim to further simplify packaging by making Java software more modular and more explicit about its dependencies.
08 September 2008, 10:00 AM
Harry Li
UT Austin
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: FlightPath: Obedience vs. Choice
Abstract:
In this talk, I will present FlightPath, a novel peer-to-peer streaming application that provides a highly reliable data stream to a dynamic set of peers. FlightPath offers a more stable stream than previous works by several orders of magnitude. I will explain the techniques we use to maintain such stability despite peers that act maliciously and selfishly. More broadly, this talk will discuss the core of FlightPath's success: approximate equilibria. I will highlight how these equilibria let us rigorously design incentives to limit selfish behavior, yet also provide the flexibility to build practical systems. Specifically, I will show how we use epsilon-Nash equilibria to engineer a live streaming system to use bandwidth efficiently, absorb flash crowds, adapt to sudden peer departures, handle churn, and tolerate malicious activity.
27 August 2008, 4:00 PM
Geoffrey Washburn
EPFL, Switzerland
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: "Foundations for the Scala Language"
Abstract:
The Scala language (http://www.scala-lang.org/) aims to unify object-oriented and functional programming, while maintaining full interoperability with the Java language. However, while Scala has been under active development since 2003, there has yet to be a satisfactory formal model of Scala. There are several calculi that come close, but all have discrepancies in expressive power, some are lacking complete proofs, and some are unsound. In this talk, I will give a short introduction to Scala, review several calculi that fall short of providing a formal model of Scala, and give an overview of the calculus I have been developing, Scala Classic, that will help fill this gap in the foundations of Scala.
25 July 2008, 11:00 AM
Daniel Kroening
Oxford University
Saarbrücken, Building MPI-SWS, Room 007
Title: Verifying C++ programs that use the STL
Abstract:
We describes a flexible and easily extensible predicate abstraction-based approach to the verification of STL usage, and observe the advantages of verifying programs in terms of high-level data structures rather than low-level pointer manipulations. We formalize the semantics of the STL by means of a Hoare-style axiomatization. The verification requires an operational model conservatively approximating the semantics given by the C++ standard. Our results show advantages (in terms of errors detected and false positives avoided) over previous attempts to analyze STL usage.
17 July 2008, 2:00 PM
Ina Schaefer
TU Kaiserslautern
Saarbrücken, Building MPI-SWS, Room 007
Title: Integrating Formal Verification into the Model-based Development of Adaptive Embedded Systems
Abstract:
Model-based development of adaptive embedded systems is an approach to deal with the increased complexity adaptation imposes on system design. Integrating formal verification techniques into this design process providesmeans to rigorously prove critical properties. However, most verification tools are based on foundational models, e.g. automata, unable to express intuitive notions used in model-based development appropriately. Furthermore, automatic methods such as model checking are only efficiently applicable to systems of limited sizes due to the state-explosion problem. Our approach to alleviate these problems uses a semantics-based integrationof model-based development and formal verification for adaptive embedded systems allowing to capture design-level models at a high level of abstraction. Verification complexity induced by the applied modelling concepts is reduced by verified model transformations. These transformations include model slicing, data domain abstractions and compositional reasoning techniques. The overall approach as well as the model transformations have been evaluated together with the development of an adaptive vehicle stability control syste
17 July 2008, 3:00 PM
Michael Ernst
MIT
Saarbrücken, Building MPI-SWS, Room Rotunda 6th floor
Title: Practical pluggable types for Java
Abstract:
This talk introduces the Checker Framework, which supports adding pluggable type systems to the Java language in a backward-compatible way. A type system designer defines type qualifiers and their semantics, and a compiler plug-in enforces the semantics. Programmers can write the type qualifiers in their programs and use the plug-in to detect or prevent errors. The Checker Framework is useful both to programmers who wish to write error-free code, and to type system designers who wish to evaluate and deploy their type systems. The Checker Framework includes new Java syntax for expressing type qualifiers; declarative and procedural mechanisms for writing type-checking rules; and support for flow-sensitive local type qualifier inference and for polymorphism over types and qualifiers. The Checker Framework is well-integrated with the Java language and toolset. We have evaluated the Checker Framework by writing 5 checkers and running them on over 600K lines of existing code. The checkers found real errors, then confirmed the absence of further errors in the fixed code. The case studies also shed light on the type systems themselves.
14 July 2008, 4:00 PM
Athicha Muthitacharoen
MIT
Saarbrücken, Building MPI-SWS, Room Rotunda 6th floor
Title: The Expandable Network Disk
Abstract:
In this talk, I will present my recent work on the Expandable Network Disk (END). END aggregates storage on a cluster of machines into a single virtual disk. END's main goals are to offer good performance during normal operation, and to resume operation quickly after changes in the cluster, specifically machine crashes, reboots, and additions. END achieves these goals using a two-layer design, in which storage ``bricks'' hold two kinds of information. The lower layer stores replicated immutable ``chunks'' of data, each indexed by a unique key. The upper layer maps each block address to the key of its current content; each mapping is held on two bricks using primary-backup replication. This separation allows END flexibility in where it stores chunks and thus efficiency: it writes new chunks to bricks chosen for speed, it moves only address mappings (not data) when bricks fail and recover, it fully replicates new writes when a brick is unavailable, and it uses chunks on a recovered brick without risk of staleness. The END prototype's write throughput on a cluster of 16 PC-based bricks is 150 MByte/s with 2x replication, about 70% of the aggregate throughput of the underlying hardware. END continues after a single brick failure, re-incorporates a rebooting brick, and expand to include a new brick after a few seconds of reduced performance during each change. (Joint work with Robert Morris.)
03 July 2008, 3:00 PM
Neal Glew
Intel Corporation
Saarbrücken, Building MPI-SWS, Room Rotunda 6th floor
Title: Ct and Pillar: Building a Foundation for Many-Core Programming
Abstract:
Seemingly fundamental limitations in hardware manufacturing are driving an industry-wide move away from speedy but complex single core processors towards simpler but massively parallel many-core processors. The job of discovering parallelism (and hence achieving performance) on these new chips is left to software: that is, the programmers and their tools. Parallel programming has traditionally been a specialty area requiring extensive expertise, and non-deterministic concurrency introduces vast new classes of exceptionally difficult to eliminate bugs. In short, the job of programming becomes much harder on many-core processors. In order for programmers to cope successfully with these challenges, the software tools used to program many-core processors must take a giant leap forward. Specifically, programming abstractions and languages must be designed to allow programmers to easily express parallelism in a way that is scalable, performant, and most of all, correct. This talk discusses the problem in more detail, and describes two projects aimed at supporting this goal. The Pillar implementation language is a C-like high level compiler target language intended to provide the key sequential and concurrent constructs needed to efficiently implement task-parallel languages, while the Ct language is a system for exploiting the key area of data-parallelism using ideas from functional programming. Together, these two systems provide a foundation upon which a wide variety of abstractions and languages for expressing parallelism can be built.
30 June 2008, 5:00 PM
Corneliu Popeea
National University of Singapore
Saarbrücken, Building MPI-SWS, Room Rotunda 6th floor
Title: Disjunctive Invariants for Modular Static Analysis
Abstract:
We study the application of modular static analysis to prove program safety and detection of program errors. In particular, we shall consider imperative programs that rely on numerical invariants. To handle the challenges of disjunctive analyses, we introduce the notion of affinity to characterize how closely related is a pair of disjuncts. Finding related elements in the conjunctive (base) domain allows the formulation of precise hull and widening operators lifted to the disjunctive (powerset extension of the) base domain. We have implemented a static analyzer based on the disjunctive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost. Our second objective is to support either a proof of the absence of bugs in the case of a valid program or bug finding in the case of a faulty program. We propose a dual static analysis that is designed to track concurrently two over-approximations: the success and the failure outcomes. Due to the concurrent computation of outcomes, we can identify two significant input conditions: a never-bug condition that implies safety for inputs that satisfy it and a must-bug condition that characterizes inputs that lead to true errors in the execution of the program.
18 June 2008, 10:30 AM
Liuba Shrira
Brandeis University
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: "Split Snapshots: A New Approach to Time Travel in Storage"
Abstract:
Kurzweil says, computers will enable people to live forever and doctors will be doing backup of your memories by late 2030. This talk is not about that, yet. Instead, the remarkable drop in disk costs makes it possible and attractive to retain past application states and store them for a long time for "time-travel". A still open question is how to best organize long-lived past state storage? Split snapshots are a recent approach to virtualized past states that is attractive for several reasons. Split snapshots are persistent, can be taken with high-frequency, and theyare transactionally consistent. Unmodified database application code can run against them. Like no other approach, they provide low-cost discriminated garbage collection of unneeded snapshots, a useful feature in long-lived systems. Lastly, compared to a temporal database, split snapshots are significantly simpler and more general since they virtualize disk blocks rather than logical records. Several novel techniques underly split snapshots. An extended recovery invariant allows to create consistent copy-on-write snapshots without blocking, a new kind of persistent index provides fast snapshot access, and a new snapshot storage organization incrementally garbage collects selected copy-on-write snapshots without copying and without creating disk-fragmentation. Measurements of a prototype system indicate that the new techniques are efficient and scalable, imposing minimal ($4\%$) performance penalty on a storage system, on expected common workloads. (Joint work with Ross Shaull and Hao Xu)
29 May 2008, 3:00 PM
Rob Sherwood
University of Maryland
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: "Securing and Understanding the Internet"
Abstract:
Despite its increasing importance in our lives, the Internet remains insecure and its global properties unknown. Spam, phishing, and Denial of Service (DoS) attacks have become common, while global properties as basic as the router-connectivity graph continue to elude researchers. Further, these two problems are inter-related: curtailing abuse exposes gaps in knowledge of the Internet's underlying structure, and studying the underlying structure exposes new techniques to curtail abuse. My research leverages this insight by working on both securing and understanding the Internet. In this talk, I first discuss my work in securing the Internet by describing Opt-Ack, a DoS attack on the network using optimistic acknowledgments. With this attack, malicious TCP receivers "optimistically" acknowledge packets they did not receive and cause unwitting TCP senders to flood the network. Using Opt-Ack, the resulting traffic flood is hundreds to millions of times the attacker's true bandwidth. I demonstrate randomly skipped segments, an efficient and incrementally deployable solution to the Opt-Ack attack. Second, I describe my work in understanding the Internet with DisCarte, a constraint-solving system that infers the Internet router-connectivity graph. DisCarte uses disjunctive logic programming to cross-validate topology information from TTL-limited traceroute probes and the often ignored IP Record Route option against observed network engineering practices. Compared to previous techniques, router-connectivity graphs produced by DisCarte are more accurate and contain more features.
27 May 2008, 4:00 PM
Virgile Prevosto
CEA, Saclay
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: Specification and Analysis of C(++) programs with Frama-C and ACSL.
Abstract:
D Frama-C is a framework dedicated to build static analyzers for C programs and make them cooperate to achieve better results. One important component of this cooperation is the ANSI/ISO C Specification Language (ACSL), a JML-like language allowing to formally specify the behavior of C functions and statements. The analyses can indeed generate verification conditions as ACSL formulas that will be taken as input by the other ones (and hopefully discharged at some point). This talk will first present the existing Frama-C analyses. Then, we will have a look at the main ACSL constructions. Last, we will show how these constructions can be used for the specification of existing code, and how Frama-C could be extended to deal with C++.
30 April 2008, 11:00 AM
Himabindu Pucha
School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania
Saarbrücken, Building MPI-SWS, Room 019 (simultaneous videocast to Uni Kaiserslautern, Building 34, Room 217)
Title: Rethinking bulk data transfers for next-generation applications
Abstract:
How did you use the Internet today? The answer to this question has significantly evolved in the last decade. Ten years ago, we were browsing simple websites with text and images, and communicating via instant messaging and emails. In addition to these applications, today's users are engaging in on-demand video streaming, multimedia conferencing, and sharing files from software updates to personal music, and as a result transferring large volumes of data (of the order of Mbytes) more frequently than ever. Hence, bulk data transfers at the core of these applications are becoming increasingly important and are expected to provide high throughput and efficiency. Contrary to these expectations, however, our study of file sharing networks confirms previous observations that bulk data transfers are slow and inefficient, motivating the need to rethink their design. In this talk, I will present my approach to address a prominent performance bottleneck for these bulk data transfers: Lack of sufficient sources of data to download from. My work addresses this challenge by (1) exploiting network peers that serve files similar to the file being downloaded, and (2) by coupling all the available network resources with similar data on the local disk of a receiver. My talk will also highlight the system design and implementation for the above solutions. For example, I will discuss handprinting, a novel and efficient algorithmic technique to locate the additional similar network peers with only a constant overhead. Finally, a transfer system that simultaneously benefits from disk and network is required to work well across a diverse range of operating environments and scenarios resulting from varying network and disk performance. I will present the design principles for an all-weather transfer system that adapts to a wide spectrum of operating conditions by monitoring resource availability.
09 April 2008, 2:00 PM
Kashi Vishwanath
University of California, San Diego
Saarbrücken, Building MPI-SWS, Room 019
Title: Demystifying Internet Traffic
Abstract:
The Internet has seen a tremendous growth since its inception four decades ago. With its increasing importance, there has been a growing emphasis on improving the reliability of the infrastructure. One approach to delivering such reliability is for design engineers, network administrators and researchers to stress test potential solutions against a wide variety of deployment scenarios. For instance, web hosting services would wish to ensure that they can deliver target levels of performance and availability under a range of conditions. Similarly, Internet Service Providers (ISPs) would benefit from understanding future growth in traffic demands at individual routers in its network as a function of emerging applications and expanding user base. I argue that one of the key ingredients required to carry out such studies is a deep understanding of Internet traffic characteristics. This talk will try to uncover some of the mysteries surrounding Internet traffic, including its rich structure. I will thus describe the principles and key insights that led to the development of the Swing traffic generator. Swing is the first tool to reproduce realistic and responsive Internet-like traffic in a testbed. Starting from observing packets across a given link, Swing automatically extracts parameters for its detailed multi-level model. It then uses this model to generate live traffic that looks qualitatively similar to the original traffic. More interestingly, Swing provides the user with meaningful knobs to project traffic demands into the future. This includes changing assumptions about user popularity of applications, planned upgrades to the network as well as change in the semantics of applications.
07 April 2008, 3:00 PM
Dimitrios Vytiniotis
University of Pennsylvania
Saarbrücken, Building MPI-SWS, Room Rotunda
Title: Practical Type Inference for first-class Polymorphism
Abstract:
Type inference is a key component of modern, statically typed, functional programming languages, such as Caml and Haskell. It allows programmers to omit many excessive---and in some cases all---type annotations from programs. A different key component of modern programming languages is polymorphism. However, languages with polymorphism typically have ad-hoc restrictions on where and what kind of polymorphic types may occur. Supporting ``first-class'' polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve without sacrificing type inference. In this talk I will explain the difficulties with type inference for first-class polymorphism, give a historic roadmap of the research on this topic, and present a new type system for first-class polymorphism that improves on earlier proposals: it is an extension of ML type inference; it has a simple, declarative specification; typeability is robust to program transformations; and the specification enjoys a sound, complete and decidable type inference algorithm. This is joint work with Stephanie Weirich and Simon Peyton Jones.
06 March 2008, 4:00 PM
Bryan Ford
MIT
Saarbrücken, Building MPI-SWS, Room 019
Title: Intuitive Global Connectivity for Personal Mobile Devices
Abstract:
Network-enabled mobile devices are quickly becoming ubiquitous in the lives of ordinary people, but current technologies for providing ubiquitous global *connectivity* between these devices still require experts to set up and manage. Users must allocate and maintain global domain names in order to connect to their devices globally via DNS, they must allocate a static IP address and run a home server to use Mobile IP or set up a virtual private network, they must configure firewalls to permit desired remote access traffic while filtering potentially malicious traffic from unknown parties, and so on. This model of "management by experts" works for organizations with administrative staff, but is infeasible for most consumers who wish to set up and manage their own personal networks. The Unmanaged Internet Architecture (UIA) is a suite of design principles and experimental protocols that provide robust, efficient global connectivity among mobile devices while relying for configuration only on simple, intuitive management concepts. UIA uses "personal names" rather than traditional global names as handles for accessing personal devices remotely. Users assign these personal names via an ad hoc device introduction process requiring no central allocation. Once assigned, personal names bind securely to the global identities of their target devices independent of network location. Each user manages one namespace, shared among all the user's devices and always available on each device. Users can also name other users to share resources with trusted acquaintances. Devices with naming relationships automatically arrange connectivity when possible, both in ad hoc networks and using global infrastructure when available. We built a prototype implementation of UIA that demonstrates the utility and feasibility of these design principles. The prototype includes an overlay routing layer that leverages the user's social network to provide robust connectivity in spite of network failures and asymmetries such as NATs, a new transport protocol implementing a novel stream abstraction that more effectively supports the highly parallelized and media-oriented applications demanded on mobile devices, and a flexible security framework based on proof-carrying authorization (PCA) that provides "plug-in" interoperability with existing secure naming and authentication systems. Bryan Ford is a faculty candidate
03 March 2008, 4:00 PM
Matthew Might
Georgia Institute of Technology
Saarbrücken, Building MPI-SWS, Room 019
Title: "Static analysis of higher-order programs"
Abstract:
The expressive power of functional and object-oriented languages derives in part from their higher-orderness: through closures and objects, code becomes data. This talk focuses on meeting the challenges that such power poses for static analysis and its clients. (To make the talk more accessible, a brief history of the higher-order analysis is included.) Since its discovery in the 1980s, higher-order control-flow analysis (CFA) has enabled many critical program optimizations, such as flow-directed inlining and static virtual-method resolution. Over the past two decades, much research in higher-order analysis focused on improving the speed and precision of CFA. Despite frequent encounters with the limits of CFAs, little progress had been made in moving beyond them, as measured by the kinds of optimizations made possible and the kinds of questions made answerable. The key limitation of CFAs is the inherently coarse approximation that they inflict upon environment structure. This talk centers on my development of environment analysis---techniques which break through these limitations of twenty years standing. Of particular note is that these techniques evade the cost/precision tradeoff usually found in program analyses: compared to previous techniques, they provide improvements in both power and precision, yet also reduce the cost of the compile-time analysis in practice. Using environment analysis as a foundation, my recent work on logic-flow analysis has continued to expand the reach of higher-order analysis beyond optimization and into realms such as security and verification. Matthew Might is a faculty candidate
29 February 2008, 11:00 AM
Petr Kuznetsov
Max Planck Institut for Software Systems
Saarbrücken, Building MPI-SWS, Room 019
Title: "Failure Detectors and Topology of Distributed Computing"
Abstract:
Making the right model assumptions is crucial in developing robust and efficient computing systems. The ability of a model to solve distributed computing problems is primarily defined by the /synchrony assumptions/ the model makes. Given that many problems in distributed computing are impossible to solve in the asynchronous way, it is very important to determine the minimal synchrony assumptions that are sufficient to solve a given problem. These assumptions can be conveniently encapsulated in the /weakest failure detector/ abstraction. In this talk, I will focus on defining the "weakest failure detector ever": the failure detector that is strong enough to circumvent /some/ asynchronous impossibility and, at the same time, necessary to circumvent /any/ asynchronous impossibility. In this context, I will consider the /geometrical/ approach, based on modeling a system state of as a high-dimensional geometrical object, and a distributed computation as an evolution of this object in space. This approach has been shown instrumental in characterizing the class of tasks solvable in /asynchronous/ systems. I will argue that applying these ideas to /partially synchronous/ systems may lead to automatic derivations of the weakest failure detectors for various distributed computing problems, and, eventually, to establishing a theory of distributed computational complexity.
20 December 2007, 2:00 PM
Juan Navarro Perez
University of Manchester
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: "Encodings of Bounded LTL Model Checking in EffectivelyPropositional Logic"
Abstract:
We present an encoding that is able to specify LTL bounded model checking problems within the Bernays-Schönfinkel fragment of first-order logic. This fragment, which also corresponds to the category of effectively propositional problems (EPR) of the CASC system competitions, allows a natural and succinct representation of both a software/hardware system and the property that one wants to verify. This is part of the research I did during my PhD studies at the University of Manchester, which deals with finding problems suitable for encoding within the effectively propositional class of formulas, and aims to encourage the interest on theorem proving in this restricted fragment of first order logic.
13 December 2007, 9:00 AM
Meeyoung Cha
KAIST
Saarbrücken, Building MPI-SWS, Room 019
Title: "Trace-driven analysis of streaming services: A deep look into YouTube and a nationwide IPTV"
Abstract:
Multimedia streaming is becoming an integral part of people's life. In this talk, I will present data analysis on user's viewing behaviors based on two streaming services: YouTube and IPTV. YouTube is the largest VoD service for user generated contents (UGC). Nowadays, UGC sites are creating new viewing patterns and social interactions, empowering users to be more creative, and developing new business opportunities. In this talk, I will present the intrinsic statistical properties of video popularity based on real traces from YouTube. Understanding the popularity characteristics is important because it can bring forward the latent demand created by bottlenecks in the system (e.g. poor search and recommendation engines, lack of metadata, etc). Another popular form of streaming is IPTV. After many years of academic and industry work, we are finally witnessing a thriving of IP multicast in large scale deployment of IPTV services. In the second part of this talk, I will present for the first time previously hidden TV viewing habits based on real traces. I will also discuss the feasibility of using peer-to-peer distribution for scalable IPTV system and supporting advanced viewing controls such as DVD-like functionalities, content recommendations, and target advertisements.
30 November 2007, 11:00 PM
Ramki Gummadi
MIT
Saarbrücken, Building MPI-SWS, Room 024
Title: Reliable and efficient programming abstractions for sensor networks
Abstract:
It is currently difficult to build practical and reliable programming systems out of distributed and resource-constrained sensor devices. The state of the art in today's sensornet programming is centered around nesC. nesC is a nodelevel language---a program is written for an individual node in the network---and nesC programs use the services of the TinyOS operating system. In this talk, I will describe an alternate approach to programming sensor networks that significantly raises the level of abstraction over today's practice. The critical change is one of perspective: rather than writing programs from the point of view of an individual node, programmers implement a central program that conceptually has access to the entire network. This approach pushes to the compiler the task of producing node-level programs that implement the desired behavior. I will present the Pleiades programming language, its compiler, and its runtime. The Pleiades language extends the C language with constructs that allow programmers to name and access node-local state within the network and to specify simple forms of concurrent execution. The compiler and runtime system cooperate to implement Pleiades programs efficiently and reliably. First, the compiler employs a novel program analysis to translate Pleiades programs into message-efficient units of work implemented in nesC. The Pleiades runtime system orchestrates execution of these units, using TinyOS services, across a network of sensor nodes. Second, the compiler and runtime system employ novel locking, deadlock detection, and deadlock recovery algorithms that guarantee serializability in the face of concurrent execution. We illustrate the readability, reliability and efficiency benefits of the Pleiades language through detailed experiments, and demonstrate that the Pleiades implementation of a realistic application performs similar to a hand-coded nesC version that contains more than ten times as much code.
19 November 2007, 2:00 PM
Ales Smrcka
Brno University of Technology
Saarbrücken, Building MPI-SWS, Room Rotunda 6th floor
Title: Transforming RTL Design to Counter Automaton
Abstract:
Abstract: The languages for the description of a hardware design in RTL level (e.g., VHDL or Verilog) allow to specify a generic description. Such a description contains one or more parameters which make the generic nature of a design (e.g, the number of items in a buffer or the width of inputs and output of arithmetic operation). A new approach to formal verification of generic hardware designs will be presented. The proposed approach is based on a translation of such designs to counter automata. These main topics of modelling and the verification will be discussed in more details: the translation of VHDL constructs to counter automata, specification of an environment of modelled hardware component, specification of safety properties over a design, and some experimental results with ARMC and Blast.
24 October 2007, 10:30 AM
Boris Köpf
ETH Zuerich
Saarbrücken, Building MPI-SWS, Room 023
Title: Formal Models for Side-Channel Attacks
Abstract:
Side-channel attacks have become so effective that they pose a real threat to the security of cryptographic algorithms. This threat is not covered by traditional notions of cryptographic security and models for proving resistance against it are only now emerging. In this talk, I will present work on such a model. It is based on concrete and realistic assumptions about the attacker and it is tailored to synchronous hardware, where faithful system models are available. The model leads to meaningful metrics for assessing the resistance of a system to side-channel attacks. I will show how these metrics can be computed and be used for analyzing nontrivial hardware implementations for their vulnerability to timing attacks. I will conclude with a number of directions for further research.
27 September 2007, 3:00 PM
Domagoj Babic, UBC.
U of British Columbia
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: Structural Abstraction of Software Verification Conditions--
Abstract:
Precise software analysis and verification require tracking the exact path along which a statement is executed (path-sensitivity), the different contexts from which a function is called (context-sensitivity), and the bit-accurate operations performed. Previously, verification with such precision has been considered too inefficient to scale to large software. In this talk, Domagoj presents a novel approach to solving such verification conditions, based on an automatic abstraction-checking-refinement framework that exploits natural abstraction boundaries present in software. Experimental results show that our approach scales to over 200,000 lines of real C code.
12 September 2007, 11:00 AM
Katerina Argyraki
EPFL, Switzerland
Saarbrücken, Building MPI-SWS, Room rotunda 6th floor
Title: Loss and Delay Accountability for the Internet
Abstract:
The Internet provides no information on the fate of transmitted packets, and end systems cannot determine who is responsible for dropping or delaying their traffic. As a result, they cannot verify that their ISPs are honoring their service level agreements, nor can they react to adverse network conditions appropriately. While current probing tools provide some assistance in this regard, they only give feedback on probes, not actual traffic. Moreover, service providers could, at any time, render their network opaque to such tools. I will present AudIt, an explicit "accountability interface" for the Internet, through which ISPs can pro-actively supply feedback to traffic sources on loss and delay, at administrative-domain granularity. AudIt benefits not only end systems, but also ISPs, because---in contrast to probing tools---it allows them to control the amount and quality of information revealed about their internal structure and policy. I will show that AudIt is resistant to ISP lies in a business-sensible threat model and can be implemented with a modest NetFlow modification. Finally, I will discuss a Click-based prototype, which introduced less than 2% bandwidth overhead on real traces from a Tier-1 ISP.
25 May 2007, 2:00 PM
Prof.Siva Ram Murthy
IIT Madras
Saarbrücken, Building E1 4 - MPI-INF, Room 021
Title: Lifetime Driven MAC Protocols for Ad Hoc Networking
Abstract:
In the last few years, there has been a big interest in Ad Hoc Wireless Networks as they have tremendous military and commercial potential. An Ad Hoc Wireless Network is a wireless network, comprising of mobile nodes (which can also serve as routers) that use wireless transmission, having no infrastructure (central administration such as a Base Station in a Cellular Wireless Network or an Access Point in a Wireless LAN). Ad Hoc Wireless Networks can be set up anywhere and anytime as they eliminate the complexities of infrastructure setup. Ad Hoc wireless Networks find applications in several areas. Some of these include: military applications (establishing communication among a group of soldiers for tactical operations as setting up of a fixed infrastructure in enemy territories or in inhospitable terrains may not be possible), collaborative and distributed computing, emergency operations, wireless mesh networks, wireless sensor networks, and hybrid (integrated Cellular and Ad hoc) wireless networks. In this talk, I first present a brief overview of the major issues that influence the design and performance of Ad Hoc Wireless Networks. As the performance of any wireless network hinges on the Medium Access Control (MAC) protocol, more so for Ad Hoc Wireless Networks, I present, in detail, novel distributed homogeneous and heterogeneous battery aware MAC protocols, which take benefit of the chemical properties of the batteries and their characteristics, to provide fair node scheduling and increased network and node lifetime through uniform discharge of batteries.
26 April 2007, 3:00 PM
Andrey Rybalchenko
Ecole Polytechnique Fédérale de Lausanne
and Max Planck Institute for Computer Science
Saarbrücken, Building E1 4 - MPI-INF, Room 019
Title: Abstraction for Liveness and Safety
Abstract:
We present new approaches to verification of liveness and safety properties of software. Proving liveness properties of programs is central to the process of ensuring that software systems can always react. Verification of liveness properties had been an open problem since 1970s, due to the lack of modular termination arguments and adequate abstraction techniques. We highlight our experience in developing the theoretical foundations for the first software verification tool for termination that provides capacity for large program fragments (of more than 20,000 lines of code) together with support for programming language features such as arbitrarily nested loops, pointers, function-pointers, side-effects, etc. We also describe our experience in applying the tool on device driver dispatch routines from the Windows operating system. In the second part of the talk, we will focus on abstraction techniques that are at heart of state-of-the-art verification tools for safety. We address their limitations, which severely restrict the practical applicability. We propose a new approach for finding abstraction of a program that overcomes the inherent limitations of current abstraction refinement schemes.
24 April 2007, 4:00 PM
Michael D. Ernst
MIT
Saarbrücken, Building E1 3 - Hörsaal Gebäude, Room HS 003
Title: Feedback-directed random test generation
Abstract:
We present a technique that improves random test generation by incorporating feedback obtained from executing test inputs as they are created. Our technique builds inputs incrementally by randomly selecting a method call to apply and finding arguments from among previously-constructed inputs. As soon as an input is built, it is executed and checked against a set of contracts and filters. The result of the execution determines whether the input is redundant, illegal, contract-violating, or useful for generating more inputs. The technique outputs a test suite consisting of unit tests for the classes under test. Passing tests can be used to ensure that code contracts are preserved across program changes; failing tests (that violate one or more contract) point to potential errors that should be corrected. Our experimental results indicate that feedback-directed random test generation can outperform systematic and undirected random test generation, in terms of coverage and error detection. On four small but nontrivial data structures (used previously in the literature), our technique achieves higher or equal block and predicate coverage than model checking (with and without abstraction) and undirected random generation. On 14 large, widely-used libraries (comprising 780KLOC), feedback-directed random test generation finds many previously-unknown errors, not found by either model checking or undirected random generation.
19 April 2007, 3:00 PM
Derek Dreyer
Toyota Technological Institute at Chicago
Saarbrücken, Building E1 4 - MPI-INF, Room 019
Title: Expanding and Exploiting the Expressive Power of Modules
Abstract:
Modularity is widely viewed as a central concept in the design of robust software. Programming languages vary widely, however, in the kinds of modularity mechanisms they support, leading to the mistaken impression that there are fundamental tradeoffs between different paradigms of modular programming. The high-level goal of my research is to design languages that overcome these tradeoffs and combine the benefits of existing mechanisms. In this talk, I will describe my work on using the ML module system as a basis for developing next-generation module languages. ML provides an excellent starting point because of its powerful support for both data abstraction (implementor-side modularity) and generic programming (client-side modularity). Nevertheless, there are ways in which ML's module language is unnecessarily inflexible and in which the expressive power of ML modules has not been exploited to its full potential. In the first part of the talk, I will compare the support for generic programming offered by ML modules with that offered by Haskell's "type classes". Modules emphasize explicit program configuration and namespace control, whereas type classes emphasize implicit program configuration and overloading. In fact, I show that it is possible to support both styles of programming within one language, by exploiting the expressive power of ML modules and encoding type classes directly in terms of existing ML module mechanisms. In the second part of the talk, I will discuss the problem of extending ML with one of the most frequently requested features---recursive modules. The lack of support for this feature is a key stumbling block in incorporating ML-style modules into object-oriented languages, in which recursive components are commonplace. The primary difficulty with recursive modules is something called the "double vision" problem, which concerns the interaction of recursion and data abstraction. I trace the problem back to a deficiency in the classical type-theoretic account of data abstraction (namely, existential types), and I show how a novel interpretation of data abstraction as a computational effect leads to an elegant solution.
16 April 2007, 3:00 PM
Eno Thereska
Carnegie Mellon University
Saarbrücken, Building E1 4 - MPI-INF, Room 019
Title: Enabling what-if explorations in distributed systems
Abstract:
With a large percentage of total system cost going to system administration tasks, self-management remains a difficult and important goal in systems. As a step towards the self-management vision, I will present a framework we have developed that enables systems to be self-predicting and answer ``what-if'' questions about their behavior with little or no administrator involvement. We have built a Resource Advisor inside two real systems: Microsoft's SQL Server database and the Ursa Minor storage system at Carnegie Mellon University. The Resource Advisor helps with upgrade and data placement decisions and provides what-if interfaces to external administrators (and internal tuning modules). The Resource Advisor is based on efficient system behavioral models that enable robust predictions in multi-tier systems. Bio: Eno Thereska is a PhD student at Carnegie Mellon University working with Prof. Greg Ganger. Eno has broad research interests in computer systems. Currently he is investigating ways to make the management of distributed systems easier. An approach he is currently pursuing puts sufficient instrumentation and modeling within the system, enabling it to answer several important what-if questions without outside intervention. He is interested in applying methods from queuing analysis (for components build from scratch) and machine learning (for legacy components) to this problem. As a testbed he is using Ursa Minor, a cluster-based storage system being deployed at Carnegie Mellon for researching system management issues. Concrete what-if questions in this system are about the effect of resource upgrades, service migration and data distribution. Eno received the Masters of Science (MS) degree in Electrical and Computer Engineering in 2003 at Carnegie Mellon University and the Bachelor of Science (BS) degree in Electrical and Computer Engineering and Computer Science in 2002 also at CMU. ------------------------------
04 April 2007, 3:00 PM
Rodrigo Rodrigues
INESC-ID, Lisbon
Saarbrücken, Building MPI-SWS, Room 019
Title: Scalable Byzantine Fault Tolerance
Abstract:
The research presented in this talk attempts to extend Byzantine fault tolerance protocols to provide better scalability. I will cover two axes of scalability in such systems. First, I will focus on systems with a large number of nodes, where existing solutions are not well-suited, since they assume a static set of replicas, or provide limited forms of reconfiguration. In the context of a storage system we implemented, I will present a membership service that is part of the overall design, but can be reused by any large-scale Byzantine-fault-tolerant system. The membership service provides applications with a globally consistent view of the set of currently available servers. Its operation is mostly automatic, to avoid human configuration errors; it can be implemented by a subset of the storage servers; it tolerates arbitrary failure of the servers that implement it; and it can itself be reconfigured. The second aspect of scalability of Byzantine-fault-tolerant systems that this talk discusses is scalability with the size of the replica group (and, consequently, the number of faults that the system tolerates). I show a new replication protocol called HQ, that combines quorum-based techniques that are more scalable when there is no contention with more traditional state-machine replication protocols with quadratic inter-replica communication like Castro-Liskov's BFT that are useful for resolving concurrency issues.
02 November 2006, 4:00 PM
Ken Calvert
Laboratory for Advanced Networking, University of Kentucky
Saarbrücken, Building E1 4 - MPI-INF, Room Rotunda 6th floor
Title: Scalable Network Management Using Ephemeral State
Abstract:
It is widely acknowledged that today's network management tools are inadequate. Although the existing managment protocol (SNMP) has been and remains indispensible, it offers neither the scalability nor the functionality needed to manage large systems. Active/programmable networks and mobile agent systems have been proposed as alternative network management solutions that offer more functionality and potentially better scalability. Unfortunately, the flexibility of these (heavyweight) approaches comes with its own set of problems which prevent them from being widely adopted. This talk will describe the use of ephemeral state processing (ESP) to efficiently monitor and collect information from large networks. ESP is a lightweight router-based programmable building block that can solve a range of network management problems while avoiding the problems that plague more complex approaches. Moreover, the simplicity of ESP allows it to be made available as a general-purpose service for all packets in the network. We demonstrate the utility of the service by showing how it can be used to solve some common network management problems. (Joint work with J. Griffioen)
13 October 2006, 2:00 PM
Dan Wallach
Department of Computer Science,
Rice University, Houston, Texas
Saarbrücken, Building E1 4 - MPI-INF, Room 019
Title: Electronic Voting: Risks and Research
Abstract:
Hanging chads, among other issues with traditional voting systems, have sparked great interest in managing the election process through the use of newer electronic voting systems. While computer scientists, for the most part, have been warning of the perils of such action, vendors have forged ahead with their products, claiming increased security, reliability, and accuracy. Many municipalities have adopted electronic systems and the number of deployed systems is rising. To the limited extent that independent security analyses have been published, the results have raised serious reservations about the quality of these systems to resist attacks. This talk will describe problems we and other researchers have discovered and will consider the limitations of the certification processes that should have guaranteed some quality control. These issues, in turn, give rise to a variety of interesting research problems that span computer science, human factors, and public policy. In this talk, we will consider how both established and open research in software engineering, distributed systems, and cryptography can and should impact the next generation of voting systems.
03 July 2006, 2:00 PM
Devika Subramanian
Rice University
Saarbrücken, Building MPI-SWS Saarbruecken, Room 024
Title: Adaptive Embedded Systems
Abstract:
Adaptive Embedded Systems While embedded systems are ubiquitous, adaptive ones are not. My research goal is to push the science and engineering of adaptive embedded systems by exploring the addition of adaptivity to a diverse variety of complex systems. I will present my work on four current projects (1) tracking human learning on a complex visual-motor task (2) predicting conflict from events data extracted from wire stories (3) customizing application-specific compiler optimization sequences, and (4) learning regulatory networks in normal and cancer cells.
24 April 2006, 3:00 PM
Jean-Philippe Martin
University of Texas at Austin
Saarbrücken, Building E1.4, Room 024
Title: Byzantine Fault-Tolerance and Beyond
Abstract:
Computer systems should be trustworthy in the sense that they should reliably answer requests from legitimate users and protect confidential information from unauthorized users. Building this kind of systems is challenging, even more so in the increasingly common case where control is split between multiple administrative domains. Byzantine fault tolerance techniques can elegantly provide reliability without overly increasing the complexity of the system and have recently earned the attention of the system community. In the first part this talk I discuss some of the contributions I have made toward practical Byzantine fault tolerance---in particular, how to reduce the cost of replication and how to reconcile replication with confidentiality. In the second part of the talk I argue that Byzantine fault-tolerance alone is not sufficient to deal with cooperative services under multiple administrative domain, where nodes may deviate from their specification not just because they are broken or compromised, but also because they are selfish. To address this challenge, I propose BAR, a new failure model that combines concepts from Byzantine fault-tolerance and Game Theory. I will describe BAR, present an architecture for building BAR services, and briefly discuss BAR-B, a BAR-tolerant cooperative backup system.
06 April 2006, 3:00 PM
Viktor Kuncak
MIT CSAIL
Saarbrücken, Building E1 4 - MPI-INF, Room 022
Title: Modular Static Analysis with Sets and Relations
Abstract:
We present a new approach for statically analyzing data structure consistency properties. Our approach is based on specifying interfaces of data structures using abstract sets and relations.This enables our system to independently verify that 1) each data structure satisfies internal consistency properties and each data structure operation conforms to its interface; 2) the application uses each data structure interface correctly, and maintains the desired global consistency properties that cut across multiple data structures. Our system verifies these properties by combining static analyses, constraint solving algorithms, and theorem provers, promising an unprecedented combination of precision and scalability. The combination of different techniques is possible because all system components use a common specification language based on sets and relations. In the context of our system, we developed new algorithms for computing loop invariants, new techniques for reasoning about sets and their sizes, and new approaches for extending the applicability of existing reasoning techniques. We successfully used our system to verify data structure consistency properties of examples based on computer games, web servers, and numerical simulations. We have verified implementations and uses of data structures such as linked lists with back pointers and iterators, trees with parent pointers, two-level skip lists, array-based data structures, as well as combinations of these data structures. This talk presents our experience in developing the system and using the system to build verified software.
23 February 2006, 4:00 PM
Cormac Flanagan
University of California, Santa Cruz
Saarbrücken, Building 46.1 - MPII, Room 024
Title: Type Systems for Multithreaded Software
Abstract:
Developing correct multithreaded software is very challenging, due to the potential for unintended interference between threads. We present type systems for verifying two key non-interference properties in multithreaded software: race-freedom and atomicity. Verifying atomicity is particularly valuable since atomic procedures can be understood according to their sequential semantics, which significantly simplifies subsequent (formal and informal) correctness arguments. We will describe our experience applying these type systems and corresponding type inference algorithms to standard multithreaded benchmarks and other applications, and illustrate some defects revealed by this approach.
14 February 2006, 4:00 PM
Albrecht Schmidt
LMU Muenchen
Saarbrücken, Building MPI-SWS, Room 024 - Harald Ganzinger Hoersaal
Title: Interacting with Ubiquitous Computing Systems
Abstract:
Computing and communication devices are pervasively embedded into our everyday environments. Interaction in the context of the real world includes more and more interacting with complex mobile and embedded information systems. In many cases such interaction is multimodal and distributed between public and personal mobile devices. Advances in underlying network, processing, perception, and actuation technologies as well as new production techniques, such as 3D-printing, allow unprecedented options for creating novel user interfaces. However, as constraints that applied to the domain of mechanical and electrical user interfaces are not given anymore, there is a great risk of creating user interfaces where the conceptual model is not understandable anymore. To make pervasive computing usable, establishing appropriate interaction paradigms and metaphors is the great challenge. Context-Aware Interaction, Implicit Interaction and Tangible User Interfaces are novel approaches which take into account that the interaction with information happens in the real world and is conceptually embedded into foreground tasks carried out by the user. To explore opportunities and challenges several prototypical systems were designed, implemented, and evaluated. Using case studies the talk presents innovative mobile phone applications that make use of contextual information, novel interactive devices, and conventional objects and computers that are enriched by pervasive technologies. This will outline the interplay between pervasive technologies, mobile systems and user experience. Concentrating on what information is created and what information is consumed by the user while performing a task in the real world is the basic idea of Embedded Interaction. The focus is not on a single technology or a specific device. The aim is to seek optimal support for a task considering all technologies available in a certain context. This requires an understanding of different parameters of novel input and output technologies. The talk concludes with an outlook on research challenges that arise from the concept of Embedded Interaction related to current developments in the field of pervasive computing.
14 November 2005, 11:00 AM
Ulrich Kremer
Rutgers University
Saarbrücken, Building MPI-SWS, Room 024
Title: Programming Ad-hoc Networks of Mobile Devices
Abstract:
Ad-hoc networks of mobile devices such as smart phones and PDAs represent a new and exciting distributed system architecture. Building distributed applications on such an architecture poses new design challenges in programming models, languages, compilers, and runtime systems. This talk will introduce SpatialViews, a high-level language designed for programming mobile devices connected through a wireless ad-hoc network. SpatialViews allows specification of virtual networks with nodes providing desired services and residing in interesting spaces. These nodes are discovered dynamically with user-specified time constraints and quality of result (QoR). The programming model supports ``best-effort'' semantics, i.e., different executions of the same program may result in ``correct'' answers of different quality. It is the responsibility of the compiler and runtime system to produce a high-quality answer for the particular network and resource conditions encountered during program execution. Example applications will be used to illustrate the different features of the SpatialViews language, and to demonstrate the expressiveness of the language and the efficiency of the compiler generated code. Sample applications include sensor network applications that collect and aggregate sensor data within the network, applications that use dynamic service installation and computation offloading, and augmented-reality gaming. The efficiency of the compiler generated code is verified through simulation and physical measurements. The reported results show that SpatialViews is an expressive and effective language for ad-hoc networks. In addition, compiler optimizations can significantly improve response times and energy consumption. More information about the language, compiler and runtime system, including a distribution of our prototype system, can be found at http://www.cs.rutgers.edu/spatialviews .
14 September 2005, 2:30 PM
Gilles Muller
Ecole des Mines de Nantes
Saarbrücken, Building MPI-SWS, Room 24
Title: Coccinelle: A Language-Based Approach to Managing the Collateral Evolution of Linux Device Drivers
Abstract:
The Linux operating system is undergoing continual evolution. Evolution in the kernel and generic driver modules often triggers the need for corresponding evolutions in specific device drivers. Such collateral evolutions are tedious, because of the large number of device drivers, and error-prone, because of the complexity of the code modifications involved. We propose an automatic tool, Coccinelle, to aid in the driver evolution process. In this talk, we examine some recent evolutions in Linux and the collateral evolutions they trigger, and assess the corresponding requirements on Coccinelle.
08 September 2005, 11:00 AM
Vivien Quema
Institut National Polytechnique de Grenoble, INRIA Rhône-Alpes, France
Saarbrücken, Building 46.1 - MPII, Room 024
Title: DREAM: a Component Framework for the Construction of Resource-Aware, Dynamically Configurable Communication Middleware
Abstract:
In this talk, we present the work we are conducting at INRIA Rhône-Alpes on the design of component-based framework for the construction of autonomous systems. Modern distributed computing systems are becoming increasingly complex. A major trend currently is to build autonomous systems, i.e. systems that reconfigure themselves upon occurrence of events such as software and hardware faults, performance degradation, etc. Building autonomous systems requires both a software technology allowing the development of administrable systems and the ability to build control loops in charge of regulating and optimizing the behavior of the managed system. In this talk, we will mainly focus on the first requirement, i.e. providing a software technology for the development of administrable systems. We argue that better configurability can be reached through the use of component-based software frameworks. In particular, we present DREAM, a software framework for the construction of message-oriented middleware (MOMs). Several MOMs have been developed in the past ten years. The research work has primarily focused on the support of various non functional properties like message ordering,reliability, security, scalability, etc. Less emphasis has been placed on MOM configurability. From the functional point of view, existing MOMs implement a fixed programming interface (API) that provides a fixed subset of asynchronous communication models (publish/subscribe, event/reaction, message queues, etc.). From the non-functional point of view, existing MOMs often provide the same non-functional properties for all message exchanges, which reduces their performance. To overcome these limitations, we have developed DREAM (Dynamic REflective Asynchronous Middleware), a component framework for the construction of dynamically reconfigurable communication systems. The idea is to build a middleware as an assembly of interacting components, which can be statically or dynamically configured to meet different design requirements or environment constraints. DREAM provides a component library and a set of tools to build, configure and deploy middleware implementing various communication paradigms. DREAM defines abstractions and provides tools for controlling the use of resources (i.e. messages and activities) within the middleware. Moreover, it builds upon the Fractal component model, which provides support for hierarchical and dynamic composition. DREAM has been successfully used for building various forms of communication middleware: publish-subscribe (JMS), total order group communication protocols, probabilistic broadcast,asynchronous RPC, etc.
24 August 2005, 3:00 PM
Timothy Roscoe
Intel Research Berkeley
Saarbrücken, Building E1 4 - MPI-INF, Room 24
Title: Implementing Declarative Overlays
Abstract:
Overlay networks are used today in a variety of distributed systems ranging from file-sharing and storage systems to communication infrastructures. Overlays of various kinds have recently received considerable attention in the networked systems research community, partly due to the availability of the PlanetLab planetary-scale application platform. However, a broader historical perspective is that overlay functionality has implicitly long been a significant component of wide-area distributed systems. Despite this, designing, building and adapting these overlays to an intended application and the target environment is a difficult and time consuming process. To ease the development and the deployment of such overlay networks, my research group at Intel Berkeley in conjunction with the University of California at Berkeley is building P2, a system which uses a declarative logic language to express the overlay networks in a highly compact and reusable form. P2 can express a Narada-style mesh network in 13 rules, and the Chord structured overlay in only 35 rules. P2 directly parses and executes such specifications using a dataflow architecture to construct and maintain the overlay networks. I'll describe the P2 approach, how our implementation works, and give some experimental results showing that the performance and robustness of P2 overlays is acceptable.
08 July 2005, 10:00 AM
Petr Kouznetsov
EPFL
Saarbrücken, Building 46.1 - MPII, Room 024
Title: Latest news about lock-free object implementations
Abstract:
Lock-free implementations of shared data objects do not rely on any form of mutual exclusion, and thereby allow processes to overcome adverse operating system affects. Wait-free implementations provide the strongest form of lock-freedom and guarantee that every process can complete its operation, regardless of the execution speeds of other processes. They are in this sense very appealing, but turn out to be impossible or very expensive to achieve in many practical settings. Recently, researchers suggested a weaker liveness property, called obstruction-freedom, that guarantees progress only when there is no contention, which is argued to be the most common case in practice. However, the notion of contention was very widely interpreted, and, as a result, the limitations of implementations ensuring only these weaker properties remained unclear. We formally define an adequate measure of contention, which we call step contention, and present a generic obstruction-free implementation that ensures progress for step contention-free operations. Our implementation is linear in time and space with respect to the number of concurrent processes. We show that these complexities are asymptotically optimal, and hence generic obstruction-free implementations are inherently expensive.
30 May 2005, 5:00 PM
Krishna Gummadi
University of Washington
Saarbrücken, Building 46.1 - MPII, Room 024
Title: Measurement-driven Modeling and Design of Internet-scale Systems
Abstract:
The Internet is huge, complex, and rapidly evolving. Understanding how today's Internet-scale systems work is challenging, but crucial when designing the networks and applications of tomorrow. In this talk, I will describe how I have used a combination of measurement, modeling, and analysis to understand two Internet-scale systems: (1) peer-to-peer (P2P) file-sharing systems and their workloads, and (2) indirection routing systems that recover from Internet path failures. In part because of the rise in popularity of P2P systems, multimedia workloads have become the dominant source of Internet traffic. Our measurements show that multimedia workloads are substantially different from traditional Web workloads. Based on an analysis of a 6-month long trace of the Kazaa P2P system, I will propose a new model for multimedia workloads and will use it to explain how a few, simple, fundamental factors drive them. In the second part of my talk, I will focus on understanding Internet path failures and indirection-based recovery schemes. I will first characterize the frequency and location of Internet path failures that occur in practice. Using insights drawn from our measurements, I will show how a simple, stateless, and scalable scheme called "one-hop source routing" achieves close to the maximum possible recovery attainable by any indirection routing scheme. I will also relate experiences we gained from implementing and deploying one-hop source routing on PlanetLab.
11 April 2005, 4:00 PM
Sean Rhea
UC Berkley
Saarbrücken, Building 46.1 - MPII, Room 024
Title: OpenDHT: A Public DHT Service
Abstract:
Large-scale distributed systems are hard to deploy, and distributed hash tables (DHTs) are no exception. To lower the barriers facing DHT-based applications, we have created a public DHT service called OpenDHT. Designing a DHT that can be widely shared, both among mutually-untrusting clients and among a variety of applications, poses two distinct challenges. First, there must be adequate control over storage allocation so that greedy or malicious clients do not use more than their fair share. Second, the interface to the DHT should make it easy to write simple clients, yet be sufficiently general to meet a broad spectrum of application requirements. In this talk I will describe our solutions to these design challenges. I'll also report on our early deployment experiences with OpenDHT and describe the variety of applications already using the system.
07 April 2005, 5:00 PM
George Candea
Stanford University
Saarbrücken, Building 46.1 - MPII, Room 024
Title: A Reboot-based Approach to High Availability
Abstract:
Application-level software failures are a dominant cause of outages in large-scale software systems, such as e-commerce, banking, or Internet services. The exact root cause of these failures is often unknown and the only cure is to reboot. Unfortunately, rebooting can be expensive, leading to nontrivial service disruption or downtime even when clusters and failover are employed. In this talk I will describe the "crash-only design," a way to build reboot-friendly systems. I will also present the "microreboot," a technique for surgically recovering faulty application components without disturbing the rest. I will argue quantitatively that recovery-oriented techniques complement bug-reduction efforts and provide significant improvements in software dependability. We applied the crash-only design and microreboot technique to a satellite ground station and an Internet auction system. Without fixing any bugs, microrebooting recovered most of the same failures as process restarts, but did so more than an order of magnitude faster and with an order of magnitude savings in lost work. Simple, cheap recovery engenders a new way of thinking about failure management. First, we can prophylactically microreboot to rejuvenate a software system by parts; this averts failures induced by software aging, without ever having to bring the system down. Second, we can mask failure and recovery from end users through transparent call-level retries, turning failures into human-tolerable sub-second latency blips. Finally, having made recovery very cheap, it makes sense to microreboot at the slightest hint of failure -- if the microreboot is indeed necessary, we speed up recovery; if not, the impact is negligible. As a result, we productively employed failure detection based on statistical learning, which reduces false negatives at the cost of more frequent false positives. We also closed the monitor-diagnose-recover loop and built an autonomously recovering Internet service, exhibiting orders of magnitude higher availability than previously possible.
Career opportunities:
New buildings:
Lectures:
Computing research organizations in the surrounding area:
