Formal verification of high-level synthesis

High-level synthesis (HLS), which refers to the automatic compilation of software into hardware, is rapidly gaining popularity. In a world increasingly reliant on application-specific hardware accelerators, HLS promises hardware designs of comparable performance and energy efficiency to those coded by hand in a hardware description language such as Verilog, while maintaining the convenience and the rich ecosystem of software development. However, current HLS tools cannot always guarantee that the hardware designs they produce are equivalent to the software they were given, thus undermining any reasoning conducted at the software level. Furthermore, there is mounting evidence that existing HLS tools are quite unreliable, sometimes generating wrong hardware or crashing when given valid inputs. To address this problem, we present the first HLS tool that is mechanically verified to preserve the behaviour of its input software. Our tool, called Vericert, extends the CompCert verified C compiler with a new hardware-oriented intermediate language and a Verilog back end, and has been proven correct in Coq. Vericert supports most C constructs, including all integer operations, function calls, local arrays, structs, unions, and general control-flow statements. An evaluation on the PolyBench/C benchmark suite indicates that Vericert generates hardware that is around an order of magnitude slower (only around 2× slower in the absence of division) and about the same size as hardware generated by an existing, optimising (but unverified) HLS tool.

Advanced AI Hardware Designs Based on FPGAs

Artificial intelligence (AI) and machine learning (ML) technology enable computers to run cognitive tasks such as recognition, understanding, and reasoning, which are believed to be processes that only humans are capable of, using a massive amount of data [...]

A Hardware Platform for Ensuring OS Kernel Integrity on RISC-V

The OS kernel is typically preassumed as a trusted computing base in most computing systems. However, it also implies that once an attacker takes control of the OS kernel, the attacker can seize the entire system. Because of such security importance of the OS kernel, many works have proposed security solutions for the OS kernel using an external hardware module located outside the processor. By doing this, these works can realize the physical isolation of security solutions from the OS kernel running in the processor, but they cannot access the inner state of the processor, which attackers can manipulate. Thus, they elaborated several methods to overcome such limited capability of external hardware. However, those methods usually come with several side effects, such as high-performance overhead, kernel code modifications, and/or excessively complicated hardware designs. In this paper, we introduce RiskiM, a new hardware-based monitoring platform to ensure kernel integrity from outside the host system. To deliver the inner state of the host to RiskiM, we have devised a hardware interface architecture, called PEMI. Through PEMI, RiskiM is supplied with all internal states of the host system essential for fulfilling its monitoring task to protect the kernel. To empirically validate our monitoring platform’s security strength and performance, we have fully implemented PEMI and RiskiM on a RISC-V based processor and FPGA, respectively. Our experiments show that RiskiM succeeds in the host kernel protection by detecting even the advanced attacks which could circumvent previous solutions, yet suffering from virtually no aforementioned side effects.

Taylor-Series-Based Reconfigurability of Gamma Correction in Hardware Designs

Gamma correction is a common image processing technique that is common in video or still image systems. However, this simple and efficient method is typically expressed using the power law, which gives rise to practical difficulties in designing a reconfigurable hardware implementation. For example, the conventional approach calculates all possible outputs for a pre-determined gamma value, and this information is hardwired into memory components. As a result, reconfigurability is unattainable after deployment. This study proposes using the Taylor series to approximate gamma correction to overcome the aforementioned challenging problem, hence, facilitating the post-deployment reconfigurability of the hardware implementation. In other words, the gamma value is freely adjustable, resulting in the high appropriateness for offloading gamma correction onto its dedicated hardware in system-on-a-chip applications. Finally, the proposed hardware implementation is verified on Zynq UltraScale+ MPSoC ZCU106 Evaluation Kit, and the results demonstrate its superiority against benchmark designs.

LifeLine for FPGA Protection: Obfuscated Cryptography for Real-World Security

Over the last decade attacks have repetitively demonstrated that bitstream protection for SRAM-based FPGAs is a persistent problem without a satisfying solution in practice. Hence, real-world hardware designs are prone to intellectual property infringement and malicious manipulation as they are not adequately protected against reverse-engineering.In this work, we first review state-of-the-art solutions from industry and academia and demonstrate their ineffectiveness with respect to reverse-engineering and design manipulation. We then describe the design and implementation of novel hardware obfuscation primitives based on the intrinsic structure of FPGAs. Based on our primitives, we design and implement LifeLine, a hardware design protection mechanism for FPGAs using hardware/software co-obfuscated cryptography. We show that LifeLine offers effective protection for a real-world adversary model, requires minimal integration effort for hardware designers, and retrofits to already deployed (and so far vulnerable) systems.

FIVER – Robust Verification of Countermeasures against Fault Injections

