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 Tools annual

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 monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

Modern processors can offer hardware primitives that allow a process to runin isolation. These primitives implement a trusted execution environment (TEE)in which a program can run such that the integrity and confidentiality of itsexecution are guaranteed. Intel's Software Guard eXtensions (SGX) is an exampleof such primitives and its isolated processes are called \emph{enclaves}. Theseguarantees, however, can be easily thwarted if the enclave has not beenproperly designed. Its interface with the untrusted software stack is arguablythe largest attack surface that adversaries can exploit; unintendedinteractions with untrusted code can expose the enclave to memory corruptionattacks, for instance. In this paper, we propose a notion of an \emph{orderly}enclave which splits its behaviour into several execution phases each of whichimposes a set of restrictions on accesses to untrusted memory, phasetransitions and registers sanitisation. A violation to these restrictionsindicates an undesired behaviour which could be harnessed to perpetrate attacksagainst the enclave. We also introduce \Analyser{}: a tool that uses symbolicexecution to carry out the validation of an enclave against our notion of anorderly enclave; in this process, it also looks for some typicalmemory-corruption vulnerabilities. We discuss how our approach can prevent andflag enclave vulnerabilities that have been identified in the literature.Moreover, we have evaluated how our approach fares in the analysis of somepractical enclaves. \Analyser{} was able to identify real vulnerabilities onthese enclaves which have been acknowledged and fixed by their maintainers.

Guardian: symbolic validation of orderliness in SGX enclaves