David von Oheimb's Computer Science Curriculum Vitae

Area	From	To
CPUs	8-bit microprocessors	32-bit SPARC/x86
Operating systems	Basic proprietary OSs	Unix and derivatives
Programming languages	Machine code	Functional & object-orientated
Debugging	Single-stepping the CPU	Formal program verification
Application software	Numeric calculations	Theorem provers

Early experience: pocket computers

1981

First encounter with electronics, in particular logic circuits, on a children's summer camp

1984

My personal IT career began with an innocent programmable pocket calculator, which I used for facilitating basic gliding performance calculations for model airplanes. Within a week I realized that I needed a more powerful computing device, which, according to my pupil's budget, was a Sharp PC-1401 pocket computer, programmable with BASIC.

1985

Soon I gained more interest in the implementation rather than application of this machine and started learning the machine language of its exotic 8-bit microprocessor. I hand-coded my own disassembler and analyzed parts of its operating system and the BASIC interpreter.

1986

Having earned some money with a summer job, I bought a Sharp PC-1600, featuring much more hardware and software power. Having learnt how to deal with its Zilog Z80 microprocessor, I disassembled and analyzed large chunks of its 96KB ROM and developed my own disassembler, macro assembler, and debugger.

1987

When I started selling this software via a users' magazine, my skills were discovered by a HW&SW distributor and publisher focusing on pocket computers. I got contracted with this (one-man) firm to author a system programmer's manual and develop a text-processor for the PC-1600.

Maturing to state-of-the art computing: home and personal computers

1988

Meanwhile, I could afford letting a dream come true: Using the most enhanced home computer of that time, the Commodore Amiga 2000. On this machine I got to know higher-level system programming with C and state-of-the art multitasking system software. Except for a RAM disk driver and some (frustrating) experiments with neuronal network simulations, I did not develop - or even sell - serious software.

1989

Having heard of the INMOS Transputer, I was fascinated by this promising approach and even considered developing system software for the excellent distributed operating system Helios by Perihelion Software. I had already reverse-engineered the kernel of this system (reporting several bugs to its developers), but unfortunately there was general sobering about the Transputer hype, and I also ran out of time as I meanwhile had finished school and my military service began.

1990

Working at the staff unit of an airforce base, I was given the nice opportunity to exercise my computer hobby by writing software keeping track of the pilots' training flights. I must, though, admit that this program became quite a mess, written on a PC with dBase, and I'm not sure if they actually could make good use of it.

The academic approach: workstations and global networks

1991

In this year I began studying Computer Science at the nearest university known for its good education in this area: The TU München. Though the rather high-level teaching there suited my interests and capabilities for mathematics and technology, in particular the math courses in the first two years were quite challenging, but it was worth it.

1992

In the Ferienakademie ('holiday academy', a kind of summer school) of our university in Sarntal (South Tyrol), I encountered the charm of high-level (functional and logic) programming. Somehow connected to this event, I was invited to begin a student job at Prof. Broy's chair. There, among other things, I was introduced to LaTeX and making use of the Internet.

1993

After successfully passing the intermediate tests, I finally could deepen my knowledge in my favourite subjects: the theory of programming languages as an application of discrete mathematics, in particular semantics and logics, but also more technical issues like advanced concepts of operating systems and distributed computing. On the other hand, I also became interested in relating computer science with humane discipline, namely through computational linguistics. (Later, it turned out that I had too high expectations on the maturity of this field, and thus I abandoned it.)

1994

I was lucky to take part in the Ferienakademie again, this time in a course on distributed algorithms and computing. In that year I got to know Prof. Tobias Nipkow and his research assistants working on their interactive theorem prover Isabelle. I was inspired to familiarize with this system and did a major a student project with it: RALL, a proof system for abstract relation algebra, which I had the privilege to publish on the CADE conference later.

1995

As an excursion to the distributed systems track, I did a verification case study with Isabelle for the FOCUS framework as a student job. At the same time I made further use of my Isabelle expertise, developing a datatype package within HOLCF as my master thesis.

