My Personal Page: Jan Tobias Mühlberg

contact | brief | publications | projects | friends | archive | disclaimer

Me/Contact current occupation: Postdoc at KU Leuven, DistriNet Research Group, SecureChange, STREWS and TENSE projects previously: senior staff scientist at the University of Bamberg, Software Technologies Research Group; Ph.D. student at the University of York, PLASMA Research Group; researcher at the University of Applied Sciences in Brandenburg e-mail: jtmuehlberg@gmail.com, jantobias.muehlberg@cs.kuleuven.be pgp-key: muehlber.asc; available on public keyservers keyid: 1024D/5BC905EC 2002-03-20 fingerprint: 9DC9 9968 98D5 3673 5C57 A98B 930B AF48 5BC9 05EC GitHub: https://github.com/muehlber LinkedIn: http://uk.linkedin.com/pub/jan-tobias-muehlberg/6/2A0/754 Facebook: http://www.facebook.com/jtmuehlberg further contact information is available here and here. Interests My work and research interests are in software security and formal verification and validation of software systems, specifically in the field of embedded systems and low-level operating system components. I am particularly interested in security architectures for safety-critical embedded systems and for the Internet of Things. Currently I am exploring use-cases for embedded Protected Module Architectures and formal verification techniques that allow the secure deployment and use of distributed event-driven software components. Further fields of my interest cover abstraction techniques, model checking, decision procedures and embedded systems design, focusing on synchronous languages, correctness proofs and the application of automated (formal) testing techniques. Keywords/Computer Science: software engineering, software security, automated software verification, model checking, semantics of programming languages, reactive and synchronous programming languages, reactive control systems, real time systems, industrial control systems, automotive computing, program analysis and program abstraction, SMT solving, separation logic, memory models and heap abstraction, analysis of object code programs, security protocols, cryptography Biology/Entomology: I'm lacking the time to do much but I'm interested in the biology of beetles, specifically Chrysomelidae and Silphidae. Hobbies: far too many -- I'm changing them from time to time

"Nach dem Aufstand des 17. Juni Ließ der Sekretär des Schriftstellerverbandes In der Stalinallee Flugblätter verteilen Auf denen zu lesen war, daß das Volk Das Vertrauen der Regierung verscherzt habe Und es nur noch durch verdoppelte Arbeit Zurückerobern könne. Wäre es da Nicht einfacher, die Regierung Löste das Volk auf und Wählte ein anderes?" -- Bertolt Brecht, "Die Lösung"

In brief: Research and Teaching

