|
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.
|
TWC: Small: Memory Analysis and Machine-Code Verification Techniques for Multiprocessor Systems