Publications de Johannes Kinder

High System-Code Security with Low Overhead

Jonas Benedict Wagner, George Candea, Volodymyr Kuznetsov, Johannes Kinder

Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like ...

2015

Prototyping Symbolic Execution Engines for Interpreted Languages

George Candea, Stefan Bucur, Johannes Kinder

Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monume ...

ACM2014

Advantageous State Merging During Symbolic Analysis

George Candea, Stefan Bucur, Volodymyr Kuznetsov, Johannes Kinder

A determination is made regarding whether to merge two symbolic analysis states. A first state corresponds to a first path through a program to a program location and a second state corresponds to a second path through the program to the program location. ...

2013

Automated Debugging for Arbitrarily Long Executions

George Candea, Cristian Zamfir, Baris Can Cengiz Kasikci, Johannes Kinder, Edouard Bugnion

One of the most energy-draining and frustrating parts of software development is playing detective with elusive bugs. In this paper we argue that automated post-mortem debugging of failures is feasible for real, in-production systems with no runtime record ...

2013

Making Automated Testing of Cloud Applications an Integral Component of PaaS

George Candea, Stefan Bucur, Johannes Kinder

Traditional testing is inadequate for the complexity of modern cloud application software stacks. While the platform-as-a-service (PaaS) model has streamlined application development and deployment, its multiple abstraction layers and dependencies have mad ...

2013

Towards Static Analysis of Virtualization-Obfuscated Binaries

Johannes Kinder

Virtualization-obfuscation protects a program from manual or automated analysis by compiling it into bytecode for a randomized virtual architecture and attaching a corresponding interpreter. Static analysis appears to be helpless on such programs, where on ...

IEEE2012

Efficient State Merging in Symbolic Execution

George Candea, Stefan Bucur, Volodymyr Kuznetsov, Johannes Kinder

Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the num ...

ACM2012

Alternating Control Flow Reconstruction

Johannes Kinder

Unresolved indirect branch instructions are a major obstacle for statically reconstructing a control flow graph (CFG) from machine code. If static analysis cannot compute a precise set of possible targets for a branch, the necessary conservative over-appro ...

Springer2012

Efficient State Merging in Symbolic Execution

George Candea, Stefan Bucur, Volodymyr Kuznetsov, Johannes Kinder

Symbolic execution has proven to be a practical technique for building automated test case generation and bug finding tools. Nevertheless, due to state explosion, these tools still struggle to achieve scalability. Given a program, one way to reduce the num ...

Assoc Computing Machinery2012

Supporting Domain-Specific State Space Reductions through Local Partial-Order Reduction

Johannes Kinder

IEEE2011