• Publications on DBLP, ACM, Google (there's a full list including technical reports and talks below)
• Topics for final year projects:
  • Static Verification of Sancus Modules
  • Verified FreeRTOS: Case Studies in Software Verification
  • Probing Unknown Malware Infrastructures with Binary Analysis
  • Incremental Clustering of Unknown Malware using Network Behaviours
  • Learning Dynamic Data Structures from Compiled Programs
  • Further Information -- get in touch if you are interested in one of these topics or if you have your own idea for a thesis that is related to my research.
• Demonstrating and Teaching at KU Leuven:
  • Secure Software Development (Ontwikkeling van veilige software, OVS)
  • Object-Oriented Programming (Objectgericht programmeren, OGP)
  • Software Design (Software-ontwerp, SWOP)

Papers, Presentations, Essays, etc.

• coming soon:       "Securing Distributed Embedded Computing With a Minimal TCB" -- Jan Tobias Mühlberg (joint work with Job Noorman, Jo Van Bulck and Frank Piessens); 15th International Conference on Software QA and Testing on Embedded Systems (QA&TEST 2016): abstract
• "POSTER: Identifying Dynamic Data Structures in Malware" -- Thomas Rupprecht, Xi Chen, David H. White, Jan Tobias Mühlberg, Herbert Bos and Gerald Lüttgen; CCS 2016: pdf, bibtex
• "Security guarantees for the execution infrastructure of software applications" -- Frank Piessens, Dominique Devriese, Jan Tobias Mühlberg and Raoul Strackx; SecDev 2016: pdf, bibtex
• "Nuevos desafíos en el Software Embedded" -- Jan Tobias Mühlberg and Silvia Nuñez. Written for tecnonews.info: es-pdf, en-pdf
• "An Implementation of a High Assurance Smart Meter using Protected Module Architectures -- Jan Tobias Mühlberg, Sara Cleemput, Mustafa A. Mustafa, Jo Van Bulck, Bart Preneel, Frank Piessens; WISTP 2016: pdf, bibtex, supplements
• "Towards Safe Enclaves" -- Neline van Ginkel, Raoul Strackx, Jan Tobias Mühlberg, Frank Piessens; HotSpot 2016: pdf, bibtex
• "Towards Availability and Real-Time Guarantees for Protected Module Architectures" -- Jo Van Bulck, Job Noorman, Jan Tobias Mühlberg, Frank Piessens; MASS 2016: pdf, bibtex
• "Verifying Linked-List Programs and Beyond" -- Jan Tobias Mühlberg; DSI/dsOli Day in Bamberg, Germany, 2016-01-15: abstract, slides, Workshop Programme
• "Lightweight and flexible trust assessment modules for the Internet of Things" -- Jan Tobias Mühlberg (joint work with Job Noorman and Frank Piessens); 14th International Conference on Software QA and Testing on Embedded Systems (QA&TEST 2015): slides, Conference Programme
• "Learning assertions to verify linked-list programs" -- Jan Tobias Mühlberg, David White, Mike Dodds, Gerald Lüttgen and Frank Piessens; SEFM 2015: pdf, slides, bibtex, 10.1007/978-3-319-22969-0_3
• "Lightweight and flexible trust assessment modules for the Internet of Things" -- Jan Tobias Mühlberg, Job Noorman and Frank Piessens; ESORICS 2015: pdf, slides, bibtex, supplements, 10.1007/978-3-319-24174-6_26
• "Secure resource sharing for embedded protected module architectures" -- Jo Van Bulck, Job Noorman, Jan Tobias Mühlberg and Frank Piessens; WISTP 2015: pdf, bibtex, supplements, 10.1007/978-3-319-24018-3_5
• "Software Verification with VeriFast: Industrial Case Studies" -- Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs and Frank Piessens; Science of Computer Programming ( SCP): pdf, bibtex, 10.1016/j.scico.2013.01.006
• "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; International Journal on Software Tools for Technology Transfer (STTT): pdf, bibtex, 10.1007/s10009-012-0256-8
• "HyperForce: Hypervisor-enForced Execution of Security-Critical Code" -- Francesco Gadaleta, Nick Nikiforakis, Jan Tobias Mühlberg and Wouter Joosen; IFIP International Information Security and Privacy Conference (IFIP SEC 2012): pdf bibtex, 10.1007/978-3-642-30436-1_11
• "Sound Formal Verification of Linux's USB BP Keyboard Driver" -- Willem Penninckx and Jan Tobias Mühlberg and Jan Smans, Bart Jacobs and Frank Piessens; NASA Formal Methods Symposium (NFM 2012): pdf, bibtex, 10.1007/978-3-642-28891-3_21
• "D6.6: Development-Time and On-Device Interplay" -- Arnaud Fontaine, Olga Gadyatskaya, Frank Piessens, Isabelle Simplot-Ryl, Jan Tobias Mühlberg, Fabio Massacci, Anton Phillipov, Pedro Capelastegui, Bart Jacobs and Pieter Philippaerts; SecureChange public project deliverable, March 2012: pdf, bibtex
• "Hello rootKitty: A lightweight invariance-enforcing framework" -- A video by Francesco Gadaleta, Nick Nikiforakis and Jan Tobias Mühlberg. We show a Linux kernel being compromised by installing malicious package that contains a rootkit. Then we show how "hello rootkitty" detects the attack and silently repairs the compromised kernel. Background is explained in a paper (10.1007/978-3-642-24861-0_15) by Francesco Gadaleta, Nick Nikiforakis, Yves Younan and Wouter Joosen
• "Combining Formal Methods and Testing: A Case Study on FreeRTOS" -- Jan Tobias Mühlberg, joint work with Leo Freitas; talk at the 10th International Conference on Software QA and Testing on Embedded Systems (QA&Test 2011) in Bilbao: abstract, pdf, bibtex, Conference Programme
• "Verifying FreeRTOS: from requirements to binary code" -- Jan Tobias Mühlberg and Leo Freitas; short paper for the International Workshop on Automated Verification of Critical Systems 2011 (AVoCS 2011): pdf, bibtex, slides
• "Orchestrating Security and System Engineering for Evolving Systems" -- Fabio Massacci and Fabrice Bouquet and Elizabeta Fourneret and Jan Jürjens and Mass Soldal Lund and Sebastien Madelenat and Jan Tobias Mühlberg and Federica Paci and Stephane Paul and Frank Piessens and Bjornar Solhaug and Sven Wenzel; Invited paper at ServiceWave 2011: pdf, bibtex, 10.1007/978-3-642-24755-2_12
• "Verifying Compiled File System Code" -- Jan Tobias Mühlberg and Gerald Lüttgen; Formal Aspects of Computing -- Applicable Formal Methods (FACJ): pdf, bibtex, 10.1007/s00165-011-0198-z
• "Squeezing Wine" -- A very short guide on how to upgrade your wine installation on Debian-Squeeze: html
• "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; 17th International SPIN Workshop on Model Checking of Software (SPIN 2010), 27th to 29th September 2010: paper (pdf), bibtex, slides (pdf), 10.1007/978-3-642-16164-3_2
• "Model Checking Pointer Safety in Compiled Programs" -- Jan Tobias Mühlberg; PhD Thesis, Department of Computer Science, University of York, September 2009: thesis (pdf), bibtex, also available at whiterose.ac.uk.
• "Parallelization of Decision Procedures" -- Alexander Ditter and Jan Tobias Mühlberg; D-CON 2010, Introduction to a discussion session on parallel SMT solving, University of Bamberg, 04th March 2010: abstract (txt), slides (pdf)
• "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; Technical Report 85/2010, Faculty of Information Systems and Applied Computer Sciences, The University of Bamberg, February 2010: paper (pdf), bibtex, also available at opus-bayern.de.
• "Symbolic Object Code Analysis" -- Jan Tobias Mühlberg and Gerald Lüttgen; Monday Afternoon Club, University of Bamberg (MAC 2009/2010); 25th January 2010: slides (pdf)
• "Wie bleibt unser Geheimnis geheim?" -- Jan Tobias Mühlberg, slides for a workshop on cryptography for girls at the age of 10 to 14 ("Mädchen und Technik"), University of Bamberg, November 4th 2009: abstract (txt), slides (pdf)
• "Verifying Compiled File System Code" -- Jan Tobias Mühlberg and Gerald Lüttgen; Brazilian Symposium on Formal Methods (SBMF 2009); 21st August 2009: paper (pdf), bibtex, slides (pdf), 10.1007/978-3-642-10452-7_21
• "Model-Checking the Linux Virtual File System" -- Andy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg and Radu Siminiceanu; Verification, Model Checking, and Abstract Interpretation (VMCAI 2009); January 2009: paper (pdf), bibtex, additional material, 10.1007/978-3-540-93900-9_10
• "Is Your Program Memory Safe? -- Can we use bounded model checking to find memory safety violations in compiled programs?" -- Thesis Seminar given on 10th July 2008 in York: slides (pdf)
• "Slicing Object Code -- and finding memory safety violations" -- talk given at a PLASMA seminar in York on 28th February 2008 and in a Theory-Seminar in Birmingham on 29th February 2008: slides (pdf), abstract
• scade2brick -- I'm back to playing with Lego and SCADE, and hence there's a new release of scade2brick. It's supporting rotation sensors now: website
• "Model Checking Linux's Virtual File System" -- talk on the report below, given at the Workshop on the Verifiable File Store Mini-Challenge (part of Grand Challenge 6: Dependable Systems Evolution), 18th December 2007, BCS HQ, London: slides (pdf)
  I gave this talk a second time in the HISE-seminar on 04th March 2008 in York
• "Model-checking Part of a Linux File System" -- Andy Galloway, Jan Tobias Mühlberg, Radu Siminiceanu and Gerald Lüttgen; Technical Report YCS-2007-423, Department of Computer Science, University of York, UK, November 2007: paper (pdf), bibtex, additional material
• "Proceedings of the 1st York Doctoral Symposium on Computing" -- Jan Tobias Mühlberg and Juan Ignacio Perna (editors), Technical Report YCS-2007-421, Department of Computer Science, University of York, UK, October 2007: proceedings (pdf), bibtex
• "FUN with Lego Mindstorms" -- PLASMA talk given together with Matthew Naylor on 01 March 2007: slides (pdf), abstract.
  Matthew wrote a nice paper on "Behavioural Circuit Design in Lava" which covers the second part of this talk in detail. It's published in issue 7 of The Monad.Reader. Just the article: paper (pdf)
• "Studie zum Innovationsverhalten deutscher Software-Entwicklungsunternehmen" -- A study commissioned by the Federal Ministry of Education and Research of Germany, December 2006, authored by Friedrich-L. Holl, Katharina Menzel, Peter Morcinek, Jan Tobias Mühlberg, Ingo Schäfer and Hanno Schüngel: book (pdf), bibtex
• "Metastudie Open-Source-Software und ihre Bedeutung für Innovatives Handeln" -- A study commissioned by the Federal Ministry of Education and Research of Germany, December 2006, authored by Hartmut Heinrich, Friedrich Holl, Katharina Menzel, Jan Tobias Mühlberg, Ingo Schäfer and Hanno Schüngel: book (pdf), bibtex
• scade2brick -- Prepare C code generated by SCADE for compilation with brickOS: website
• "BLASTing Linux Code" -- a paper and related material for FMICS 2006, co-authored by Gerald Lüttgen: additional material, pdf, slides, bibtex, 10.1007/978-3-540-70952-7_14
• "Software-Engineering und Software-Qualität in Open-Source-Projekten" published in Open Source Jahrbuch 2006: pdf bibtex

Projects/Activities

• Sancus -- a protected module architecture for networked embedded devices
• VeriFast -- a sound verifier for C and Java programs
• SecureChange -- techniques and tools that ensure "lifelong" compliance to evolving security, privacy and dependability requirements for long-running evolving software systems
• Förderverein Großtrappenschutz e.V. -- unfortunately I can't spend as much time in environmental protection as I would like to

Friends, nice people, random links

• Los Comandantes -- You've to put on a barett with a red star for their concerts!
• Nick Nikiforakis
• Francesco Gadaleta

contact | brief | publications | projects | friends | archive | disclaimer