PowerCourt: Formally Judging Benign-Looking Circuits in Multi-Tenant FPGA Environments

In the era of Cloud Computing and High Performance Computing as a Service, multiple customers run their software and hardware on the same physical devices. This opens new opportunities for attackers, like Denial of Service (DoS) attacks on shared cloud Field Programmable Gate Arrays (FP-GAs). DoS attacks work by employing a malicious hardware design as a tenant on a shared FPGA device, draining the FPGA’s power budget. This paper aims at identifying potentially malicious circuits before they are deployed to the FPGA, using formal verification. Our methodology, PowerCourt, provides an accurate worst-case power estimation based on switching activity. It computes metadata about the design that enables service providers to classify designs as malicious. The method checks formal properties that verify whether a design can exceed a custom threshold and whether this threshold can be exceeded repeatedly. We demonstrate the effectiveness of our approach using various hardware designs. For example, for a trojan that enables excessive switching, we show that we can detect it offline and disable it during runtime