Skip directly to content

Minimize RSR Award Detail

Research Spending & Results

Award Detail

Awardee:NORTH DAKOTA STATE UNIVERSITY
Doing Business As Name:North Dakota State University Fargo
PD/PI:
  • Sudarshan K Srinivasan
  • (701) 231-7217
  • sudarshan.srinivasan@ndsu.edu
Award Date:07/01/2021
Estimated Total Award Amount: $ 352,167
Funds Obligated to Date: $ 352,167
  • FY 2021=$352,167
Start Date:10/01/2021
End Date:09/30/2024
Transaction Type:Grant
Agency:NSF
Awarding Agency Code:4900
Funding Agency Code:4900
CFDA Number:47.070
Primary Program Source:040100 NSF RESEARCH & RELATED ACTIVIT
Award Title or Description:SaTC: CORE: Small: Formal Verification Techniques For Microprocessor Security Vulnerabilities and Trojans
Federal Award ID Number:2117190
DUNS ID:803882299
Parent DUNS ID:803882299
Program:Secure &Trustworthy Cyberspace
Program Officer:
  • Alexander Jones
  • (703) 292-8950
  • alejones@nsf.gov

Awardee Location

Street:Dept 4000 - PO Box 6050
City:FARGO
State:ND
ZIP:58108-6050
County:Fargo
Country:US
Awardee Cong. District:00

Primary Place of Performance

Organization Name:North Dakota State University Fargo
Street:Dept 4000 - PO Box 6050
City:FARGO
State:ND
ZIP:58108-6050
County:Fargo
Country:US
Cong. District:00

Abstract at Time of Award

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.

For specific questions or comments about this information including the NSF Project Outcomes Report, contact us.