Dissertação

{en_GB=Secure Storage with a Small, Verified TCB} {} EVALUATED

{pt=Nos sistemas de armazenamento atuais, polı́ticas relativas aos dados guardados são mantidas por relações complexas entre múltiplas camadas de software não verificado e com possı́veis defeitos. Por exemplo, na maioria dos sistemas operativos, as polı́ticas de ficheiros são mantidas pelo sistema operativo, ligado a dispositivos de armazenamento onde o sistema de ficheiros e os dados estão guardados. Consequentemente, as polı́ticas podem não ser mantidas no caso de falhas do sistema operativo ou outros componentes nesta cadeia de confiança. Neste trabalho apresentamos Secure Verified Storage (SVS), uma arquitectura de armazenamento e firmware para SSD formalmente verificado que garante polı́ticas de dados na camada de armazenamento, completamente independente do sistema operativo e sistemas de ficheiros em camadas superiores. Isto garante que no caso de uma falha numa componente num nı́vel superior, propriedades relativas à confidencialidade e integridade dos dados guardados são mantidas. Implementamos o firmware em C e assembly ARM em 8000 linhas de código, utilizando uma versão alterada da biblioteca mbedtls para obter SSL sobre ATA e suportar multi-operações atómicas através de uma API de batches. Para além da arquitectura de SVS e uma implementação totalmente funcional, propomos técnicas sistemáticas para verificar propriedades sobre firmware de dispositivos embebidos com modelos de memória personalizados, que utilizamos para fazer uma verificação formal parcial de propriedades de SVS . Utilizando frama-c, provámos a segurança em runtime do firmware, a correção funcional de algumas estruturas de dados e provamos ainda a integridade e confidencialidade do nosso firmware relativamente à API de leitura e escrita ATA., en=In today’s storage systems, policies related to stored data are maintained by complex relations of multiple levels of non-bug-free, unverified software. For instance, on most operating systems, filesystem policies are maintained and checked by the operating system connected to the storage device(s) where the filesystem and data is stored. This leads to the policies not being maintained in case there are failures in the operating system or other unverified components in this chain of trust. In this work we propose Secure Verified Storage (SVS), a formally verified SSD firmware and storage architecture that enforces data policies at the storage layer, fully independent from the operating system and filesystems at upper levels. This ensures that in case of a fault of an upper component, properties related to confidentiality and integrity of data stored on SVS are maintained. We implemented the whole firmware in C that compiles to ARM in around 8000 LoC, making use of a custom version of the mbedtls library to provide SSL over ATA, and supporting atomic multi-operations through a batch API. Besides the SVS architecture and fully functional implementation, we propose systematic techniques to verify rich security properties of embedded devices firmware under custom memory models, and we used them to do a partial formal verification of confidentiality and integrity properties of SVS . By using frama-c, we proved runtime security of the firmware code, functional correctness of a few data structures, and proved integrity and confidentiality of our firmware with respect to the ATA read/write API}
{pt=Armazenamento Seguro, Firmware, Verificação e Sistema de Polı́ticas, Segurança, en=Secure Storage, Firmware, Verification and Policy System, Security}

Novembro 14, 2019, 8:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

Rodrigo Seromenho Miragaia Rodrigues

Departamento de Engenharia Informática (DEI)

Professor Catedrático

ORIENTADOR

Pedro Miguel dos Santos Alves Madeira Adão

Departamento de Engenharia Informática (DEI)

Professor Auxiliar