Events 2020

Distributed synthesis and negotiations

Anca Muscholl Universite de Bordeaux
04 Dec 2020, 10:00 am - 11:00 am
Virtual talk
SWS Distinguished Lecture Series
This talk will be a survey of instances of the synthesis problem in distributed models with rendez-vous synchronization. I will talk about synthesis for distributed automata within the theory of Mazurkiewicz traces and about the simpler model of negotiation diagrams (aka as workflow nets). 

---

Please contact Office for Zoom details. 

Towards Human Behavior Modeling from (Big) Data: From smart rooms, cars and phones to COVID-19

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

--

Please contact office for Zoom link details
Read more

Internet Measurements: From IPv6 Scanning to the COVID-19 Pandemic

Oliver Gasser MPI-INF - D3
02 Dec 2020, 12:15 pm - 1:30 pm
Virtual talk
Joint Lecture Series
Internet measurements are an important tool to analyze the deployment of protocols, evaluate the performance, resilience, and security of Internet hosts, and to generally better understand the current state of the Internet. In this talk we will introduce the concept of Internet measurements and show its applications, ranging from techniques for scanning the IPv6 Internet, to analyzing the impact of the COVID-19 pandemic on Internet traffic. We show that overall, traffic volumes increased after lockdowns have been imposed. ...
Internet measurements are an important tool to analyze the deployment of protocols, evaluate the performance, resilience, and security of Internet hosts, and to generally better understand the current state of the Internet. In this talk we will introduce the concept of Internet measurements and show its applications, ranging from techniques for scanning the IPv6 Internet, to analyzing the impact of the COVID-19 pandemic on Internet traffic. We show that overall, traffic volumes increased after lockdowns have been imposed. Furthermore, traffic of remote working and video conferencing applications increases, whereas other parts of the Internet traffic decrease during the pandemic.
Read more

High-Throughput and Predictable VM Scheduling for High-Density Workloads

Manohar Vanga Max Planck Institute for Software Systems
26 Nov 2020, 3:30 pm - 4:30 pm
Kaiserslautern building G26, room 111
SWS Student Defense Talks - Thesis Defense
In the increasingly competitive public-cloud marketplace, improving the efficiency of data centers is a major concern. One way to improve efficiency is to consolidate as many VMs onto as few physical cores as possible, provided that performance expectations are not violated. However, as a prerequisite for increased VM densities, the hypervisor’s VM scheduler must allocate processor time efficiently and in a timely fashion. As we show in this thesis, contemporary VM schedulers leave substantial room for improvements in both regards when facing challenging high-VM-density workloads that frequently trigger the VM scheduler. ...
In the increasingly competitive public-cloud marketplace, improving the efficiency of data centers is a major concern. One way to improve efficiency is to consolidate as many VMs onto as few physical cores as possible, provided that performance expectations are not violated. However, as a prerequisite for increased VM densities, the hypervisor’s VM scheduler must allocate processor time efficiently and in a timely fashion. As we show in this thesis, contemporary VM schedulers leave substantial room for improvements in both regards when facing challenging high-VM-density workloads that frequently trigger the VM scheduler.

As root causes, we identify (i) high runtime overheads and (ii) unpredictable scheduling heuristics. To better support high VM densities, we propose Tableau, a VM scheduler that guarantees a minimum processor share and a maximum bound on scheduling delay for every VM in the system. Tableau combines a low-overhead, core-local, table-driven dispatcher with a fast on-demand table-generation procedure (triggered on VM creation/teardown) that employs scheduling techniques typically used in hard real-time systems. In an evaluation of Tableau and three current Xen schedulers on a 16-core Intel Xeon machine, Tableau is shown to improve tail latency (e.g., a 17x reduction in maximum ping latency compared to Credit) and throughput (e.g., 1.6x peak web server throughput compared to RTDS when serving 1 KiB files with a 100 ms SLA). Further, we show that, owing to its focus on efficiency and scalability, Tableau provides comparable or better throughput than existing Xen schedulers in dedicated-core scenarios as are commonly employed in public clouds today.

