Protegendo aplicativos Web Made Simple e Scalable
A microkernel nippy matematicamente provado ser livre de bugs * e utilizados para proteger drones de pirataria, será lançado como open source amanhã.
O L4 seguro baseado em-métodos formais incorporado (seL4) microkernel foi desenvolvido por boffins australianos no National ICT Australia (NICTA) e fez parte do programa de alta Garantia de Cyber Sistemas Militar de Defesa de Projetos de Pesquisa Avançada da Agência dos EUA eclodiram em 2012 para impedir que hackers que batem aves não tripulados para fora do céu.
Notou-se que o membro mais avançado e altamente seguro da família microkernel L4 devido ao seu uso de métodos formais que não impactam o desempenho. Um microkernel difere de kernels monolíticos - como os kernels Linux e Windows - executando o máximo de código possível - desde os motoristas aos serviços do sistema - no espaço do usuário, fazendo com que a coisa toda mais modular e (em teoria) mais estável.
Amanhã ao meio-dia Australian Eastern Standard Time (GMT +10) todo o código fonte do seL4 incluindo provas e código adicional usado para construir sistemas fiáveis será lançado sob a licença GPL v2.
Um grupo global de matemática e gurus de aviação dos gostos de Boeing e Rockwell Collins se juntou a uma equipe de pesquisadores dedicados NICTA no projeto que envolveu o sistema operacional seL4 projetado para detectar e folha de tentativas de invasão.
NICTA pesquisador sênior Doutor junho Andronick disse que o kernel deve ser considerado por quem a construção de sistemas críticos, tais como pacemakers e carros rico em tecnologia.
"Se o seu software é executado no kernel seL4, você tem a garantia de que, se uma falha ocorre em uma parte do sistema, ele não pode se propagar para o resto do sistema e, em particular, as partes críticas", disse Andronick início deste mês.
"Nós fornecemos uma prova matemática formal que este kernel seL4 está correta e garante o isolamento entre os componentes."
NICTA demonstrado em um vídeo como um zangão que executando a plataforma poderia detectar tentativas de invasão de estações terrestres que normalmente causam o software de vôo para morrer e que a aeronave cair.
"O que estamos demonstrando aqui é que se uma das estações terrestres é malicioso, e envia um comando para o robô para parar o software de vôo, o avião disponível no mercado irá aceitar o comando, mate o software e simplesmente cair do céu, ", disse Andronick.
Demonstração zangão dos pesquisadores, ao invés, detectar a intrusão em temp, piscam suas luzes LED e voar para longe. Isso pode garantir que as missões de drones reais poderiam continuar em caso de tentativas de invasão por combatentes.
Andronick disse seL4 que entram em jogo quando a equipe adicionou mais funcionalidades, incluindo navegação, vôo autônomo e componentes de controle de missão.
Em profundidade informações sobre seL4 estava disponível no site da NICTA e dentro do papel abrangente de verificação formal de um sistema operacional microkernel . ®
* Isso é bug livre de acordo com a verificação formal de sua especificação; falhas de projeto nas especificações não são contadas pela equipe.
via Alimentação (Feed)
Nenhum comentário:
Postar um comentário