Skip to content
@RPTU-EIS

Chair of Electronic Design Automation

Lehrstuhl für Entwurf informationstechnischer Systeme der RPTU in Kaiserslautern

CHAIR OF ELECTRONIC DESIGN AUTOMATION | University of Kaiserslautern (RPTU)

Research

The focus of our current research activities is on the design and verification of Embedded Systems and Systems-on-Chip (SoC). We are interested in both the hardware and the low-level software (firmware) of the systems. Some of our research projects are particularly focused on the interaction between hardware and software.

Besides targeting traditional design goals such as high performance and low power consumption, a particular objective of our research is to make contributions to achieving functional safety and security of the designed and manufactured systems. The requirement for functional safety and security is driven by an increased use of embedded systems technology in safety- and security-critical applications such as in avionics and automotive systems (e.g., autonomous cars). Another driver of this research field are new manufacturing techniques in “smart factories” (Industry 4.0) which impose new challenges on the safety of embedded systems technology as well as on the confidentiality of the data being processed. Current research topics are:

  • Detection of Security Vulnerabilities in Hardware through exhaustive formal Methods 1234
  • Design and Implementation of Mitigations targeting Transient Execution Side Channels and Timing Attacks 56
  • Correct-by-Construction Embedded System Design using "Property-First Design" 789

Footnotes

  1. M.R. Fadiheh, A. Wezel, J. Mueller, J. Bormann, S. Ray, J. Fung, S. Mitra, D. Stoffel, W. Kunz: An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors. In IEEE Transactions on Computers, Jan. 2023

  2. J. Müller, M.R. Fadiheh, A.L. Duque Antón, T. Eisenbarth, D. Stoffel, W. Kunz: A Formal Approach to Confidentiality Verification in SoCs at the Register Transfer Level. In Proceedings of the 58th ACM/IEEE Design Automation Conference (DAC '21), Dec. 2021, pp. 991-996

  3. L. Deutschmann, J. Müller, M.R. Fadiheh, D. Stoffel, W. Kunz: Towards a formally verified hardware root-of-trust for data-oblivious computing. In Proceedings of the 59th ACM/IEEE Design Automation Conference (DAC '22), July 2022, pp. 727–732.

  4. D. Mehmedagic, M.R. Fadiheh, J. Mueller, A.L. Duque Antón, D. Stoffel, W. Kunz: Design of Access Control Mechanisms in Systems-on-Chip with Formal Integrity Guarantees. In 32nd USENIX Security Conference, 2023

  5. T. Jauch, A. Wezel, M.R. Fadiheh, P. Schmitz, S. Ray, J. Fung, C.W. Fletcher, D. Stoffel, W. Kunz: Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD), Nov. 2023, pp. 1-9

  6. P. Schmitz, T. Jauch, A. Wezel, M.R. Fadiheh, T. Tiemann, J. Heller, T. Eisenbarth, D. Stoffel, W. Kunz: Okapi: A Lightweight Architecture for Secure Speculation Exploiting Locality of Memory Accesses. arXiv preprint, 2023, 2312.08156 (cs.CR)

  7. T. Ludwig, J. Urdahl, D. Stoffel, W. Kunz: Properties First – Correct-By-Construction RTL Design in System-Level Design Flows. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, July 11, 2019

  8. T. Ludwig, M. Schwarz, J. Urdahl, L. Deutschmann, S. Hetalani, D. Stoffel, W. Kunz: Property Driven Development of a RISC-V CPU. On Proceedings of DVCON US, 2019

  9. S. Udupi, J. Urdahl, D. Stoffel, W. Kunz: Exploiting Hardware Unobservability for Low-Power Design and Safety Analysis in Formal Verification-Driven Design Flows. In IEEE Transactions on Very Large Scale Integration Systems, Vol. 27, No. 6, June 2019

Pinned Loading

  1. SecureBOOM SecureBOOM Public

    Formally proven secure design of the RISC-V core BOOM (Berkeley Out-of-Order Machine) w.r.t. transient execution attacks (e.g., Meltdown and Spectre)

    Verilog 4 1

  2. upec-boom-verification-suite upec-boom-verification-suite Public

    This repository contains the verification suite for verifying Berkeley Out-of-Order Machine (BOOM) against transient execution attacks based on the Unique Program Execution Checking (UPEC) approach.

    Verilog 13 2

  3. thesis-template thesis-template Public

    LaTeX template for Bachelor and Master theses at EIS chair

    TeX

  4. VDSProject VDSProject Public

    This repository contains the basic files for the class project of the course "Verification of Digital Systems"

    C++ 4 35

  5. OpenTitan_with_Access_Control OpenTitan_with_Access_Control Public

    OpenTitan Silver Release v5 copy for security improvements

    SystemVerilog 2 2

  6. symbolic-pmp symbolic-pmp Public

    This repository contains a symbolic and secure configuration template for the RISC-V Physical Memory Protection (PMP) to be used in SV/SVA based verification flows.

    SystemVerilog 3

Repositories

Showing 10 of 16 repositories
  • thesis-template Public

    LaTeX template for Bachelor and Master theses at EIS chair

    RPTU-EIS/thesis-template’s past year of commit activity
    TeX 0 0 0 0 Updated Jul 2, 2024
  • RISCV-Core Public

    5-stage RISC-V core (RV32IM) with pipelining designed for educational purposes by RPTU Kaiserslautern, Germany

    RPTU-EIS/RISCV-Core’s past year of commit activity
    C 12 9 0 0 Updated May 22, 2024
  • ADSProject Public

    This repository contains the basic files for the class project of the course "Architecture of Digital Systems I"

    RPTU-EIS/ADSProject’s past year of commit activity
    Scala 2 5 0 0 Updated Mar 28, 2024
  • .github Public
    RPTU-EIS/.github’s past year of commit activity
    0 0 0 0 Updated Feb 22, 2024
  • Security-Conscious-Hardware Public

    Collection of experiments on data-oblivious hardware designs that dynamically adjust their latency

    RPTU-EIS/Security-Conscious-Hardware’s past year of commit activity
    SystemVerilog 1 0 0 0 Updated Jan 30, 2024
  • UPEC-DIT Public

    This repository contains experiments and results on using UPEC to prove data-independent timing in hardware.

    RPTU-EIS/UPEC-DIT’s past year of commit activity
    3 1 0 0 Updated Jan 18, 2024
  • VDSProject Public

    This repository contains the basic files for the class project of the course "Verification of Digital Systems"

    RPTU-EIS/VDSProject’s past year of commit activity
    C++ 4 35 0 1 Updated Dec 13, 2023
  • rocket-chip-inclusive-cache Public Forked from chipsalliance/rocket-chip-inclusive-cache

    An RTL generator for a last-level shared inclusive TileLink cache controller

    RPTU-EIS/rocket-chip-inclusive-cache’s past year of commit activity
    Scala 0 Apache-2.0 13 0 0 Updated Nov 19, 2023
  • OpenTitan_with_Access_Control Public

    OpenTitan Silver Release v5 copy for security improvements

    RPTU-EIS/OpenTitan_with_Access_Control’s past year of commit activity
    SystemVerilog 2 Apache-2.0 2 0 0 Updated Nov 9, 2023
  • SecureBOOM Public

    Formally proven secure design of the RISC-V core BOOM (Berkeley Out-of-Order Machine) w.r.t. transient execution attacks (e.g., Meltdown and Spectre)

    RPTU-EIS/SecureBOOM’s past year of commit activity
    Verilog 4 1 0 0 Updated Sep 5, 2023

Top languages

Loading…

Most used topics

Loading…