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

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

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.