This time, on a different note. This is a joint work with Pedro Antonino, Senior Research Scientist at the Blockhouse Technology Limited, and A. W. Roscoe, Professor of Computing Science at Oxford University, Senior Research Fellow in Computer Science at University College Oxford, Director of the University College Oxford Blockchain Research Centre, and Founder and Director of the Blockhouse Technology Limited. We began and undertook this work over the past months, before long I took up a position of Software Engineer at the Blockhouse Technology Limited back in May 2020.
- P. Antonino, W. A. W. l, and A. W. Roscoe, “Guardian: symbolic validation of orderliness in sgx enclaves.” 2021.
[Bibtex]@inproceedings{AntoninoWoloszynRoscoe:Guardian:-symbolic-validation-of-orderliness-in-SGX-enclaves, archiveprefix = {arXiv}, author = {Pedro Antonino and Wojciech Aleksander Wo{\l}oszyn and A. W. Roscoe}, date-added = {2021-05-15 17:10:14 +0200}, date-modified = {2021-05-15 17:10:14 +0200}, eprint = {2105.05962}, journal = {Computer Science arXiv}, keywords = {under-review}, note = {Under review}, primaryclass = {cs.CR}, title = {Guardian: symbolic validation of orderliness in SGX enclaves}, year = {2021}}
Abstract. Modern processors can offer hardware primitives that allow a process to run in isolation. These primitives implement a trusted execution environment (TEE) in which a program can run such that the integrity and confidentiality of its execution are guaranteed. Intel’s Software Guard eXtensions (SGX) is an example of such primitives and its isolated processes are called enclaves. These guarantees, however, can be easily thwarted if the enclave has not been properly designed. Its interface with the untrusted software stack is arguably the largest attack surface that adversaries can exploit; unintended interactions with untrusted code can expose the enclave to memory corruption attacks, for instance. In this paper, we propose a notion of an orderly enclave which splits its behaviour into several execution phases each of which imposes a set of restrictions on accesses to untrusted memory, phase transitions and registers sanitisation. A violation to these restrictions indicates an undesired behaviour which could be harnessed to perpetrate attacks against the enclave. We also introduce Guardian: a tool that uses symbolic execution to carry out the validation of an enclave against our notion of an orderly enclave; in this process, it also looks for some typical memory-corruption vulnerabilities. We discuss how our approach can prevent and flag enclave vulnerabilities that have been identified in the literature. Moreover, we have evaluated how our approach fares in the analysis of some practical enclaves. Guardian was able to identify real vulnerabilities on these enclaves which have been acknowledged and fixed by their maintainers.
Follow through the arXiv for a pdf of the article and access the Guardian source code at GitHub.
- P. Antonino, W. A. W. l, and A. W. Roscoe, “Guardian: symbolic validation of orderliness in sgx enclaves.” 2021.
[Bibtex]@inproceedings{AntoninoWoloszynRoscoe:Guardian:-symbolic-validation-of-orderliness-in-SGX-enclaves, archiveprefix = {arXiv}, author = {Pedro Antonino and Wojciech Aleksander Wo{\l}oszyn and A. W. Roscoe}, date-added = {2021-05-15 17:10:14 +0200}, date-modified = {2021-05-15 17:10:14 +0200}, eprint = {2105.05962}, journal = {Computer Science arXiv}, keywords = {under-review}, note = {Under review}, primaryclass = {cs.CR}, title = {Guardian: symbolic validation of orderliness in SGX enclaves}, year = {2021}}
