Bachelor- and Master-Seminar

Dear All,

the next seminar takes place on 17.2. at 14:30.

Session A 14:30:
Pit Jost

https://cispa-de.zoom.us/j/96786205841?pwd=M3FOQ3dSczRabDNLb3F1czVXVUpvdz09

Meeting-ID: 967 8620 5841
Kenncode: BT!u5=

Session A:

14:00-14:30 

No talk this week.

14:30-15:00

Speaker: Pit Jost
Type of talk: Bachelor Intro Talk
Advisor: Prof. Dr. Andreas Zeller
Supervisor: Dr. Rafael Dutra
Title: Automated generation of format-aware Fuzzers using FormatFuzzer

Abstract: Fuzzing is an automated testing technique used to execute computer programs with a high number of automatically generated, often ill-formed inputs in order to trigger unexpected behavior such as hangs, crashes or undesired outputs which can be a sign for the presence of vulnerabilities that can be exploited. As file formats tend to be very complex, programs often validate the structure of their inputs at an early parsing stage. Randomly generated files will likely not match the expected structure, thus are discarded during this early stage. Due to this, purely random fuzzing only reaches low code coverage, making it inefficient.

In this thesis, the novel fuzzing technique FormatFuzzer is used. FormatFuzzer uses a structure-aware approach that works by compiling descriptions of binary file formats, referred to as binary templates, into executables that can be used to parse, generate and mutate binary files compliant to their respective format specifications. These binary templates contain all information required to generate and parse structurally valid files of a given format. The files generated by FormatFuzzer are expected to perform better than conventional fuzzing approaches, as due to their structure-awareness, the files are most likely to pass the parsing stage of a given program, thus reaching higher code coverage.

The main focus in this thesis will be on developing reliable binary templates in order to support formats for which no binary templates optimized for generation with FormatFuzzer exist. As a starting point, existing templates made publicly available by 010 Editor are used. These templates work fine for parsing, but are not intended for file generation, as they are missing important information about specific values that need to be present at specific positions in the generated files in order for them to be valid, such as magic bytes. To tackle this issue, this information is added to the existing templates. Furthermore, the process of developing binary templates will be facilitated for future work by the introduction of new features into the binary template language, by automating parts of the process or by using new procedures. The efficiency of the resulting templates will finally be evaluated, and the results will be compared with related work.

15:00-15:30

Dear All,

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

Session A 14:00-15:00:
Paul Szymanski - Mara Schulze - Leon Brettschneider

https://cispa-de.zoom.us/j/96786205841?pwd=M3FOQ3dSczRabDNLb3F1czVXVUpvdz09

Meeting-ID: 967 8620 5841
Kenncode: BT!u5=

Session B
Dominik Sautter - Marvin Hoffmann

https://cispa-de.zoom.us/j/99025989421?pwd=cWJIM29LYktsbStxTXlKUStZRi9MUT09

Meeting-ID: 990 2598 9421
Kenncode: 3mZyE$

Session A:

14:00-14:30 

Speaker: Paul Szymanski
Type of talk: Bachelor Intro
Advisor: Cristian-Alexandru Staicu
Title: A Study of State-of-the-Art Call Graph Creation Approaches for JavaScript

Call graph creation is an important stepping stone for building sophisticated static analyses, e.g., taint analysis. However, many state-of-the art tools perform poorly when faced with real-world code. That is, many of the available call graph creation tools for JavaScript are extremely fragile and thus, fail to produce a call graph when certain language constructs are present in the analysed code. For example, many such tools only support ECMAScript 5 features, while practitioners rely on more modern syntax. Some call graph creation tools solve this problem by performing a transpilation step, e.g., using Babel, on the code before processing it further. Although these transformations are assumed to be preserving the functionality of the code, the transformations might result in different call graphs. This might be the case for other kinds of transformations, like obfuscation and minification, as well.
The goal of this bachelor thesis is to study existing call graph creation algorithms and identify their limitations, i.e. which language constructs are the most difficult to analyse. Additionally, we are interested in identifying code transformation techniques with the highest impact on the performance of static call graph algorithms, both beneficial and detrimental.

14:30-15:00

Speaker: Mara Schulze
Type of talk: Bachelor Intro Talk
Advisor: Prof. Christian Rossow
Title: Detecting Cryptojacker Malware in Sandnet purely through network indicators

Abstract:
Many cryptocurrencies require great computational work in order to verify their block chain. This is computationally expensive, and as an incentive to participate in the verification process a small reward is being given to the person who solves a mathematical riddle first, thus "mines" the block. Malware authors exploit that by letting the computations run on the victim's computer and then claiming the reward for themselves.

Sandnet is a dynamic analysis environment, belonging to CISPA. It runs Malware for a long time (ca. one hour) and puts out network based indicators like the domains the malware specimen connects to, the packet size, the connection time etc.

I want to detect Cryptojacker malware purely by the statistics that Sandnet is producing.

15:00-15:30

Speaker: Leon Bettscheider
Type of talk: Master Final
Advisor: Prof. Dr. Andreas Zeller
Supervisor:Dr.Rahul Gopinath
Title: Concolic Grammar Refinement for Stateful Fuzzing
Abstract:
Fuzz testing is a widely deployed automated software testing technique which has been used to discover many security-critical software bugs.
Fuzzing probes the program under test for faulty behavior by running it repeatedly on automatically generated inputs.
One of the problems with fuzzing is that, to be effective, fuzzers need to generate plausible inputs that reach nontrivial parts of the program.

Effective fuzzing of stateful programs, such as database engines or web servers, is challenging because generated inputs need to be syntactically valid to be accepted by the parser, and semantically valid with respect to the current ephemeral program state in order to reach deep functionality.

While grammar-based fuzzing presents a method to generate syntactically valid inputs at a high rate, such inputs are typically not semantically valid in the case of stateful programs. For example, the validation of inputs may depend on the state of the program in question (such as session IDs), which are hard to produce using random chance.
    
To overcome this limitation, we propose a novel grammar refinement strategy for stateful programs.
We start with a context-free grammar, and leverage concolic execution of generated inputs to mine state-based constraints that need to be satisfied.
These constraints are then lifted to the grammar, which results in a grammar that automatically fine tunes itself towards inputs that can reach deeper and deeper code paths in the current execution.
    
We implement our grammar refinement technique on top of a concolic execution engine for the C programming language.
We demonstrate a proof of concept on SQLite that shows the ability of our approach to mine existing table and column names from the database.
In addition, we combine our approach with a state-of-the-art grammar fuzzer and compare it with grammar fuzzing alone in an experiment on SQLite.
Our evaluation suggests that grammar refinement enhances fuzzing if the targeted state information contains a sufficiently high level of entropy.

Session B:

14:00-14:30

Speaker: Dominik Sautter
Type of talk: Bachelor Intro
Advisor: Giancarlo Pellegrino
Title: Detecting Client-Side XSS via Code Property Graphs
Abstract:
The automated detection of web vulnerabilities is challenging and, to date, mostly performed by manually inspecting the source code. A promising idea to ease the automated detection of vulnerabilities is using canonical representations for programs via code-property graphs (CPG) and identify vulnerable behaviors via graph traversals.
CPGs for web applications are in their infancy, i.e., XSS/SQLi for PHP program (PHPJoern) or to detect a client-side CSRF (JAW), and we know very little about their generality and adequacy at detecting other client-side vulnerabilities. This thesis will start from the existing CPG for client-side JavaScript programs as implemented by JAW and evaluate its adequacy in detecting a severe and popular client-side vulnerability, i.e., client-side XSS. The evaluation of the implementation will be made on 10 applications which will be selected by their popularity and problem base. This talk will present a short overview of CPG and the success of it in PHP, C/C++ and JS, as well as an outlook how the upcoming work will be structured and evaluated.

14:30-15:00

Speaker: Marvin Hoffmann
Type of talk: Bachelor Final Talk
Advisor: Alfusainey Jallow, Dr.-Ing. Sven Bugiel
Title: Gamified Crowd-Sourcing the Security Classification of Stack Overflow Code Snippets

