Events 2017

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.

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

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
Renato Mancuso is a doctoral candidate in the Department of Computer Science at the University of Illinois at Urbana-Champaign. He is interested in high-performance cyber-physical systems with a specific focus on techniques to enforce strong performance isolation and temporal predictability in multi-core systems. He has published around 20 papers in major conferences and journals. His papers were awarded a best student paper award and a best presentation award at the Real-Time and Embedded Technology and Applications Symposium (RTAS) in 2013 and 2016 respectively. He was the recipient of a Computer Science Excellence Fellowship and a finalist for the Qualcomm Innovation Fellowship. Some of the design principles for real-time multi-core computing proposed in his research have been officially incorporated in recent certification guidelines for avionics systems. They have also been endorsed by government agencies industries and research institutions worldwide. He received a B.S. in Computer Engineering with honors (2009) and a M.S. in Computer Engineering with honors (2012) from the University of Rome "Tor Vergata".

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 ?nance 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 dif?culty 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 ?le 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.