Publications
Identifying attackers by using machine
learning on unstructured cyber threat
intelligence
Using cyber threat intelligence in automated processing systems requires structured data as input. Cyber threat intelligence on the Internet, however, often appears as unstructured cyber threat reports (CTRs) written by cyber security researchers. Such CTRs often, without knowing the actual adversary behind an attack, contain information regarding techniques and tools applied by the adversary during the execution of the attack. Due to their lack of structure, CTRs are difficult to work with and information must be manually extracted. In this work, we developed a machine learning based tool that helps identifying the adversary having executed the attack described by a CTR.
Personal Research, Switzerland (2020)
A formal semantics for Viper
The Verification Infrastructure for Permission-based Reasoning (Viper) is a suite of tools developed by the Chair of Programming Methodology research group at ETH Zurich. Viper includes an intermediate language which is based on a flexible permission model and aims to allow for simple encodings of permission-based reasoning techniques implemented in front-end tools such as Chalice. As of today, the intermediate language of Viper lacks a formal semantics. Thus, encodings of front-end languages into Viper cannot formally be reasoned about and the verification of a program encoded into Viper cannot rigorously be argued to be sound with respect to the semantics of the front-end tool language. This thesis presents the first formal semantics for a chosen subset of Viper. Moreover, an encoding [_] of a subset of Chalice into Viper is defined and proven sound: if an encoded Chalice program [p] verifies with respect to the semantics of Viper then p verifies with respect to the semantics of Chalice.
Master Thesis, ETH Zurich (2016)
Perfect forward secrecy with PACE
This report describes the iterative development of the PACE protocol. The starting point is a simple challenge-response protocol and the final refinement leads to PACE, a protocol satisfying perfect forward secrecy for a session key as well as mutual agreement for the parties on the session key.
Semester Project, ETH Zurich (2016)
Register allocation based on
chordality of SSA-form program
interference graphs
This report describes the structure, implementation and performance evaluation of a non-iterative register allocator making use of program properties induced by the Static-Single-Assignment (SSA) form. Most salient, SSA renders a programs interference graph chordal. Since chordal graphs are a subset of perfect graphs and perfect graphs can be recognized and optimally colored in polynomial time, allocating registers for programs in SSA form can be optimally done in polynomial time. Together with the possibility to destroy SSA in a color-preserving manner, those properties allow to diverge from the classical iterative register allocation process, as exploited in our implementation and described in this report.
Semester Project, ETH Zurich (2014)
Recursively enumerable sets and
undecidable problems
This seminar handout explains fundamental questions in complexity theory in terms of recursion theory. The handout was a contribution to a seminar that focused on mathematical ideas and philosophical questions at the interface of logic and computer science.
Seminar Handout, ETH Zurich (2014)
SSA based flow-sensitive points-to
analysis via value flow graph
reachability using binary decision
diagrams
In 2011, Oracle Labs Australia Researchers Cristina Cifuentes et al. presented a flow-sensitive points-to analysis algorithm that, as a novelty at this time, reduced the analysis to a graph reachability problem. Performance evaluations conducted indicated that this new reduction can lead to significant runtime improvements over previously established methods. However, it was also found that for some benchmarks the space requirements of the new algorithm can be up to an order of magnitude higher. In this thesis we implemented the algorithm presented by Cifuentes into LLVM and investigated the effect on the algorithms space and time requirements when C++ STL sets are replaced by Binary Decision Diagrams as representations of the points-to sets involved. We found that by using Binary Decision Diagrams, the algorithm experiences a runtime slowdown of 27.3% while the space requirements can be reduced up to 65.6% for large enough benchmarks.
Bachelor Thesis, ETH Zurich (2014)
Three paradoxes of infinity with
explanations
These essays investigate the seemingly paradoxical nature of three questions arising from mathematical notions of infinity. The essays were a contribution to a seminar that focused on notions of infinity in philosophy, mathematics, logic and physics.
Seminar Essays, ETH Zurich (2012)