Automated verification of a software system

摘要

Software code of a software system (e.g., a software stack) may be verified as conforming to a specification. A high-level language implementation of the software system may be compiled using a compiler to create an assembly language implementation. A high-level specification corresponding to the software system may be translated to a low-level specification. A verifier may verify that the assembly language implementation functionally conforms to properties described in the low-level specification. In this way, the software system (e.g., a complete software system that includes an operating system, device driver(s), a software library, and one or more applications) may be verified at a low level (e.g., assembly language level).

主权项

1. A computer-implemented method comprising:
receiving software code written in a high-level language, the software code comprising multiple components including an operating system and at least one application; compiling the software code to create assembly language code corresponding to the software code; receiving a high-level specification specifying one or more functions performed by the software code; generating a low-level specification based at least in part on the high-level specification; verifying that an output of the assembly language code does not enable secret data to be determined, the secret data comprising one or more private keys; verifying that the assembly language code behaves in accordance with the low-level specification to perform the one or more functions specified by the high-level specification; and providing an indication that the assembly language code has been verified to perform the one or more functions.