End-to-end security for hardware running verified software

Patent metadata

Field	Value
Publication number	US-9363087-B2
Application number	US-201414505236-A
Country	US
Kind code	B2
Filing date	Oct 2, 2014
Priority date	Oct 2, 2014
Publication date	Jun 7, 2016
Grant date	Jun 7, 2016

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

What is claimed is:

1. 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 to conform to a software specification, the software system including an operating system and a software application;
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 only to the software system;
sending first credentials signed by the secure hardware to the external application, wherein the first credentials identifies 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.

2. The one or more computer-readable memory storage devices of claim 1 , 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.

3. The one or more computer-readable memory storage devices of claim 1 , 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.

4. The one or more computer-readable memory storage devices of claim 1 , wherein verifying that the software system conforming to the software specification comprises:
determining that an assembly language implementation of the software system implements a functionally correct version of the software specification.

5. The one or more computer-readable memory storage devices of claim 1 , wherein verifying that the software system conforming to the software specification comprises:
demonstrating remote equivalence.

6. The one or more computer-readable memory storage devices of claim 5 , wherein demonstrating remote equivalence comprises:
determining a functional correctness of properties described in the software specification; and
proving noninterference between at least two components of the software system.

7. 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, the software system verified as conforming to a software specification, the software system including an operating system and a software application;
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 only 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.

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

9. The server of claim 7 , 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.

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

11. The server of claim 7 , 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.

12. The server of claim 7 , 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.

13. The server of claim 12 , wherein:
the server comprises secure hardware; and
the verifying further comprises demonstrating secure remote equivalence.

14. The server of claim 7 , wherein the acts further comprise:
verifying that a first component of the software system is incapable of subverting a second component of the software system before determining that the software system conforms to a specification.

15. 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 to conform to a software specification, wherein the software system includes an operating system and a software application, and wherein the public key corresponds to a private key that is known only 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 being executed by the secure hardware.

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

17. The computer-implemented method of claim 15 , further comprising:
demonstrating remote equivalence between the software system and the software specification.

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

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

20. The computer-implemented method of claim 15 , 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
• Microsoft Technology Licensing Inc

Inventors

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

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

• H04L9/0825

  using asymmetric-key encryption or public key infrastructure [PKI], e.g. key signature or public key certificates · 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