Palestra da Série de Seminários: Projeto e verificação de arquiteturas de controle de fluxo de informação com o Prof. Arthur Azevedo de Amorim da University of Pennsylvania

Universidade Estadual de Campinas - UNICAMP
Instituto de Computação - IC

P A L E S T R A  D A  S É R I E   D E   S E M I N Á R I O S
 
Sexta 17/05/2013
Horário: 14h00 às 15h00min.
Sala 316 - IC 3
 
Arthur Azevedo de Amorim
University of Pennsylvania
 

Título: Projeto e verificação de arquiteturas de controle de fluxo de informação
 
Resumo:
 
Sistemas computacionais atuais sofrem de inúmeras vulnerabilidades,que podem culminar em falhas graves em seu funcionamento e sua segurança. Tipicamente, tais problemas são fruto da interação dediversos componentes defeituosos, limitando o poder de soluções queagem isoladamente sobre uma parte do sistema. Diante desse cenário, é natural se perguntar como seria o computador se pudéssemos reprojetá-lo do zero, sem nos preocuparmos com interoperabilidade com sistemas legado. O projeto SAFE tenta responder a essa questão com uma nova proposta de organização para a pilha computacional, incluindo nova arquitetura, novo sistema operacional, nova linguagem de programação e novo ecossistema de aplicações, todos projetados conjuntamente e tendo verificação em vista.
 
Nessa palestra, farei uma breve introdução ao projeto SAFE, expondo alguns de seus aspectos fundamentais e discutindo em mais detalhe o uso de verificação no projeto. Um dos nossos principais objetivos é poder controlar o fluxo de informação no sistema, impedindo que dados vazem indevidamente e garantindo sua integridade. Falarei sobre alguns modelos de arquiteturas simples para controle de fluxo de informação que estamos desenvolvendo, combinando testes aleatórios e provas mecanizadas para validar nossas ideias e poder integrá-las no produto
final.
 
Sobre o palestrante:
 
Nascido em Campinas, Arthur Azevedo de Amorim é formado em Engenharia da Computação pela Unicamp e em Engenharia pela École polytechnique. Atualmente é estudante de doutorado na University of Pennsylvania, trabalhando com Benjamin Pierce em linguagens de programação e verificação formal.