Portrait of Johannes Kinder

Johannes Kinder

Senior Lecturer

Room 104, McCrea Building
E-Mail: first.last at rhul.ac.uk
Office phone: +44-1784-27-6549
Office hours: Mon 14:00–15:00, Fri 13:00–14:00

Research Interest

My research focuses on assessing and improving the reliability and security of software, in particular with the help of automated tools. This requires me to cross back and forth between the fields of programming languages, software engineering, and systems security. My principal interests lie in program analysis for real-world systems, runtime monitoring and instrumentation, and specification and detection of malware.

At Royal Holloway, I am affiliated with the Systems Security Research Lab and the Centre for Software Language Engineering.

Prospective PhD Students

I am looking for motivated and talented PhD students to work with me in the area of program analysis and security. My work is a mix of mathematical reasoning about programs and applied systems hacking – so ideally you should enjoy doing both. If you are interested, please write me an e-mail with your CV and a few lines about yourself. Currently open positions are advertised under vacancies, but additional funding opportunities can be found.

Program Committees

I am / have been serving on the program committees of the following conferences and workshops.

ESSoS 2017, SPRO 2016, RV 2016, PPREW-5, ESSoS 2016 (PC member and Doctoral Symposium Chair), SPRO 2015, SAS 2014, ICST 2014, PPREW-4, EUC 2014, ICST 2013, PPREW 2013, EDCC 2012, SOFSEM 2012, SEW 2012, SEW 2011

I am lucky to be working with the following PhD students:

MobSec: Malware and Security in the Mobile Age

Sponsored by UK EPSRC (EP/L022710/1) and a donation from Intel Security (formerly McAfee Labs UK).

A main theme of the project will be mobile applications analyses to extract behavioural information necessary for effective policy enforcement and mobile malware mitigation techniques. To this end, we have recently presented CopperDroid, an approach to perform dynamic behavioral analysis of Android malware. CopperDroid presents a unified analysis to characterize low-level OS-specific and high-level Android-specific behaviors. A number of research questions including the automatic, comprehensive, and faithful reconstruction of Android apps behaviors, the reliable identification of behaviors triggered by malware embedded in benign applications, event-behavior attributions, and the simulation of complex UI interactions are still open and will be explored by MobSec.

We will further focus on detection of malicious mobile applications a particularly challenging task in the mobile landscape that largely sees malware repackaged (and embedded) in benign apps, and the enforcement of fine-grained security policies to contain malicious behaviors—abstracting away (or limiting) users involvement (as opposed to the state-of- the-art). Hardware-supported virtualization to provide efficient in-device mitigations against mobile threats.

Symbolic Execution for Test Generation and Bug Finding

Symbolic execution runs a program with symbolic instead of concrete inputs. Using an automated constraint solver, a symbolic execution engine can check, one path at a time, whether an input exists that could violate an assertion. The exponential number of paths in real-world programs is a fundamental problem limiting the effectiveness of symbolic execution. By dynamically merging paths, we were able to cover orders of magnitude more paths on the GNU Coreutils (using the Cloud 9 engine). Future testing targets include cloud application stacks, which require special care to disentangle the multiple parsing and processing layers.

Jakstab: Static Analysis of x86 Executables

Jakstab allows to statically analyze binaries directly, without relying on any preprocessing. It integrates disassembly, control flow graph reconstruction, and abstract interpretation in a single process. Jakstab was successfully used to verify Windows device driver binaries and generate control flow graphs for Windows and Linux binaries. Because it avoids making assumptions about well-behavedness of code, its particularly good at working with unconventional and hand-written machine code. In ongoing work, Jakstab is being extended to remove obfuscation layers from malware by static analysis. Jakstab is open source and designed to be extensible by custom analysis and binary frontends. Check it out on jakstab.org.

Behavioral Malware Detection

Simple and fast static matching of malware signatures is no longer able to cope with the rapid release cycles of malware and the large number of malware variants generated by construction kits. The Mocca malware detector is built on a model checking algorithm that verifies the control flow graphs of binaries against a behavioral malware specification given in the custom temporal logic CTPL. A single specification can then match and thus detect an entire family of malware.

By Train

The fastest way from central London is to take the Waterloo - Reading train and get off at Egham (37 min from Waterloo). Look up connections from anywhere in London.

From Egham station, you can either walk (20 min), take the shuttle bus (10 min, during term time), or take a taxi (5 min). Click here for a detailed map.

By Car

The college is two miles from Junction 13 of the M25. You can enter campus through the main gate at Founder's Building, but you will need to have a space reserved for you since parking is by permit only.

By Plane

The nearest airport to Royal Holloway is is London Heathrow. You can take a Taxi from there to reach campus in about 15 min, or take bus 71 from Terminal 5 or bus 441 from Heathrow Central Bus Station (30-40 min).

From London Gatwick, the fastest route is to take the train to Clapham Junction and change to a Waterloo-Reading train to Egham (about 1h10 total travel time).