Events 2017

Your Photos Expose Your Social Circles - Social Relation Recognition from 5 Social Domains

Qianru Sun
MPI-INF - D4
Joint Lecture Series
05 Jul 2017, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Social relations are the foundation of human daily life. Developing techniques to analyze such relations in visual data such as photos bears great potential to build machines that better understand people at a social level. Additionally through better understanding about such hidden information in exposed photos we would like to inform people about potential privacy risks. Social domain-based theory from social psychology is a great starting point to systematically approach social relation recognition. The theory provides a coverage of all aspects of social relations and equally is concrete and predictive about the visual attributes and behaviors defining the relations in each domain. Our work provides the first photo dataset built on this holistic conceptualization of social life that is composed of a hierarchical label space of social domains and social relations and contributes the first models to recognize such domains and relations and find superior performance for attribute based features. Beyond the encouraging performances we have some findings of interpretable features that are in accordance with the predictions from social psychology literature. Our work mainly contributes to interleave visual recognition and social psychology theory that has the potential to complement the theoretical work in the area with empirical and data-driven models of social life.

Towards an Approximating Compiler for Numerical Computations

Eva Darulova
Max Planck Institute for Software Systems
Joint Lecture Series
07 Jun 2017, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Computing resources are fundamentally limited and sometimes an exact solution may not even exist. Thus when implementing real-world systems approximations are inevitable as are the errors introduced by them. The magnitude of errors is problem-dependent but higher accuracy generally comes at a cost in terms of memory energy or runtime effectively creating an accuracy-efficiency tradeoff. To take advantage of this tradeoff we need to ensure that the computed results are sufficiently accurate otherwise we risk disastrously incorrect results or system failures. Unfortunately the current way of programming with approximations is mostly manual and consequently costly error prone and often produces suboptimal results.

In this talk I will present our vision and efforts so far towards an approximating compiler for numerical computations. Such a compiler would take as input exact high-level code with an accuracy specification and automatically synthesize an approximated implementation which is as efficient as possible but verifiably computes accurate enough results.

Digital Knowledge: From Facts to Rules and Back

Daria Stepanova
MPI-INF - D5
Joint Lecture Series
03 May 2017, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Knowledge Graphs (KGs) are huge collections of primarily encyclopedic facts which are automatically extracted from the Web. Prominent examples of KGs include Yago DBPedia Google Knowledge Graph. We all use KGs when posing simple queries like "capital of Saarland" to Google. Internally such queries are translated into machine readable representations which are then issued against the KG stored at the backend of the search engine. Instead of syntactically relevant Web pages the actual answer to the above query "Saarbrücken" is then output to the user as a result.

However since KGs are automatically constructed they are often inaccurate and incomplete. In this talk I will investigate how deductive and inductive reasoning services could be used to address these crucially important issues. More specifically first I will present an approach for repairing inconsistencies in hybrid logical systems that can be built on top of KGs. Second I will describe a method for inductive learning of rules with exceptions from KGs and show how these are applied for deriving missing facts.

Digital Knowledge: From Facts to Rules and Back

Daria Stepanova
MPI-INF - D5
Joint Lecture Series
03 May 2017, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
Knowledge Graphs (KGs) are huge collections of primarily encyclopedic facts which are automatically extracted from the Web. Prominent examples of KGs include Yago DBPedia Google Knowledge Graph. We all use KGs when posing simple queries like "capital of Saarland" to Google. Internally such queries are translated into machine readable representations which are then issued against the KG stored at the backend of the search engine. Instead of syntactically relevant Web pages the actual answer to the above query "Saarbrücken" is then output to the user as a result.

However since KGs are automatically constructed they are often inaccurate and incomplete. In this talk I will investigate how deductive and inductive reasoning services could be used to address these crucially important issues. More specifically first I will present an approach for repairing inconsistencies in hybrid logical systems that can be built on top of KGs. Second I will describe a method for inductive learning of rules with exceptions from KGs and show how these are applied for deriving missing facts.

On Rationality of Nonnegative Matrix Factorization

James Worrell
University of Oxford
SWS Distinguished Lecture Series
02 May 2017, 10:30 am - 1:30 pm
Saarbrücken building E1 5, room 002
simultaneous videocast to Kaiserslautern building G26, room 112
The nonnegative rank of a nonnegative m x n matrix M is the smallest number d such that M can be written as the product M = WH of a nonnegative m x d matrix W and a nonnegative d x n matrix H.  The notions of nonnegative rank and nonnegative matrix factorization have a wide variety of applications including bioinformatics computer vision communication complexity document clustering and recommender systems. A longstanding open problem is whether when M is a rational matrix the factors W and H in a rank decomposition M=WH can always be chosen to be rational.  In this talk we resolve this problem negatively and discuss consequences of this result for the computational complexity of computing nonnegative rank.

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

