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 doctorate: 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. In my spare time I provided major improvements to the Thunderbird add-on Duplicate Contacts Manager.
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.

Industrial and open-source IT security development

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 for enrolling certificates of field devices, based on the protocol EST and its implementation by Cisco, called libEST.
Early that year I submitted to Cisco a large chunk of source code containing major improvements and extensions of libEST. For the rest of the year we struggled to get these and some further contriubtions reviewed and accepted by this open-source — but not open-minded — project, with little success.
Partly out of our bad experience with contributing to libEST, but mostly because we found that the more flexible Certificate Management Protocol actually fits our needs better, we moved on to CMP. I started improving and extending CMP for OpenSSL, an implementation by Nokia. I also did minor contributions to the OpenSC project to their PKCS#11 tool.
My contributions to CMPforOpenSSL turned out to take quite much effort, too, but this time it was very fruitful because Martin Peylo, the initiator and maintainer of that open-source project, proved very open to substantial improvements. Related to that activity I started in August actively contributing to the OpenSSL project.
In April we officially (re-)started an upstream contribution of CMP to OpenSSL. To this end we had moved the project to GitHub and submitted the first pull request in late July. After initial feedback we split the contribution in twelve chunks, which we have been contributing since them.
In my spare time I extended and open-sourced my little GPX track converter tool GPXConv and started directly contributing to the Pannellum open-source panorama viewer project. I also revived the Thunderbird add-on Duplicate Contacts Manager on my own repository because the original developers were not reachable any more.
That year I pushed forward the contribution of CMP to OpenSSL, which worked out slowly but steadily. I also made and published major extension to a CMP client implementation for embedded systems with the help of a working student and made the Duplicate Contacts Manager compatible with Thunderbird version 68+.
In January I was invited to become an OpenSSL Committer. This was very helpful in getting the remaining chunks of the CMP contribution included in time — the last chunk was merged in min-June. It also motivated and enabled me to do many more general improvements to OpenSSL, not only regarding certificate handling.
In September, finally OpenSSL 3.0 was released, including the CMP implementation and many other improvements of mine, for instance on the HTTP client. Over the years before I had developed also a high-level API for it, called generic CMP Client, as well as a convenience layer for OpenSSL certificate management etc. called Security Utilities, both of which were open-sourced around the same time.
For several years we had been working on the Lightweight CMP Profile and related standardization documents regarding CMP. This year we were able to get it through the IETF Working Group Last Call. We also continued working on a draft of BRSKI-AE, for which I had taken editorship.
I started developing SolBatSim, a precise simulation for photovoltaic systems optionally including energy storage.
In November, finally the Lightweight CMP Profile and related documents became RFCs, and during this year we continued pushing support of the new CMP features defined there to OpenSSL. For the whole year we were working also on a self-contained version of CMP Updates, called RFC4210bis, where we added support for KEM keys. I mostly finished developing SolBatSim.
[Valid HTML5] URL: https://ddvo.net/cv.html,  created in 1999, Last modified: Sat Jun 15 17:49:57 CEST 2024