David von Oheimb's Computer Science Curriculum Vitae

In the 1980s and '90s, departing from the very basics, I got up-to-speed with the overall IT development, which can be summarized as:

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

First encounter with electronics, in particular logic circuits, on a children's summer camp.
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.
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.
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.
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

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.
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.
Working at the staff unit of an air force 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

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.
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.
After successfully passing the intermediate tests, I finally could deepen my knowledge in my favorite 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.)
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.
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

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.
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 supervisor, mainly people from England) and analyzing other related work stimulated progress.
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.
As a second large work package 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.
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.
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

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.
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+.
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 successor of the SLE 66. I also did some fundamental research on information flow.
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.
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.
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 (w.r.t. security) part of the German health card system.
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.
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.
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, then Siemens VDO) to implement a secure software upgrade module for an embedded system.
At work, I was mostly busy with the third and final year of AVANTSSAR and contributing to the development of the software upgrade module mentioned above. I also spent quite some time on private IT projects, developing a HyperText Bible, fixing a couple of notorious bugs in Thunderbird and Lightning, and getting some familiarity with Android 2.2 and geolocation using GPS. With my HTC Desire featuring a wonderful AMOLED display, I'm meanwhile back to pocket computers - just some 300 times faster and with a million times higher memory capacity than in 1984 :-)
After pretty annoying and time-consuming experience with various regressions and the immature Unity desktop of Ubuntu Linux 11.04, I allowed myself a MacBook Air, and for pragmatic reasons also got a cheap Windows 7 netbook. This certainly opened new horizons for me and made some things simpler, but on the other hand it cost me quite some effort to unify the user interfaces (e.g., keyboard shortcuts) of the three operating systems to allow for their seamless promiscuous use.
Since early 2011 and well into 2013 my work at Siemens was mostly part of AVANTSSAR's successor project SPaCIoS, which aimed at security testing based on various formal methods. I focused on improving and extending the Java implementation of the ASLan++ translator, which - similarly to the other AVANTSSAR Tools, unfortunately were never really finished, and only unofficially released.
As part of SPaCIoS, I spent together with two colleagues some effort into research and a related prospective publication enhancing non-interference for state-oriented systems, yet this starved on resources. I was glad that instead my contributions to practical industrial security rose.

Practical IT security at industry

Since 2011, I had been working on system architecture as well as implementation and certification support for the security of smart metering systems, but also for toll system onboard units and SCADA (i.e., production information and control) systems.
In spring I started working on a new major project: a client-server application prototype used to enroll identity certificates of field devices, based on the EST protocol, designed and implemented mostly by Cisco.
[Valid HTML5] URL: http://ddvo.net/cv.html Last modified: Fri Jul 31 20:07:37 CEST 2015