Palestra: Micro-Policies: Formally Verified, Tag-Based Security Monitors
0 views
Skip to first unread message
Rodolfo Azevedo
May 30, 2015, 3:13:11 PM5/30/15
to mo...@googlegroups.com, people-lsc
Segunda as 10h, sala 351
Micro-Policies: Formally Verified, Tag-Based Security Monitors
Muitas falhas de segurança presentes nos sistemas computacionais de
hoje em dia podem ser reparadas com monitores dinânimos que verificam
continuamente sua execução. Infelizmente, o uso de tais monitores
incorre em geral em altos custos de desempenho, tornando-os
inadequados para muitas aplicações. Nesta palestra, apresentarei um
modelo de programação para monitores baseado em uma nova extensão de
hardware, a PUMP (Programmable Unit for Metadata Processing), ambos
desenvolvidos por nosso grupo de pesquisa. O modelo pode ser usado
para garantir diversas propriedades de segurança em sistemas, como
proteção de memória de alta granularidade, isolação de componentes,
entre outras, e pode ser executado eficientemente, graças à
PUMP. Discutirei como implementamos alguns monitores usando esse
mecanismo e como empregamos um assistente de prova para verificar
formalmente a corretude dos mesmos. Falarei também sobre o
funcionamento da PUMP, algumas otimizações que nosso grupo
desenvolveu, e experimentos para medir sua eficácia.
Arthur Azevedo de Amorim é atualmente estudante de doutorado em
ciência da computação na University of Pennsylvania, EUA, onde
trabalha sob a supervisão de Benjamin Pierce desde 2011. Formou-se em
engenharia de computação pela Unicamp e engenharia pela Ecole
polytechnique (França) em 2010.
Muitas falhas de segurança presentes nos sistemas computacionais de
hoje em dia podem ser reparadas com monitores dinânimos que verificam
continuamente sua execução. Infelizmente, o uso de tais monitores
incorre em geral em altos custos de desempenho, tornando-os
inadequados para muitas aplicações. Nesta palestra, apresentarei um
modelo de programação para monitores baseado em uma nova extensão de
hardware, a PUMP (Programmable Unit for Metadata Processing), ambos
desenvolvidos por nosso grupo de pesquisa. O modelo pode ser usado
para garantir diversas propriedades de segurança em sistemas, como
proteção de memória de alta granularidade, isolação de componentes,
entre outras, e pode ser executado eficientemente, graças à
PUMP. Discutirei como implementamos alguns monitores usando esse
mecanismo e como empregamos um assistente de prova para verificar
formalmente a corretude dos mesmos. Falarei também sobre o
funcionamento da PUMP, algumas otimizações que nosso grupo
desenvolveu, e experimentos para medir sua eficácia.
Arthur Azevedo de Amorim é atualmente estudante de doutorado em
ciência da computação na University of Pennsylvania, EUA, onde
trabalha sob a supervisão de Benjamin Pierce desde 2011. Formou-se em
engenharia de computação pela Unicamp e engenharia pela Ecole
polytechnique (França) em 2010.
Reply all
Reply to author
Forward
0 new messages