Abstract:Stack Overflow is the most widely used forum for developers and IT experts to solve programming issues. Since the answers often contain code snippets solving the problem, prior studies have shown that many snippets are copied and pasted into developer codebases without having a detailed look at it. This behavior causes security breaches in many software products because these code snippets often are insecure. For example,the posted solution could be out of date and not address recent security fixes.
To avoid insecure software, we want to provide a security indication of code snippets posted on Stack Overflow. We investigated if we can classify code snippets using a crowdsourcing approach. Therefore, we built to our knowledge the first web-based crowdsourcing platform to gamify code snippets’ security classification. We presented 150 Java code snippets to security-focused users during the test run and let them classify the snippets into secure or insecure by swiping right or left on our web page. Afterward, we evaluated the classification of the five most classified snippets by inspecting them manually again. With this approach, we can offer researchers an alternative way beneath machine learning approaches and experts classifying to categorize code on Stack Overflow and build the basis for helping developers to write more secure code.

15:00-15:30

Dear All,

the next seminar takes place on 6.1. at 14:00.

Session A:
Pavithra Krishna - David Butscher - Marc Katz 

https://cispa-de.zoom.us/j/96786205841?pwd=M3FOQ3dSczRabDNLb3F1czVXVUpvdz09

Meeting-ID: 967 8620 5841
Kenncode: BT!u5=
 

14:00-14:30 

Speaker:Pavithra Krishna
Type of talk: Master Intro talk
Advisor: Prof.Dr.Andreas Zeller
Supervisor:Dr.Rahul Gopinath
Title:Fuzzing the Extended Berkeley PacketFilter verifier using Grammars

Abstract:
The use of the Linux Kernel is widespread in several Linux-based distributions. One feature which is a part of the Linux kernel is BPF(Berkeley Packet Filter), introduced in the 1990s. BPF makes it possible for a user-space process with minimum privileges to directly provide a filter program to the kernel space, which is of the highest privileges. Then the kernel provides only those packets that match the filter to the user process. From the efficiency point of view, this saves time, memory space. The evolution of this technology today has extended in many ways into being called eBPF (Extended Berkeley Packet Filter). It supports the filtering of packets from the network and allows programs to be attached to trace points to gain information about the process and CPU resources. This mechanism also forms the basis of Seccomp(Secure Computing) BPF, which is a provision to filter the system calls between the user and kernel space. As a security mechanism, it has an in-built static analyzer called the eBPF verifier, which stands as a doorman to ensure that the user-supplied programs are safe to execute. Therefore any flaw or vulnerability in the eBPF verifier gives direct control over the kernel. There is a possibility to leak memory addresses, read-write access to arbitrary locations, etc. A self-test framework is currently used to do the security testing of the eBPF verifier. A couple of research activities in the past primarily use the existing self-test framework with well-known mutation-based fuzzers. Hence this indicates that there is a scope for improvement using other techniques to find deeper bugs. This paper aims to find deeper bugs using Grammar-based Fuzzing as the core technique.  Additionally, the work also attempts to optimize the overall Fuzzing process by reusing input fragments from existing program code fragments while generating new ones using the Grammar.

14:30-15:00

Speaker: David Butscher
Type of talk: Bachelor Intro
Advisor: Ben Stock
Title: Measuring the Impact of the Crawling Context on the Results of Web Scanners

Abstract:
Web scanners are essential tools for security researchers. They are used to measure the occurrence of security flaws in the known web. Unfortunately, their efficiency suffers from multiple limitations. One limitation is that in the first phase - the crawling phase - the crawling module needs to explore as many resources of a domain as possible. The found URLs are the input for the attack modules in the second phase. Hence the efficiency of the whole web scanner depends on the efficiency of the crawler module. This work aims to identify factors that influence the success of web scanners, especially in the crawling phase. To reach this goal, we will change the context of the crawling process and examine the results of the applied attack modules. We will target three factors in detail:
1. IP address: the change of the IP addresses could mitigate the countermeasures of web application firewalls against known attackers. There is also a possibility that some sites are only accessible from particular locations.
2. User-Agent: site owners may deliver multiple versions of their site customized for the end-user device.
3. Authentication: signed up users may access pages that unknown users will never be able to reach. Since authentication in an automated fashion is not trivial, we will mainly focus on websites that offer SSO.

We will use a limited set of top domains listed by Tranco for our experiments. For our evaluation, we will run the web scanner without modifications and later with one modified factor. Afterward, we will count the number of detected security flaws. In this way, we can measure the direct influence of the changes to the crawling context.

15:00-15:30

Speaker: Marc Katc    
Type of talk: Bachelor Intro
Advisor: Ben Stock
Title: Nasty Tag Soup - How gracious HTML parsing helps Mallory

Abstract: HTML is one of the first technologies that came with the invention of the internet and evolved around the last 30 years, sometimes in more than one direction. Today, with HTML 5 as the current version, the standard itself acknowledges that faulty implementations are common and can even influence the specification itself. Because of this and back- and forward compatibility, modern browsers are not strict about the parsing of HTML and often times reveal huge differences in their parsing routines.
The goal of this bachelor’s thesis is to analyze the gray areas of gracious HTML parsing in different browsers, to evaluate the security implications that come with it as well as to understand the consequences of stricter parsing of security relevant HTML parts in the wild. In particular, we identify tags that are or become more dangerous if they are parsed in violation to their specifications and create recommendations for parsing routines. We are also using crawled web data to measure the frequency of misused HTML tags in the wild and therefore estimate the impact on usability of stricter parsing.

Dear All,

the next seminar takes place on 23.12. at 14:00.

Session A:
Yu-De Lin - Amir Heinisch

https://cispa-de.zoom.us/j/96786205841?pwd=M3FOQ3dSczRabDNLb3F1czVXVUpvdz09

Meeting-ID: 967 8620 5841
Kenncode: BT!u5=
 

14:00-14:30 

Speaker: Yu-De Lin
Type of talk: Master intro
Advisor: Dr. Nils Ole Tippenhauer
Title: Extracting DNN Models from Embedded Devices via the Power Side-channel

Abstract: As hardware becomes more and more powerful, running deep neural networks on embedded devices are more popular than ever. Many hardware vendors have developed their own AI chips inside their own products or selling development kits for their AI-powered boards. The era of edge computing has arrived. However, the new threats on these AI devices are emerging too. Since there is only little security protection for embedded devices where AI models are used, the intellectual property is under high risks of being stolen or leaked.
In our project, we are investigating how the attacker can extract AI models on the chip in the physical layer. In particular, we focus on the power-side channel, which is less complicated to setup compared to EM-channels in prior work . In addition, we design a framework with the aid of machine learning that the attacker can use to automate the attack to reverse engineer the achitecture and the weights of models.

14:30-15:00

Speaker: Amir Heinisch
Type of talk: Bachelor Thesis Intro Talk
Advisor: Dr. Nils Ole Tippenhauer
Title: Leveraging Trusted Execution Environments to Implement Trustworthy Motor Controls

Abstract:

Every modern vehicle nowadays contains a large scale of digital controllers. Many new attack
vectors arise. For physical attackers (especially tuners) there are many new ways to
manipulate vehicles (e.g. modify firmware to increase performance) and with that violate the law.
Protecting against these threats requires technical mechanisms to verify regulations.

In this thesis we implement and evaluate a method to detect, prevent and even report
violations with the help of Trusted Execution Environments. In particullar we want
to run code in a secure environment which is able to verify control decisions made by
complex motor control software. For this we will build a proof of concept using the
ARM TrustZone technology on the latest STM32L5 microcontroller. This allows us to
evaluate such an approach and show its feasibility.

15:00-15:30

Dear All,

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

Reminder: You should always upload your talk info until Wednesday night BEFORE the week of your talk.

Session A 14:00-15:00:
Alexander Rassier - Anania Tesfaye

https://cispa-de.zoom.us/j/96786205841?pwd=M3FOQ3dSczRabDNLb3F1czVXVUpvdz09

Meeting-ID: 967 8620 5841
Kenncode: BT!u5=

Session B
Vera Resch - Andreas Hanuja - Pavithra Krishna

https://cispa-de.zoom.us/j/99025989421?pwd=cWJIM29LYktsbStxTXlKUStZRi9MUT09

Meeting-ID: 990 2598 9421
Kenncode: 3mZyE$

Session A:

14:00-14:30 

Speaker: Alexander Rassier
Type of talk: Master Final
Advisor: Dr.-Ing. Ben Stock
Title: CIDeR: Automatically Implementing Nonce-Based Content Security Policies

Abstract:
Not a single day goes by without the majority of people using the Web for work and leisure, which is why Web sites are a primary target for malicious attackers. Server-Side Cross-Site Scripting is still considered one of the most dangerous vulnerabilities in the Web. There are many ways to mitigate the effects of malicious scripts, such as the Content Security Policy (CSP), but research has shown that creating a secure CSP is a difficult endeavour: Less than 10\% of Web sites that deploy one do it in a way that cannot be easily bypassed. Most Web developers struggle with creating a secure CSP that does not break the functionality of the Web site by blocking too much.

