Post on 12-Nov-2020
transcript
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Veri�cação Formal de Kernel
Glauber Módolo Cabral
Universidade Estadual de Campinas - UNICAMPInstituto de Computação - ICMO806 - Tópicos em Sistemas Operacionais
Seminário
Outubro de 2007
1 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Roteiro
Introdução
Veri�cação Formal de Kernel
seL4
Formalização e Veri�cação
Referências
[EKD+07][EKK06][TKH05][KNEH07]
2 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Haskell
I Linguagem funcional de programação: Implementa osconceitos de λ-Cálculo (programação através de aplicações defunções);
I Fortemente tipi�cada: todo elemento possui tipo (pré-de�nidoou calculado automaticamente no contexto);
I Avaliação preguiçosa: um argumento de uma função só éavaliado quando é usado no cálculo;
I Pura: não permite alterar o estado do sistema (efeitoscolaterais) a menos das partes envolvidas no cálculo de umafunção.
I Mônadas são utilizadas para seqüenciar operações com efeitoscolaterais, encapsulando as alterações;
I Literate Haskell: permite documentação em LATEXjunto aocódigo.
3 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
De�nições
Veri�cação formal
Técnica que visa a garantir, através de provas matemáticas, queum programa comporta-se da forma especi�cada.
Micro-kernelKernel projetado para ser mínimo em tamanho de código e emfunções providas.
4 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Problemas
Kernel
I Desenvolvimento bottom-up;I Código muito grande;I Interfaces de alto-nível sofrem alterações para acomodar
código de mais baixo-nível durante o desenvolvimento;
Veri�cação Formal
I Desenvolvimento top-down;I Ausência de escalabilidade nas técnicas;I Ausência de provadores e�cientes para projetos grandes;I Veri�car programas com efeitos colaterais é complicado.
5 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Abordagem dos programadores de kernel
6 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Abordagem de métodos formais
7 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Vantagens
I É a unica maneira de garantir a con�abilidade de um kernelpra todo evento possível;
I Garante a ausência de erros de software;I Com as ferramentas atuais, o custo mantém-se na mesma
ordem de grandeza em relação às técnicas tradicionais;
8 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
seL4 - Secure Embedded L4
De�nição
I Derivado do micro-kernel L4;I Criado para provêr uma base segura para o desenvolvimento de
sistemas embarcados;
Objetivos de segurança
I Controle da comunicação entre aplicações:I garantir isolamento entre sub-sistemasI garantir isolamento das informações de uma aplicação em
relação a outras.
I Gerenciamento da memória física utilizada pelo kernel:I garantir disponibilidade de memória para serviços do kernel;I prevêr o tempo de execução das operações.
9 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
seL4 - Visão Geral
10 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
seL4 - Propriedades Desejadas na Metodologia
I API com especi�cação precisa, em oposição a descrições feitasem linguagem natural e em forma de manuais;
I Expôr detalhes de implementação para mostrar a possibilidadede uma implementação de alta performance;
I Permitir a construção de sistemas mais complexos usando aAPI resultante;
I Permitir formalização do sistema;I Tornar possível o uso da metodologia por programadores de
kernel, não adeptos a métodos formais.
11 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
seL4 - Metodologia empregada (1)
I Literate Haskell: especi�cação e implementação da API;I Protótipo escrito em Haskell;I Validação através de um emulador ARM: binários de códigos
em C são executados sobre o kernel;
Justi�cativa
I Haskell não permite efeitos colaterais;I Permite explorar detalhes de implementação de maneira fácil.
12 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Metodologia empregada (2)
13 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Simulador ARM
14 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Problemas para a veri�cação
I Kernel grande (3000 loc);I Extensões do compilador GHC não possuem modelos formais;I Ferramentas existentes não fazem análise do código (Haskell +
HOL);I É possível não haver terminação (recursão in�nita);I Sistema de tipos de HOL é fraco para modelar mônadas de
forma abstrata.
15 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Soluções encontradas
Terminação
I Há pouca recursão;I Todas as chamadas de sistemas terminam;I Prova manual de terminação.
Mônadas
I Sistema de tipos de HOL permite modelar instâncias concretasde mônadas;
I Mônadas concretas bastam para modelar as propriedadesdesejadas;
I HOL possue uma sintaxe parecida com a de Haskell paraseqüenciar ações.
16 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Re�nando para código C
I C é bem conhecido pelos programadores de Kernel;I Permite otimizações posteriores;I Permite incluir Assembly para alta performance.
17 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Problemas em C evitados
I Pode-se assumir como dados os detalhes de máquina:endian-ness, comportamento dos operadores aritméticos,tamanho dos bytes (8 bits ou não);
I Ausência de efeitos colaterais permite ignorar a ordem deavaliação de expressões;
I Comportamentos inde�nidos são ilegais: divisão por zero,escrever em memória não alocada;
I Aritmética de ponteiros: adicionar guardas para garantir que oresultado seja um endereço válido para o tipo de dado.
18 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Guardas
I Expressão booleana sobre os estados do programa;I Simulam veri�cações complicadas em tempo de execução;I Isabele/HOL exige que a guarda seja verdadeira sempre que o
código posterior estiver prestes a ser executado;I Flexibilidade na de�nição:
I Em sistemas onde o endereço zero guarda o início de um vetor
de exceções, escrita e leitura de ponteiros nulos devem ser
permitidos;I Escrita de memória não-alocada pode ser parte do gerenciador
de memória; a leitura ainda pode ser tratada como erro de
tempo de execução.
19 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Veri�cação formal
20 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Referências I
Kevin Elphinstone, Gerwin Klein, Philip Derrin, TimothyRoscoe, and Gernot Heiser.Towards a practical, veri�ed kernel.In Proc. 11th Workshop on Hot Topics in Operating Systems,page 6, San Diego, CA, USA, may 2007.Online proceedings athttp://www.usenix.org/events/hotos07/tech/.
Kevin Elphinstone, Gerwin Klein, and Rafal Kolanski.Formalising a high-performance microkernel.In Rustan Leino, editor, Workshop on Veri�ed Software:
Theories, Tools, and Experiments (VSTTE 06), MicrosoftResearch Technical Report MSR-TR-2006-117, pages 1�7,Seattle, USA, August 2006.
21 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Referências II
Gerwin Klein, Michael Norrish, Kevin Elphinstone, and GernotHeiser.Verifying a high-performance micro-kernel.In 7th Annual High-Con�dence Software and Systems
Conference, Baltimore, MD, USA, May 2007.
Harvey Tuch, Gerwin Klein, and Gernot Heiser.Os veri�cation � now!In Margo Seltzer, editor, Proc. 10th Workshop on Hot Topics
in Operating Systems (HotOS X), 2005.to appear.
22 / 23
Roteiro Introdução Veri�cação Formal de Kernel seL4 Formalização e Veri�cação Referências
Agradecimentos
Obrigado!
Perguntas?
Contato:glauber.cabral@students.ic.unicamp.br
23 / 23