STARSS: Small: Automatic Synthesis of Verifiably Secure Hardware Accelerators

专用硬件加速器在从移动的设备到计算中心的计算范围内越来越受欢迎。这些专用硬件引擎有望显著提高计算性能和能源效率，这对现代社会的各个方面都至关重要。然而，硬件专业化也增加了设计复杂性，并引入了许多新的安全挑战，这些挑战尚未得到充分探讨。该项目正在开发ASSURE，这是一个设计自动化框架，可以从高级编程语言中合成可验证的安全硬件加速器。自动高级综合流程在生产率和易于验证方面提供了相当大的好处。该项目还包括教育组件，如硬件安全主题整合到计算机工程课程和正在进行的高中外展工作，通过为期一周的暑期课程，为代表性不足的少数民族高中学生.ASSURE利用和建立在高层次综合（HLS），它编译的行为规范到优化的寄存器传输级电路的最新进展.与最近提出的安全感知HLS方法不同，ASSURE还提供了正式的机制来验证合成加速器的所需安全属性确实得到了保证。具体而言，正在探索两个主要的研究方向：（1）开发HLS工具，该工具允许设计者指定加速器的输入/输出的安全级别，并将安全级别之间的信息流限制表示为安全网格;以及（2）创建安全检查器，其使得能够独立且正式地验证自动生成的硬件加速器的信息流安全属性。

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.