Verificando a Confidencialidade e Integridade da Memória em Ambientes de Execução Confiável Intel TDX

A criptografia é amplamente utilizada para proteger a confidencialidade dos dados quando estão em trânsito ou em repouso. No entanto, a criptografia por si só não é suficiente para garantir a confidencialidade dos dados em uso. Um Ambiente de Execução Confiável (TEE) proporciona garantia de três propriedades principais: confidencialidade dos dados, integridade dos dados e integridade do código para dados em uso. Isso é feito através da habilitação de isolamento e armazenamento seguro dentro de um sistema. É um grande desafio verificar os requisitos de segurança em um TEE, uma vez que o isolamento e o armazenamento seguro exigem interação complexa entre diferentes componentes, como o sistema operacional, hipervisor, firmware e hardware. Neste artigo, realizamos uma análise de segurança abrangente das Extensões de Domínio de Confiança da Intel (TDX) para confidencialidade e integridade da memória. Especificamente, analisamos a arquitetura Intel TDX para derivar invariantes. Geramos afirmações de segurança (propriedades) para os invariantes com base na análise de Máquinas de Estado Finito (FSM). Utilizamos verificação de modelo para validar as propriedades de segurança. Também realizamos análise estática do código TDX para verificar várias vulnerabilidades, incluindo estouro de buffer, segurança de ponteiros e questões aritméticas. Uma extensa avaliação experimental demonstra que nossa estrutura proposta é adequada para verificar a arquitetura Intel TDX. Também conseguimos identificar inconsistências na especificação do TDX.