In order to help with the generation and deployment of a secure and usable CSP for Django Web applications we have created CIDeR ("CSP Implementation Done Right"), an Intellij/PyCharm plugin for automatically implementing a secure nonce-based CSP. We then evalutated this tool on several popular Django applications on GitHub -- also in comparison to other tools that offer automatic CSP generation -- in order to confirm the security of the created CSPs. Furthermore, we conducted a pilot study in order to evaluate the usability and perceived security of our plugin.

Our evaluation shows that CIDeR is able to automatically generate and deploy secure nonce-based CSPs for Django projects without breaking any functionality of the Web site. These CSPs are shown to be more secure than the ones generated by the other automation tools. Moreover, CIDeR seems to be usable and able to assist developers in creating a secure CSP, even without them having a deeper knowledge of client-side Web security or the security mechanism itself.

14:30-15:00

Speaker: Anania Tesfaye
Advisor: Ben Stock

No info provided

15:00-15:30

No talk this week. If you want to speak, mail bamaseminar@cispa.saarland

Session B:

14:00-14:30

Speaker: Vera Resch
Type of talk: Master Intro
Advisor: Dr. Rahul Gopinath
Title: URL-Fuzzing

Abstract: Uniform Resource Locators(URLs) allow to quickly and precisely navigate today's web. Similar to the specifications of other web standards, such as HTML, the WHATWG maintains the URL specification as a living standard. However, because different applications use URLs for a multitude of purposes, there exists a variety of implementations of URL parsers, most of which claim to follow the URL standard.
    This thesis uses grammar-based fuzzing together with a grammar of the current URL standard to examine how close the relationship between URL parsers and the standard is. In detail, this consists of testing the URL parsers included in the browsers Firefox and Chromium, as well as a selection of stand-alone URL parsers with inputs generated by executing a grammar-based fuzzer on the URL grammar. Additionally, this thesis evaluates the errors encountered during test execution as well as the code coverage achieved in the selected URL parsers.

14:30-15:00

Speaker: Andreas Hanuja
Type of talk: Bachelor Thesis Final Talk
Advisor: Prof. Dr. Andreas Zeller
Title: Generating and Parsing Binary File Formats with FormatFuzzer

Abstract:

Modern fuzzers are used worldwide for automated software testing and to regularly find weak points in common programs. Many randomly generated inputs are used to search for errors in the program flow. But if the input files expected by the target program must have a complex structure, it is hardly possible to generate useful input by pure chance.
Thus, current research tries to modify the fuzzer, by giving it background knowledge about the expected input structure.

In contrast to previous proposals, we use a novel framework called FormatFuzzer. FormatFuzzer automatically compiles high-efficiency generators and parsers from a file format specification. In this work, we propose how we can extend existing specifications to support new formats. We use the synthesized generators to evaluate different metrics, like their speed, the correctness of the outputs, and the variety of generated files. If we combine our generators with American Fuzzy Lop (AFL), we expect that we can increase the efficiency of AFL in fuzzing programs that parse binary files.

15:00-15:30

Dear All,

the next seminar takes place on 25.11. at 14:00. There is only one session this week.

Session A 14:00-15:00:
Marvin Hoffmann - Huda Dawoud - Tobias Lorig

https://cispa-de.zoom.us/j/95888788125?pwd=ZWRCeGdqRnVRTnpsdnVPQVBiYzg5QT09

Meeting-ID: 958 8878 8125
Kenncode: ^nk14M

Session A:

14:00-14:30 

Speaker: Marvin Hoffmann
Type of talk: Bachelor Intro Talk
Advisor: Alfusainey Jallow, Dr.-Ing. Sven Bugiel
Title: Gamified Crowd-Sourcing the Security Classification of Stack Overflow Code Snippets

Abstract: Stack Overflow is the most widely used forum for developers and IT experts to solve programming issues. Since the answers often contain code snippets solving the problem, prior studies have shown that many snippets are copied and pasted into developer codebases without having a detailed look at it. This behavior causes security breaches in many software products because these code snippets often are insecure. For example, the posted solution could be out of date and not address recent security fixes.
To avoid insecure software, we want to provide a security indication of code snippets posted on Stack Overflow. Therefore, we built the first web-based crowdsourcing platform to gamify the security classification of code snippets. We crawled code snippets from Stackoverflow, grouped them according to the programming language, and display the snippets to security-focused users to classify.
The game allows users to classify snippets into secure or insecure by swiping right or left on our web page. With this, we can offer researchers an alternative way to classify code on Stack Overflow and help developers to write more secure code.

14:30-15:00

Speaker: Huda Dawoud
Type of talk: Master Intro
Advisor: Sven Bugiel
Title: Detecting the Misuse of the Accessibility Service in Mobile Apps
Abstract:
The Accessibility Service is a very powerful service introduced by Google, which provides powerful capabilities to mobile applications such as allowing them to perform clicks on behave of user, retrieve window content, receive key events and many more. In other words, it is a way to override the security design of the Android system, in order to provide capabilities to assist users with disabilities, which is the only goal intended by introducing this service. However, developers do not hesitate to exploit any available services that may help them provide competitive features to users, even if by using them in a manner different from what they were designed for. Google has attempted to crack down on such apps by asking them to explain how they are using the Accessibility Service to help users with disabilities. Otherwise, they will be removed from the Google play. But it seems that Google eventually gave up by the fact that there are a lot of popular applications that use this service for purposes other than helping the disabled users such as Password Managers. This raises a great concern considering the powerful capabilities an app could gain when it convinces the user to enable the Accessibility service for it. Starting from this point, we will try in our thesis to come up with an approach that detect any app tries to misuse the accessibility service.

15:00-15:30

Speaker: Tobias Lorig
Type of talk: Bachelor Thesis Intro Talk
Advisor: Prof. Dr. Andreas Zeller
Title: Fuzzing Binary File Formats with Inputs from Hell

Abstract:

Fuzzing is a form of automated software testing. Inputs with specific properties are fed
into a target program, intended to trigger lines of code in unforeseen ways and provoking
unintended behavior. This may be expressed in the form of bugs, crashes or vulnerabilities.
Generational fuzzing heavily relies on information about the structure of inputs, expected
by the target program. This structure can be formulated as a grammar and then be utilized as
the basis for generating new inputs for fuzzing.

In this thesis a new approach on generational fuzzing is formulated, combining different ideas
from previous technologies, in order to generate context-dependent binary files. Because of the
vast amount of existing file formats and their property to always be highly structured,
binary files are excellent candidates for fuzzing. The proposed tool will be able to
automatically generate grammars of popular file extensions, while implementing all syntactic
and semantic constrains listed in their respective, official file format specifications.
Additionally, a so-called probability distribution is utilized to improve the quality of
generated files by raising the probability of accessing less popular branches and values
during file generation. These may be able to trigger less tested code in the target,
resulting in a higher chance of unexpected behavior.

Dear All,

the next seminar(s) take place on 11.10. at 14:00 or 14:30 respectively, see below.

Session A 14:00-15:00:
Jens Heyens - Annika Caroline Grieser

https://cispa-de.zoom.us/j/94706374076?pwd=WExQVVNmUEdMZG54Um0xbHU2emVBdz09

Meeting-ID: 947 0637 4076
Kenncode: 7J#EiW

Session B 14:30-15:30:
Daniel Emmel - Moritz Wilhelm

https://cispa-de.zoom.us/j/98241395646?pwd=YTNIbDFjYml5K25hOTFFV0V0WjJBQT09

Meeting-ID: 982 4139 5646
Kenncode: 7M?vug

Session A:

14:00-14:30 

Speaker: Jens Heyens    
Type of talk: Bachelor Thesis final 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: Annika Carolin Grieser
Type of talk: Bachelor Thesis Final Talk
Advisor: Dr. Katharina Krombholz
Title: Exploratory evaluation of the methodology of in-situ data collection using a modified Mycroft

Abstract:
 Smart speaker try to ease daily life tasks. However, they carry risks, because they are integrated into our daily lives and are equipped with microphones.
