Bachelor- and Master-Seminar

Dear All,

the next seminar(s) take place on 28.10. at 14:00.

Update: The survey conducted suggests that you prefer to keep two parallel sessions, so nothing will change.

Session A:
Daniel Weber - Tobias Faber - Tom Fischer

https://cispa-de.zoom.us/j/99055946393?pwd=c01qZGtNN0xjNUtBY0dkcjY2WmU5QT09

Meeting-ID: 990 5594 6393
Kenncode: 7s*n^V

Session B:
Jens Heyens - Niklas Medinger - Sven Fackert

https://cispa-de.zoom.us/j/95445217887?pwd=OTMvUDhCSlp3OEpoZ0hxN2x4eWFKUT09

Meeting-ID: 954 4521 7887
Kenncode: 2p.%i4

Session A:

14:00-14:30 

Speaker: Daniel Weber
Type of talk: Bachelor Final Talk
Advisor: Ahmad Ibrahim

Title:
Automated Identification of Building Blocks for Microarchitectural Side Channels

Abstract:
In the last decade, we have seen various side-channel attacks against different CPU com-
ponents. These attacks typically rely on researchers studying processors’ documentation
to identify a potentially vulnerable component. Afterward, researchers manually reserve
engineer the component and use the built knowledge to exploit it as a side channel.
Hence, finding a new side channel is a time-consuming process.
This work aims to find microarchitectural side channels in an automated manner. We
present Osiris, a fuzzer that directly tests the hardware it is running on. Osiris executes
various combinations of instructions from the x86 instruction set architecture and observes
their behavior. Afterward, it uses these observations to identify instruction sequences
that act as building blocks for microarchitectural side channels.
We tested Osiris on different microarchitectures and automatically found all known
side channels matching our search pattern. Additionally, we identified five novel side
channels without knowledge of the underlying microarchitectural components they
abused. We conclude that it is possible to find different types of side channels for a
given microarchitecture automatically. Adversaries can use the information provided by
Osiris to mount side-channel attacks or in the context of Transient Execution Attacks.
Therefore, we stress that to defending against such attacks reliably, requires fixing the
root cause of these vulnerabilities.

14:30-15:00

Speaker: Tobias Faber
Type of talk: Bachelor Final
Advisor: Giancarlo Pellegrino
Title: Evaluating Strengths and Shortcomings of Web Scanners when Crawling Web Applications

Abstract: Web crawlers have been in existence for a long time with their main focus on gathering information on the web but there are also security focused crawlers which are more aggressive in exploring the web applications. They forge URLs to find secret ones and test inputs for possible vulnerabilities. But how efficient is this and will they find the interesting parts of the web app? In this thesis the focus will be on executed code and state changing operations which are triggered by the crawler's behavior. We will try to find out if there are differences between crawling strategies or if a random crawler is just as good. To accomplish this we will be instrumenting PHP Web Applications to track the crawler.

 

15:00-15:30

Speaker: Tom Fischer
Type of talk: Bachelor Thesis Final Talk
Advisor: Dr. Nico Döttling
Title: Efficient Field Extension for Oblivious Linear Evaluation

Abstract: Secure multi-party computation is a subfield of cryptography, where participants want to evaluate a joint function over their private data without sharing their data. The Oblivious linear function evaluation (OLE) is an inportant building block in such cryptographic protocols and lets two parties jointly evaluate y=ax+b. The difficulty here lies in the fact, that one party sends a and b and learns nothing about the other parties input, and the other party sends x and learns y and nothing about a and b. As of lately, several UC-secure OLE protocols have been published under both semi-honest and malicious adversarial settings. But to the best of my knowledge all of these recently proposed protocols focused on input values over prime fields and none for extension fields. In this work, I propose a UC-secure OLE protocol for extension fields in a semi-honest setting that reduces its security to prime field OLE primitives.

Session B:

14:00-14:30

Speaker: Jens Heyens    
Type of talk: Bachelor Thesis  talk
Advisor: Dr. Katharina Krombholz
Title: Assisting Developers in Making Security Decisions

Abstract:
Static analysis tooling has been deployed in various contexts to assist developers
in making security decisions. While static analysis has been touted as a great
advance in ensuring secure coding practices, usability and efficacy studies have
been lacking. In this work, we will look at how to improve usability of these tools
and whether or not they have an impact on real-world vulnerabilities. Based on
previous work and recommendations, a tool for consolidation of multiple static
analysers has been developed to aid developers. We then chose the Bandit static
analyser to further evaluate its efficacy on a set of 79 real-world vulnerabilities
from 2018 and 2019, of which Bandit was able to correctly identify seven.

14:30-15:00

Speaker: Niklas Medinger
Type of talk: Bachelor Final
Advisor: Cas Cremers
Title: Exploring Automatic Lemma Generation for the Tamarin Prover

Abstract:
Security protocols are all around us. Their applications range from securing our communication
via messaging apps to protecting the credentials we use to log into our bank accounts.
As a result, these protocols need to be reliable and secure. One way to achieve this
is to formally model and verify protocols with verification tools such as ProVerif or
the Tamarin prover. Unfortunately, modeling a protocol and verifying its desired
security properties takes-depending on its complexity-up to months of work.
As the desired security properties are often not automatically provable by the
tool of choice, a significant part of the verification process involves the manual step-wise refinement of auxiliary
statements (lemmas) that, ultimately, imply the desired security properties.

Aiming to cut down the time and manual work needed to verify a protocol formally, we develop
an approach to generate auxiliary lemmas for the Tamarin prover automatically. To do so,
we first identify common patterns in auxiliary lemmas needed to verify typical protocols
with Tamarin. Based on these patterns, we then devise an algorithm that automatically generates
auxiliary lemmas, and we implement this algorithm in the form of a preprocessing tool for Tamarin.
Finally, we evaluate our tool on suited models from Tamarin's GitHub repository.
Our evaluation shows that all but one generated lemma can be proved automatically by Tamarin
and that their impact on the time Tamarin needs to verify protocols varies with the considered protocol model.

15:00-15:30

Speaker: Sven Fackert
Type of talk: Master Thesis Intro Talk
Supervisor: Prof. Dr. Andreas Zeller
Advisor: Alexander Kampmann
Title: A User Study on the Effectiveness of Test-Based Debugging Diagnoses

Abstract:
The Alhazen algorithm was created to support software engineers in diagnosing why computer programs fail. Given a failure-inducing input it determines features (like the length or the value of elements of the input) that cause a malfunction. While experiments have shown that Alhazen can drastically reduce the debugging space, there is still a need for empirical evidence that it actually helps software engineers to fix bugs faster and better. This presentation summarizes the proposed work of a master thesis that aims to (1) prepare a design for an experimental user study, (2) to develop necessary tools and a technical infrastructure to conduct the study remotely and (3) to verify it in a pilot study, involving approximately 20 student subjects.