Confira !!
Uma nova série de patch foi postada implementando Runtime Verification (RV) para o kernel Linux.
Aqui está como a série de patch Runtime Verification é resumida por Daniel Bristot de Oliveira da Red Hat, que tem trabalhado neste esforço por anos para verificar o comportamento do kernel:
A verificação de tempo de execução (RV) é um método leve (mas rigoroso) que complementa as técnicas clássicas de verificação exaustiva (como verificação de modelo e prova de teorema) com uma abordagem mais prática para sistemas complexos.
Em vez de depender de um modelo de baixa granularidade de um sistema (por exemplo, uma reimplementação de um nível de instrução), o RV trabalha analisando o traço da execução real do sistema, comparando-o com uma especificação formal do comportamento do sistema.
O uso de autômato determinístico para RV é uma abordagem bem estabelecida.
...
Aqui estou propondo uma abordagem mais prática para o uso de autômatos determinísticos para verificação em tempo de execução, e inclui:
- Uma interface para controlar a verificação.
- Uma ferramenta e conjunto de cabeçalhos que permite a geração automática de código do monitor RV (Monitor Synthesis).
Dado que RV é um consumidor de rastreamento, o código está sendo colocado dentro do subsistema de rastreamento (Steven e eu estamos conversando sobre isso há algum tempo).
Nesta RFC ainda não estou propondo nenhum modelo complexo. Em vez disso, estou apresentando apenas monitores simples que ajudam a ilustrar o uso da geração automática de código e da interface RV. Isso é importante para permitir que outros pesquisadores e desenvolvedores comecem a usar / estender esse método.
Também é importante mencionar que este trabalho foi fortemente motivado pela utilização do Linux em sistemas críticos de segurança, principalmente pelas pessoas envolvidas no Projeto Elisa.
Mais detalhes sobre a verificação do tempo de execução do Linux por meio desta apresentação da Red Hat Research:
Até a próxima !!
Nenhum comentário:
Postar um comentário