Users are often unaware of these risks and use smart speakers without any privacy precautions.
In-situ studies are a method of obtaining more detailed information on the application of smart speakers, on security precautions and the general usage process.
In contrast to other methods, such as laboratory studies, they offer the advantage of observing user behaviour with smart speakers in the user's everyday environment.
For in-situ studies with smart speakers, data collection is a challenge because the data is sensitive. For ethical reasons, it is inconceivable to record every user conversation.
The presented bachelor thesis conducts an exploratory evaluation of a modified open-source smart speaker called 'Mycroft' to enable targeted data acquisition in in-situ studies with smart speakers.
It contains a tool that allows to intervene in user processes and to collect data, e.g. through surveys.
This bachelor thesis evaluates this tool iteratively regarding its capabilities, possibilities and configurations in the context of security and privacy.
The results reveal that it can be used in many different ways, integrated into a usage scenario including context-specified questions or as a user-controlled functionality asking general questions.
 Furthermore, the tool's questions should be precise and short. During the iterative evaluation of the tool, I solved major user challenges and improved the tool's capabilities.

15:00-15:30

No talk this week.

Session B:

14:00-14:30

14:30-15:00

Speaker: Daniel Emmel
Type of talk: Bachelor Intro Talk
Advisor: Ben Stock
Title: SynthTT: Jamming Client-Side XSS with synthesized TrustedTypes sanitizers

Abstract: With the great importance and popularity of the web to today's world, it is an unfortunate truth that
there exist many malicious entities who try to take advantage of common web vulnerabilites to make profit from damaging innocent users.

One of the most common web vulnerabilites is client-side Cross-site-scripting (XSS), which can occur when a website's code uses
dangerous, DOM modifying sinks with attacker-controllable input. This vulnerability in particular can be devastating to the user,
as it allows an attacker to execute arbitrary Javascript in the authorization context of the user.
One new proposed mitigation is called Trusted Types. Essentially, it follows an allowlist based approach: Each input that a DOM modifying sink
is called with must pass through a Trusted Types sanitizer, where it can be filtered to no longer be problematic.

Though this may seem like a good idea, it raises the immediate challenge that third-party content in the wild will often write a lot
of dynamic HTML, Javascript and URLs into the document via the problematic sinks. Since this usage is however benign, the Trusted Types
sanitizer should allow it, while non-intended sink calls should be prohobited.

In this thesis, I attempt to automate this process by auto-generating sanitizers for third-party content based on their previously observed
benign sink usage behaviour.

15:00-15:30

Speaker: Moritz Wilhelm
Type of talk: Bachelor Intro
Advisor: Ben Stock
Title: Enabling Widespread Deployment of CSP through Retrofitting

Abstract:
As the last decade has shown, the web has won - and with it the countless attackers and scammers who are trying to make a profit by attacking users and website operators around the world.

The most fundamental security mechanism on the web is the same-origin-policy (SOP) which restricts the capabilities of JavaScript. It only allows two websites to access each other via the Document Object Model (DOM) if their origins match. Thus, a malicious script on one website cannot easily steal sensitive user data originating from another website using the DOM.
However, cross-site scripting (XSS) vulnerabilities undoubtedly belong to the biggest threats on the web. These code injection vulnerabilities, typically found within web applications, enable an attacker to bypass the SOP and execute potentially arbitrary code within the current user's context.

The Content Security Policy (CSP) is one of the various mechanisms which try to mitigate XSS attacks. In principle, it attempts to alleviate the effects of such attacks by restricting which resources may be loaded on the website. In particular, this is achieved through specifying allowed scripting resources, either by their URL, via hashes of trusted JavaScript code, or by adding nonces.
Over the years, CSP has undergone several developments and has been continuously expanded with new directives. Nevertheless, not all browsers support all of the newest additions to CSP and fail to integrate them without a significant delay or at all. For this reason, web developers cannot rely on the current standard of CSP. These browser inconsistencies make it very challenging to impossible to create a CSP that reliably behaves in the same way for all users.

In this thesis, I try to tackle these inconsistencies by re-implementing unsupported CSP functionalities dynamically and re-establishing the intended browser behavior on the client-side without having to patch any browsers. Thereby, I try to find out if and to what extent it is possible to retrofit the security on the web without a disproportionate complexity and overhead.

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.

Dear All,

the next seminar(s) take place on 14.10. at 14:00 or 14:30 respectively, as described below.

Update: We consider offering Sessions A and B not in parallel, but after each other (maybe with a 30 minute break) This change will naturally not affect the already planned dates, but would be for the future. This would allow to take part in two sessions in one day, however we want to check, whether this change works with your schedules time-wise, so please fill out the following form:
https://forms.gle/qch5hs86tZFNu5Sc8

Session A takes places 14:30-15:30 just this once:
Priyasha Chatterjee - Matthias Michels

Zoom-Meeting beitreten
https://cispa-de.zoom.us/j/91374615292?pwd=b3pHRVZ2NHRNSlIyc3VIK3BmL2RvUT09

Meeting-ID: 913 7461 5292
Kenncode: 4R#TUW

Session B takes place 14:00-15:30 as usually:
Guido Battiston - Omar Renawi - Robin Ohs

Zoom-Meeting beitreten
https://cispa-de.zoom.us/j/98624092269?pwd=aVg1Rk1yUUYvTnpJNy9yelZVRFBzUT09

Meeting-ID: 986 2409 2269
Kenncode: 3u.euk

Session A:

14:00-14:30 

No talk in this slot this week.

14:30-15:00

Speaker: Priyasha Chatterjee
Type of talk: Master Thesis Intro Talk
Advisor: Prof. Dr. Katharina Krombholz
Title: Usable Privacy Enhancement in the context of Smart Home Systems

Abstract: As ubiquitous computing becomes more widespread, so does the market for voice-controlled smart devices which afford a convenience that did not exist before. Voice control is still developing, but the major players in the market have already made substantial progress, leading to large-scale adoption and interest in voice-controlled technology and particularly in smart home systems. Smart home systems allow smart devices to connect to a hub, such as Amazon's Alexa, or Google Nest, which are essentially smart speakers allowing users to control them by voice. The global smart speaker market is currently worth 7.5bn USD and is projected to grow at 34% per year for the next five years, which means more and more people are going to be adopting the use of these systems and devices. However, while these systems provide users with great convenience, users have also found that they need to settle on a trade-off between security and convenience. Smart speakers are listening constantly and potentially recording sensitive information, which is then at risk of falling into the hands of malicious actors. There is evidence of smart speakers performing unrequested actions that lead to compromise of users' sensitive data, of data from smart speakers being used to triangulate and locate users from these recordings, of companies not being 100% transparent with their policies about such smart speakers. In fact, in 2019, 41% of all smart home users were found to have been apprehensive about privacy around their devices.
While there already exist two commercially available devices to deal with some of these concerns, by allowing users to prevent themselves from being constantly recorded, neither of these have been developed taking users’ ideas into consideration. This thesis proposes to find an effective solution that is designed with the users in mind. The goal is to have a prototype based on recommendations for what is found to be usable by the users. This shall be approached in the following way: the first stage comprises a basic questionnaire and interview, including a drawing task, to ascertain how users feel about the need for privacy enhancement around smart home systems, and to gain some creative insight into what users feel is the most convenient form factor for them. The next stage involves coding and analysing user responses to answer the research questions, and then creating a database of suggested design ideas. These design ideas are then used for the next stage, which is the participatory design stage. Here, the participants brainstorm further, work with low-fidelity prototypes, and provide their valuable inputs. The expected outcome of this stage is the development of refined ideas for usable privacy enhancement tools that can be developed for future use.

15:00-15:30

Speaker: Matthias Michels
Type of talk: Bachelor Thesis Final Talk
Advisor: Ben Stock
Title: Revisiting vulnerability notifications
Abstract:

New security vulnerabilities in websites are discovered daily. One way
to decrease the number of vulnerable websites is to notify the
respective website operator about the issue. However, prior research
has shown that security issues often do not get resolved, even after
sending notifications.

In this thesis, we investigate how the effectivity of such
notifications can be increased. We especially look into how different
incentives affect the number of fixed websites. We do this by
automatically checking over 10 million domains for known security
problems in their websites and notifying their respective operator in
the case we found a vulnerability. By using differently phrased
notifications, we hope to find characteristics, which lead to more
successful notifications.

Session B:

14:00-14:30

Speaker:Guido Battiston
Type of talk:Master Intro Talk
Advisor:Dr. Robert Künnemann
Title:Playing CATSS and MAUS: a theory of privilege escalation and applications to simulated pentesting

