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

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

• 批准号: 1319109
• 负责人: Jose Meseguer
• 金额: $ 25万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2016-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319109&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中指定的系统的执行和分析。本项目将开发用于符号分析的通用可扩展性技术，这些技术可以同时联合收割机结合可满足性模理论（SMT）约束求解、基于重写和统一的分析以及基于自动机的模型检查的能力，以分析超出每种单独技术范围的各种系统。具体地说，该项目的目标是：（一）开发可扩展符号分析的语义基础，结合SMT求解、重写和缩小，以及基于自动机的模型检查;（二）赋予Maude形式规格说明系统以基于这些基础的组合符号分析能力;以及（iii）通过案例研究展示这种组合和可扩展的符号技术在分析以下领域的挑战性系统时的力量：模型检查、定理证明、编程语言、加密协议以及实时和网络物理系统。Maude拥有大量的用户，他们正在研究安全和可信系统的方法。这些用户在开发过程中随时准备使用新的技术和工具。对于关键系统，即使是很小的安全问题也可能导致灾难性的故障，这项基础研究将为自动化和可扩展的检查提供严格的技术和工具。