SaTC: STARSS: Small: Tackling the Corner Cases: Finding Security Vulnerabilities in CPU Designs

SaTC：STARSS：小型：解决极端情况：查找 CPU 设计中的安全漏洞

基本信息

批准号：
1816637
负责人：
Cynthia Sturton
金额：
$ 33.33万
依托单位：
University of North Carolina at Chapel Hill
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-10-01 至 2022-09-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1816637&HistoricalAwards=false
关键词：
SaTC STARSS Small Tackling Corner

项目摘要

Computing hardware including processors, memory banks, and communication busses can harbor vulnerabilities that allow an attacker to gain unauthorized access to the programs and data on a machine. Hardware designers and security experts expend considerable time and effort to eliminate these vulnerabilities early in the design stage. The focus of this research is to support these activities towards improving efficiency and outcomes. In developing the methodologies and tools to find and contextualize hardware security vulnerabilities, this research will move the field of security validation of hardware designs forward.The research targets the security validation of central processing units in the design stage. The project has two goals: 1) To identify security critical properties of a processor. These properties will be stated in a temporal logic over the register transfer level design. 2) To develop the methodology and tools to automatically find and contextualize violations of those properties. A key innovation of this research will be the application of symbolic execution to hardware designs. In order to make symbolically executing a complex hardware design through multiple clock cycles feasible, the research will develop a targeted, backward search strategy.If successful, the project has the potential to significantly reduce the opportunity for a malicious actor to launch an effective attack against hardware, improving the security of computer systems.The tools, testbenches, papers, and presentations resulting from this research will be available at a site linked from https://cs.unc.edu/~csturton.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.

计算包括处理器，内存库和通信总线在内的硬件可能会留下漏洞，从而使攻击者能够获得对机器上程序和数据的未经授权访问。硬件设计师和安全专家花费了大量时间和精力来消除设计阶段的早期这些漏洞。这项研究的重点是支持这些活动以提高效率和结果。在开发方法和工具以查找和上下文化硬件安全漏洞时，本研究将推动硬件设计的安全验证领域。该研究针对设计阶段中央处理单元的安全验证。该项目有两个目标：1）确定处理器的安全关键属性。这些属性将在寄存器传输级设计上的时间逻辑中说明。 2）开发方法和工具，以自动查找并将其上下文化对这些属性的行为。这项研究的关键创新将是将符号执行的应用到硬件设计。为了通过可行的多个时钟循环来象征性地执行复杂的硬件设计，该研究将制定有针对性的后退搜索策略。如果成功，该项目有可能大大减少恶意演员发动有效攻击的机会硬件，改善计算机系统的安全性。该研究产生的工具，测试台，论文和演示文稿将在https://cs.unc.edu/~csturton.this奖励的网站上获得。使用基金会的知识分子优点和更广泛的审查标准，通过评估被认为值得支持。

项目成果

期刊论文数量（6）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Mining Security Critical Linear Temporal Logic Specifications for Processors

采矿安全关键的线性时态逻辑处理器规范

DOI：
10.1109/mtv.2018.00013
发表时间：
2018
期刊：
19th International Workshop on Microprocessor and SOC Test and Verification (MTV
影响因子：
0
作者：
Deutschbein, Calvin;Sturton, Cynthia
通讯作者：
Sturton, Cynthia

Evaluating Security Specification Mining for a CISC Architecture

评估 CISC 架构的安全规范挖掘

DOI：
10.1109/host45689.2020.9300291
发表时间：
2020
期刊：
2020 IEEE Hardware Oriented Security and Trust (HOST
影响因子：
0
作者：
Deutschbein, Calvin;Sturton, Cynthia
通讯作者：
Sturton, Cynthia

End-to-End Automated Exploit Generation for Processor Security Validation

用于处理器安全验证的端到端自动漏洞利用生成

DOI：
10.1109/mdat.2021.3063314
发表时间：
2021
期刊：
IEEE Design & Test
影响因子：
2
作者：
Zhang, Rui;Deutschbein, Calvin;Huang, Peng;Sturton, Cynthia
通讯作者：
Sturton, Cynthia

Isadora: Automated Information Flow Property Generation for Hardware Designs

DOI：
10.1145/3474376.3487286
发表时间：
2021-06
期刊：
Proceedings of the 5th Workshop on Attacks and Solutions in Hardware Security
影响因子：
0
作者：
Calvin Deutschbein;Andres Meza;Francesco Restuccia;R. Kastner;C. Sturton
通讯作者：
Calvin Deutschbein;Andres Meza;Francesco Restuccia;R. Kastner;C. Sturton

Transys: Leveraging Common Security Properties Across Hardware Designs