Automated verification of a software system

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 multiple components.