Curriculum Vitae

Marcus Völp
Technische Universität Dresden
Department of Computer Science
Institute for System Architecture
D-01062 Dresden

Phone: +49 (0)351 / 463 - 38350
Email: voelp@os.inf.tu-dresden.de
Homepage: http://os.inf.tu-dresden.de/~voelp

Personal Information

Family status: married
Country of birth:  Germany
Place of birth: Frankfurt
Date of birth: 18th April 1977

Objectives

My research interests focus on various aspects of building and verifying microkernel-based systems. Examples include energy awareness, information-flow security and real-time scheduling for mixed-criticality settings. Recently I also had a look into the verification of cyber-physical systems. Currently, I'm looking into alternative system designs for highly heterogeneous processor architectures. Our goal is to develop a profound understanding of kernel-less operating systems and of the hardware and software requirements to use these kernels in wildly heterogeneous processor architectures. Two of the building blocks of this work are elastic representations of workloads and the interplay between enlightened runtimes and system-wide schedulers to exploit latent parallelism inside applications.

Outline of Scientific Career

since 2012 Research Group Leader of the ESF young researcher group IMData at the Technische Universität Dresden
10/2013 - 04/2014 Post Doctoral Research Scholar at the Logical Systems Lab of Prof. Andre Platzer at the Carnegie Mellon University, Pittsburgh, USA
since 02/2011 Postdoc at the Technische Universität Dresden
Operating Systems Research Group,
08/2003 - 01/2011 PhD student at the Technische Universität Dresden
Operating Systems Research Group,
Advisor: Prof. Hermann Härtig.
2006 Internship with Prof. Bart Jacob's
Digital Security Group at the Radboud Universiteit Nijemegen
Nijmegen, the Netherlands
2005 Internship with Prof. Chan-Ik Park's
System Software Lab at the Pohang Technical University (PosTech),
Pohang, Korea
2003 Internship with the
Advanced Systems Technology Group of
ST Microelectronics Rousset, France
2001 Internship: Extreme Blue
IBM Research and Development in Boeblingen, Germany
04/2000 - 02/2003 Research student and teaching assistant with the
System Architecture Group
Universitaet Karlsruhe, Germany
1999 Internship with the
SW Speech Technology Group
IBM Research in Heidelberg, Germany
10/1997 - 02/2003 Diploma in Computer Science
Universität Karlsruhe (TH), Germany

Scientific Activities

Journal Reviews: The Computer Journal (Oxford Journals) 2012
International Journal of Information Security 2012
Secondary Reviewer for Prof. Härtig: SOSP, EuroSys, Usenix ATC, RTSS, RTAS, ECRTS, ESORICS, VEE, OSPERT, OPODIS

Teachning Experience

I'm currently giving an introductory course on cyber-physical systems design and verification. The course material (to the degree it is ready) can be found here: http://www.inf.tu-dresden.de/index.php?node_id=3682&ln=en. During my Diploma and PhD studies, I contributed to the basic and advanced operating system courses at Universität Karlsruhe and at Technische Universität Dresden. Below is a list of lectures I gave in the advanced operating-systems courses for master and diploma students.

  • Microkernel Construction:
    • "Mechanisms for Privilege Transfer and Revocation"
  • Distributed Operating Systems:
    • "Synchronization in Parallel Systems"
    • "Security: Foundations, Security Policies, Capabilities"
  • Real-Time Systems:
    • "Hardware"
    • "Hard Real-Time Multiprocessor Scheduling"
  • Advanced Systems Programming:
    • "C++ Types, Pointer, Pointer Arithmetic"

Prior Research

PostDoc - Technische Universität Dresden

Before I joined IMData, I worked with Marcus Hähnel on energy utility functions (EUF) and on utility accrual scheduling. Our approach focuses on determining operation modes of hardware components. We found modes to dominate the energy consumption of these components. Resource utility functions propagate low-level energy characteristics to higher-level components of the hardware / software stack. Our RAPL-based short time energy sampling approach received a best student paper award and is currently used by two other projects in HAEC. In the joint DFG project QuaOS between Prof. Baier, Prof. Härtig and Dr. Tews, I contributed to a new verification approach for quantitative properties for low-level operating-system code. This approach combines probabilistic model checking with a controlled measurement-based analysis, which determines the necessary model parameters.

PhD Studies - Technische Universität Dresden

My PhD studies focused on provable data confidentiality in microkernels and microkernel-based systems. During these studies, I developed a specialized security type system for low-level operating-system code and a non-interference secure scheduler. The role of the parametric type system is to identify possible information channels in low-level system primitives. Combined with the kernel-level isolation mechanisms and a consequent re-instantiation of servers for differently classified subsystems, this type system can be used to formally confirm the system's confidentiality guarantees. The scheduler and an accompanying resource locking protocol improve this isolation by provably avoiding scheduling-related timing channels. Both the scheduler and the locking protocol preserve the real-time guarantees of the system.

While working on my PhD, I assisted in the day-to-day operation of the EU project ROBIN and joined an activity of Prof. Bart Jacobs' group in Nijmegen to formally verify a module of the NOVA microhypervisor. During this work, I developed precise formal memory models for x86 processor architectures. The models consider virtual aliasing and side-effects induced by memory-mapped devices. For these models, I have proven a formal result stating when memory behaves as expected. I also participated in the development of a C++ semantics and an accompanying rewriting system, which is able to automatically simplify fractions of C++ code that contain no or only trivial loops. Immediately after joining the Operating-Systems Group of Technische Universität Dresden, I contributed to the design and implementation of the L4.Sec microkernel and co-supervised Bernhard Kauer's diploma thesis on this topic.

Internship ST Microelectronics

During my internship at the Advanced Systems Technology Group of ST Microelectronics I worked on hardware security enhancements, which resulted in four hardware patents about a new processor architecture concept (asymmetric multi-context machines) and three new security extensions for multiprocessor systems (secure bootstrapping, memory bus encryption and memory access control). All four patents have been accepted in France / Europe as well as in the US.

Diploma Studies - Universität Karlsruhe

During my diploma studies, I contributed to the design and implementation of an L4-family microkernel for small- scale multiprocessor systems. I also worked with Dr. Kevin Elphinstone and Prof. Jochen Liedkte on algorithms and bandwidth-reservation schemes for coordinating access to the memory busses of real-time multiprocessor systems.

Interests

I enjoy exploring interesting scientific and technological phenomena with kids in the kindergarten. Some of the topics we explored are: "How to make chocolate?", "Sets and fractions - math with Haribo and cakes.", "How to make paper?", "Bending light" (with Prof. Eng), "Animated movies: stop motion and motion capture films.", and a brief introduction into quarks and the early stages of the universe to answer a question by one of the kids: "Why are stars made out of gas?". Jumping on a big trampoline and practicing rope-skipping tricks are real fun as are some of the good old adventure games. Best of all is of course having fun with my own kids.