As the complexity of System-on-Chip (SoC) designs continues to increase, ensuring thorough verification becomes a significant challenge for system integrators. The complexity of verification can result in undetected bugs. Unlike software or firmware bugs, hardware bugs are hard to fix after deployment and they require additional logic, i.e., patching logic integrated with the design in advance in order to patch. However, the absence of a standardized metric for defining “patchability” leaves system integrators relying on their understanding of each IP and security requirements to engineer ad hoc patching designs. In this paper, we propose a theoretical patchability quantification method to analyze designs at the Register Transfer Level (RTL) with provided patching options. Our quantification defines patchability as a combination of observability and controllability so that we can analyze and compare the patchability of IP variations. This quantification is a systematic approach to estimate each patching architecture’s ability to patch at run-time and complements existing patching works. In experiments, we compare several design options of the same patching architecture and discuss their differences in terms of theoretical patchability and how many potential weaknesses can be mitigated.

This work presents a power side-channel analysis (SCA) of a lightweight cryptography (LWC) algorithm, XOODYAK, implemented on an FPGA. First, we perform generic leakage detection tests for two phases of authenticated encryption with associated data (AEAD) mode, namely INITIALIZE, and ABSORB. Second, we develop novel hypothetical attack models for correlation power analysis (CPA) and demonstrate a success rate (SR) of 92%/82% and minimum-traces-to-disclosure (MTD)=13K/38K on the INITIALIZE/ABSORB phases, respectively. Third, we evaluate ABSORB against Profiled SCA using convolutional neural network (CNN), and achieve SR=96%/64% and MTD=2K/16K on the test set for the same/different keys used for training, respectively. Finally, we suggest low-overhead countermeasures to protect against these SCA attacks.

Spectre and Meltdown attacks proved Transient Execution Side Channels to be a notable challenge for designing secure microarchitectures. Various countermeasures against these threats were proposed on the electronic system level. However, addressing all possible attack scenarios requires the design and analysis of bit-and cycle-accurate implementations. We present a novel secure-by-construction RTL design methodology based on a new hardware protection framework underpinned by a generic control infrastructure that can be integrated into industry-grade microarchitectures. The methodology uses formal verification to systematically detect possible leakage paths and to customize the generic infrastructure accordingly for the design. We propose an iterative flow which semi-automatically leads to an RTL design that is guaranteed to be secure w.r.t. transient execution attacks. A case study for the methodology is conducted on BOOMv3, an open-source RISC-V processor with a deep out-of-order pipeline, and the resulting secure RTL design is benchmarked on an FPGA setup. Our design outperforms a design based on conservative countermeasures, improving the incurred overhead by$\boldsymbol{3}\times/\boldsymbol{4}\times$(depending on the threat model) while maintaining the same level of security.

Hardware (HW) security issues have been emerging at an alarming rate in recent years. Transient execution attacks, such as Spectre and Meltdown, in particular, pose a genuine threat to the security of modern computing systems. Despite recent advances, understanding the intricate implications of microarchitectural design decisions on processor security remains a great challenge and has caused a number of update cycles in the past. This papers addresses the need for a new approach to HW sign-off verification which guarantees the security of processors at the Register Transfer Level (RTL). To this end, we introduce a formal definition of security with respect to transient execution attacks, formulated as a HW property. We present a formal proof methodology based onUnique Program Execution Checking (UPEC)which can be used to systematically detect all vulnerabilities to transient execution attacks in RTL designs. UPEC does not exploit any a priori knowledge on known attacks and can therefore detect also vulnerabilities based on new, so far unknown, types of channels. This is demonstrated by two new attack scenarios discovered in our experiments with UPEC. UPEC scales to a wide range of HW designs, including in-order processors (RocketChip), pipelines with out-of-order writeback (Ariane), and processors with deep out-of-order speculative execution (BOOM). To the best of our knowledge, UPEC is the first RTL verification technique that exhaustively covers transient execution side channels in processors of realistic complexity.

To satisfy various design requirements and application needs, designers integrate multiple intellectual property blocks (IPs) to produce a system on chip (SoC). For improved survivability, designers should be able to patch the SoC to mitigate potential security issues arising from hardware IPs; for increased flexibility, we propose adding programmable hardware-based support for monitoring and bug mitigation. However, it is a challenge to decide how much additional cost a designer should expend up front to deal with unknown, future issues. We propose an approach that guides designers toward maximizing the benefits of adding “patchability” to various IPs in the system, given a target resource overhead. We frame the design problem as an integer quadratic program and show that our approach achieves superior patchability compared to the naïve and baseline approaches for a given cost limit. Experimental results show that when we set a cost limit of 2% field-programmable gate array adaptive logic module usage, our solution can generate a viable patching infrastructure with six patching blocks offering patches for seven different services in our case study.

