Formal Verification of EDP Enclave Entry & Exit Code

Without the use of confidential computing platforms, data is increasingly difficult to protect. This challenge becomes complex in situations with different owners of either code or data. Take for example hospitals and companies that provide healthcare systems that wish to collaborate and develop AI without explicitly sharing patient data or the AI model. There are multiple stakeholders involved: the hospitals, the AI company, the cloud provider that hosts the platform, the operating system vendor, and many others. With a hierarchical security model, the trusted computing base (TCB) runs quickly into millions of lines of code. Chances of patient data or the AI model leaking will be too large for many stakeholders to put this scenario into practice. By using confidential computing either party can guarantee the confidentiality of data.

Confidential computing platforms such as Intel SGX (Software Guard eXtensions) can provide strong security guarantees to support these use cases. Such platforms enable software components called enclaves to be created with zero trust in system software. Even when an attacker manages to infect privileged software such as the operating system or the hypervisor, the security guarantees of enclaves remain intact. Only software running within the enclave needs to be trusted.

Fortanix’ Enclave Development Platform (EDP) provides a straightforward way for programmers to develop trustworthy enclaves using the Rust programming language. EDP elevates hardware features provided by Intel SGX to higher-level programming language constructs. This ensures that software engineers do not need to know all intrinsic details of Intel SGX. The security features provided by SGX and EDP were the subject of a previous blog post.

Impact of Incomplete Enclave Entry and Exit code

EDP bridges hardware-level security guarantees and software constructs. In this article we focus only on the security measures around enclave entries and exits. When an enclave is called (see Figure 1, step 1), the processor verifies only an extremely limited set of its state. For example, the processor ensures that one of the entry points defined at compile time is called. But it is up to enclave code to ensure that processor features it depends on, are in the correct state. EDP ensures this by sanitizing the entire processor state (step 2) before turning execution control over to the enclave author’s Rust code (step 3). Any mistake in this glue code may inadvertently enable an attacker to extract sensitive information from the enclave. As this code is shared by all enclaves build with EDP, its correctness is paramount.

Enclave Entry and Exit code

Figure 1: EDP entry code sanitizes the processor state within the enclave before the developer’s Rust code gets executed. Similarly, EDP exit code removes potentially sensitive data before execution control is returned to the surrounding process.

As an example of what EDP needs to ensure, consider the processor’s #DF (direction flag) in the rflags register. At the Rust code level it is assumed that this flag is clear by default. The Rust compiler will not produce code to clear this flag before emitting string operations. Intel SGX does not verify nor change this flag when an enclave is called and may thus be under control of an attacker. The state of this flag, however, affects the behavior of the enclave code significantly. String operations will operate forward when the direction flag is set and backward when it is cleared. It is thus paramount that EDP resets this flag before control is transferred to Rust code. Failure to do so may lead to incorrect computations and exposure of sensitive data.

Similarly, when it is required for computation, the Rust compiler may emit code to copy sensitive data such as cryptographic keys from enclave memory to a processor register. It will, however, not overwrite this register when computation finishes. Nor will Intel SGX erase processor state by default when enclaves are exited. It is up to EDP to properly sanitize processor state (step 4) before exiting the enclave (step 5).

Formal Verification

Security vulnerabilities in EDP may affect the security of all enclaves build with it. To provide strong security guarantees to developers we turned to formal verification of enclave entry and exit code. We have collaborated [2] with Ulviyya Mammadzada (KU Leuven) under the mentorship of Msc. Kobe Vrancken (KU Leuven), Dr Raoul Strackx (Fortanix), and the supervision of Prof. Dr. Frank Piessens to formally verify EDP’s entry and exit code.

Verification was performed in two steps. First, a formal model was built of the enclave’s entry and exit code. This model allowed us to track changes to the processor and memory state for every executed assembly instruction. Second, the Verifast verifier was used to verify the functional correctness of the model. Based on lessons learned from earlier academic work [1], we verified that EDP provides the following guarantees. (i) When the processor starts executing Rust code it is in the state assumed by the Rust compiler. An attacker cannot influence the processor state such as controlling the direction flag. (ii) Upon enclave exit processor state is overwritten completely with non-sensitive data, except for data returned explicitly by the enclave. (iii) Only memory areas reserved by EDP for entry/exit code are accessed. Memory regions used by the enclave itself will thus not be modified by an enclave exit.

The Verifast verifier uses symbolic execution to guarantee that the asserted conditions will always hold. In contrast to using fuzzers where only a subset of the search space is checked, symbolic execution ensures that the entire search space is covered. This gives much stronger evidence that the specified conditions hold. The verification was done on EDP code already used in production enclaves. No problems with the existing code were discovered. When EDP’s entry or exit needs updating (e.g., to add new features), the model and proof will need to be updated as well. We may automate this process in the future. EDP is the first enclave SDK to be able to provide such formal guarantees.

Conclusion

Confidential computing platforms are designed to provide strong security guarantees to sensitive data and code. This can only be achieved through secure SDKs. At Fortanix we developed EDP to provide software engineers the tools to build trustworthy enclaves. Fortanix’ Enclave Development Platform is the only development kit for SGX whose enclave entry and exit code has been formally verified.

References

EDP Product Page

Share this post:

Get our blog updates in your inbox: