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

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

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.