Another common requirement in public clouds is the ability to use idle cycles in the system to perform low-priority background work, without affecting the performance of primary VMs (which are typically paid for by customers). The primary obstacle to achieving this is the lack of strong performance guarantees for VMs, which Tableau provides. We present the design of a background scheduler that enables a lower-priority class of VMs to use any idle cycles in the system, and present results showing that they have low impact on the performance of table-driven VMs, making it practical for cloud environments.

Finally, VM churn and workload variations in multi-tenant public clouds result in changing interference patterns at runtime, resulting in performance variation. In particular, variation in last-level cache (LLC) interference has been shown to have a significant impact on virtualized application performance in cloud environments. We present a novel approach for dealing with such dynamically changing interference, which involves periodically regenerating tables that provide the same guarantees on utilization and scheduling latency for all VMs in the system, but have different LLC interference characteristics.

We present two strategies to mitigate LLC interference: a randomized approach, and one that uses performance counters to detect VMs running cache-intensive workloads and selectively mitigate interference. Our results show that randomizing tables works well for mitigating worst-case slowdowns due to cache interference, while the performance-counter-based approach requires a more robust mechanism for detecting interfering VMs in order to match the performance of the randomized approach.
Read more

Can You Believe It? Security and Privacy Case Studies in Online Advertising, Misinformation, and Augmented Reality

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

--

Contact SWS Office for Zoom link details
Read more

Intelligibility Throughout the Machine Learning Life Cycle

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

--

Please contact Office for the Zoom details.
Read more

Experiments in Machine Behavior: Cooperating with and through machines

Iyad Rahwan Max Planck Institute for Human Development
11 Nov 2020, 3:00 pm
Virtual talk
SWS Distinguished Lecture Series
Human cooperation is fundamental to the success of our species. But emerging machine intelligence poses new challenges to human cooperation. This talk explores two interrelated problems: How can we humans cooperate *through* machines--that is, agree among ourselves on how machines should behave? And how can we cooperate *with* machines--that is, convince self-interested machines to cooperate with us. The talk will then propose an interdisciplinary agenda for understanding and improving our human-machine ecology.

--

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

--

Please contact SWS Office for Zoom details

Experiments in Machine Behavior: Cooperating with and through machines

Iyad Rahwan Max Planck Institute for Human Development
11 Nov 2020, 3:00 pm
Virtual talk
SWS Distinguished Lecture Series
Human cooperation is fundamental to the success of our species. But emerging machine intelligence poses new challenges to human cooperation. This talk explores two interrelated problems: How can we humans cooperate *through* machines--that is, agree among ourselves on how machines should behave? And how can we cooperate *with* machines--that is, convince self-interested machines to cooperate with us. The talk will then propose an interdisciplinary agenda for understanding and improving our human-machine ecology. -- Join Zoom Meeting https://zoom.us/j/99600775577?pwd=b21ZcTUyU2Z0N1VUUTRpa3JQWllyUT09 Meeting ID: 996 0077 5577 Passcode: 906631
Human cooperation is fundamental to the success of our species. But emerging machine intelligence poses new challenges to human cooperation. This talk explores two interrelated problems: How can we humans cooperate *through* machines--that is, agree among ourselves on how machines should behave? And how can we cooperate *with* machines--that is, convince self-interested machines to cooperate with us. The talk will then propose an interdisciplinary agenda for understanding and improving our human-machine ecology. -- Join Zoom Meeting https://zoom.us/j/99600775577?pwd=b21ZcTUyU2Z0N1VUUTRpa3JQWllyUT09 Meeting ID: 996 0077 5577 Passcode: 906631

Simple models for optimizing driver earnings in ride-sharing platforms

Evimaria Terzi Boston University
04 Nov 2020, 4:00 pm - 05 Nov 2020, 1:00 am
Virtual talk
SWS Distinguished Lecture Series
On-demand ride-hailing platforms like Uber and Lyft are helping reshape urban transportation, by enabling car owners to become drivers for hire with minimal overhead. Such platforms are a multi-sided market and offer a rich space for studies with socio-economic implications. In this talk I am going to address two questions:

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

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

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

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

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

Ensuring Compliance with Data Privacy and Usage Policies in Online Services

