This is the code for the master's thesis: "Design and Verification of extensible Intel SGX entry code" at the KU Leuven (faculty of Engineering - Computer Science - Distrinet).
Supervisor: Prof. dr. Ir. Frank Piessens
Assistant-Supervisors: dr. Raoul Strackx, dr. Ir. Neline van Ginkel, Ir. Kobe Vrancken
- We simplified the Fortanix EDP entry code. This was done by eliminating all conditional branching in the assembly code. By doing this, as much code as possible was translated to the higher-level Rust language.
- We improved the extensibility of the code. The use of the Rust programming language facilitizes code extension.
- Using a benchmark, we show that the performance of the modified entry code is similar to the original.
- We show that the simplified ABI-layer still provides substantial security guarantees. This is shown by using the Angr binary analysis framework in combination with Rust’s strong security guarantees.
- We give an extensive overview of the current state of Rust verifiers.
This repo has been divided into a few folders. Each of these folder has its own use case. More information is available within each folder in the form of a README.
This folder contains the files needed to prove certain safety principles about the entry code. It uses angr, a binary analysis framework written in Python.
This file contains a script that automatically scans the entry code for certain "code simplicity metrics".
This file contains code that was used to create timing benchmarks.
This file contains the actual entry code.
The standard Rust license (i.e. both the MIT license and the Apache License (Version 2.0)) has been followed where possible.
Note: the folder containing the angr code is licensed under the GNU Affero General Public License.