News
Next Seminar on 8.12.2021
Written on 06.12.2021 11:51 by Stella Wohnig
Dear All,
The next seminar(s) take place on 8.12. at 14:00.
Session A: (RA3,5)
Jannis Rautenstrauch - Peter Stolz - Alaeddine Abroug
https://cispa-de.zoom.us/j/96786205841?pwd=M3FOQ3dSczRabDNLb3F1czVXVUpvdz09
Meeting-ID: 967 8620 5841
Kenncode: BT!u5=
Session B: (RA 2,4)
Stanimir Iglev - Tim Speicher - Yavor Ivanov
https://cispa-de.zoom.us/j/99025989421?pwd=cWJIM29LYktsbStxTXlKUStZRi9MUT09
Meeting-ID: 990 2598 9421
Kenncode: 3mZyE$
Session A:
14:00-14:30
Speaker: Jannis Rautenstrauch
Type of talk: Master Final
Advisor: Dr. Ben Stock, Dr. Giancarlo Pellegrino
Title: XS-Leaks - How affected are browsers and the web?
Research Area: RA5: Empirical and Behavioural Security
Abstract: Cyberattacks causing considerable damages to businesses and users are in the news almost every week. Cross-Site information leaks (XS-Leaks) are one type of web attack targeting users. In such attacks, victims visit a malicious website that infers information about them on other sites by abusing browser side-channels. Inferred information can reach from access detection to deanonymization. The scientific community has known XS-Leaks since the 2000s. Still, there is not enough information available to estimate how big of an issue such attacks are for the web ecosystem today.
This thesis aims to close this knowledge gap with two approaches. One approach is evaluating how different browser side-channels behave in modern web browsers by observing several channels for 387,072 responses. The other approach is scanning as many websites as possible for vulnerable URLs using a newly created fully automated pipeline.
The results show that browser behavior significantly differs. Studying the differences, we discovered ten security-relevant bugs and reported them to two browser vendors. With the does-it-leak pipeline, we detected vulnerable URLs on 258 out of 352 tested sites, presenting the largest study of XS-Leaks to date.
Based on the results of this thesis, we conclude that XS-Leaks pose a considerable problem for the web ecosystem, as most websites are currently vulnerable, and millions of users could be heavily affected. However, the results also show that websites have the means to be XS-Leak-free and that getting rid of differing edge case behavior in browsers could reduce the attack surface by about 50%.
14:30-15:00
Speaker: Peter Stolz
Type of talk: Bachelor Final
Advisor: Dr. Ben Stock
Title: To hash or not to hash: Asecurity assessment of the CSP directive unsafe-hashes
Research Area: RA3|5
Abstract: Content Security Policy (CSP) is a great way to mitigate Cross-site scripting (XSS) if used correctly. CSP has the experimental directive "unsafe-hashes" to whitelist certain inline event handlers and style attributes.
Before browsers add support for it we analysed how many event handlers can be abused to trigger XSS if an attacker reuses them on a malicious tag.
We built an analysis pipeline using dynamic analysis with taint tracking and forced execution to find flows from the attacker controlled tag to dangerous functions.
This allowed us to determine if it is a useful feature or if it should be abandoned because it implies a false sense of security for the most part.
We found 0.06% of distinct handlers to have dangerous flows among the Alexa Top 1000 and through manual analysis verfified their exploitability.
As only a low portion of event handlers contain such issues we conclude that unsafe-hashes is an easily adaptable method to harden a website against XSS and it can be used in a process to a robust CSP.
15:00-15:30
Speaker: Alaeddine Abroug
Type of talk: Intro Bachelor
Advisor: Dr. Michael Schwarz
Title: Automated Reverse Engineering of LLC Addressing
Research Area: RA3
Abstract:
Caches have proven themselves as an integral component when in the design of high performance processors. Modern cache architectures provide a multi-level structure, where the Last Level Cache (L3) is further subdivided into cache slices. Those slices are shared and distributed among all cores in multi-core processors. Each slice is assigned a fraction of the address space for load balancing. A side effect of this performance optimization is that it made cache side-channel attacks across cores more complex. As the mapping from addresses to slices is undocumented, attacks cannot simply target specific cache parts. In this bachelor thesis, we implement a fully automated methodology to reverse engineer this undocumented mapping function. Reverse engineering the address-to-slice mapping function is key to constructing reliable cache-eviction sets in a fast way. Based on our reverse engineering, we show the first Prime+Probe attack on SGX on 6-core CPUs. Due to the non-linearity of the mapping function for these CPUs, such attacks were previously not possible.
Session B:
14:00-14:30
Speaker: Stanimir Iglev
Type of talk: Bachelor Intro
Advisors: Björn Mathis, Leon Bettscheider
Supervisor: Prof. Dr. Andreas Zeller
Title: Transpiling Schema Languages to Grammars
Research Area: RA4
Abstract:
Testing programs, which expect highly-structured inputs, has proven to be a challenging problem. Grammar-based fuzzing is a promising approach to address this issue. The idea behind it is to enhance the fuzzer with a grammar, which describes the input language of the program under test, and use it to produce syntactically valid inputs. However, due to the diversity of data format languages, it is hard to construct a universal grammar representation which is able to express the variety of restrictions that are applicable to the inputs.
As a result, fuzzers are very often tailored to work with a specific format or application and use a representation of grammar that is designed to function effectively with the targeted data format. This creates a layer of incompatibility between different fuzzer implementations. We present an approach to reduce this problem by creating a set of transpilers for the conversion of input specifications. More precisely, we convert schema documents to grammars.
Schema languages are very often used to define the structure and later validate the data accepted by programs. These languages allow the developers to assert that the input data satisfies certain conditions, thus they specify exactly what constitutes valid inputs. Most well-established data formats provide such schema vocabularies. By translating these input specifications into grammars, we can use them not only for input validation, but also for input generation. Hence, we believe that being able to convert different input languages to a single grammar format will enhance already existing fuzzers and provide a strong candidate for a unified grammar representation.
We propose a set of transpilers which make use of these schema documents to generate an input grammar for the program under test. Our tools are able to translate the constraints described by the schema, to production rules in the resulting grammar by utilizing an intermediate tree representation. We focus our attention on the two most widely used data interchange formats and their schema languages, namely JSON Schema and W3C XML Schema Definition Language (XSD).
We plan to evaluate the correctness and viability of our tools against real-world applications with the intention to guarantee that they can be used to enhance fuzzers and aid developers in finding defects in their programs. In order to assess the correctness of produced grammars, we perform a set of checks, which ensure that all symbols are defined and reachable from the start symbol. Furthermore, we evaluate the validity of documents, produced by generated grammars. To do so, we enhance a fuzzer with such a grammar and generate a vast amount of documents, which are then validated against the original input schema. Moreover, we conduct a comparative analysis between a fuzzer, augmented with a grammar generated by our tools, and other fuzzers. Our plan is to run them against a set of real-world applications and track metrics such as code coverage and depth of explored paths.
We believe that the proposed tools can be powerful instruments for the generation of complex test inputs and that they belong in the arsenal of every software tester. To the best of our knowledge, we present a novel way to translate input specifications into grammars for the production of highly-structured inputs.
14:30-15:00
Speaker: Tim Speicher
Type of talk: Bachelor Intro
Supervisor: Prof. Zeller
Advisor: Rafael Dutra
Title: Targeted Fuzzing using FormatFuzzer
Research Area: RA4
Abstract:
One big limitation of most modern fuzzer is the lack of controllability in terms of where and what exactly they are fuzzing. In many cases you want to focus the fuzzing on a small part of the hole functionalty, instead of testing all at once. Most modern fuzzer cannot distinguish between lower and higher prioritized fuzzing targets.
The goal of this thesis is to implement a mechanism to support targeted fuzzing, to concentrate the fuzzing on especially definded targets. We will implement this strategy in the FormatFuzzer, which is a structure-aware fuzzing tool. Having a specification for a file format in this case a binary template, the Format Fuzzer can be used as generator as well as parser and mutator for files of this format. When parsing a file, it produces a parse tree, which defines an order and hierachy of chunks in the file. Chunks in this context is generally spoken to refer to any struct or variable of the binary template. Format Fuzzer can mutate each chunk individually, without changing the rest of the file. This can be used to concentrate the fuzzing on chunks, that are related to our target of fuzzing.
15:00-15:30
Speaker: Yavor Ivanov
Type of talk: Bachelor Introduction
Advisor: Dr. Robert Künnemann, Kevin Morio
Title: Existential lemmas in Tamarin: towards more efficient sanity checks
Research Area: RA2
Abstract: Tamarin is a symbolic verification tool for security protocols. It can be used to
automatically prove that a protocol fulfills certain security properties specified as lemmas.
The majority of protocol models also contain lemmas that check if a protocol is executable.
Tamarin is optimized for proving security properties, which affects the constraint-reduction steps,
the selection heuristics used, and the traversal order of the proof tree.
Consequently, the resolution of sanity checks is not as efficient as it could be.
This work’s goal is to increase the efficiency with which sanity checks are performed.
We propose a solution consisting of three components: a modification of Tamarin’s
constraint-reduction steps, an optimization of the utilized heuristics, and using sequential
DFS as the default proof tree traversal strategy. Afterwards, we are going to evaluate each
of the new features with the help of a script to determine if they produce a substantial
performance increase.