This thesis reports an investigation into authorisation models, as used in identity and access management. It proposes new versions of an authorisation model, the Tees Confidentiality Model (TCM), and presents formal specifications in B, and verifications and implementations of the key concepts using Spec Explorer, Spec# and LinQ. After introducing the concepts of authorisation and formal models, a formal methods specification in B of Role Based Access Control (RBAC) is presented. The concepts in RBAC have heavily influenced authorisation over the last two decades, and most of the research has been with their continued development. A complete re-working of the ANSI RBAC Standard is developed in B, which highlights errors and deficiencies in the ANSI Standard and confirms that B is a suitable method for the specification of access control. A formal specification of the TCM in B is then developed. The TCM supports authorisation by multiple concepts, with no extra emphasis given to Role (as in RBAC). The conceptual framework of Reference Model and Functional Specification used in the ANSI RBAC Standard is used to structure the TCM formal model. Several improvements to the original TCM are present in the formal specification, notably a simplified treatment of collections. This new variation is called TCM2, to distinguish it from the original model. Following this, a further B formal specification of a TCM reduced to its essential fundamental components (referred to as TCM3) was produced. Spec Explorer was used to animate this specification, and as a step towards implementation An implementation of TCM3 using LinQ and SQL is then presented, and the original motivating healthcare scenario is used as an illustration. Finally, classes to implement the versions of the TCM models developed in the thesis are designed and implemented. These classes enable the TCM to be implemented in any authorisation scenario. Throughout the thesis, model explorations, animations, and implementations are illustrated by SQL, C# and Spec# code fragments. These illustrate the correspondence of the B specification to the model design and implementation, and the effectiveness of using formal specification to provide robust code.

As enterprises migrate their data to cloud infrastructure, they increasingly need a flexible, scalable, and secure marketplace for collaborative data creation, analysis, and exchange among enterprises. Security is a prominent research challenge in this context, with a specific question on how two mutually distrusting data owners can share their data. Confidential Computing helps address this question by allowing to perform data computation inside hardware-based Trusted Execution Environments (TEEs) which we refer to as enclaves, a secured memory that is allocated by CPU. Examples of hardware-based TEEs are Advanced Micro Devices (AMD)-Secure Encrypted Virtualization (SEV), Intel Software Guard Extensions (SGX) and Intel Trust Domain Extensions (TDX). Intel SGX is considered as the most popular hardware-based TEEs since it is widely available in processors targeting desktop and server platforms. Intel SGX can be programmed using Software Development Kit (SDK) as development framework and Library Operating Systems (Library OSes) as runtimes. However, communication with software in the enclave such as the Library OS through system calls may result in performance overhead. In this project, we design confidential data transactions among multiple users, using Intel SGX as TEE hardware and Occlum as Library OS. We implement the design by allowing two clients as data owners share their data to a server that owns Intel SGX capable platform. On the server side, we run machine learning model inference with inputs from both clients inside an enclave. In this case, we aim to evaluate Occlum as a memory-safe Library Operating System (OS) that enables secure and efficient multitasking on Intel SGX by measuring two evaluation aspects such as performance overhead and security benefits. To evaluate the measurement results, we compare Occlum with other runtimes: baseline Linux and Graphene-SGX. The evaluation results show that our design with Occlum outperforms Graphene-SGX by 4x in terms of performance. To evaluate the security aspects, we propose 11 threat scenarios potentially launched by both internal and external attackers toward the design in SGX platform. The results show that Occlum security features succeed to mitigate 10 threat scenarios out of 11 scenarios overall. / När företag migrerar sin data till molninfrastruktur behöver de i allt högre grad en flexibel, skalbar och säker marknadsplats för gemensam dataskapande, analys och utbyte mellan företag. Säkerhet är en framstående forskningsutmaning i detta sammanhang, med en specifik fråga om hur två ömsesidigt misstroende dataägare kan dela sina data. Confidential Computing hjälper till att ta itu med den här frågan genom att tillåta att utföra databeräkning i hårdvarubaserad TEEs som vi kallar enklaver, ett säkert minne som allokeras av CPU. Exempel på maskinvarubaserad TEEs är AMD-SEV, Intel SGX och Intel TDX. Intel SGX anses vara den mest populära maskinvarubaserade TEEs eftersom det finns allmänt tillgängligt i processorer som riktar sig mot stationära och serverplattformar. Intel SGX kan programmeras med hjälp av SDK som utvecklingsram och Library Operating System (Library OSes) som körtid. Kommunikation med programvara i enklaven, till exempel Library OS via systemanrop, kan dock leda till prestandakostnader. I det här projektet utformar vi konfidentiella datatransaktioner mellan flera användare, med Intel SGX som TEE-hårdvara och Occlum som Library OS. Vi implementerar designen genom att låta två klienter som dataägare dela sina data till en server som äger Intel SGX-kompatibel plattform. På serversidan kör vi maskininlärningsmodell slutsats med ingångar från båda klienterna i en enklav. I det här fallet strävar vi efter att utvärdera Occlum som ett minnessäkert Library OS som möjliggör säker och effektiv multitasking på Intel SGX genom att mäta två utvärderingsaspekter som prestandakostnader och säkerhetsfördelar. För att utvärdera mätresultaten jämför vi Occlum med andra driftstider: baslinjen Linux och Graphene-SGX. Utvärderingsresultaten visar att vår design med Occlum överträffar Graphene-SGX av 4x när det gäller prestanda. För att utvärdera säkerhetsaspekterna föreslår vi elva hotscenarier som potentiellt lanseras av både interna och externa angripare mot designen i SGX-plattformen. Resultaten visar att Occlums säkerhetsfunktioner lyckas mildra 10 hotscenarier av 11 scenarier totalt.

Please read the abstract in the dissertation. / Dissertation (MSc)--University of Pretoria, 2009. / Chemical Engineering / unrestricted

<p>In today’s world, cloud machines store an ever-increasing amount of sensitive user data, but it remains challenging to guarantee the security of our data. This is because a cloud machine’s system software—critical components like the operating system and hypervisor that can access and thus leak user data—is subject to attacks by numerous other tenants and cloud administrators. Trusted execution environments (TEEs) like Intel SGX promise to alter this landscape by leveraging a trusted CPU to create execution contexts (or enclaves) where data cannot be directly accessed by system software. Unfortunately, the protection provided by TEEs cannot guarantee complete data security. In particular, our data remains unprotected if a third-party service (e.g., Yelp) running inside an enclave is adversarial. Moreover, data can be indirectly leaked from the enclave using traditional memory side-channels.</p> <p><br></p> <p>This dissertation takes a significant stride towards strong user data protection in cloud machines using TEEs by defeating the critical threats of adversarial cloud services and memory side-channels. To defeat these threats, we systematically explore both software and hardware designs. In general, we designed software solutions to avoid costly hardware changes and present faster hardware alternatives.</p> <p><br></p> <p>We designed 4 solutions for this dissertation. Our Chancel system prevents data leaks from adversarial services by restricting data access capabilities through robust and efficient compiler-enforced software sandboxing. Moreover, our Obliviate and Obfuscuro systems leverage strong cryptographic randomization and prevent information leakage through memory side-channels. We also propose minimal CPU extensions to Intel SGX called Reparo that directly close the threat of memory side-channels efficiently. Importantly, each designed solution provides principled protection by addressing the underlying root-cause of a problem, instead of enabling partial mitigation.</p> <p><br></p> <p>Finally, in addition to the stride made by our work, future research thrust is required to make TEEs ubiquitous for cloud usage. We propose several such research directions to pursue the essential goal of strong user data protection in cloud machines.</p>