-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Quer trazer a discussão In Topic de novo?
Eu falei com o Robert Watson (FreeBSD Foundation) a umas duas semanas atras, quando o paper que deu origem a isso tudo foi publicado, e perguntei quando teríamos uma coisa assim no FreeBSD, e a resposta foi: "Nunca! Porque a comunidade não tem idéia de quão benéfico isso poderia ser pro projeto" Entender e ter condições de discutir este tipo de tópico, é em geral o que difere um Cientista da Computação de um Micreiro (leia-se prático). Jean Paulo Henrique wrote: > É isso ai lista continuamos a thread... pois a aula está muito > interessante... > > 2009/10/26 Jean Everson Martina <ever...@inf.ufsc.br> > > >>>> Um pequeno programa é uma exceção. Algum programa (como esse que você >>>> falou, talvez), com o espírito acadêmico (principalmente), pode tratar >>>> exceções. O que não deixa de ter validade empírica, mesmo sabendo da >>>> existência do Teorema da Parada. > Você esta confundido a abrangência do teorema de parada. Ele diz que não > existe algorítimo genérico para decidir a parada para todos os pares > entrada-programa. O que não quer dizer que não existe solução para casos > específicos. > > Sobre a validade empírica, você pode explicar o que é uma validade > formal então? > > De novo, se você estiver correto de que tudo é empírico, um player como > a MS, não investiria mais de 2 milhões de libras no projeto Terminator > (o que prova que não é brincadeirinha acadêmica): > > > http://research.microsoft.com/en-us/um/cambridge/projects/terminator/default.htm > > O Terminator é um dos maiores responsáveis pelo aumento de estabilidade > do XP, Vista e 7. Você vê hoje muito menos telas azuis e crashes, porque > o drivers certificados foram sendo verificados quanto a não parada. Sim, > se está longe de ter a verificação formal completa de um SO de uso > genérico. Mas eu digo que em 15 anos isso será um fato. > > Na verdade, tem outros projetos semelhantes sobre verificação de chips > usando métodos automatizados e logica de ordem mais alta, que são usados > pela ARM (100% do que a ARM faz é verificado formalmente, e eles são a > maior plataforma de Micro-processadores hoje). A Intel e AMD também > fazem mas não em 100% dos casos. > > Aqui mesmo (Grupo de Teoria da Computação de Cambridge), temos projetos > com a NSA pra verificação formal de micro-processadores criptográficos, > , com a Cisco e Boeing na área de roteamento, com a IBM na área de > módulos java e com a Intel na verificação de assembly x86, etc > > Meu PhD é sobre verificação formal de protocolos criptográficos, onde > parte da pesquisa já foi bancada pela VISA (verificação do SET) e pelo > Internet Consortium (Verificação do SSL). Hoje o governo brasileiro (que > me banca) tem interesse em verificar os grandes protocolos no cenário > nacional, tais como SPB, NF-e e OpenHSM. É por isso que eu to aqui. > > Sobre uma outra pergunta na discussão sobre a usabilidade deste > microkernel: Sim ele é utilizável e funcional, mas dentro da plataforma > e objetivos à que se propõe. > > > Jean - ------------------------- Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd >> > ------------------------- > Histórico: http://www.fug.com.br/historico/html/freebsd/ > Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.8 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkrle+AACgkQQN0Max56WicXnwCgmSgxz/IOiAmyFWIj80QHmNWA Ez0AnitUbLbgK2CBEs5jmiMfqDbe/rwM =Lr0k -----END PGP SIGNATURE----- ------------------------- Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
