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

点击翻译按钮获取中文摘要

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.