English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Hardware support for isolated execution (e.g., ARM TrustZone) enables the development of a trusted execution environment (TEE) that ensures the security of the code and data while communicating with a compromised rich execution environment (REE). The ability to satisfy various security services is complicated and usually consists of trusted applications, a trusted kernel and a secure monitor. However, formally verifying the security of an entire TEE security remains challenging. We present a methodology for designing a TEE in a way that enables verification of its security properties. Our methodology consists of forcing a trusted application and kernel to communicate with an REE via a narrow interface and compile and link them with a small secure monitor that implements the interface and runs at the highest privilege level. We provide functional verification of the secure monitor to ensure that it correctly switches the TEE/REE, communicates with the REE at a pre-defined memory space and has no integer overflow vulnerability. We also perform a verification of the secure monitor's scheduler to ensure that it satisfies information flow noninterference. We present a modular verification framework that can prove an end-to-end security property for cross-language programmes (e.g., C and assembly languages). Our evaluation suggests that the methodology scales to real-world TEE applications.

A Design and Verification Methodology for a TrustZone Trusted Execution Environment