SaTC: CORE: Small: Formal Verification Techniques For Microprocessor Security Vulnerabilities and Trojans

微处理器是用于执行软件程序的电路，用于重要的应用，如金融系统、ˇ医疗设备、汽车、ˇ发电厂等。最近发现了一种名为Spectre的方法，可以从现代微处理器中泄露私人数据。还发现了光谱的几个变种。形式验证是一套使用数学证明来检查设计是否正确运行的技术。已经为微处理器开发了许多这样的形式验证ˇ技术。这个项目的目标是扩展这些正式的验证技术，以检查微处理器设计是否容易受到Spectre及其变体的影响。该项目的智力优势是开发了形式属性，以检查微处理器设计对Spectre、熔毁和相关安全缺陷的抗毁性。对属性的检查还将标记可能导致这些漏洞的错误或特洛伊木马程序。该项目还将研究和开发精化图、微处理器专用抽象、不变量、组成推理和功能实例化技术，以确保有效和可扩展的验证。该项目的研究活动本身就是有益于社会的。微处理器的使用无处不在，安全正成为这一扩张过程中的一大麻烦。此外，该项目将通过为高中生提供为期两周的带实验室经验的“数字电子和计算机设计”暑期课程，旨在提高妇女和代表不足的少数族裔对计算机工程的参与。提出的新想法是利用新闻媒体对Spectre和Meltdown的广泛报道以及学生对微处理器设计和计算机工程的相关兴趣。该项目预计将产生以下类型的数据：(1)处理器模型和验证属性；(2)为生成验证基准而编写的Python脚本；(3)将在会议和期刊上发表的论文；以及(4)教学材料，如电源插图、说明手册和作业。这些数据将在北达科他州立大学主办的项目网页上提供(见下文链接)，只要它用于学术或行业的研究或教学目的。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Microprocessors are circuits used to execute software programs and are used in important applications such as financial systems,ˇmedical devices, cars,ˇpower plants etc. Recently a method called Spectre was found that could leak private data from modern microprocessors. Several variations of Spectre have also been discovered. Formal verification is a set of techniques that use mathematical proofs to check if a design behaves correctly. Many such formal verificationˇtechniques have been developed for microprocessors. The goal of this project is to extend these formal verification techniques to check if microprocessor designs are vulnerable to Spectre and its variations. The intellectual merits of the project are the development of formal properties to check invulnerability of microprocessor designs to Spectre, Meltdown, and related security flaws. The checking of the properties will also flag bugs or trojans that can induce these flaws. The project will also study and develop refinement-maps, microprocessor-specific abstractions, invariants, compositional reasoning, and functional instantiation techniques required to ensure efficient and scalable verification. The research activities of the project are in themselves beneficial to society. Microprocessors are used pervasively and security is becoming a big hassle in this expansion. In addition, the project will aim to improve participation of women and underrepresented minorities in Computer Engineering by offering two-week summer courses on "Digital Electronics and Computer Design" with lab experience for high school students. The novel idea proposed to improve recruitment and participation will be to exploit the wide coverage of Spectre and Meltdown in the news media and the associated interest generated among students in microprocessor design and Computer Engineering.The project is expected to generate the following types of data: (1) Processor models and verification properties; (2) Python scripts written to generate verification benchmarks; (3) Papers that will be published in conferences and journals; and (4) Teaching materials such as power point slides, instruction manuals, and assignments. The data will be available on the project web page (see link below) hosted by North Dakota State University as long as it is of use either for research or teaching purposes to academics or industry.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.