My doctoral thesis: developing and applying theory of programming languages

1996

Even before finishing my CS diploma that year, I was invited by Prof. Nipkow to join his new project Bali analyzing Java with Isabelle, which I gladly accepted.

1997

I first investigated the security-related issue of type-safety for the Java language. For this endeavor to become a success, I had to put together all my experience on programming language design and semantics, implementation techniques, formal logic, software engineering, and project management. Of course, also discussions with colleagues (apart from my supervisior, mainly people from England) and analyzing other related work stimulated progress.

1998

This year was dominated by publications of the results obtained by then, giving talks on conferences, seminars and workshops, and writing papers, for example contributing to a survey on Java research. I also took part in some teaching efforts, giving courses on Java to both fresh students and mature maths teachers.

1999

As a second large workpackage within project Bali, I developed a Hoare logic for Java, where handling side-effecting expressions and planning the (meta-level) soundness and completeness proofs were the main challenges. Besides the project work, I also took part (as a staff member) in the NATO summer school in Marktoberdorf, that year focusing on foundations of secure computation.

2000

After finishing my work on the Hoare logic, this year was governed by writing up my PhD thesis. I finished it exactly at the end of my fourth year of employment as a research assistant. In the autumn I took part in the Ferienakademie the third time, this time as a tutor.

2001

In February, just about two months after submitting my thesis, I had the final (oral) exam, and immediately after this the official PhD party. By the summer, I finished my research work at TUM.

Industrial research and consulting: formal methods applied to IT security

2001

When looking for a new field of activity that should be both important for our society and challenging to me, I decided to enter IT security. Siemens Corporate Technology offered me a good position as a ``Research Scientist''. This security department there offers security analysis, consulting and specialized solution development to both Siemens-internal and external customers.

2002

Working on a formal security analysis project, I developed the Interacting State Machines (ISMs) formalism for modeling and verifying reactive systems, which has been used e.g. for certifying the Infineon SLE 66 smart card processor according to Common Criteria EAL 5+.

2003

In this year, among others, I extended the ISM formalism and applied it analyzing the complex RBAC of a medical information system by Siemens Healthcare and the memory management system of the Infineon SLE 88, in this way contributing to the EAL 5+ certification of this 32-bit successsor of the SLE 66. I also did some fundamental research on information flow.

2004

Having gained more experience with Siemens projects, when our team was re-constructed, I obtained the project management for the Siemens part of the EU project AVISPA: Automated Validation of Internet Security Protocols and Applications, and a security analysis project for the Boeing Electronic Distribution of Software (BEDS), and consequently was promoted to a Senior Research Scientist. I also became secretary of the ForTIA: Formal Techniques Industrial Association. Concerning the verification techniques used, my focus changed from interactive theorem proving to automatic model checking.

2005

I gave talks and tutorials at various occasions on my specific field of activity, formal security analysis. Still having good contacts with academia, I even got a university teaching mandate at both Munich universities to give a lecture on this subject. Moreover, I was proud to be part in the very successful closing of the project AVISPA and assisted in two further EU IST FET Open proposals, including the immediate successor to AVISPA.

2006

I gave two invited talks about formal security analysis in industry, though my focus was gradually shifted to security architecture consulting and certification according to the Common Criteria. I spent a very pleasant and productive month at Boeing Research & Technology in Bellevue near Seattle, examined security architecture alternatives of a digital tachograph, and provided support for evaluating (wrt. security) part of the German health card system.

2007

I continued working on the security of the digital tachograph and our projects with Boeing, contributing to three publications with them and spending again more than a month in the Seattle area.

2008

I became the Siemens site leader of the newly started EU project AVANTSSAR: Automated VAlidatioN of Trust and Security of Service-oriented ARchitectures and continued serving as a programme committee member of various IT security related workshops like the ACM SAC Security Track and Open Source Software Certification.

2009

On the scientific side, I co-designed the AVANTSSAR Specification Language (ASLan). On the business side, I did major contributions to the acquisition and execution of an order by Continental Automotive (formerly VDO) to implement a secure software upgrade module for an embedded system.