End-to-end security for hardware running verified software

Patent metadata

Field	Value
Publication number	US-2016248592-A1
Application number	US-201615144200-A
Country	US
Kind code	A1
Filing date	May 2, 2016
Priority date	Oct 2, 2014
Publication date	Aug 25, 2016
Grant date	—

Abstract

A verified software system may be executable on secure hardware. Prior to being executed, the software system may be verified as conforming to a software specification. First credentials attesting to an identity of the software system may be sent to an external application. Second credentials signed by a provider of the secure hardware may be sent to the external application. The second credentials may attest to an identity of the secure hardware. The external application may securely exchange one or more messages with a software application of the software system. For example, the one or more messages may be decryptable only by the external application and the software application to provide confidentiality for each message. As another example, an attestation may vouch for an identity of a sender of each of the one or more messages to attest to an integrity of each message.

First claim

1 . (canceled)

2 . One or more computer-readable memory storage devices storing instructions that, when executed by one or more processors, program the one or more processors to perform acts comprising:
executing, by secure hardware, a software system that has been verified at an assembly language level to conform to a software specification, wherein the software system includes an operating system and a software application, and wherein a particular component of the software system is incapable of subverting other components of the software system; sending a public key from the software application to an external application that is external to the software system, wherein the public key corresponds to a private key that is known to the software system; sending first credentials signed by the secure hardware to the external application, wherein the first credentials indicate that the public key is associated with the software system; and sending second credentials comprising a second certificate signed using a second key by a provider of the secure hardware to the external application, the second credentials attesting to an identity of the secure hardware.

3 . The one or more computer-readable memory storage devices of claim 2 , wherein the acts further comprise:
sending a first message signed with the public key, the public key indicating that the first message was sent by the software system.

4 . The one or more computer-readable memory storage devices of claim 2 , wherein the acts further comprise:
receiving a second message signed using the public key, the second message readable by the software system but unreadable by other software systems.

5 . The one or more computer-readable memory storage devices of claim 2 , wherein the acts further comprise:
determining that an assembly language implementation of the software system implements a functionally correct version of a low-level version of the software specification.

6 . The one or more computer-readable memory storage devices of claim 2 , wherein the acts further comprise:
demonstrating remote equivalence between the software system and a low-level version of the software specification.

7 . The one or more computer-readable memory storage devices of claim 2 , wherein the acts further comprise:
determining a functional correctness of properties described in a low-level version of the software specification; and proving noninterference between at least two components of the software system.

8 . A server comprising:
one or more processors; and a memory device storing instructions executable by the one or more processors to perform acts comprising:
performing a verified boot of a software system that is verified at an assembly language level as conforming to a low-level software specification, wherein the software system includes an operating system and a software application, and wherein a particular component of the software system is incapable of subverting other components of the software system;
sending a public key from the software application to an external application that is external to the software system, the public key generated based on and corresponding to a private key that is known to the software system;
sending a first certificate signed by secure hardware to the external application, wherein the first certificate identifies that the public key is associated with the software system; and
sending a second certificate signed using a second key by a provider of the secure hardware to the external application, the second certificate attesting to an identity of the secure hardware.

9 . The server of claim 8 , wherein the acts further comprise:
determining that an assembly language implementation of the software system implements a functionally correct version of the low-level software specification.

10 . The server of claim 8 , wherein the acts further comprise:
sending a first message signed with the public key, the public key indicating that the first message was sent by the software system.

11 . The server of claim 10 , wherein the acts further comprise:
proving noninterference between at least two components of the software system.

12 . The server of claim 8 , wherein the acts further comprise:
sending a second message signed using the public key, the second message readable by the software system but unreadable by other software systems.

13 . The server of claim 8 , wherein the acts further comprise:
verifying that the software system conforms to a software specification before performing the verified boot of the software system, the verifying comprising demonstrating remote equivalence.

14 . The server of claim 8 , wherein:
the server comprises secure hardware.

15 . The server of claim 8 , wherein the acts further comprise:
determining a functional correctness of properties described in the low-level software specification.

16 . A computer-implemented method comprising:
receiving, by an external application that is external to a software system, a public key from the software system, the software system executed by secure hardware and verified at an assembly language level to conform to a low-level software specification, wherein the software system includes an operating system and a software application, wherein a particular component of the software system is incapable of subverting other components of the software system, and wherein the public key corresponds to a private key that is known to the software system; receiving, by the external application, first credentials signed by the secure hardware, wherein the first credentials attest that the public key is associated with the software system; receiving, by the external application, second credentials comprising a second certificate signed using a second key by a provider of the secure hardware attesting to an identity of the secure hardware; and authenticating, by the external application, the first credentials and the second credentials to determine that the public key was provided by the software system.

17 . The computer-implemented method of claim 16 , further comprising:
determining that an assembly language implementation of the software system implements a functionally correct version of the low-level software specification.

18 . The computer-implemented method of claim 16 , further comprising:
demonstrating remote equivalence between the software system and the low-level software specification.

19 . The computer-implemented method of claim 16 , further comprising:
determining that a system hash associated with the software system matches a previous hash that was provided before the software application began executing on the secure hardware.

20 . The computer-implemented method of claim 16 , further comprising:
receiving, from the software system, a first message signed with the public key; and authenticating, using the public key, that the first message was sent by the software application.

21 . The computer-implemented method of claim 16 , further comprising:
sending, to the software system, a second message signed with the public key, wherein the second message is decryptable using a private key maintained by the software application.

Assignees

• Microsoft Technology Licensing Llc

Inventors

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

Classifications

• G06F21/57 Primary

  Certifying or maintaining trusted computer platforms, e.g. secure boots or power-downs, version controls, system software checks, secure updates or assessing vulnerabilities · CPC title

• G06F2221/034

  Test or assess a computer or a system · CPC title

• H04L63/0823

  using certificates (cryptographic mechanisms or cryptographic arrangements for entity authentication involving certificates H04L9/3263) · CPC title

• H04L9/3247 Primary

  involving digital signatures · CPC title

• H04L9/3268

  using certificate validation, registration, distribution or revocation, e.g. certificate revocation list [CRL] · CPC title