Abstract: Companies use risk estimation techniques to analyze their net-
works, prioritize problems and compute mitigation strategies. These
techniques operate on a model of the network, which is acquired by
scanning for known vulnerabilities from public databases. Naturally,
information about the effect of an exploit is scarce, so most models
feature adversaries that advance hop by hop without taking into consideration the security lattice of the individual host.
This master thesis presents the implementation and evaluation of a fully comprehensive system for
network scanning and risk analysis based on host-level privileges, called CATSS/MAUS. Not only
can CATSS/MAUS determine the vulnerability of a network, it can
also propose countermeasures, specifically those that ‘break a chain’
of privilege escalations.

14:30-15:00

Speaker:Omar Renawi
Type of talk: Intro Talk
Advisor: Nico Döttling and Stella Wohnig
Title: The Relationship between Verifiable Delay Function (VDF) And Time-Lock Puzzle (TLP)

Abstract: The question of whether Verifiable Delay Function (VDF) implies Time-Lock Puzzle (TLP) or whether Time-Lock Puzzle implies Verifiable Delay Function has been investigated for a while, but this seems to be a hard problem. In this work, we will investigate this problem further by making stronger assumptions. In particular, we will assume the existence of Witness Encryption and show that Verifiable Delay Function and Witness Encryption imply Time-Lock Puzzle.

15:00-15:30

Speaker: Robin Ohs
Type of talk: Bachelor Final Talk
Advisor: Prof. Dr. Andreas Zeller, Nataniel P. Borges Jr.
Title:Testing apps with probabilisticgrammars

Abstract: In the past, users interacted with applications by typing program
     names with parameters into the command-line or bash. This command
     line apps could easily and systematically be tested by attaching
     different command-line arguments to the call of the program.
     Nowadays the interaction with modern applications is different.
     Instead of command-line arguments, applications create graphical
     user interfaces (GUI) which give users the ability to interact with
     visible elements on their screen via click, hold and swipe or even
     fill out input elements by typing text into them. Specifically,
     applications or operating systems for touch devices in the mobile
     field, like apps for Android make use of this approach.
     Without automation in the testing of an app, an app developer needs
     to write tests for every element of his UI with all its possible
     interactions that a user could use to interact with the application.
     An approach to automate test generating for apps are UI grammars.
     Originally mostly used to test compilers, context-free grammars can
     also be used to create tests for Android applications by mining the
     GUI of the application. In this thesis, the objective is to find a
     way to combine automatically mined grammars for the same application
     and find useful rules which decide how these grammars are getting
     merged.

Dear All,

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

Session A:
Florian Nawrath - Marvin Moog - David Schäfer

https://cispa-de.zoom.us/j/93234867227?pwd=dDFYOEVQbWYxOEM5STAvU1l1UUdJZz09

Meeting-ID: 932 3486 7227
Kenncode: 6H@Tmh

Session B:
Markus Demmel - Andreas Hanuja - Florian Grün

https://cispa-de.zoom.us/j/97895494427?pwd=WHlRUU13dXFFMHFNWkJyaFU0SkFRdz09

Meeting-ID: 978 9549 4427
Kenncode: 2m+1e6

Session A:

14:00-14:30 

Speaker: Florian Nawrath
Type of talk: Bachelorthesis Intro Talk
Advisor: Sven Bugiel
Title: Already logged in or still looking for your password? Quantitative testing of the users FIDO 2 infrastructure

Abstract:
With the release of FIDO 2 (Fast Identity Online) integration of passwordless authentication methods has become easier to use. The general problem is the users acceptance and adaption of this password alternatives. Even when being properly integrated the problem is still the availability of suitable authenticators on the users side. This study aims to unveil the users possibility to make use of FIDO 2 authentication methods, when forced to on an exemplary site. Therefore the goal is to provide insights into technical as well as hardware limitations and restrictions from every-day end users.

14:30-15:00

Speaker: Marvin Moog

Title: Evaluating Adoption and Obstacles of NSC in Android
Kind of talk: Bachelor, final
Advisor: Dr. Sven Bugiel
Abstract:
Nowadays, almost every app needs to be connected to the Internet to serve a useful purpose and therefore has to protect potentially sensitive data during transit. However, several studies in the past have shown that many Android apps are vulnerable to Man-in-the-Middle attacks. In order to simplify the handling of SSL/TLS, and thus increase security, the Network Security Config (NSC) was introduced in Android 7.0, and allows developers to customize their network security settings without modifying the app code.

This bachelor thesis investigates how much the Android market has accepted NSC, if there are obstacles to use it, and whether security has improved as a result, by automatically analyzing the 1,500 most downloaded apps. It highlights that NSC is used by 41.22% of the apps, where every second NSC is used to allow cleartext traffic app-wide. Other security-relevant features of NSC are rarely used and are still frequently implemented manually. A manual analysis of 10 seemingly insecure apps found half of them to have connections that could be MITM attacked.

15:00-15:30

Speaker: David Schäfer
Type of talk: Bachelor Final Talk
Advisor: Dr.-Ing. Sven Bugiel
Title: System Support for Attesting Apps to Services

Abstract:
Already for a long time, mobile applications have become a lucrative business for many companies. Frequently, these just implement basic functionalities and provide the full range of functions only with an active remote service interaction. Particularly in paid apps, it is important for service providers that the information exchanged are only available to certain applications. But, because dynamic authentication is hard to realize in a distributed system, this can be quite challenging. Additionally, because application installation packages can be signed by self-signed certificates and therefore do not provide a chain-of-trust, they can be manipulated and published by everyone. In such a case, it is hard to determine for the remote service whether it is communicating with the genuine application or a compromised version. Therefore, app attestation has become an important concept of today's application development. In this bachelor thesis, I have designed and implemented a system-internal solution for attesting apps to services, which, in contrast to many existing approaches, operates independently from external support. It is based on existing security features of current Android versions and, in combination with hardware-protected security, can provide verifiable and reliable evidence about the integrity of an application and the underlying system.

Session B:

14:00-14:30

Speaker: Markus Demmel
Type of talk: Bachelor Final Talk
Advisor: Rahul Gopinath
Title: Differential Testing

Abstract: We live in a well-connected world in which almost any device is connected to the internet and able to communicate with other devices. This exchange of communication is based on standards like different protocols and data exchange formats. One of these exchange formats is JavaScript Object Notation (JSON). JSON is a popular way to exchange data due to it being very efficient and language independently. That means that any developer can use JSON easily to exchange data with others regardless of the program language or the operating system. The first specification of JSON was published by Douglas Crockford at the beginning of this millennium. Meanwhile, there are several specifications that describe how JSON should be parsed. However, developers do not hold onto these specifications. As a result, there are JSON parsers that parse invalid JSON. This bachelor thesis investigated the consequences of this on the most popular and widespread parsers.

14:30-15:00

Speaker: Andreas Hanuja
Type of talk: Bachelor Thesis Intro Talk
Advisor: Prof. Dr. Andreas Zeller
Title: Generating andParsing Binary File Formats with FormatFuzzer

Abstract:

Modern fuzzers are used worldwide for automated software testing and to regularly find weak points in common programs. Many randomly generated inputs are used to search for errors in the program flow. But if the input files expected by the target program must have a complex structure, it is hardly possible to generate useful input by pure chance.
Thus, current research tries to modify the fuzzer, by giving it background knowledge about the expected input structure.

In contrast to previous proposals, we use a novel framework called FormatFuzzer. FormatFuzzer automatically compiles high-efficiency generators and parsers from a file format specification. In this work, we propose how we can extend existing specifications to support new formats. We use the synthesized generators to evaluate different metrics, like their speed, the correctness of the outputs, and the variety of generated files. If we combine our generators with American Fuzzy Lop (AFL), we expect that we can increase the efficiency of AFL in fuzzing programs that parse binary files.

15:00-15:30

Speaker: Florian Grün
Type of talk: Bachelor Thesis Final Talk
Advisor: Rahul Gopinath
Title: ARM Processor Fuzzing via QEMU

Abstract:

Each processor manufacturer hands out documentation of all usable processor instructions for their specific processor architectures. However, not all possible sequences of instructions are well-defined in those documentations; hence, their execution is undefined. This bachelor thesis describes the implementation of a tool capable of testing a QEMU-emulated ARM architecture. It is used to investigate if there appears any recognizable misbehavior when trying to execute undefined sequences of instructions.
    
