Formal Verification of Confidentiality Guarantees in a Blinded Memory SoC

Thumbnail Image
Files
master_Sadri_Sinaki_Parsa_2024.pdf (988.2 KB)
Journal Title
Journal ISSN
Volume Title
Perustieteiden korkeakoulu | Master's thesis
Unless otherwise stated, all rights belong to the author. You may download, display and print this publication for Your own personal use. Commercial use is prohibited.
Author
Date
2024
Department
Major/Subject
Security and Cloud Computing
Mcode
SCI3113
Degree programme
Master’s Programme in Security and Cloud Computing (SECCLO)
Language
en
Pages
77+1
Series
Abstract
Outsourced computation has become a common practice, raising critical concerns about data privacy and security. These concerns include direct access to client data by the service provider or malicious entities on the server, which can expose sensitive information. Additionally, indirect access through side-channel vulnerabilities, such as attacks from other tenants on the server, poses a significant threat. The Blinded Memory (BliMe) architecture addresses these issues by implementing a hardware-enforced taint tracking policy, ensuring that sensitive data remains confidential and cannot be compromised even in the presence of malicious software or side-channel attacks. This thesis addresses the challenge of ensuring confidentiality in a System-on-a-Chip (SoC) implementing the BliMe architecture. This work models a BliMe system that supports multiple CPUs, accelerators, and various peripherals, all communicating through a shared bus. The model introduces a peripheral firewall that enables the integration of untrusted and I/O peripherals while preserving the system's confidentiality guarantees. Using the F* programming language, we formally verify that the modeled BliMe system maintains confidentiality across all system components. This thesis's contributions extend the BliMe architecture and introduce a model for BliMe systems that formally guarantees confidentiality in outsourced computation. The findings provide a foundation for future research in hardware security and formal verification.
Description
Supervisor
Gunn, Lachlan
Thesis advisor
Gunn, Lachlan
Keywords
blinded memory, formal verification, security, F*, BliMe, FStar
Other note
Citation
Permanent link to this item
https://urn.fi/URN:NBN:fi:aalto-202409016133
Collections
[dipl] Perustieteiden korkeakoulu / SCI