Room: 12-528

Tel: +49 631 205 4785

E-Mail: johannes.mueller(at)rptu.de

GitHub: https://github.com/kangoojim/

Courses:

• Embedded Systems Laboratory (Labor Digitaltechnik II)

Research Interests:

I am currently researching in the fields hardware security and formal methods. My interests include in particular:

• Microarchitectural timing side-channels
• Compositional HW/FW security verification
• Formal security verification in complex system-on-chips (SoCs)

Publications:

• A. Duque Antón, J. Müller, P. Schmitz, T. Jauch, A. Wezel, L. Deutschmann, M. R. Fadiheh, D. Stoffel, and W. Kunz, “VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL”, ACM/IEEE International Conference on Computer Aided Design (ICCAD'24), 2024 (to be published)
   
• J. Müller, A. Duque Antón, L. Deutschmann, D. Mehmedagić, C. Rodrigues, D. Oliveira, K. Devarajegowda, M. R. Fadiheh, S. Pinto, D. Stoffel, and W. Kunz, “MCU-Wide Timing Side Channels and Their Detection”, 61th IEEE/ACM Design Automation Conference (DAC'24), San Francisco, June 2024
   
• A. Duque Antón, J. Müller, L. Deutschmann, M. R. Fadiheh, D. Stoffel, and W. Kunz, “A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators”, Design, Automation & Test in Europe Conference and Exhibition (DATE'24), Valencia, April 2024
   
• L. Deutschmann, Y. Kazhalawi, J. Seckinger, A. Duque Antón, J. Müller, M.R. Fadiheh, D. Stoffel, and W. Kunz, “Data-Oblivious and Performant: On Designing Security-Conscious Hardware”,  25th IEEE Latin American Test Symposium (LATS'24), 2024
   
• P. Schmitz, J. Mueller, C. Bartsch, D. Stoffel and W. Kunz, "UPEC-PN: Exhaustive constant time verification of low-level software using property checking," MBMV 2023; 26th Workshop, Freiburg, 2023, pp. 1-8.
   
• A. L. Duque Antón, J. Müller, M.R. Fadiheh, D. Stoffel, W. Kunz: Fault Attacks on Access Control in Processors: Threat, Formal Analysis and Microarchitectural Mitigation. In IEEE Access, 2023.
   
• D. Mehmedagic, M.R. Fadiheh, J. Müller, A.L. Duque Antón, D. Stoffel, W. Kunz: Design of Access Control Mechanisms in Systems-on-Chip with Formal Integrity Guarantees. In USENIX Security Symposium, Aug. 9-11, 2023, Anaheim, USA. (accepted)
   
• L. Deutschmann, J. Müller, M. R. Fadiheh, D. Stoffel, and W. Kunz, “Towards a Formally Verified Hardware Root-of-Trust for Data-Oblivious Computing”, 59th IEEE/ACM Design Automation Conference (DAC'22), San Francisco, July 2022. (Best Paper Award )
   
• M. R. Fadiheh, Alex Wezel, Johannes Müller, Joerg Bormann, Sayak Ray, Jason M Fung, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz, "An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors," in IEEE Transactions on Computers, doi: 10.1109/TC.2022.3152666.
   
• J. Müller, M.R. Fadiheh, A. Duque Antón, T. Eisenbarth, S. Ray, J. Fung, D. Stoffel, W. Kunz: Extending UPEC: “A Formal Approach to Confidentiality Verification in SoCs”, Intel Side-Channel Academic Program Workshop (SCAP) 2021
   
• J. Müller, M.R. Fadiheh, A. Duque-Antón, T. Eisenbarth, D. Stoffel, W. Kunz: "A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level". 58th Annual Design Automation Conference, (DAC'21), 2021
   
• J. Müller, M.R. Fadiheh, A. Duque Antón, D. Stoffel, W. Kunz: Extending UPEC: “Security Issues in Hardware/Firmware interaction – Can a formal analysis of (just) the hardware help?”, edaWorkshop 2020
   
• J. Müller, M.R. Fadiheh, A. Duque Antón, S. Ray, J. Fung, D. Stoffel, W. Kunz: “Extending UPEC: From Confidentiality to Integrity, from Core to SoC”, Intel Side-Channel Academic Program Workshop (SCAP) 2020
   
• M.R. Fadiheh, J. Müller, R. Brinkmann, S. Mitra, D. Stoffel, W. Kunz: A formal approach for detecting vulnerabilities to transient execution attacks in out-of-order processors. 57th Annual Design Automation Conference, (DAC'20), 2020
   
• M.R. Fadiheh, J. Müller, A. Duque-Anton, S. Mitra, J. Fung, D. Stoffel, W. Kunz: A Systematic Approach to Detecting Microarchitectural Security Vulnerabilities by RTL Hardware Verification, Intel Side-Channel Academic Program (SCAP) Workshop 2020, (recording: https://wolke12.eit.uni-kl.de/index.php/s/2XAfUaaT8VLnOZy)
   
• M.R. Fadiheh, J. Müller, A. Duque-Anton, S. Mitra, D. Stoffel, W. Kunz: A Formal Approach for Detecting Vulnerabilities to Transient Execution Attacks in Out-of-order Processors, Intel Side-Channel Academic Program Workshop (SCAP) 2020, (recording: https://wolke12.eit.uni-kl.de/index.php/s/b7fWl5WA4iKTGY3)