Miyaji Laboratory

Trusted Execution Environment (TEE) is one of the isolation environment technologies that aim to protect sensitive data in the base system such as firmware and OS. However, many TEEs are implemented using C, a Turing-complete programming language. Thus, removing the risk of memory management is an issue. Also, a BOOMERANG bug that allows unauthorized access to system information of a general- purpose OS has been reported due to the TEE structure. As a solution to this, we built Baremetalisp TEE, which is implemented in Rust, a memory-safe programming language, and made BLisp, an API definition language for TEE. BLisp is based on the concept of an effect system, which prevents unintended behavior by explicitly describing the I/O of data and functions. In addition, we built a program to transpile BLisp to Coq in order to enable formal verification of BLisp code. Furthermore, to enable dynamic updating of the system, we implemented the functionality to incorporate external functions into BLisp. As a result, we created a TEE Shell that can dynamically update its functions while guaranteeing memory safety and semantic correctness.