SHF: Small: Efficient Verification of Nonlinear Arithmetic

SHF：小型：非线性算术的高效验证

基本信息

批准号：
1714593
负责人：
Paul Beame
金额：
$ 45万
依托单位：
University of Washington
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-09-01 至 2021-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1714593&HistoricalAwards=false
关键词：
SHF Small Efficient Verification Nonlinear

项目摘要

In recent decades, formal methods have produced many successes in proving properties of hardware and software artifacts. However, the lack of general efficient methods to verify designs that involve nonlinear arithmetic -- arithmetic that involves integer multiplication -- has been a major impediment to the effectiveness of verification methods in a broad array of applications. Among many other applications, computations that depend on nonlinear arithmetic are at the heart of CPU designs, cryptography, and structures for efficient storage of data for easy retrieval. This project is focused on achieving efficient verification of hardware and software designs that include nonlinear arithmetic. This project explores methods for extending the most widely effective class of current verification methods, which at their heart use Boolean satisfiability (SAT) solvers, to handle designs that include integer multiplication. The investigators have shown that certain properties of integer multiplication circuits that have been conjectured to be representative of the difficulty of verifying nonlinear arithmetic can be efficiently verified in systems of inference that capture the capabilities of state-of-the-art SAT solvers. This project leverages and extends these theoretical insights to develop practical methods that will succeed in a broad range of verification tasks for software and hardware artifacts that use nonlinear arithmetic. The research results will be widely disseminated in open source tools for people to use for verification leading to software and hardware with a higher level of trustworthiness, including in safety-critical applications that people rely on every day.

近几十年来，正式方法在证明硬件和软件工件的特性方面取得了许多成功。但是，缺乏验证涉及非线性算术的设计（涉及整数乘法的算术）的设计的主要障碍，这是验证方法在广泛的应用程序中的有效性的主要障碍。在许多其他应用中，取决于非线性算术的计算是CPU设计，密码学和结构的核心，可有效地存储数据，以便于检索。该项目的重点是实现包括非线性算术在内的硬件和软件设计的有效验证。该项目探讨了扩展最广泛有效类的当前验证方法的方法，这些方法本地使用布尔值满意度（SAT）求解器来处理包括整数乘法的设计。研究人员表明，在捕获最先进的SAT求解器的能力的推理系统中，可以有效验证整数乘电路的某些特性，以代表了验证非线性算术的难度。该项目利用并扩展了这些理论见解，以开发实用方法，这些方法将在使用非线性算术的软件和硬件伪像的广泛验证任务中取得成功。该研究结果将被广泛传播到开源工具中，供人们用于验证，从而导致具有更高水平的可信度的软件和硬件，包括人们每天依靠的关键安全应用程序。