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

微处理器是用于执行软件程序的电路，并用于重要的应用程序，如金融系统，电子医疗设备，汽车，电子发电厂等。幽灵的几个变种也被发现。形式验证是一组使用数学证明来检查设计行为是否正确的技术。许多这样的形式化验证技术已经被开发用于微处理器。该项目的目标是扩展这些形式验证技术，以检查微处理器设计是否容易受到Spectre及其变体的影响。该项目的智力价值是开发形式属性，以检查微处理器设计对Spectre，Meltdown和相关安全缺陷的抗毁性。检查属性还将标记可能导致这些缺陷的错误或特洛伊木马。该项目还将研究和开发细化映射，微处理器特定的抽象，不变量，组合推理和功能实例化技术，以确保有效和可扩展的验证。该项目的研究活动本身对社会有益。微处理器被广泛使用，安全性在这种扩展中成为一个大问题。此外，该项目还将为高中生提供为期两周的“数字电子和计算机设计”暑期课程，并提供实验室经验，以提高妇女和代表性不足的少数民族对计算机工程的参与。为了提高招募和参与的新颖性，建议利用新闻媒体对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.