Automated Verification of a Software System

• US 20160098562A1
• Filed: 10/02/2014
• Published: 04/07/2016
• Est. Priority Date: 10/02/2014
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Hawblitzel, Chris, Lorch, Jacob R., Howell, Jonathan R., Zill, Brian D., Parno, Bryan
• Granted Patent: US 9,536,093 B2
• Time in Patent Office: Days
• US Class Current: 1/1
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 21/52 during program execution, e.g. stack integrity ; Preventing unwanted data erasure; Buffer overflow
• CPC Class Codes: G06F 21/572 Secure firmware programming, e.g. of basic input output system [BIOS]
• CPC Class Codes: G06F 2221/033 Test or assess software
• CPC Class Codes: G06F 8/41 Compilation

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

Claims

1-20. -20. (canceled)

21. A computer-implemented method 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 the assembly language code performs the one or more functions; and

providing an indication that the assembly language code has been verified to perform the one or more functions.

22. The computer-implemented method of claim 21, further comprising:

verifying that a first component of the multiple components is incapable of subverting a second component of the multiple components.

23. The computer-implemented method of claim 21, further comprising:

verifying an equivalence between an individual component of the multiple components and a corresponding state machine in the low-level specification.

24. The computer-implemented method of claim 21, wherein the high-level specification includes at least one of a pre-condition, a post-condition, or a termination metric.

25. The computer-implemented method of claim 21, wherein:

the software code includes an assertion regarding a plurality of states entered into by the software code.

26. The computer-implemented method of claim 25, 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.

27. The computer-implemented method of claim 21, wherein:

the high-level specification comprises an idiomatic specification specifying feature subsets used by the software code.

28. The computer-implemented method of claim 21, further comprising:

optimizing the assembly language code.

29. 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 the assembly language code performs the one or more functions; and

providing an indication that the assembly language code has been verified to perform the one or more functions.

30. The computing device of claim 29, 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.

31. The computing device of claim 29, 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.

32. The computing device of claim 29, 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.

33. The computing device of claim 29, 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.

34. The computing device of claim 29, wherein the operations further comprise:

verifying that a software application included in the software code provides outputs that do not enable secret data to be determined, the secret data comprising one or more private keys.

35. The computing device of claim 29, 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.

36. 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 the assembly language code performs the one or more functions; and

providing an indication that the assembly language code has been verified to perform the one or more functions.

37. The one or more memory storage devices of claim 36, wherein the operations further comprise:

proving a functional correctness of the software code; and

proving relational properties of the software code.

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

39. The one or more memory storage devices of claim 36, wherein the operations further comprise:

determining that the assembly language code implements a functionally correct version of the low-level specification.

40. The one or more memory storage devices of claim 36, 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 multiple components.