Recent advances in program verification show that we are on the verge of being able to prove correctness of safety and security critical software systems. But the proofs only establish correctness with respect to a model of the underlying processor on which the code executes. Unfortunately, the community lacks high-fidelity, carefully tested specifications of widely-used processors, such as Intel's x86 family of processors. This severely limits efforts in making software reliable and secure, from software assurance to malware analysis to sandboxing technologies. The goal of this project is to provide tools for building, reasoning about, and validating models of widely-used processors. The proposed research will result in public specifications of common processors, which will benefit a wide range of software applications. It will help improve the dependability and security of critical software applications.
The investigators' approach to building processor models is carefully designed to support reuse of components across different architectures and different applications. In particular, they propose to formalize two domain-specific languages that will make it easy to specify decoders and instruction semantics. The tools for these languages will include support for efficient execution so that the models can be tested against implementations. To demonstrate the efficacy of these tools, the investigators will build and validate models of both the x86 and ARM families of processors. They will also investigate applications of these models by building correctness proofs of verifiers for inlined reference monitors and by integrating them as the target languages of a verified compiler. The investigators plan to expend efforts on building a community of researchers for formal processor models and to involve this community to give feedback, improve, and use the models. The project will also provide excellent opportunities for training undergraduate students and for developing new curriculum materials on formal methods.