To do so, the grammar-based F1 prototype fuzzer, combined with a self-written instruction grammar manually derived from an instruction set description, is used. Being able to create a massive amount of instruction inputs, they are executed on the emulated ARM processor architecture. The target of this fuzzing campaign is a QEMU-emulated ARM Cortex-A9 processor, and it is tested in user as well as in supervisor execution mode.

Dear All,

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

Session A:
Christian Becker - Nils Michael - Nicolas Müller

https://zoom.us/j/96243458340?pwd=WVdzSEJNdmk1Z0JOL2E3UjVZc1EvUT09

Meeting-ID: 962 4345 8340
Kenncode: 7G=Lsi

Session B:
Xhelal Likaj - Tom Fischer

https://zoom.us/j/96804078593?pwd=VnZ1RFoxa1Z3Y2VjSW5rei83aEtiZz09

Meeting-ID: 968 0407 8593
Kenncode: 1f@p*^

Session A:

14:00-14:30 

Speaker: Christian Becker    
Type of talk: Master final talk
Advisor: Dr. Sven Bugiel
Title: Mapping the Multi-Layer Attack Surface of Android’s Native System Libraries

Abstract:

Android is wide spread, and by far the most used operating system for mobile devices.
Providing a wide range of functionality like the calendar, a camera, banking, or messaging
apps these devices store a lot of private sensitive data. Therefore protecting those should
be and is a top priority. Not only the Android Open Source Project (AOSP) but also many
researchers investigated and improved the security. Recent approaches are proposing
solutions in order to protect apps from being compromised, but privacy protection also
relies on the integrity of Android itself, especially of its middleware including Java
(Framework) and native (C/C++ libraries) code. Native code, directly consuming
user input, has been already exploited in the past (e.g. stagefright) which showed the
tremendous impact of vulnerabilities at this point as they can immediately affect every
Android user. However, often users can only pass data to Android’s framework (i.e.
APIs). Therefore the goal of this thesis is to evaluate whether vulnerabilities in native
code can be exploited through passing malicious data to API calls. Due to the range
of functionality Android comes with a huge code base and is a very complex system to
investigate. To overcome this challenge, we present a static analysis tool to automate
and support this investigation. It consists of several exchangeable modules: A pattern
based vulnerability scanner (Joern) for native code, a backwards slicer for native and
Java code and a linker to enable backwards slicing across the Java Native Interface (JNI).
Since apps usually need to access libraries via the Framework, which is implementing the
policy enforcement point and redirecting the calls to the libraries via the JNI, the results
of this tool map the attack surface from native to Java code meaning whenever there is a
bug in native code, it can be derived whether this can be exploited through an API call
from an app and thus poses an actual vulnerability with a high impact. The results can
also be used for fuzzing as it highly reduces the targets by locating the attack surface
and thus increase efficiency

14:30-15:00

Speaker: Nils Michael
Type of talk: Bachelor Thesis Final Talk
Advisor: Prof. Dr. Sven Bugiel
Title:  Exploiting Humans to Create Covert-Channels on Mobile Devices

Abstract:

Covert Channels have been researched both on traditional computing systems as well
as on mobile devices. While for the former there are more than four decades worth
of research including defense mechanisms to prevent data leaks, for the latter these
advancements are still ongoing. More and more attack vectors are being discovered which
make the use of mobile-specific entities like light-sensors or third-party libraries and
SDKs used in mobile apps. With these, there is a vast number of possible channel carriers
used in so called "collusion attacks". These attacks circumvent the Android permission
system and process-isolation without being detected in order to communicate secretly
between two applications with different permissions. That way, the two applications
can unite their respective permissions which are needed to, e.g., leak user data to the
attacker.
For the sensor-based channels, which make the use of different motion sensors (like the
accelerometer or gyroscope as the channel carriers), most related work automates the
process of the covert data transmission through the channels, as the transmission is
independent of user interaction. This thesis focuses on the transmission which is caused
by the user without her knowing, e.g., simply by playing a game. By exploiting the users
for the transmission over covert channels, this will make it even harder to detect. Since
users are error-prone, various aspects like transmission error-detection and -correction
have to be taken into account.

15:00-15:30

Speaker: Nicolas Müller
Type of talk: Bachelor Intro Talk
Advisor: Dr.-Ing. Sven Bugiel
Title: App Piracy in Android

Abstract:
The world of mobile apps is consistently increasing, more and more apps are published in diverse Android app markets. With these increasing stats, apps might get pirated and plagiarism in those markets, especially in unofficial app markets, is often the case. It is also not uncommon that original apps get copied and used to spread most Android malware. Apps get copied with their original functionality, but an attacker might include malicious code and republish those apps to spread the malware. Users often do not recognize those pirated apps and are mostly unaware of a different behavior of the app. Furthermore, commercial apps may get copied and republished for free without the original author's permission to do so, or advertisement of an app might get stripped both shrinking developer's income.
This thesis will study common procedures on how an app is pirated. It will also investigate different defense mechanisms developers include in their apps and how app developers usually try to mitigate piracy and plagiarism of their apps.

Session B:

14:00-14:30

Speaker: Xhelal Likaj
Type of talk: Master thesis final talk
Advisor: Giancarlo Pellegrino
Title: A field study of anti-CSRF countermeasures used in practice