Security verification is an important part of the hardware design process. Security verification teams can uncover weaknesses, vulnerabilities, and flaws. Unfortunately, the verification process involves substantial manual analysis to create the threat model, identify important security assets, articulate weaknesses, define security requirements, and specify security properties that formally describe security requirements upon the hardware. This work describes current hardware security verification practices. Many of these rely on manual analysis. We argue that the property generation process is a first step towards scalable and reproducible hardware security verification.

To help prevent hardware security vulnerabilities from propagating to later design stages where fixes are costly, it is crucial to identify security concerns as early as possible, such as in RTL designs. In this work, we investigate the practical implications and feasibility of producing a set of security-specific scanners that operate on Verilog source files. The scanners indicate parts of code that might contain one of a set of MITRE's common weakness enumerations (CWEs). We explore the CWE database to characterize the scope and attributes of the CWEs and identify those that are amenable to static analysis. We prototype scanners and evaluate them on 11 open source designs - 4 system-on-chips (SoC) and 7 processor cores - and explore the nature of identified weaknesses. Our analysis reported 53 potential weaknesses in the OpenPiton SoC used in [email protected], 11 of which we confirmed as security concerns.

System integrators create heterogeneous systems-on-chip (SoCs) by integrating numerous third-party intellectual property blocks (3PIPs) to achieve application-specific design goals. With increasing intellectual property (IP) complexity, 3PIPs can suffer from hardware bugs or they can inadvertently introduce other software-exploitable security threats to the SoC. To ensure the ongoing survivability of new SoCs, we need infrastructure for patching newly discovered IP issues after an SoC has been deployed. To address the increasing risks from 3PIPs, we explore the feasibility and limitations of implementing monitoring and mitigation capabilities in hardware. Our proposed monitoring and mitigation patch (MoP) blocks provide a defensive foundation against critical IP-centric issues, focusing on situations where a system integrator only has interface-level visibility of 3PIP designs. The MoPs are distributed throughout the SoC to monitor and mitigate issues directly in hardware and transparently for potentially compromised software-the MoPs are resilient against run-time compromised software and firmware. We ensure that these monitors are reconfigurable after deployment by implementing them using embedded-FPGAs or as a reprogrammable, fixed-design module. We perform a case study of numerous IP-types and model a selection of security-relevant issues and bugs in the IPs, exploring the relative complexity and potential resource overhead. Our study shows the utility of our proposed approach, with MoP blocks requiring less than ~1.5% of the adaptive logic modules (ALMs) in a Cyclone V FPGA for interface monitoring and issue mitigation per IP.

We present an effective methodology for formally verifying security-critical flows in a commercial System-on-Chip (SoC) which involve extensive interaction between firmware (FW) and hardware (HW). We describe several HW-FW interaction scenarios that are typical in commercial SoCs. We highlight unique challenges associated with formal verification of security properties of such interactions and discuss our approach of property-specific abstraction and software model checking to circumvent those challenges. To the best of our knowledge, this is the first exposition on formal co-verification of security-specific HW-FW interactions in the context and scale of a commercial SoCs. Despite traditional scalability challenges, we demonstrate that many such flows are amenable to effective formal verification.

Formal security verification of firmware interacting with hardware in modern Systems-on-Chip (SoCs) is a critical research problem. This faces the following challenges: (1) design complexity and heterogeneity, (2) semantics gaps between software and hardware, (3) concurrency between firmware/hardware and between Intellectual Property Blocks (IPs), and (4) expensive bit-precise reasoning. In this paper, we present a co-verification methodology to address these challenges. We model hardware using the Instruction-Level Abstraction (ILA), capturing firmware-visible behavior at the architecture level. This enables integrating hardware behavior with firmware in each IP into a single thread. The co-verification with multiple firmware across IPs is formulated as a multi-threaded program verification problem, for which we leverage software verification techniques. We also propose an optimization using abstraction to prevent expensive bit-precise reasoning. The evaluation of our methodology on an industry SoC Secure Boot design demonstrates its applicability in SoC security verification.