Aastha Mehta Max Planck Institute for Software Systems
03 Nov 2020, 2:30 pm - 3:30 pm
Saarbrücken building E1 5, room 029
SWS Student Defense Talks - Thesis Defense
Online services collect and process a variety of sensitive personal data that is subject to complex privacy and usage policies. Complying with the policies is critical and often legally binding for service providers, but it is challenging as applications are prone to many disclosure threats. In this thesis, I present two compliance systems, Qapla and Pacer, that ensure efficient policy compliance in the face of direct and side-channel disclosures, respectively.

Qapla prevents direct disclosures in database-backed applications (e.g., ...
Online services collect and process a variety of sensitive personal data that is subject to complex privacy and usage policies. Complying with the policies is critical and often legally binding for service providers, but it is challenging as applications are prone to many disclosure threats. In this thesis, I present two compliance systems, Qapla and Pacer, that ensure efficient policy compliance in the face of direct and side-channel disclosures, respectively.

Qapla prevents direct disclosures in database-backed applications (e.g., personnel management systems), which are subject to complex access control, data linking, and aggregation policies. Conventional methods inline policy checks with application code. Qapla instead specifies policies directly on the database and enforces them in a database adapter, thus separating compliance from the application code.

Pacer prevents network side-channel leaks in cloud applications. A tenant’s secrets may leak via its network traffic shape, which can be observed at shared network links (e.g., network cards, switches). Pacer implements a cloaked tunnel abstraction, which hides secret-dependent variation in tenant’s traffic shape, but allows variations based on non-secret information, enabling secure and efficient use of network resources in the cloud.

Both systems require modest development efforts, and incur moderate performance overheads, thus demonstrating their usability.
Read more

Diagnosing the data ecosystem

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

Towards Ultra-Reliable CPS: Reliability Analysis of Distributed Real-Time Systems

Arpan Gujarati Max Planck Institute for Software Systems
22 Oct 2020, 3:30 pm - 4:30 pm
Kaiserslautern building E1 5, room 111
SWS Student Defense Talks - Thesis Defense
In the avionics domain, "ultra-reliability" refers to the practice of ensuring quantifiably negligible residual failure rates in the presence of transient and permanent hardware faults. If autonomous Cyber-Physical Systems (CPS) in other domains, e.g., autonomous vehicles, drones, and industrial automation systems, are to permeate our everyday life in the not so distant future, then they also need to become ultra-reliable. However, the rigorous reliability engineering and analysis practices used in the avionics domain are expensive and time consuming, ...
In the avionics domain, "ultra-reliability" refers to the practice of ensuring quantifiably negligible residual failure rates in the presence of transient and permanent hardware faults. If autonomous Cyber-Physical Systems (CPS) in other domains, e.g., autonomous vehicles, drones, and industrial automation systems, are to permeate our everyday life in the not so distant future, then they also need to become ultra-reliable. However, the rigorous reliability engineering and analysis practices used in the avionics domain are expensive and time consuming, and cannot be transferred to most other CPS domains. The increasing adoption of faster and cheaper, but less reliable, Commercial Off-The-Shelf (COTS) hardware is also an impediment in this regard.

Motivated by the goal of ultra-reliable CPS, this dissertation shows how to soundly analyze the reliability of COTS-based implementations of actively replicated Networked Control Systems (NCSs)—which are key building blocks of modern CPS—in the presence of transient hardware faults. When an NCS is deployed over field buses such as the Controller Area Network (CAN), transient faults are known to cause host crashes, network retransmissions, and incorrect computations. In addition, when an NCS is deployed over point-to-point networks such as Ethernet, even Byzantine errors (i.e., inconsistent broadcast transmissions) are possible. The analyses proposed in this dissertation account for NCS failures due to each of these error categories, and consider NCS failures in both time and value domains. The analyses are also provably free of reliability anomalies. Such anomalies are problematic because they can result in unsound failure rate estimates, which might lead us to believe that a system is safer than it actually is.

Specifically, this dissertation makes four main contributions. (1) To reduce the failure rate of NCSs in the presence of Byzantine errors, we present a hard real-time design of a Byzantine Fault Tolerance (BFT) protocol for Ethernet-based systems. (2) We then propose a quantitative reliability analysis of the presented design in the presence of transient faults. (3) Next, we propose a similar analysis to upper-bound the failure probability of an actively replicated CAN-based NCS. (4) Finally, to upper-bound the long-term failure rate of the NCS more accurately, we propose analyses that take into account the temporal robustness properties of an NCS expressed as weakly-hard constraints.

By design, our analyses can be applied in the context of full-system analyses. For instance, to certify a system consisting of multiple actively replicated NCSs deployed over a BFT atomic broadcast layer, the upper bounds on the failure rates of each NCS and the atomic broadcast layer can be composed using the sum-of-failure-rates model.
Read more

Understanding and Evolving the Rust Programming Language

Ralf Jung Max Planck Institute for Software Systems
21 Aug 2020, 11:00 am - 12:00 pm
Saarbrücken building E1 5, room 021
simultaneous videocast to building , room / Meeting ID: 6312
SWS Student Defense Talks - Thesis Defense
Rust is a young systems programming language that aims to fill the gap between high-level languages with strong safety guarantees and low-level languages that give up on safety in exchange for more control.

Rust promises to achieve memory and thread safety while at the same time giving the programmer control over data layout and memory management. This dissertation presents two projects establishing the first formal foundations for Rust, enabling us to better understand and evolve this language:

RustBelt and Stacked~Borrows. ...
Rust is a young systems programming language that aims to fill the gap between high-level languages with strong safety guarantees and low-level languages that give up on safety in exchange for more control.

Rust promises to achieve memory and thread safety while at the same time giving the programmer control over data layout and memory management. This dissertation presents two projects establishing the first formal foundations for Rust, enabling us to better understand and evolve this language:

RustBelt and Stacked~Borrows.

RustBelt is a formal model of Rust's type system, together with a soundness proof establishing memory and thread safety. The model is also able to verify some intricate APIs from the Rust standard library that internally encapsulate the use of unsafe language features.

Stacked Borrows is a proposed extension of the Rust specification which enables the compiler to use Rust types to better analyze and optimize the code it is compiling. The adequacy of this specification is not only evaluated formally, but also by running real Rust code in an instrumented version of Rust's Miri interpreter that implements the Stacked Borrows semantics. RustBelt is built on top of Iris, a language-agnostic framework for building higher-order concurrent separation logics.

This dissertation gives an introduction to Iris and explains how to build complex high-level reasoning principles from a few simple ingredients. In RustBelt, this technique is used to introduce the lifetime logic, a separation logic account of borrowing, which plays a key role in the Rust type system.
Read more

Internet Measurements: Evaluating Deployment and Security Practices

Oliver Gasser MPI-INF - D3
01 Jul 2020, 12:15 pm - 1:15 pm
Saarbrücken building E1 3, room HS 2
Joint Lecture Series
-

Comprehensive and Practical Policy Compliance in Data Retrieval Systems

Eskam Elnikety Max Planck Institute for Software Systems
24 Jun 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Saarbrücken building E1 5, room / Meeting ID: 6312
SWS Student Defense Talks - Thesis Defense
Data retrieval systems such as online search engines and online social networks process many data items coming from different sources, each subject to its own data use policy. Ensuring compliance with these policies in a large and fast-evolving system presents a significant technical challenge since bugs, misconfigurations, or operator errors can cause (accidental) policy violations. To prevent such violations, researchers and practitioners develop policy compliance systems.

Existing policy compliance systems, however, are either not comprehensive or not practical. ...
Data retrieval systems such as online search engines and online social networks process many data items coming from different sources, each subject to its own data use policy. Ensuring compliance with these policies in a large and fast-evolving system presents a significant technical challenge since bugs, misconfigurations, or operator errors can cause (accidental) policy violations. To prevent such violations, researchers and practitioners develop policy compliance systems.

Existing policy compliance systems, however, are either not comprehensive or not practical. To be comprehensive, a compliance system must be able to enforce users' policies regarding their personal privacy preferences, the service provider's own policies regarding data use such as auditing and personalization, and regulatory policies such as data retention and censorship. To be practical, a compliance system needs to meet stringent requirements: (1) runtime overhead must be low; (2) existing applications must run with few modifications; and (3) bugs, misconfigurations, or actions by unprivileged operators must not cause policy violations.

In this thesis, we present the design and implementation of two comprehensive and practical compliance systems: Thoth and Shai. Thoth relies on pure runtime monitoring: it tracks data flows by intercepting processes' I/O, and then it checks the associated policies to allow only policy-compliant flows at runtime. Shai, on the other hand, combines offline analysis and light-weight runtime monitoring: it pushes as many policy checks as possible to an offline (flow) analysis by predicting the policies that data-handling processes will be subject to at runtime, and then it compiles those policies into a set of fine-grained I/O capabilities that can be enforced directly by the underlying operating system.
Read more

Security and Privacy Guarantees in Machine Learning with Differential Privacy

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

CANCELLED The (In)Security of Modern Communication: From Guesses to Guarantees

Cas Cremers CISPA
03 Jun 2020, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
-

Mtac2: Strongly-Typed Tactic- and Meta-Programming for Coq

Jan-Oliver Kaiser Max Planck Institute for Software Systems
27 May 2020, 10:30 am - 11:30 am
Saarbrücken building E1 5, room Online
SWS Student Defense Talks - Thesis Proposal
With growing interest in interactive theorem proving comes an increasing demand for proof automation. In many interactive proof assistants proof automation means constructing tactics that perform proof steps automatically.

In systems such as Coq, following the Curry-Howard Correspondence, proofs are terms and tactics are metaprograms. Proof scripts produce proof terms step by step until the resulting term inhabits the type dictated by the theorem to be proved. Consequently, metaprogramming facilities are vital to perform large scale proof mechanizations in Coq. ...
With growing interest in interactive theorem proving comes an increasing demand for proof automation. In many interactive proof assistants proof automation means constructing tactics that perform proof steps automatically.

In systems such as Coq, following the Curry-Howard Correspondence, proofs are terms and tactics are metaprograms. Proof scripts produce proof terms step by step until the resulting term inhabits the type dictated by the theorem to be proved. Consequently, metaprogramming facilities are vital to perform large scale proof mechanizations in Coq.

While Coq offers several mechanism for metaprogram (and tactic) construction they all come with severe restrictions on either applicability or expressiveness. With our work on Mtac2, a metaprogramming and tactic language for Coq, we aim to offer an alternative that covers a large set of use cases while simultaneously offering static type guarantees about the output of metaprograms and tactics.
Read more

Formal Synthesis for Robots

Hadas Kress-Gazit Cornell University
25 May 2020, 4:00 pm - 5:00 pm
Kaiserslautern building G26, room online
SWS Distinguished Lecture Series
In this talk I will describe how formal methods such as synthesis – automatically creating a system from a formal specification – can be leveraged to design robots, explain and provide guarantees for their behavior, and even identify skills they might be missing. I will discuss the benefits and challenges of synthesis techniques and will give examples of different robotic systems including modular robots, swarms and robots interacting with people.

CANCELLED: Computer Science Competitions @ SIC

Julian Baldus, Marian Dietz, Simon Schwarz Fachrichtung Informatik - Saarbrücken
01 Apr 2020, 12:15 pm - 1:15 pm
Saarbrücken building E2 2, room Günther-Hotz-HS
Joint Lecture Series
-

*Remote Talk* Improve Operations of Data Center Networks with Physical-Layer Programmability

Yiting Xia Facebook
26 Mar 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
Physical-layer programmability enables the network topology to be changed dynamically. In this talk, the speaker will make a case that cloud data center networks can be significantly easier to manage with physical-layer programmability. Three example network architectures will be shown as different use cases of this approach. ShareBackup enhances reliability through sharing backup switches efficiently network-wide, where a backup switch can be brought online instantaneously to recover from failures. Flat-tree solves the problem of choosing the right network topology for different cloud services by dynamically changing topological clustering characteristics of the network. ...
Physical-layer programmability enables the network topology to be changed dynamically. In this talk, the speaker will make a case that cloud data center networks can be significantly easier to manage with physical-layer programmability. Three example network architectures will be shown as different use cases of this approach. ShareBackup enhances reliability through sharing backup switches efficiently network-wide, where a backup switch can be brought online instantaneously to recover from failures. Flat-tree solves the problem of choosing the right network topology for different cloud services by dynamically changing topological clustering characteristics of the network. OmniSwitch is a universal building block of data center networks that supports automatic device wiring and easy device maintenance. At the end of the talk, the speaker will briefly introduce an ongoing follow-up research that extends physical-layer programmability from data center networks to backbone networks.
Read more

*Remote Talk* Learning efficient representations for image and video understanding

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

*Remote Talk* Fairness in machine learning

Niki Kilbertus University of Cambridge and MPI for Intelligent Systems, Tübingen
16 Mar 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
Machine learning increasingly supports consequential decisions  in health, lending, criminal justice or employment that affect the wellbeing of individual members or entire groups of our society. Such applications raise concerns about fairness, privacy violations and the long-term consequences of automated decisions in a social context. After a brief introduction to fairness in machine learning, I will highlight concrete settings with specific fairness or privacy ramifications and outline approaches to address them. I will conclude by embedding these examples into a broader context of socioalgorithmic systems and the complex interactions therein.
Machine learning increasingly supports consequential decisions  in health, lending, criminal justice or employment that affect the wellbeing of individual members or entire groups of our society. Such applications raise concerns about fairness, privacy violations and the long-term consequences of automated decisions in a social context. After a brief introduction to fairness in machine learning, I will highlight concrete settings with specific fairness or privacy ramifications and outline approaches to address them. I will conclude by embedding these examples into a broader context of socioalgorithmic systems and the complex interactions therein.

*Remote Talk* Democratizing Error-Efficient Computing

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

Search-based automated program repair and testing

Shin Hwei Tan Southern University of Science and Technology, Shenzhan, China
10 Mar 2020, 10:00 am - 11:00 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029 / Meeting ID: 6312
SWS Colloquium
Software testing remains the key technique for detection of functionality errors and vulnerabilities. Automated test generation typically involves searching in a huge input domain. Similarly many other software engineering activities such as software debugging and automated repair can be seen as large search problems. Despite advances in constraint solving and symbolic reasoning, major practical challenges in the use of automated testing and automated program repair, as opposed to manual testing and manual repair include (a) the lack of specifications, ...
Software testing remains the key technique for detection of functionality errors and vulnerabilities. Automated test generation typically involves searching in a huge input domain. Similarly many other software engineering activities such as software debugging and automated repair can be seen as large search problems. Despite advances in constraint solving and symbolic reasoning, major practical challenges in the use of automated testing and automated program repair, as opposed to manual testing and manual repair include (a) the lack of specifications, leading to problems such as overfitting patches and test-suite bias, and (b) learning curve in using these automated tools, leading to the lack of deployment. In this talk, I will present pragmatic solutions to address these challenges. Lack of specifications can be alleviated by implicitly exploiting lightweight specifications from comment-code inconsistencies, past program versions, or other program artifacts. Lack of deployment can be alleviated via systematic approaches towards collaborative bug finding. Such a collaborative approach can contribute to automated program repair as well as testing.
Read more

CANCELLED: Model checking under weak memory concurrency

Viktor Vafeiadis Max Planck Institute for Software Systems
04 Mar 2020, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
Model checking is an automatic approach for testing and verifying programs, and has proven to be very effective in a number of settings ranging from hardware designs to intricate low-level systems software. In this talk, I will present our recent research on applying model checking to weakly consistent concurrent programs. I will explain the key challenges involved in making model checking effective in this setting and how to address them.

Learning by exploration in an unknown and changing environment

Qingyun Wu University of Virginia
27 Feb 2020, 2:00 pm - 3:00 pm
Saarbrücken building E1 5, room SB 029
simultaneous videocast to Kaiserslautern building G26, room KL 111 / Meeting ID: 6312
SWS Colloquium
Learning is a predominant theme for any intelligent system, humans or machines. Moving beyond the classical paradigm of learning from past experience, e.g., supervised learning from given labels, a learner needs to actively collect exploratory feedback to learn the unknowns. Considerable challenges arise in such a setting, including sample complexity, costly and even outdated feedback.

In this talk, I will introduce our themed efforts on developing solutions to efficiently explore the unknowns and dynamically adjust to the changes through exploratory feedback. ...
Learning is a predominant theme for any intelligent system, humans or machines. Moving beyond the classical paradigm of learning from past experience, e.g., supervised learning from given labels, a learner needs to actively collect exploratory feedback to learn the unknowns. Considerable challenges arise in such a setting, including sample complexity, costly and even outdated feedback.

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

Compactness in Cryptography

Giulio Malavolta UC Berkeley and CMU
25 Feb 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
The communication complexity of secure protocols is a fundamental question of the theory of computation and has important repercussions in the development of real-life systems. As an example, the recent surge in popularity of cryptocurrencies has been enabled and accompanied by advancements in the construction of more compact cryptographic machinery. In this talk we discuss how to meet the boundaries of compactness in cryptography and how to exploit succinct communication to construct systems with new surprising properties. ...
The communication complexity of secure protocols is a fundamental question of the theory of computation and has important repercussions in the development of real-life systems. As an example, the recent surge in popularity of cryptocurrencies has been enabled and accompanied by advancements in the construction of more compact cryptographic machinery. In this talk we discuss how to meet the boundaries of compactness in cryptography and how to exploit succinct communication to construct systems with new surprising properties. Specifically, we consider the problem of computing functions on encrypted data: We show how to construct a fully-homomorphic encryption scheme with message-to-ciphertext ratio (i.e. rate) of 1 – o(1), which is optimal. Along the way, we survey the implication of cryptographic compactness in different contexts, such as proof systems, scalable blockchains, and fair algorithms.
Read more

Software Testing as Species Discovery

Marcel Böhme Monash University
10 Feb 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
A fundamental challenge of software testing is the statistically well-grounded extrapolation from program behaviors observed during testing. For instance, a security researcher who has run the fuzzer for a week has currently no means (i) to estimate the total number of feasible program branches, given that only a fraction has been covered so far, (ii) to estimate the additional time required to cover 10% more branches (or to estimate the coverage achieved in one more day, ...
A fundamental challenge of software testing is the statistically well-grounded extrapolation from program behaviors observed during testing. For instance, a security researcher who has run the fuzzer for a week has currently no means (i) to estimate the total number of feasible program branches, given that only a fraction has been covered so far, (ii) to estimate the additional time required to cover 10% more branches (or to estimate the coverage achieved in one more day, resp.), or (iii) to assess the residual risk that a vulnerability exists when no vulnerability has been discovered. Failing to discover a vulnerability, does not mean that none exists—even if the fuzzer was run for a week (or a year). Hence, testing provides no formal correctness guarantees.

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

Hybrid optimization techniques for multi-domain coupling in cyber-physical systems design

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

Designing responsible information systems

Asia J. Biega Microsoft Research Montreal, Canada
07 Feb 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: 6312
SWS Colloquium
Information systems have the potential to enhance or limit opportunities when mediating user interactions. They also have the potential to violate privacy by accumulating observational data into detailed user profiles or by exposing people in sensitive contexts. This talk will cover measures and mechanisms we have proposed for mitigating various threats to user well-being in online information ecosystems. In particular, I am going to focus on two contributions in the areas of algorithmic fairness and privacy. ...
Information systems have the potential to enhance or limit opportunities when mediating user interactions. They also have the potential to violate privacy by accumulating observational data into detailed user profiles or by exposing people in sensitive contexts. This talk will cover measures and mechanisms we have proposed for mitigating various threats to user well-being in online information ecosystems. In particular, I am going to focus on two contributions in the areas of algorithmic fairness and privacy. The first contribution demonstrates how to operationalize the notion of equity in the context of search systems and how to design optimization models that achieve equity while accounting for human cognitive biases. The second ties our empirical work on profiling privacy and data collection to concepts in data protection laws. Finally, I will discuss the necessity for a holistic approach to responsible technology, from studying different types of harms, through development of different types of interventions, up to taking a step back and refusing technologies that cannot be fixed by technical tweaks.
Read more

Spectector: Principled Detection of Speculative Information Flows

Jan Reineke Fachrichtung Informatik - Saarbrücken
05 Feb 2020, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
The recent Spectre attacks exploit speculative execution and microarchitectural side channels, such as caches, to leak sensitive information. Since the underlying hardware vulnerabilities are here to stay in billions of deployed devices, software countermeasures have been developed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and we develop Spectector, ...
The recent Spectre attacks exploit speculative execution and microarchitectural side channels, such as caches, to leak sensitive information. Since the underlying hardware vulnerabilities are here to stay in billions of deployed devices, software countermeasures have been developed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. We put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and we develop Spectector, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations. We implement Spectector in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place Spectre countermeasures.
Read more

veribetrfs: Verification as a Practical Engineering Tool

Jon Howell VMware Research, Bellevue, WA, USA
17 Jan 2020, 10:30 am - 11:30 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111 / Meeting ID: VMR 6312
SWS Distinguished Lecture Series
Recent progress in systems verification have shown that verification techniques can scale to thousands of lines. It is time to ask whether verification can displace testing as an effective path to software correctness. The veribetrfs project is developing a verified high-performance storage system. A primary goal of the project is to reduce verification methodology to engineering practice. Veribetrfs is developed using the Iron★ methodology, a descendent of the Ironclad and IronFleet projects. So far, we have a key-value store with 100k iops performance and strong guarantees against data loss. ...
Recent progress in systems verification have shown that verification techniques can scale to thousands of lines. It is time to ask whether verification can displace testing as an effective path to software correctness. The veribetrfs project is developing a verified high-performance storage system. A primary goal of the project is to reduce verification methodology to engineering practice. Veribetrfs is developed using the Iron★ methodology, a descendent of the Ironclad and IronFleet projects. So far, we have a key-value store with 100k iops performance and strong guarantees against data loss. This talk will give an overview of the methodology and describe how we have enhanced it in veribetrfs. 
Read more

Information Consumption on Social Media: Efficiency, Divisiveness, and Trust

Mahmoudreza Babaei Max Planck Institute for Software Systems
17 Jan 2020, 10:00 am - 11:00 am
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 113 / Meeting ID: 6312
SWS Student Defense Talks - Thesis Proposal
Over the last decade, the advent of social media has profoundly changed the way people produce and consume information online. On these platforms, users themselves play a role in selecting the sources from which they consume information, overthrowing traditional journalistic gatekeeping. Moreover, advertisers can target users with news stories using users’ personal data.

This new model has many advantages: the propagation of news is faster, the number of news sources is large, and the topics covered are diverse. ...
Over the last decade, the advent of social media has profoundly changed the way people produce and consume information online. On these platforms, users themselves play a role in selecting the sources from which they consume information, overthrowing traditional journalistic gatekeeping. Moreover, advertisers can target users with news stories using users’ personal data.

This new model has many advantages: the propagation of news is faster, the number of news sources is large, and the topics covered are diverse. However, in this new model, users are often overloaded with redundant information, and they can get trapped in filter bubbles by consuming divisive and potentially false information. To tackle these concerns, in my thesis, I address the following important questions: • (i) How efficient are users at selecting their information sources? We have defined three intuitive notions of users’ efficiency in social media – link (the number of sources the user follows), in-flow (the amount of redundant information she acquires), and delay efficiency (the delay with which she receives the information). We use these three measures to assess how good users are at selecting who to follow within the social media system in order to acquire information most efficiently. • (ii) How can we break the filter bubbles that users get trapped in? Users on social media sites such as Twitter often get trapped in filter bubbles by being exposed to radical, highly partisan, or divisive information. To prevent users from getting trapped in filter bubbles, we propose an approach to inject diversity in users’ information consumption by identifying non-divisive, yet informative information. We propose a new method to identify less divisive information on controversial topics using features such as the publishers’ political leaning. • (iii) How can we design an efficient framework for fact-checking? The proliferation of false information is a major problem in social media. To counter it, social media platforms typically rely on expert fact-checkers to detect false news. However, human fact-checkers can realistically only cover a tiny fraction of all stories. So, it is important to automatically prioritize and select a small number of stories for human to fact check. However, the goals for prioritizing stories for fact-checking are unclear.

We identify three desired objectives to prioritize news for fact-checking. These objectives are based on the users’ perception of the truthfulness of stories. Our key finding is that these three objectives are incompatible in practice.
Read more

Towards a Tight Understanding of the Complexity of Algorithmic Problems

Dániel Marx MPI-INF - D1
08 Jan 2020, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Joint Lecture Series
-