Securing enclaves with formal verification

Andrew Baumann
Microsoft Research, Redmond
SWS Colloquium
26 Apr 2017, 4:00 pm - 6:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
Moore's Law may be slowing but perhaps as a result other measures of processor complexity are only accelerating. In recent years Intel's architects have turned to an alphabet soup of instruction set extensions such as MPX SGX MPK and CET as a way to sell CPUs through new security features. SGX in particular promises powerful security: user-mode "enclaves" protected against both physical attacks and privileged software adversaries. To achieve this SGX's designers implemented an isolation mechanism approaching the complexity of an OS microkernel in the ISA using an inscrutable mix of silicon and microcode. However while CPU-based security mechanisms are harder to attack they are also harder to deploy and update and already a number of significant flaws have been identified. Worse the availability of new SGX features is dependent on the slowing deployment of new CPUs.

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

Comprehensive deep linking for mobile apps

Oriana Riva
Microsoft Research, Redmond
SWS Colloquium
10 Apr 2017, 10:30 am - 12:30 pm
Kaiserslautern building G26, room 112
simultaneous videocast to Saarbrücken building E1 5, room 005
Web deep links are instrumental to many fundamental user experiences such as navigating to one web page from another bookmarking a page or sharing it with others. Such experiences are not possible with individual pages inside mobile apps since historically mobile apps did not have links equivalent to web deep links. Mobile deep links introduced in recent years still lack many important properties of web deep links. Unlike web links mobile deep links must be explicitly built into apps by developers cover a small number of predefined pages and are defined statically to navigate to a page for a given link but not to dynamically generate a link for a given page. Another problem with state-of-the-art deep links is that once exposed they are hard to discover thus limiting their usage in both first and third-party experiences.

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

Graph Decomposition Problems in Image Analysis

Björn Andres
D2
Joint Lecture Series
05 Apr 2017, 12:15 pm - 3:15 pm
Saarbrücken building E1 5, room 002
A large part of image analysis is about breaking things into pieces. Decompositions of a graph are a mathematical abstraction of the possible outcomes. Breaking things (like an image itself) into pieces in a controlled way is hard. Optimization problems whose feasible solutions define decompositions of a graph are a mathematical abstraction of this task. One example is the correlation clustering problem whose feasible solutions relate one-to-one to the decompositions of a graph and whose objective function puts a cost or reward on neighboring nodes ending up in distinct components. This talk shows work by the Combinatorial Image Analysis research group that applies this problem and proposed generalizations to diverse image analysis tasks. It sketches the algorithms introduced by the group for finding feasible solutions for large instances in practice solutions that are often superior in the metrics of application-specific benchmarks. Finally it sketches the algorithm introduced by the group for finding lower bounds and points to new findings and open problems of polyhedral geometry in this context.

Local Reasoning for Concurrency, Distribution and Web Programming

Azalea Raad
Imperial College
SWS Colloquium
03 Apr 2017, 10:00 am - 1:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
In this talk I will present my research in developing local reasoning techniques in both concurrent and sequential settings.

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

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

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

Understanding & Controlling User Privacy in Social Media via Exposure

Mainack Mondal
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
31 Mar 2017, 4:00 pm - 6:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The popularity of online social media sites (OSM) like Facebook and Twitter have led to a renewed discussion about user privacy concerns today. These sites now mediate the sharing of personal information photos status updates and contacts of billions of users around the world; some OSMs even serve as the de-facto internet portal for a significant fraction of the world's population. However in OSMs users themselves are burdened to manage the privacy for the large number of social content they post. As a result often the user specified privacy settings do not match user expectation. Consequently in recent years numerous news media reports as well as research studies captured users' concern with protecting privacy of their social media content. These reports and studies boldly underline the users' urgent need for better privacy control mechanisms. Thus today the key research challenge in this space is: How do we provide improved privacy protection to OSM users for their social content? In this thesis we propose approaches to address this question.

In this talk I will first motivate my thesis research with privacy violation examples from real world which are not captured by access control the dominant privacy model today. Then I will propose exposure control a more inclusive privacy model to capture such violations. We define exposure for a content as the set of people who actually view the content. Next I will present an brief overview of our work on understanding and controlling exposure into three different real world scenarios -- (1) Understanding and controlling exposure using social access control lists (SACLs) (2) Controlling exposure by limiting large-scale social data aggregators and (3) Understanding and controlling longitudinal exposure in OSMs. i.e. how users control exposure of their old content. Finally I will expand upon the understanding and controlling longitudinal exposure in OSMs and propose our ongoing work on designing mechanisms to better control the longitudinal exposure.

