Automated verification of a software system

Patent metadata

Field	Value
Publication number	US-9536093-B2
Application number	US-201414505204-A
Country	US
Kind code	B2
Filing date	Oct 2, 2014
Priority date	Oct 2, 2014
Publication date	Jan 3, 2017
Grant date	Jan 3, 2017

Abstract

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).

First claim

What is claimed is:

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.

2. The computer-implemented method of claim 1 , further comprising:
verifying that a first component of the multiple components is incapable of subverting a second component of the multiple components.

3. The computer-implemented method of claim 1 , further comprising:
verifying an equivalence between an individual component of the multiple components and a corresponding state machine in the low-level specification.

4. The computer-implemented method of claim 1 , wherein:
the high-level specification includes:
at least one of a pre-condition, a post-condition, or a termination metric; and
one or more assertions identifying states associated with the software code; and

the computer-implemented method further comprises:
verifying a validity of the one or more assertions.

5. The computer-implemented method of claim 1 , wherein:
the software code includes an assertion regarding a plurality of states entered into by the software code.

6. The computer-implemented method of claim 5 , wherein verifying that the assembly language code performs the one or more functions comprises:
proving that the assertion regarding the plurality of states entered into by the software code is valid for all possible inputs.

7. The computer-implemented method of claim 1 , wherein:
the high-level specification comprises an idiomatic specification specifying feature subsets used by the software code.

8. The computer-implemented method of claim 1 , further comprising:
optimizing the assembly language code, the assembly language code using an intermediate verification language to describe proof obligations;
generating, by a verification engine, one or more verification conditions corresponding to the proof obligations based at least in part on the assembly language code; and
verifying, by a reasoning engine, the proof obligations.

9. A computing device comprising:
one or more processors; and
one or more memory storage devices to store instructions executable by the one or more processors to perform operations comprising:
receiving software code written in a high-level language, the software code comprising multiple components;
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 prevents secret data from being 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.

10. The computing device of claim 9 , wherein the operations further comprise:
receiving a line of the software code; and
verifying the line of the software code against the high-level specification.

11. The computing device of claim 9 , wherein the operations further comprise:
receiving a line of the software code that performs at least one function of the one or more functions; and
determining that the line of the software code fails to perform the at least one function; and
displaying an error message in which a failed precondition of the high-level specification is highlighted.

12. The computing device of claim 9 , wherein the operations further comprise:
receiving an edited portion of the software code that performs at least one function of the one or more functions; and
re-verifying that the edited portion of the software code performs the at least one function of the one or more functions.

13. The computing device of claim 9 , wherein the operations further comprise:
receiving a first file of the software code, the first file referencing an interface of a second file of the software code that was previously verified; and
importing the interface of the second file of the software code without re-verifying the second file.

14. The computing device of claim 9 , wherein the operations further comprise:
verifying that a first component of the multiple components is incapable of subverting a second component of the multiple components.

15. The computing device of claim 9 , wherein the operations further comprise:
analyzing multiple executions of a software application included in the software code;
comparing multiple outputs corresponding to the multiple executions; and
determining dependencies for all possible pairs of executions.

16. One or more memory storage devices to store instructions executable by one or more processors to perform operations comprising:
receiving software code written in a high-level language, the software code comprising multiple components;
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.

17. The one or more memory storage devices of claim 16 , wherein the operations further comprise:
proving a functional correctness of the software code; and
proving relational properties of the software code.

18. The one or more memory storage devices of claim 16 , wherein the high-level specification is expressed as at least one finite state machine.

19. The one or more memory storage devices of claim 16 , wherein the operations further comprise:
determining that the assembly language code implements a functionally correct version of the low-level specification.

20. The one or more memory storage devices of claim 16 , wherein the operations further comprise:
verifying a correctness of the software code by verifying each component of the multiple components, including verifying that a first component of the multiple components does not subvert other components of the

Assignees

• Microsoft Technology Licensing Llc

Inventors

• Hawblitzel Chris
• Parno Bryan
• Lorch Jacob R
• Howell Jonathan R
• Zill Brian D

Classifications

• G06F2221/033

  Test or assess software · CPC title

• G06F21/572 Primary

  Secure firmware programming, e.g. of basic input output system [BIOS] · CPC title

• G06F11/3604

  Analysis of software for verifying properties of programs (testing of software G06F11/3668) · CPC title

• G06F21/52 Primary

  during program execution, e.g. stack integrity {; Preventing unwanted data erasure; Buffer overflow} · CPC title

• G06F8/41

  Compilation · CPC title