EASTEND focuses on the idea that an inherently dynamic language is best served by a dynamic approach to verification. We therefore chose to use test generation by dynamic symbolic execution (DSE) to systematically cover paths through programs and check security properties along those paths. The two main lines of work were to improve DSE for real-world JavaScript code and to develop a flexible specification methodology for security properties.
The MobSec project explores research questions around the automatic, comprehensive, and faithful reconstruction of Android app behaviors, the reliable identification of behaviors triggered by malware embedded in benign applications, event-behavior attributions, and the simulation of complex UI interactions.
The goal of this project is to develop methods for assessing the impact of insecure JavaScript interfaces in Webviews: while many functions exposed through such interfaces are harmless, some can allow an attacker to obtain or manipulate sensitive information, or even to load additional privilege escalation exploits.
The idea of automated exploit generation (AEG) systems promises to democratize the art of exploit writing. An AEG system can demonstrate the severity of a bug by generating a working targeted exploit, which takes control of the program and executes a payload, such as spawning a shell.
The goal of DEMISEC is to develop techniques for automatic vetting of open source repositories, in particular for detecting implants of malicious code in source code. We will use a mix of static and dynamic techniques to achieve this goal: fuzzing or symbolic execution for differential testing of program versions, and modeling of implant code to detect dangerous patterns in code repositories using static analysis.
This project aims at gaining fundamental insights into representing high-level semantics of binary code in a way resembling human understanding of programs. Resulting models can be used to reconstruct source-level information in binaries and to find code that performs similar tasks on an abstract level.
This project focuses on defining new types of semantics for speculative execution and related micro-architectural features, built on insights from formal methods for concurrency and weak memory models. We develop a new framework based on bounded model checking to validate attacks and defenses with respect to speculative semantics.
The ForDaySec research network employs an interdisciplinary approach towards protecting everyday digitization. Our subproject aims to reliably close vulnerabilities in firmware even without manufacturer support. Based on published vulnerabilities in certain versions of open source packages, patterns are to be generated so that they can then be found directly in a firmware binary. A tailor-made patch should then be created for these vulnerabilities and applied directly to the binary file in a minimally invasive manner.
EASTEND: Efficient Automatic Security Testing for Dynamic Languages