Combining Computing, Communications and Controls in Safety Critical Systems

Professor Richard Murray
Caltech
SWS Distinguished Lecture Series
31 Mar 2017, 10:30 am - 1:30 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Flight critical subsystems in aerospace vehicles must achieve probability of failure rates of less than 1 failure in 10^9 flight hours (i.e. less than 1 failure per 100 000 years of operation).  Systems that achieve this level of reliability are hard to design hard to verify and hard to validate especially if software is involved.  In this talk I will talk about some of the challenges that the aerospace community faces in designing systems with this level of reliability and how tools from formal methods and control theory might help.  I will also describe some of the my group's work in synthesis of reactive protocols for hybrid systems and its applications to design of safety critical systems.

Hardening cloud and datacenter systems against configuration errors

Tianyin Xu
University of California
SWS Colloquium
22 Mar 2017, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Configuration errors are among the dominant causes of service-wide catastrophic failures in today's cloud and datacenter systems. Despite the wide adoption of fault-tolerance and recovery techniques these large-scale software systems still fail to effectively deal with configuration errors. In fact even tolerance/recovery mechanisms are often misconfigured and thus crippled in reality.

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

A New Approach to Network Functions

Aurojit Panda
University of Calefornia, Berkely,
SWS Colloquium
17 Mar 2017, 10:00 am - 12:00 pm
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Modern networks do far more than  just deliver packets and provide network functions -- including  firewalls caches and WAN optimizers -- that are crucial for scaling networks ensuring security and enabling new applications. Network functions were traditionally implemented using dedicated hardware middleboxes but in recent years they are increasingly being deployed as VMs on commodity servers. While many herald this move towards network function virtualization (NFV) as a great step forward I argue that accepted virtualization techniques are ill-suited to network functions. In this talk I describe NetBricks -- a new approach to building and running virtualized network functions that speeds development and increases performance. I end the talk by discussing the implications of being able to easily create and insert new network functions. 

Relational Cost Analysis

Ezgi Cicek
Max Planck Institute for Software Systems
SWS Student Defense Talks - Thesis Proposal
15 Mar 2017, 3:00 pm - 4:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Research in the programming languages community has made great progress on statically estimating the execution cost of a program. The execution cost could be the number of execution steps or any other abstract metric of resource usage. Static execution cost analysis techniques based on program analysis type systems and abstract interpretation are well-studied. However if we are interested in establishing bounds on the execution cost of a program relative to another program's cost naively combining worst- and best-case execution costs of the two programs does not work well in many cases. The reason is that such unary analysis techniques analyze the two programs in isolation ignoring the similarities between the programs and their inputs.

In this thesis proposal I propose the first relational cost analysis framework that establishes the relative cost of one program with respect to another possibly similar program by taking advantage of the similarities in their inputs and their code. Among other things such a relational cost analysis can be used to prove statements like: 1) Of two similar algorithms to solve a problem one is faster than the other without having to establish the exact complexity of either algorithm; 2) The execution cost of a program is independent of a secret input so nothing can be inferred about the secret input by observing the cost of executing the program; and 3) The cost of a program varies very little with input changes; this can aid resource allocation and scheduling. I show that in cases where the two programs and their inputs are closely related relational cost analysis is superior to non-relational analysis both in terms of precision and simplicity. Specifically I show that a refinement type and effect system provides a precise and compact mechanism for proving the relative cost of two programs. The idea behind relational cost analysis can be extended to other nontrivial domains. In particular I show that relational cost analysis can be adapted to prove upper bounds on the update costs of incremental programs.  Finally I briefly present a bidirectional technique to typecheck relational cost bounds.

Event time series analysis and its applications to social media analysis

Ryota Kobayashi
National Institute of Informatics, Japan
SWS Colloquium
14 Mar 2017, 2:09 pm - 4:39 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113
We first present an approach for analyzing the event time series namely the times of event occurrences. Interestingly the event time series appears in various fields including neuroscience (action potentials of a neuron) social media analysis (Twitter Facebook) and so on. Then we develop a framework for forecastingretweet activity through the analysis of Twitter dataset(Kobayashi & Lambiotte ICWSM 2016). This work is joint work with Renaud Lambiotte.

Privacy as a Service

