STARSS: Small: Automatic Synthesis of Verifiably Secure Hardware Accelerators

点击翻译按钮获取中文摘要

Specialized hardware accelerators are growing in popularity across the computing spectrum from mobile devices to datacenters. These special-purpose hardware engines promise significant improvements in computing performance and energy efficiency that are essential to all aspects of modern society. However, hardware specialization also comes with added design complexity and introduces a host of new security challenges, which have not been adequately explored. This project is developing ASSURE, a design automation framework that synthesizes verifiably secure hardware accelerators from high-level programming languages. The automatic high-level synthesis flow provides considerable benefit in terms of productivity and ease of verification. The project also includes educational components such as integration of hardware security topics into the computer engineering curriculum and ongoing high-school outreach efforts through a week-long summer program for underrepresented minority high-school students.ASSURE leverages and builds on the recent advances in high-level synthesis (HLS), which compiles behavioral specifications into optimized register-transfer-level circuits. Unlike recently proposed security-aware HLS methods, ASSURE further provides formal mechanisms to verify that the desired security properties of the synthesized accelerators are indeed guaranteed. Specifically, two major research thrusts are being explored: (1) developing an HLS tool that allows a designer to specify a security level for inputs/outputs of an accelerator, and express restrictions on information flows between security levels as a security lattice; and (2) creating a security checker that enables an independent and formal verification of the information flow security properties of an automatically generated hardware accelerator.