SHF: Small: Collaborative Research: Reusable Tools for Formal Modeling

最近在程序验证方面的进展表明，我们即将能够证明安全和安全关键软件系统的正确性。但是，证明仅建立了关于代码在其上执行的底层处理器的模型的正确性。不幸的是，该社区缺乏广泛使用的处理器的高保真、经过仔细测试的规格，例如英特尔的x86系列处理器。这严重限制了使软件可靠和安全的努力，从软件保证到恶意软件分析再到沙箱技术。该项目的目标是为构建、推理和验证广泛使用的处理器的模型提供工具。拟议的研究将导致公共处理器的公开规范，这将使广泛的软件应用受益。它将有助于提高关键软件应用程序的可靠性和安全性。研究人员构建处理器模型的方法是精心设计的，以支持跨不同体系结构和不同应用程序的组件重用。特别是，他们建议将两种特定于领域的语言形式化，这将使指定解码器和指令语义变得容易。这些语言的工具将包括对高效执行的支持，以便可以针对实现测试模型。为了证明这些工具的有效性，研究人员将构建并验证x86和ARM系列处理器的模型。他们还将研究这些模型的应用，为内联引用监控器构建验证器的正确性证明，并将它们整合为经过验证的编译器的目标语言。研究人员计划为正式的处理器模型建立一个研究人员社区，并让这个社区参与到提供反馈、改进和使用模型的工作中。该项目还将为培训本科生和编写有关正规方法的新课程材料提供极好的机会。

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.