Informática

Universidade Federal de Goi´ s a Programa Institucional de Iniciacao em
¸˜
Desenvolvimento Tecnol´ gico e Inovacao o ¸˜
PIBITI
´
Area: Ciˆ ncias Exatas e da Terra e Sub-´ rea: Ciˆ ncia da Computacao a e
¸˜

T´tulo do Projeto: ı ` e
Aplicacoes de Teoria da Prova a Ciˆ ncia da Computacao
¸˜
¸˜
Proponente: Vaston Goncalves da Costa
¸
Unidade: Departamento de Ciˆ ncia da Computacao - Campus Catal˜ o e ¸˜ a T´tulo do Plano de Trabalho: ı Construcao de um provador de Teoremas interativo circuito-estruturado
¸˜

Aluno: Lucas Angelo da Silveira

Matricula: 094989

Catal˜ o - 2011 a 1

Introducao
¸˜
Seguranca em sistemas de informacao e um problema n˜ o-trivial, que se apresenta em dife¸
¸˜ ´ a rentes n´veis de abstracao, tanto no n´vel de neg´ cio quanto no n´vel de sistema. Por seguranca ı ¸˜ ı o ı ¸
`
da informacao no n´vel de neg´ cio, se refere aos processos e as pessoas envolvidas em uma
¸˜
ı o empresa; por seguranca da informacao no n´vel de sistema, se refere ao software e hardware
¸
¸˜ ı sob vigilˆ ncia [Car04]. a ´
In´ meros s˜ o os casos de ataques registrados, por exemplo, pelo US-CERT, que e um dos u a centros para registro de problemas de seguranca na Internet [UC11]. Tais ataques s˜ o resul¸ a tantes, por exemplo, da quebra de um protocolo, e podem realmente impedir uma empresa de cumprir sua atividade fim.
T´ cnicas de an´ lise formal de software s˜ o mecanismos rigorosos, embasados matematie a a camente, que permitem aumentar a confianca de que um artefato de software realmente faz o
¸
que se espera que ele faca. Estas t´ cnicas incluem simulacao (ou teste), verificacao de modelos
¸
e
¸˜
¸˜
(model checking) e prova de teoremas (ordenadas, aqui, pelo custo crescente de aplicacao da
¸˜
t´ cnica). e ´
Um provador de teoremas e um procedimento, em uma l´ gica L, que, a partir de uma o f´ rmula α e um conjunto de f´ rmulas Γ (tamb´ m chamado de especificacao) exibe