Partial reconfiguration is a versatile technique to modify the functionality of field programmable gate arrays (FPGAs) at run time. When performing partial reconfiguration a dedicated intellectual property (IP) component of the FPGA vendor, i.e., the partial reconfiguration controller (PRC), among a wide range of IP components has to be used. While ensuring the functional safety of FPGA designs is well understood, ensuring hardware security still remains challenging. This applies in particular to reconfiguration-based countermeasures which are intensively used to create a moving target for an attacker. Reconfiguration-based countermeasures against side-channel attacks or differential power analysis (DPA) attacks were implemented. However, from the system security perspective, the above mentioned PRC is a critical component as was noticed by many papers before. In this work, we extend a previously proposed safety mechanism which creates a container around an IP, to encapsulate and thereby to protect and observe the PRC of a FPGA. The proposed encapsulation scheme results in an architecture comprising so-called ReCoFuses (RCFs), each capturing a specific protective goal which have to be fulfilled at any time during PRC operation. The terminology follows the classical electric installation including a fuse box. In our scheme we employ formal verification to guarantee the correctness in detecting a security violation. Only after successful verification, the RCFs are integrated into the ReCoFuse Container. Experimental results demonstrate the advantage of our approach by preventing attacks on the PRC of a system secured by partial reconfiguration.

Within the last decades, tremendous research work has been carried out on the development of software-based algorithms to solve the Boolean Satisfiability Problem. These SAT-solvers have then been heavily orchestrated for addressing complex computational tasks like the verification of circuits. In this field, most of the applied techniques focused only on the design phase of the circuit. Due to this fact, new approaches have been published in the literature solely focusing on online verification as well as self-verification. These kind of solutions strictly require Hardware (HW) SAT-solvers that can be integrated into a system while introducing only low hardware overhead and still providing high flexibility. By following these observations, this work presents SAT-Hard: In contrast to the state-of-the-art, SAT-Hard takes advantage of learning techniques to support features like clause learning and non-chronological backtracking, and combines them within a lightweight and standalone HW device. By this, a run-time speed-up of 2,000x can be achieved. Furthermore, the experimental evaluation clearly demonstrates that those complex problems can be solved in less than 20 seconds. Particularly due to its compactness, SAT-Hard is suitable for self-verification that enables the continuous verification of an integrated system during its lifetime.

Partial reconfiguration is a powerful technique to adapt the functionality of Field Programmable Gate Arrays (FPGAs) at run time. When performing partial reconfiguration a dedicated Intellectual Property (IP) component of the FPGA vendor, i.e. the Partial Reconfiguration Controller (PRC), among a wide range of IP components has to be used. While ensuring the functional safety of FPGA designs is well understood, ensuring hardware security is still very challenging. This applies in particular to reconfiguration-based countermeasures which are intensively used to form a moving target for the attacker. However, from the system security perspective a critical component is the above mentioned PRC as noticed by many papers implementing reconfiguration-based countermeasures against SCA/DPA attacks. In this work, we leverage a new proposed safety mechanism which creates a container around an IP, to encapsulate and thereby to protect and observe the PRC of an FPGA. The proposed encapsulation scheme results in an architecture consisting of so-called ReCoFuses (RCFs), each capturing a specific protective goal which have to be fulfilled at any time during PRC operation. The terminology follows the classical electric installation including a fuse box. In our scheme we employ formal verification to guarantee the correctness in detecting a security violation. Only after successful verification, the RCFs are integrated into the ReCoFuse Container. Experimental results demonstrate the advantage of our approach by preventing attacks on the PRC of a system secured by reconfiguration.

To close the ever widening verification gap, new powerful solutions are strictly required. One such promising approach aims in continuing verification tasks after production of a chip during its lifetime. This approach is called self-verification. However, for realizing self-verification tasks on-chip, verification packages have to be developed. In this paper, we propose verification package SAT-Lancer. SAT-Lancer is a compact Boolean Satisfiability (SAT) solver and has been implemented entirely on HW with the capability of solving any arbitrary SAT-instance. At the heart of SAT-Lancer is a scalable memory model, which can be adjusted to given memory constraints and allows to store the SAT-instance most effectively. In comparison to previous HW SAT-solvers, SAT-Lancer utilizes significant less area and can handle order of magnitude larger SAT-instances.