Raymond Cheng
University of Washington
SWS Colloquium
13 Mar 2017, 10:30 am - 1:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Current cloud services are vulnerable to hacks and surveillance programs that undermine user privacy and personal liberties. In this talk I present how we can build practical systems for protecting user privacy from powerful persistent threats. I will discuss Talek a private publish-subscribe protocol. With Talek application developers can send and synchronize data through the cloud without revealing any information about data contents or communication patterns of application users. The protocol is designed with provable security guarantees and practical performance 3-4 orders of magnitude better throughput than other systems with comparable security goals. I will also discuss Radiatus a security-focused web framework to protect web apps against external intrusions and uProxy a Internet censorship circumvention tool in deployment today.

Randomized Algorithms Meets Formal Verification

Justin Hsu
University of Pennsylvania
SWS Colloquium
08 Mar 2017, 10:00 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Algorithms and formal verification are two classical areas of computer science. The two fields apply rigorous mathematical proof to seemingly disparate ends---on the one hand analyzing computational efficiency of algorithms; on the other designing techniques to mechanically show that programs are correct.

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

Constrained Counting and Sampling: Bridging the Gap between Theory and Practice

Kuldeep Meel
Rice University
SWS Colloquium
07 Mar 2017, 10:00 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Constrained counting and sampling are two fundamental problems in Computer Science with numerous applications including network reliability privacy probabilistic reasoning and constrained-random verification. In constrained counting the task is to compute the total weight subject to a given weighting function of the set of solutions of the given constraints. In constrained sampling the task is to sample randomly subject to a given weighting function from the set of solutions to a set of given constraints. In this talk I will introduce a novel algorithmic framework for constrained sampling and counting that combines the classical algorithmic technique of universal hashing with the dramatic progress made in Boolean reasoning over the past two decades. This has allowed us to obtain breakthrough results in constrained sampling and counting providing a new algorithmic toolbox in machine learning probabilistic reasoning privacy and design verification. I will demonstrate the utility of the above techniques on various real applications including probabilistic inference design verification and our ongoing collaboration in estimating the reliability of critical infrastructure networks during natural disasters.

Variational Bayes In Private Settings

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

The Diffix Framework: Noise Revisited, Again

Paul Francis
Max Planck Institute for Software Systems
Joint Lecture Series
01 Mar 2017, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
A longstanding open problem in Computer Science is that of how to get high quality statistics through direct queries to databases containing information about individuals without revealing information specific to those individuals.  It has long been recognized that the key to making this work is to add noise to query answers.  The problem has been how to do this without either adding a great deal of noise to answers or limiting the number of answers an analyst can obtain.  This talk presents Diffix a new framework for anonymous database query.  Diffix adds noise in such a way that repeated answers produce the same noise: it cannot be averaged away.  This "fixed noise" mechanism however creates new opportunities for attacks.  Diffix pro-actively tests potential alternate queries to discover and prevent these attacks.  In this talk we describe the Diffix framework and present a system design that provides basic query logic and statistical operations.  We will give a brief demo of a more advanced Diffix system that operates as a commercial product.  

Learning With and From People