Abstract: Cross-Site Request Forgery (CSRF) is one of the most popular web vulnerabilities, which has been referred by many as the "Sleeping Giant".
It is a severe attack that allows an attacker to trick the victim’s browser into (unintentionally) submitting a request to a vulnerable web application.
Most web frameworks nowadays offer protection(s) against CSRF to ease the efforts of web developers. However, writing secure code is not an easy task.
Although an anti-CSRF countermeasure might be theoretically bulletproof, if it is not implemented correctly in the code, then the security falls apart.
The research question we want to tackle in this work is whether anti-CSRF countermea-sures are implemented in a robust and secure way by frameworks.
A thorough search in the literature indicates a lack of scientific research in this direction. Therefore, through this scientific work, we aim to fill this gap.
Our main contribution is conducting a fieldstudy on the implementation of anti-CSRF countermeasures by popular web frameworks.
In this work, we analyze 44 popular web frameworks of the top 5 programming languages (JS, Python, Java, PHP, C#).
The overall results of the field study showed that the implemented countermeasures are secure from most common attack vectors.
Nevertheless, it also showed that there are some attack vectors that most frameworks overlook, such as cookie tossing, Replay attacks, etc.
In some cases (e.g. Vert.x-Web, CakePHP), a trivial attack was enough to easily bypass the CSRF defense.
Furthermore, we provide a detailed explanation of how anti-CSRF countermeasures work in each framework in an attempt to help developers facing insufficient documentation.
This includes a thorough explanation, a commented source code, and many web appli-cations that can be used to test the CSRF defense further.
We conclude our work by providing some recommendations and best practices that address the implementation mistakes identified during the field study.

14:30-15:00

Speaker: Tom Fischer
Type of talk: Bachelor Thesis Intro 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.

15:00-15:30

Dear All,

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

Please remember to upload your submission info on time (= 1 week in advance, so on Wednesday)! Also, please, if you have multiple advisors who need to attend your talk, please put all of them onto your calendly registration.

Session A:
Marius Smytzek - Florian Grün - Janis Schmitt

https://zoom.us/j/96357406051?pwd=bW52em9CYUNqeG1aeC9razZEb2tVQT09

Meeting-ID: 963 5740 6051
Kenncode: 5p?d!N

Session B:
Aurora Naska - Vladislav Skripniuk

https://zoom.us/j/95417204858?pwd=cmMrSGdKcVk3NFpIZ285bHlka2hOQT09

Meeting-ID: 954 1720 4858
Kenncode: 3a*grG

Session A:

14:00-14:30 

Speaker: Marius Smytzek
Type of talk: Master Thesis intro talk
Advisor: Rahul Gopinath
Title: Mutation-Based Impact Analysis

Abstract:
Evaluating today’s complex software applications is unaccomplishable without effort. The verification of its functional correctness is achievable by testing the software to the extent that the confidence in it is significant enough to establish its overall rightness. The validation regarding stated claims or derived conclusions remains even more troublesome.

In this thesis, I propose a technique to determine the impact of single program components on the eventual result. I consider two program elements as the substantial implementation features: functions and constants. The approach utilizes dynamic mutations activatable at runtime to disable particular components. Combined with the derived outcome, the deviation to the actual result indicates the impact of the disabled element. The awareness of the essential parts of a program provides a better understanding of the origins of the outcomes. Hence, the approach could guide a developer to enhance or expand the program to improve the quality of the results. Moreover, the extracted information provides aids for validating scientific applications based on the derived claims or conclusions by researchers, which would reinforce the quality and correctness of their work.

I evaluate the approach on a diverse collection of interacting program components from a set of real-world programs and show that my approach works in practice.

14:30-15:00

Speaker: Florian Grün
Type of talk: Bachelor Thesis Intro Talk
Advisor: Rahul Gopinath
Title: ARM Processor Fuzzing via QEMU

Abstract:

Each processor manufacturer hands out documentation of all usable processor instructions
for their specific processor architectures. But not all possible sequences
of instructions are well-defined in those documentations, hence the result of their
execution is undefined. In this bachelor thesis, I will implement a tool that is capable
to test a qemu-emulated arm architecture and I will use it to investigate if there
appears any recognizable misbehavior when trying to execute undefined sequences
of instructions.

To do so, the grammar-based F1 prototype fuzzer in combination with a self-written
instruction grammar manually derived from an instruction set description will be
used. This will create a massive amount of instruction inputs that will then be
executed on the emulated ARM processor architecture. The target of this fuzzing
campaign will be a qemu-emulated ARM Cortex-A9 processor and it will be tested
in user as well as in supervisor execution mode.
 

15:00-15:30

Speaker: Janis Schmitt
Type of talk: Bachelor Thesis Final Talk
Advisor: Dr.-Ing. Sven Bugiel
Title: Hardening Android Against UI Deception Attacks

Abstract:

Imagine you want to login to your online banking app on your android phone. You open
your banking app and click on the login button. You enter your credentials, press login
and an error message informs you that the server could not be reached and asks you to
try again. What happened?
A malicious application on your phone was able to detect that the login activity of your
banking app went into foreground and launched a phishing attack by jumping infront
of the original banking app showing you a fake login screen, visually indistinguishable
from the real one. We propose a defence mechanism against this and other UI based
deception attacks without major limitations in user experience.

Session B:

14:00-14:30

Speaker: Aurora Naska
Type of talk: Master thesis intro talk
Advisor: Cas Cremers
Title: Clone detection in secure messaging

Abstract: In this work, we will examine the relationship between strong security guarantees, offered by modern protocols in the event of compromise, and the actual detection of the latter. After the compromise of one of the partners, there are two reasonable requirements from the protocol; to lock the attacker out and to detect its activity. Post-compromise security (PCS), a guarantee of "healing" the communication channel after the compromise, satisfies the first requirement while clone detection satisfies the second one. Motivated by the seem-
ingly complementary nature of the two problems, we are interested in identifying exactly how these two properties and the protocols that achieve them, are related to one another.

We therefore propose an analysis of the two aforementioned security properties and the respective protocols that achieve them, namely protocols that "heal" after a compromise and protocols that detect and approprietly flag the compromise. In the end, we want to show how these security properties are achievable in modern secure messaging protocols.

14:30-15:00

Speaker: Vladislav Skripniuk
Type of talk: Final
Advisor: Prof. Dr. Mario Fritz
Title: Black-box Watermarking for Generative Adversarial Networks

Abstract: As companies start using deep learning to provide value to their customers, the demand for solutions to protect the ownership of trained models becomes evident. Several watermarking approaches have been proposed for protecting discriminative models. However, rapid progress in the task of photorealistic image synthesis, boosted by Generative Adversarial Networks (GANs), raises an urgent need for extending protection to generative models.

We propose the first watermarking solution for GAN models. We leverage steganography techniques to watermark GAN training dataset, transfer the watermark from the dataset to GAN models, and then verify the watermark from generated images. In the experiments, we show that the hidden encoding characteristic of steganography allows preserving generation quality and supports the watermark secrecy against steganalysis attacks. We validate that our watermark verification is robust in wide ranges against several image and model perturbations. Critically, our solution treats GAN models as an independent component: watermark embedding is agnostic to GAN details and watermark verification relies only on accessing the APIs of black-box GANs.

We further extend our watermarking applications to generated image detection and attribution, which delivers a practical potential to facilitate forensics against deep fakes and responsibility tracking of GAN misuse.

15:00-15:30

Dear All,

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

Session A:
Yannick Ramb - Markus Demmel - David Schäfer

https://zoom.us/j/92752645912?pwd=Qy9xNkUwQUY0cTFOVWRVVUxYUkplUT09

Meeting-ID: 927 5264 5912
Kenncode: 4S%N7n

Session B:
Sabine Houy - Yannik Schwindt - Martin Hodapp

https://zoom.us/j/96138694694?pwd=eXdkZTFJNFJOby9DM2o4M3A4QkRUdz09

Meeting-ID: 961 3869 4694
Kenncode: 6y@GYt

Session A:

14:00-14:30 

Speaker: Yannick Ramb
Type of talk: Bachelor Thesis Final Talk
Advisor: Stefan Nürnberger
Title: CAN Traffic Synthesis Algorithms for Automated Deductions

Abstract:
Throughout the years, the importance of automotive cybersecurity in modern vehicles has been gradually increasing. As can be seen in many recent reports, the majority of cyber-attacks against modern vehicles exploit weaknesses in the vehicle’s internal communication network. Nowadays, the Controller Area Network (CAN) bus has become widely accepted as the de facto standard for in-vehicle communication networks. However, while the CAN protocol itself is publicly available, information on the exact data that is sent over the network is not. This is a great burden to research in this field since to detect flaws and vulnerabilities in the system, researchers need to manually reverse engineer CAN data collected from different vehicles. Albeit existing approaches to automate this task, one must manually reverse engineer the CAN data beforehand to develop and evaluate such algorithms. Aiming to address this issue, this thesis presents CANsimu, a tool for simulation of CAN bus networks and automatic generation of CAN data. The data produced by the tool is meant to facilitate development, evaluation and improvement of security analysis algorithms and tools by relieving researchers from performing the tedious and labor-intensive reverse engineering process.

14:30-15:00

Speaker: Markus Demmel
Type of talk: Bachelor Introduction Talk
Advisor: Rahul Gopinath
Title: Differential Testing

Abstract: We live in a well-connected world in which almost any device is connected to the internet and able to communicate with other devices. This exchange of communication is based on standards like different protocols and data exchange formats. One of these exchange formats is JavaScript Object Notation (JSON). JSON is a popular way to exchange data due to it being very efficient and language independently. That means that any developer can use JSON easily to exchange data with others regardless of the program language or the operating system. The first specification of JSON was published by Douglas Crockford at the beginning of this millennium. Meanwhile, there are several specifications that describe how JSON should be parsed. However, these specifications are not unambiguous as they leave some implementation details up to the interpretation of the developers. As a result, there are no two parsers that accept the same language.

This bachelor thesis will investigate the consequences of multiple specifications with room of interpretation on the most popular and widespread parsers. We will use Fuzzing, a technique that uses random text generation to find bugs and unpredictable behavior, to determine if these unambiguous specification result in vulnerabilities by interpreting the given JSON incorrectly.

15:00-15:30

Speaker: David Schäfer
Type of talk: Bachelor Intro Talk
Advisor: Dr.-Ing. Sven Bugiel
Title: System Support for Attesting Apps to Services

Abstract:
Android is the most used mobile operating system in the world, with a numerous amount of applications. Often, these applications use remote services to request or send certain data that needs to be kept confidential. But, attacks like 'Application Repackaging' make it hard for developers to ensure the confidential treatment of data exchange between app and remote service. Because the application installation packages can be signed by self-signed certificates and therefore do not provide a chain-of-trust, they can be manipulated and published by everyone. For a remote service it is hard to determine, if it is currently communicating with the original application or an manipulated version. Therefore, I want to create a system internal solution in this thesis, to provide an attestation of applications to services, which can be used to verify the integrity of an app and prevent data access by unauthorized applications.

Session B:

14:00-14:30

Speaker: Sabine Houy
Type of talk: Final Talk

Advisor: Matthias Fassl
Supervisor: Katharina Krombholz
Title:Comparing User Perceptions of Anti-Spyware
Apps with the Technical Reality

Abstract:
Nowadays we store an increasing amount of sensitive data like text
messages, contacts, pictures, etc. on our mobile phones. This data is
a prominent target, not only for outsiders but especially for people in
our immediate social environment, such as partners and family. These
so-called insiders are often not considered in threat models. This thesis
aims to evaluate how e ective these apps are regarding their detection ca-
pabilities and how trustworthy they appear to users. Thus, I will reverse
engineer two prominent anti-spyware applications available on the Google
PlayStore to identify their detection techniques. I will then apply qual-
itative data analysis on the reviews to compare the users' perception of
e ectiveness with the technical reality obtained through reverse engineer-
ing. The results show that both applications are capable of identifying
installed spyware applications with varying degrees of accuracy in terms
of the information provided about the detected spyware. Furthermore,
most users feel safer with anti-spyware apps and trust them, which is
appropriate in terms of technical evaluation.

14:30-15:00

Speaker: Yannik Schwindt
Type of talk: Bachelor Introductory Talk
Advisor: Jenny Rau
Title: Extending DroidMate-2 with phash state identification

Abstract:
Automated Testing is important for app developers to ensure that their apps work properly. Increasing complexity of applications leads to the need of more efficient testing platforms. A common problem for automated test engines like DroidMate-2 is recognizing already seen states
while modeling the GUI of the app under test. This decreases the efficiency since already seen states are examined as new.
In this Bachelor thesis I will try to tackle the state duplication problem by introducing phash identification to the DroidMate exploration engine and check if states are perceptually equal.

15:00-15:30

Speaker: Martin Hodapp
Type of talk: Introduction Talk
Advisor: Katharina Krombholz
Title: Should I post or should I not?

Abstract: The meaning of privacy is more and more important in all fields of our daily life. Many researchers investigated how end-user and developer try to protect their privacy and private information. Also the behavior of online user was invastigated in many papers. Most of these works focused on the technical implemantation of cryptography, data transmission and storage but not really how users see possible effects of their online behavior (for themselfe or associated people or even their employer). This work address the question, how people out of system critical public services, see or notice effects from what they post, comment or like in social media. In particular how notice german soldiers risks, impacts or threats for their comrades and the employer (the deutsche Bundeswehr) in respect to their behavior.

Dear All,

the next seminar(s) take place on 5.8. at 14:00.
As a reminder: If you hold a talk you have to upload your information one week in advance which means on *Wednesday* before the talk.

Session A:
Annika Carolin Grieser - Finn Hermeling - Johannes Lampel

https://zoom.us/j/95592194795?pwd=MUpKZHFoU0RUM05ZMjZUNldjUUJGQT09

Meeting-ID: 955 9219 4795
Kenncode: 0s^udk

Session B:
Daniel Weber - Noah Mauthe - Niklas Medinger

https://zoom.us/j/93291128233?pwd=UTJhU05PbXRhWmU0MWlXZDZEYk5EQT09

Meeting-ID: 932 9112 8233
Kenncode: 2z^GF+

Session A:

14:00-14:30 

Speaker: Annika Carolin Grieser

Title: Exploratory evaluation of a methodology of in-situ data collection using a modified Mycroft

Kind of Talk: Bachelor Thesis Intro Talk

Advisor: Dr. Katharina Krombholz

Abstract:

Artificial Intelligence is almost everywhere included in daily life. You can ask smart
speakers to do some shopping for you, to control smart homes or even to tell you some
news. This technique not only brings advantages but also carries some risks. Several
studies have shown possible attacks and privacy lacks of these devices. In-situ studies are
often conducted, to shed light on user behaviour in this context. The data collection is a
challenge for each in-situ study. It becomes even harder in smart speaker in-situ studies.
The huge challenge is the sensitivity of the data. Logging every user conversation is
inconceivable for ethical reasons. Other methodologies are not satisfactory either because
they have disadvantages such as a large time gap between usage and survey or the need
to artificially intervene in the in-situ process.
The presented Bachelor thesis performs an exploratory evaluation of a new tool which
should ease the data collection process in an in-situ study with a smart speaker. This
tool is integrated in an open-source smart speaker called ’Mycroft’. It offers the ability of
surveying the user in between his usage process with the smart speaker. The goal of this
thesis is to evaluate this tool with respect to its abilities, capabilities and configurations
in a security and privacy context.

14:30-15:00

Speaker: Finn Hermeling
Type of talk: Bachelor Thesis Outro Talk
Advisor: Stefan Nürnberger
Title: Automated Semantic Labeling For Unstructured And Unknown CAN Traffic

Abstract:
In automotive networking the Controller Area Network (CAN) standard is widely used. Car manufacturers use secret protocols to let devices communicate over this bus. Since all devices (including infotainment systems or telematic units) are physically connected to the same bus, attack vectors are being exposed and privacy concerns raised. In order to estimate the gravity of the situation and to solve these problems, it is necessary to reveal the obscure contents of CAN messages. The thesis will discuss challenges an automated labeling system for data in CAN messages faces and analyze the possibilities to solve them using machine learning. In this talk different aspects of solving these challenges are shown and various approaches evaluated and compared using both qualitative and quantitative methods.

15:00-15:30

Speaker: Johannes Lampel
Type of talk: Master Inro
Advisor: Sascha Just
Supervisor: Andreas Zeller
Title: Run Flake Run

Abstract:
Flaky tests and their manifestation in intermittent failures plaque the continuous integration process in small and large projects alike. In big companies like Google or Microsoft, the manifestation of an intermittent failure is especially costly since it causes builds, which can take several hours, to fail. To combat this problem, research and industry have come up with several approaches. Reruns, meaning a failing test is automatically rerun when it fails, are most commonly used in big companies today. In this talk, I will talk about our ideas on how we want to investigate the effectiveness of reruns in combatting intermittent failures, as well as ideas on how to make reruns more effective.

Session B:

14:00-14:30

Speaker: Daniel Weber
Type of talk: Bachelor Introduction
Advisor: Ahmad Ibrahim
Title:
Using Fuzzing to Identify x86 Leak Sequences for Timing Side Channels

Abstract:
In 2017 Meltdown and Spectre showed that we must not rely on the assumption that computer hardware is without vulnerabilities. Since then we saw various other attacks against CPU microarchitectures. These so-called transient execution attacks often rely on a covert or side channel to make microarchitectural state observable from the architectural world.

While mainly the CPU cache is abused as a side channel in such attacks, we are aware of the existence of other side channels.
Each new channel is a new way for adversaries to hide their traces and mitigate existing work to detect and prevent transient execution attacks. Therefore, identifying side channels is a key element to reliably defend against their exploitation.
To aid the ultimate goal of mitigating the threat coming from such attacks, this work tries to find
more microarchitectural side channels in an automated manner.
We develop a fuzzer that instead of testing a software component directly fuzzes the hardware it is running on.
Our fuzzer will execute various combinations of instructions from the x86 ISA and observe the behavior of these
with the ultimate goal of finding instructions that span novel timing side channels.

14:30-15:00

Speaker: Noah Mauthe
Type of talk: Bachelor Thesis final talk
Advisor: Ulf Kargén, Christian Rossow
Title:Studying the Prevalence of Anti-Decompilation Techniques in Malicious and Benign Android Applications

Abstract:

Android applications are comparatively easy to reverse engineer and are thus often
plagiarized. To protect against this threat, recent years have seen an overall increase
in obfuscation deployment in the Android ecosystem as well as numerous studies on
the subject. As most of these studies target obfuscation techniques that harden an
app against manual analysis, but not against decompilation per se, we investigate the
prevalence of anti-decompilation measures in Android applications in its current state
by employing decompilability as a proxy. By analyzing, respectively, commercial, open-
source and malware applications, we provide a comprehensive overview on the subject.
We discovered noticeable differences in decompilation failure rates between the three data
sources. Specifically, we note an increase in failure rates from open-source to commercial
and from commercial to malware applications. Nevertheless, our findings show an
unexpectedly small discrepancy in decompilability for all three datasets, warranting
further investigation in future work.

15:00-15:30

Speaker: Niklas Medinger

Title: Exploring Automatic Lemma Generation for the Tamarin Prover
Thesis Type: Bachelor Thesis
Talk Type: Intro Talk
Supervisor: Cas Cremers
Abstract:

Security protocols are all around us. Their applications range from securing the messages
we sent via Apps to protecting the passwords 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.
Since the desired security properties are often not automatically provable by the
tool, a major part of this process involves the step-wise refinement of intermediate
statements that, ultimately, imply the desired security properties. Aiming to cut down
the time and manual work needed to formally verify a protocol, this thesis identifies
common patterns in lemmas needed to verify protocols with the Tamarin prover, develops
an algorithm to automatically generate these lemmas, and evaluates its effect on the
time needed to prove the security properties of protocols.