TWC: Small: Memory Analysis and Machine-Code Verification Techniques for Multiprocessor Systems

由于硬件和软件的复杂性不断增加，确保高级程序的可靠性变得越来越困难。 该项目将开发允许程序员通过机器代码分析来机械验证软件的工具。拟议的研究将同样推进软件分析科学，以及能够执行工业软件验证的严格工具的开发。这些工具正被工业界积极用于硬件规格和分析。拟议的研究将同样推进软件分析科学，以及能够执行工业软件验证的严格工具的开发。这些工具对于验证诸如医疗、金融和运输系统等系统的安全属性特别重要。该项目通过使用x86处理器的指令集架构（伊萨）规范来机械验证用户级机器代码程序，从而扩展了现有的规范和分析工作。该规范扩展到允许验证多处理器/多线程程序和操作系统代码。 目标是确保多处理器上的程序在行为、安全和资源需求方面是正确的。重点是一个单一的机器代码模型，因为这可能足以分析所有的程序，无论源语言，只要他们编译到支持的处理器平台。 这消除了针对不同来源的软件构建、维护和验证不同验证框架的需要。 机器代码在具有复杂存储器层次结构的当代计算机系统上执行：存储器语义由于高速缓存、存储器保护机制、多处理器/多线程存储器共享、存储缓冲器、事务存储器机制、存储器同步机制和存储器更新延迟而变得复杂。这种复杂性导致了重要的内存相关的研究问题，将得到解决，以便对机器代码程序执行的原因。 例如地址转换的正确性（包括访问权限管理）和实际内存一致性模型的形式化。 这远远超出了现有静态分析工具为解决这类问题所提供的能力。

Due to the ever-increasing complexity of both hardware and software, it is becoming harder to ensure the reliability of high-level programs. The project will develop tools that permit programmers to mechanically verify software via machine-code analysis. The proposed research will similarly advance the science of software analysis, together with the development of rigorous tools capable of performing industrial software verification. The tools are actively being used by industry for hardware specification and analysis. The proposed research will similarly advance the science of software analysis, together with the development of rigorous tools capable of performing industrial software verification. The tools are important in particular for verifying security properties of systems such as medical, financial, and transportation systems. The project extends existing specification and analysis efforts by using the specification of the x86 processor's instruction-set architecture (ISA) to mechanically verify user-level machine-code programs. The specification is extended to allow verification of multiprocessor/multi-threaded programs and operating system code. The goal is a capability to ensure that programs hosted on multiprocessors are correct with respect to behavior, security, and resource requirements. The focus is on a single machine-code model, since that can be sufficient for analyzing all programs, irrespective of the source language, as long as they compile down to the supported processor platform. This eliminates the need to build, maintain, and validate different verification frameworks targeting software from different sources. Machine code executes on contemporary computer systems with complex memory hierarchies: memory semantics are complicated by caches, memory protection mechanisms, multiprocessor/multithread memory sharing, store buffers, transactional memory mechanisms, memory synchronization mechanisms, and memory update delays. This complexity leads to important memory-related research issues that will be addressed in order to reason about machine-code program execution. Examples are the correctness of address translation (including access rights management) and the formalization of a realistic memory consistency model. This goes well beyond capabilities provided by existing static-analysis tools in order to address these sorts of problems.