Fault Injection Analysis is seen as a powerful attack against implementations of cryptographic algorithms. Over the last two decades, researchers proposed a plethora of countermeasures to secure such implementations. However, the design process and implementation are still error-prone, complex, and manual tasks which require long-standing experience in hardware design and physical security. Moreover, the validation of the claimed security is often only done by empirical testing in a very late stage of the design process. To prevent such empirical testing strategies, approaches based on formal verification are applied instead providing the designer early feedback.In this work, we present a fault verification framework to validate the security of countermeasures against fault-injection attacks designed for ICs. The verification framework works on netlist-level, parses the given digital circuit into a model based on Binary Decision Diagrams, and performs symbolic fault injections. This verification approach constitutes a novel strategy to evaluate protected hardware designs against fault injections offering new opportunities as performing full analyses under a given fault models.Eventually, we apply the proposed verification framework to real-world implementations of well-established countermeasures against fault-injection attacks. Here, we consider protected designs of the lightweight ciphers CRAFT and LED-64 as well as AES. Due to several optimization strategies, our tool is able to perform more than 90 million fault injections in a single-round CRAFT design and evaluate the security in under 50 min while the symbolic simulation approach considers all 2128 primary inputs.

IDENTIFYING THE FACTORS AFFECTING THE REPLICABILITY OF OPEN SOURCE HARDWARE DESIGNS

Open-source hardware (OSH) development is a new design paradigm from a commercial perspective. Openly sharing designs of technical products is a step towards democratising access to new technologies for the benefit of individuals and communities in society. At the core of the open-source hardware definition lies the freedom for anyone to replicate the hardware based on the design. Thus, enabling this freedom is a step towards developing a successful OSH. Previous research supposes that a bill of materials and assembly instructions are enough for this. In this study, we question this assumption and investigate what other factors may influence replicability of an OSH. Using data from a survey and interviews with OSH practitioners, we identify and describe these factors, which relate to the documentation, the design and the context of the person replicating the hardware. Using these insights, we present a diagram of the replication process along with questions the person replicating the hardware would ask to check whether an OSH is replicable. Finally, we synthesise this information into practical advice for OSH projects to increase the replicability of the designs they produce, and thus the likelihood of their project's success.

Automated CNN back-propagation pipeline generation for FPGA online training

Training of convolutional neural networks (CNNs) on embedded platforms to support on-device learning has become essential for the future deployment of CNNs on autonomous systems. In this work, we present an automated CNN training pipeline compilation tool for Xilinx FPGAs. We automatically generate multiple hardware designs from high-level CNN descriptions using a multi-objective optimization algorithm that explores the design space by exploiting CNN parallelism. These designs that trade-off resources for throughput allow users to tailor implementations to their hardware and applications. The training pipeline is generated based on the backpropagation (BP) equations of convolution which highlight an overlap in computation. We translate the overlap into hardware by reusing most of the forward pass (FP) pipeline reducing the resources overhead. The implementation uses a streaming interface that lends itself well to data streams and live feeds instead of static data reads from memory. Meaning, we do not use the standard array of processing elements (PEs) approach, which is efficient for offline inference, instead we translate the architecture into a pipeline where data is streamed through allowing for new samples to be read as they become available. We validate the results using the Zynq-7100 on three datasets and varying size architectures against CPU and GPU implementations. GPUs consistently outperform FPGAs in training times in batch processing scenarios, but in data stream scenarios, FPGA designs achieve a significant speedup compared to GPU and CPU when enough resources are dedicated to the learning task. A 2.8×, 5.8×, and 3× speed up over GPU was achieved on three architectures trained on MNIST, SVHN, and CIFAR-10 respectively.

PrintrLab incubator: A portable and low-cost CO2 incubator based on an open-source 3D printer architecture

Growth in open-source hardware designs combined with the decreasing cost of high-quality 3D printers have supported a resurgence of in-house custom lab equipment development. Herein, we describe a low-cost (< $400), open-source CO2 incubator. The system is comprised of a Raspberry Pi computer connected to a 3D printer controller board that has controls for a CO2 sensor, solenoid valve, heater, and thermistors. CO2 is supplied through the sublimation of dry ice stored inside a thermos to create a sustained 5% CO2 supply. The unit is controlled via G-Code commands sent by the Raspberry Pi to the controller board. In addition, we built a custom software application for remote control and used the open-source Grafana dashboard for remote monitoring. Our data show that we can maintain consistent CO2 and temperature levels for over three days without manual interruption. The results from our culture plates and real-time PCR indicate that our incubator performed equally well when compared to a much more expensive commercial CO2 incubator. We have also demonstrated that the antibiotic susceptibility assay can be performed in this low-cost CO2 incubator. Our work also indicates that the system can be connected to incubator chambers of various chamber volumes.