Adish Singla
ETH Zürich
SWS Colloquium
28 Feb 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
People are becoming an integral part of computational systems fueled primarily by recent technological advancements as well as deep-seated economic and societal changes. Consequently there is a pressing need to design new data science and machine learning frameworks that can tackle challenges arising from human participation (e.g. questions about incentives and users' privacy) and can leverage people's capabilities (e.g. ability to learn).

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

A New Verified Compiler Backend for CakeML

Magnus Myreen
Chalmers University of Technology, Göteborg
SWS Colloquium
22 Feb 2017, 10:30 am - 1:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 112
The CakeML project has recently produced a verified compiler which we believe to be the most realistic verified compiler for a functional programming language to date. In this talk I'll give an overview of the CakeML project with focus on the new compiler in particular how the compiler is structured how the intermediate languages are designed and how the proofs are carried out. The talk will stay at a fairly high-level but I am happy to dive into details for any of the parts that I know well.

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

Safe, Real-Time Software Reference Architectures for Cyber-Physical Systems

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

Computational fair division and mechanism design

Simina Branzei
Hebrew University of Jerusalem
SWS Colloquium
20 Feb 2017, 10:00 am - 12:30 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The emergence of online platforms has brought about a fundamental shift in economic thinking: the design of economic systems is now a problem that computer science can tackle. For the first time we are able to move from the study of economic systems as natural systems to carefully designing and executing them on a computer. Prominent examples of digital market mechanisms include auctions for ads (run by companies such as Google) and electromagnetic spectrum (used by the US government). I will discuss several recent developments in fair division and mechanism design. I will start with a dictatorship theorem for fair division (cake cutting) showing that requiring truthfulness gives rise to a dictator. Afterwards I will discuss the theme of simplicity and complexity in mechanism design and more generally the interplay between economics and computation and learning.

Adventures in Systems Reliability: Replication and Replay

Ali Mashtizadeh
Stanford University
SWS Colloquium
17 Feb 2017, 10:30 am - 1:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The past decade has seen a rapid acceleration in the development of new and transformative applications in many areas including transportation medicine finance and communication. Most of these applications are made possible by the increasing diversity and scale of hardware and software systems.

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

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

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

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

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

Type-Driven Program Synthesis

Nadia Polikarpova
MIT CSAIL, Cambridge USA
SWS Colloquium
15 Feb 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Modern programming languages safeguard developers from many typical errors yet more subtle errors--such as violations of security policies--still plague software. Program synthesis has the potential to eliminate such errors by generating executable code from concise and intuitive high-level specifications. Traditionally program synthesis failed to scale to specifications that encode complex behavioral properties of software: these properties are notoriously hard to check even for a given program and so it's not surprising that finding the right program within a large space of candidates has been considered very challenging. My work tackles this challenge through the design of synthesis-friendly program verification mechanisms which are able to check a large set of candidate programs against a complex specification at once whereby efficiently pruning the search space.

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

On the Security and Scalability of Proof of Work Blockchains

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

Guiding program analyzers toward unsafe executions

Dr. Maria Christakis
University of Kent
SWS Colloquium
06 Feb 2017, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
Most static program analysis techniques do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties fail to verify properties or check properties under certain unsound assumptions such as the absence of arithmetic overflow. In the first part of the talk I will present a technique to complement partial verification results by automatic test case generation. In contrast to existing work our technique supports the common case that the verification results are based on unsound assumptions. We annotate programs to reflect which executions have been verified and under which assumptions. These annotations are then used to guide dynamic symbolic execution toward unverified program executions leading to smaller and more effective test suites.

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

Inverse Rendering

Shida Beigpour
MPI-INF - D4
Joint Lecture Series
01 Feb 2017, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Photographs as well as video frames are two-dimensional projections of three-dimensional real-world scenes. Photorealistic Computer Graphic Imagery (CGI) is usually generated by "rendering" a sophisticated three-dimensional model of a realistic scene on to a virtual camera sensor. Such process is not invertible due to the high amount of data loss. Still both physically captured photographs and synthesized photos (CGI) contain considerable amount of information about the characteristics of the scene itself. Even naïve human viewers are able to infer important information about the scene e.g. shape material illumination distance and actions solely from a single image. This is indeed much more difficult for computer systems. Inverse rendering is one of the hot-topics in computer vision in which the goal is to estimate and model the three-dimensional scene and its illumination automatically given only one or a sparse set of images from the scene. This is by nature a highly under-constraint problem which makes it very complex to solve. Yet the advancements in computation and imaging technologies (e.g. depth sensors and light-field cameras) open new horizons in this field. Inverse rendering makes many interesting applications possible including: creating novel views of the scene/objects re-lighting detecting and altering the object materials in the photographs and augmented reality.  This talk provides a brief overview of some of the state-of-the-art inverse rendering techniques and datasets with a strong focus on addressing the complexities of real-world scenarios.

Time for Text Mining and Information Retrieval

Jannik Strötgen
MPI-INF - D5
Joint Lecture Series
11 Jan 2017, 12:15 pm - 2:15 pm
Saarbrücken building E1 5, room 002
Temporal information is an important aspect in any information space and has important characteristics that make it highly eligible to be exploited in diverse text mining and information retrieval scenarios. For quite a long time only the metadata of text documents (e.g. publication dates) has been considered but with recent improvements in natural language processing (NLP) temporal expressions occurring in the content of documents (e.g. "January 2016" "next week") can be extracted and interpreted efficiently with high quality. This is particularly valuable as in many types of documents temporal expressions do not only occur frequently but also play a crucial role e.g. to anchor events in time.

In this talk after explaining the basics and challenges of the NLP task "temporal tagging" I present our approach to enrich documents with temporal information. Then I showcase several application scenarios in which we exploit automatically extracted temporal annotations for search and exploration tasks. These range from temporal information retrieval for news articles via Wikipedia-based event extraction up to the exploration of fictitious happenings in literary texts in the context of digital humanities research.