Upcoming events

Fighting Large-scale Internet Abuse

Kevin Borgolte
University of California
SWS Colloquium
26 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
The widespread access to the Internet and the ubiquity of web-based services make it easy to communicate and interact globally. Unfortunately, the software implementing the functionality of these services is often vulnerable to attacks. In turn, an attacker can exploit them to compromise and abuse the services for nefarious purposes. In my research, I aim to better understand, detect, and prevent these attacks.

In this talk, we first look at detecting website defacements, which can inflict significant harm on a website's owner or operator through the loss of sales, the loss in reputation, or because of legal ramifications. Then, we dive into how to automatically identify malware distribution campaigns, which has become a major challenge in today's Internet. Next, we look at how to mitigate the dangers of domain takeover attacks, which give attackers the same capabilities to spread misinformation or malware as vulnerabilities do, but without the actual need for a vulnerability in the affected service. Last, I will conclude by sketching interesting future directions on how to better understand, detect, and prevent Internet abuse.

Storage mechanisms and finite-state abstractions for software verification

Georg Zetzsche
SWS Colloquium
01 Mar 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
A popular approach to automatic program verification is to come up with an abstraction that reflects pertinent properties of the program. This abstraction is drawn from a class of formal models that is amenable to analysis. In the plethora of existing formal models, the aspects of programs that can be represented faithfully are typically determined by the infinite dimension of its state space, its storage mechanism. A central theme of my recent research is to obtain general insights into how the structure of the storage mechanism affects the analysis of a formal model. In the first part of my talk, I will survey results on an overarching framework of storage mechanisms developed in my doctoral work. It encompasses a range of infinite-state models and permits meaningful characterizations of when a particular method of analysis is applicable. Another current focus of my work concerns finite-state abstractions of infinite-state models. On one hand, these can be over- or under-approximations that are more efficient to analyze than infinite-state systems. On the other hand, they can serve as easy-to-check correctness certificates that are produced instead of yes-or-no answers to a verification task. Thus, the second part of my talk will be concerned with results on computing downward closures and related finite-state abstractions.

Incorporating Positional and Contextual Information into a Neural IR Model

Andrew Yates
Joint Lecture Series
07 Mar 2018, 12:15 pm - 1:15 pm
Saarbrücken building E1 5, room 002
Ad-hoc information retrieval models consider query-document interactions to produce a document relevance score for a given query and document. Traditionally, such interactions have been modeled using handcrafted statistics that generally count term occurrences within a document and across a collection. Recently, neural models have demonstrated that they provide the instruments necessary to consider query-document interactions directly, without the need for engineering such statistics.

In this talk, I will describe how positional term information can be represented and incorporated into a neural IR model. The resulting model, called PACRR, performs significantly better on standard TREC benchmarks than previous neural approaches. This improvement can be attributed to the fact that PACRR can learn to match both ordered and unordered sequences of query terms in addition to the single term matches considered by prior work. Using PACRR's approach to modeling query-document interactions as a foundation, I will describe how several well-known IR problems can be addressed by incorporating contextual information into the model; the resulting Co-PACRR model significantly outperforms the original PACRR model. Finally, I will provide a brief look inside the model to illustrate the interpretability of the learned weights and to investigate how match signals are combined by the model to produce a query-document relevance score.

Recent events

High Performance Data Center TCP Packet Processing

Antoine Kaufmann
University of Washington
SWS Colloquium
19 Feb 2018, 10:30 am - 11:30 am
Kaiserslautern building G26, room 111
simultaneous videocast to Saarbrücken building E1 5, room 029
TCP is widely used for client-server communication in modern data centers. But TCP packet handling is notoriously CPU intensive, accounting for an increasing fraction of data center processing time. Techniques such as TCP segment offload, kernel bypass, and RDMA are of limited benefit for the typical small, frequent RPCs. These techniques can also compromise protocol agility, resource isolation, overall system reliability, and complicate multi-tenancy.

I propose a unique refactoring of TCP functionality that splits processing between a streamlined fast path for common operations, and an out-of-band slow path. Protocol processing executes in the kernel on dedicated cores that enforce correctness and resource isolation. Applications asynchronously communicate with the kernel through event queues, improving parallelism and cache utilization. I show that my approach can increase RPC throughput by up to 4.1x compared to Linux. The fast-path can be offloaded to a programmable NIC to further improve performance and minimize CPU time for network processing. With hardware offload, data packets are delivered directly from application to application, while the NIC and kernel cooperate to enforce correctness and resource isolation. I show that hardware offload can increase per-core packet throughput by 10.7x compared to the Linux kernel TCP implementation.

Towards Latency Guarantees in Datacenters

Keon Jang
SWS Colloquium
15 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
A large portion of computation is now carried out in datacenter. A single datacenter hosts several 100s or 1000s of applications which share common compute and network resources in a datacenter. Isolating each application's performance, i.e., ensuring that its performance is predictable regardless of the behavior of other applications is essential to developing and deploying data center applications, since otherwise developers need to account for co-located applications, which increases development and deployment complexity. Despite its importance current approaches to performance isolation are incomplete, and focus mostly on isolating computational resources. In this talk I present two schemes for isolation network performance. The first, Silo, takes a resource allocation based approach and implements mechanisms for guaranteeing an application's network latency and throughput. The second, Express Pass, takes a congestion control based approach and fairly partitions network resources across applications.  Both approaches require no hardware (ASIC) changes, and can be deployed in today's datacenter. This shows that full application performance isolation is achievable today.

Liquid Haskell: Usable Language-Based Program Verification

Niki Vazou
University of Maryland
SWS Colloquium
12 Feb 2018, 10:30 am - 12:00 pm
Saarbrücken building E1 5, room 029
simultaneous videocast to Kaiserslautern building G26, room 111
Formal verification has been gaining the attention and resources of both the academic and the industrial world since it prevents critical software bugs that cost money, energy, time, and even lives. Yet, software development and formal verification are decoupled, requiring verification experts to prove properties of a template - instead of the actual - implementation ported into verification specific languages. My goal is to bridge formal verification and software development for the programming language Haskell. Haskell is a unique programming language in that it is a general purpose, functional language used for industrial development, but simultaneously it stands at the leading edge of research and teaching welcoming new, experimental, yet useful features.

In this talk I am presenting Liquid Haskell, a refinement type checker in which formal specifications are expressed as a combination of Haskell's types and expressions and are automatically checked against real Haskell code. This natural integration of specifications in the language, combined with automatic checking, established Liquid Haskell as a usable verifier, enthusiastically accepted by both industrial and academic Haskell users. Recently, I turned Liquid Haskell into a theorem prover, in which arbitrary theorems about Haskell functions would be proved within the language. As a consequence, Liquid Haskell can be used in Haskell courses to teach the principles of mechanized theorem proving.   

Turning a general purpose language into a theorem prover opens up new research questions - e.g., can theorems be used for runtime optimizations of existing real-world applications? - that I plan to explore in the future.