TWC: Small: Collaborative: Extensible Symbolic Analysis Modulo SMT: Combining the Powers of Rewriting, Narrowing, and SMT Solving in Maude

TWC：小：协作：可扩展符号分析 Modulo SMT：结合 Maude 中重写、缩小和 SMT 求解的能力

• 批准号: 1318848
• 负责人: Carolyn Talcott
• 金额: $ 24.95万
• 依托单位: SRI International
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1318848&HistoricalAwards=false
• 关键词: TWC; Small; Collaborative; Extensible; Symbolic

This project develops the foundations for automating verification of secure and trustworthy systems. It extends the range of analyses that are amenable to automated checking and addresses scalability. Symbolic techniques that represent possibly infinite sets of states by symbolic constraints have become important tools, but many systems of interest fall outside the scope of current techniques. There is a real need to extend and combine the power of symbolic analysis techniques to cover a much wider class of systems in order to develop the foundations for security and trustworthy software and systems.Maude is a language based on rewriting logic. Maude can be used to model a system of any kind -- for example, an algorithm, a database, a hardware system, a programming language, a network protocol, a sensor network, or the molecular biology dynamics of a cell -- using a set of rewrite rules that describe the systems behavior. The current Maude implementation provides a high performance rewrite engine, as well as built-in search, unification, and model checking tools to support execution and analysis of systems specified in Maude. This project will develop general extensibility techniques for symbolic analysis that can simultaneously combine the power of Satisfiability Modulo Theories (SMT) constraint solving, rewriting- and unification-based analysis, and automata-based model checking to analyze a wide variety of systems beyond the scope of each separate technique. Specifically, the goals of the project are to: (i) develop the semantic foundations of extensible symbolic analysis combining SMT solving, rewriting and narrowing, and automata-based model checking; (ii) endow the Maude formal specification system with combined symbolic analysis capabilities based on such foundations; and (iii) demonstrate through case studies the power of such combined and extensible symbolic techniques in analyzing challenging systems in areas such as: model checking, theorem proving, programming languages, cryptographic protocols, and real-time and cyber-physical systems. Maude has a substantial set of users who are doing research on approaches to secure and trustworthy systems. These users are poised to use the new techniques and tools as they develop. For critical systems, where even small security issues can lead to catastrophic failures, this foundational research will support rigorous techniques and tools for automated and scalable checking.

该项目为自动验证安全可靠的系统奠定了基础。它扩展了适合自动检查的分析范围，并解决了可伸缩性问题。通过符号约束表示可能无限的状态集的符号技术已经成为重要的工具，但许多感兴趣的系统不在当前技术的范围内。确实需要扩展和结合符号分析技术的力量，以涵盖更广泛的系统类别，以便为安全和可信的软件和系统奠定基础。Maude是一种基于重写逻辑的语言。Maude可以用来对任何类型的系统建模--例如，算法、数据库、硬件系统、编程语言、网络协议、传感器网络或细胞的分子生物学动力学--使用一组描述系统行为的重写规则。当前的Maude实现提供了一个高性能的重写引擎，以及内置的搜索、统一和模型检查工具，以支持Maude中指定的系统的执行和分析。这个项目将为符号分析开发通用的可扩展性技术，它可以同时结合可满足性模理论(SMT)约束求解、基于重写和统一的分析以及基于自动机的模型检查的能力，以分析超出每种单独技术范围的各种系统。具体地说，该项目的目标是：(I)开发结合SMT求解、重写和缩小以及基于自动机的模型检查的可扩展符号分析的语义基础；(Ii)在这些基础上赋予Maude形式规范系统组合的符号分析能力；以及(Iii)通过案例研究展示这种组合的和可扩展的符号技术在分析诸如模型检查、定理证明、编程语言、密码协议以及实时和网络物理系统等领域的挑战性系统方面的能力。Maude拥有一大批用户，他们正在研究安全可靠的系统的方法。这些用户准备在开发过程中使用新的技术和工具。对于关键系统，即使是小的安全问题也可能导致灾难性的故障，这项基础研究将支持用于自动化和可扩展检查的严格技术和工具。