Verificação de Modelos e Propriedades de Controle de Acesso Mandatório

Os mecanismos de controle de acesso mandatório (MAC) controlam quais usuários ou processos têm acesso a quais recursos em um sistema. As políticas de MAC estão sendo cada vez mais especificadas para facilitar o gerenciamento e a manutenção do controle de acesso. No entanto, a especificação correta das políticas é um problema muito desafiador. Para capturar formal e precisamente as propriedades de segurança às quais o MAC deve aderir, os modelos de MAC são geralmente escritos para preencher a lacuna de abstração entre políticas e mecanismos. Neste artigo, propomos uma abordagem geral para verificação de propriedades para modelos de MAC. A abordagem define uma estrutura padronizada para modelos de MAC, permitindo tanto a verificação de propriedades quanto a geração automatizada de casos de teste. A abordagem expressa modelos de MAC na linguagem de especificação de um verificador de modelos e expressa propriedades genéricas de controle de acesso na linguagem de propriedades. Em seguida, a abordagem utiliza o verificador de modelos para verificar a integridade, cobertura e confinamento dessas propriedades para os modelos de MAC e, por fim, gera casos de teste por meio de um arranjo combinatório de cobertura para as implementações do sistema dos modelos.