Verified Secure Computing using Trusted Hardware

Опубликовано 4 апреля 2017, 21:32

Security-critical applications constantly face threats from exploits in lower computing layers
such as the OS and Hypervisor, or even attacks from malicious datacenter insiders.
In order to protect sensitive data from such privileged adversaries, there is increasing development
of secure hardware primitives, such as Intel SGX, ARM TrustZone, and Sanctum RISCV extensions.
These hardware primitives enable applications to place trusted code and data into memory regions that are isolated
from all other software on the machine, and also implement cryptographic primitives for attested remote execution.
Our research explores building cloud applications with provable security guarantees,
including only these hardware primitives (i.e. nearly zero software) in the trusted computing base.
In this talk, I will demonstrate compiler and verification techniques to develop applications that can be certified
(at the level of machine code) to not leak secrets, both via their outputs and certain side channels.
Furthermore, I will show how formal models of the hardware platforms can be leveraged to provide convenient
programming abstractions, and port programs and their correctness proofs across different hardware platforms.

See more on this video at microsoft.com/en-us/research/v...