TECHNIQUES FOR THE USE OF HOARE LOGIC IN PCC / TÉCNICAS PARA O USO DO CÁLCULO DE HOARE EM PCC
AUTOR(ES)
JULIANA CARPES IMPERIAL
DATA DE PUBLICAÇÃO
2003
RESUMO
Atualmente, a maioria dos programas para computadores é obtida através da WEB. Como muitas vezes a procedência são fontes desconhecidas, é preciso se certificar de que o código se comporta como o esperado. A solução ideal seria verificar o código contra uma especificação de políticas de segurança ,contudo, isso pode consumir muito tempo.Uma outra alternativa é fazer com que o próprio código prove ser seguro. O conceito de proof-carryng code (PCC)é baseado nessa idéia : um programa carrega consigo uma prova de sua conformidade com certas políticas de segurança. Ou seja ,ele carrega uma prova a respeito de propriedades do próprio código. Portanto, os mesmos métodos froamsi usados para a verificação de programs podem se utilizados para esta tecnolgia. Considerando este fato,neste trabalho é estudado como cálculo de Hoare, em método formal para realizar a verificação de programas, aplicado a códigos-fonte escritos em uma linguagem de programação imperativa, pode ser útil á tecnica de PCC. Conseqüentemente, são pesquisados métodos para a geração de provas de correção de programas utilizando o método citado, para tornar possível a geração de provas de segurança para PCC utilizando o cálculo de Hoare.
ASSUNTO(S)
theorem proving proof-carrying code program verification proof-carrying code invariantes de loops prova de teoremas loops invariants hoare logic logica de primeira ordem seguranca safety first order logic calculo de hoare correcao de programas
ACESSO AO ARTIGO
Documentos Relacionados
- Aplication of CFD techniques for he calculation of reacting flow in riser
- Uso de técnicas de aprendizagem para classificação e recuperação de imagens
- Use of termography techniques for detection of discontinued in the GTAW process through the monitoring o the weld pool
- Estudo e desenvolvimento de técnicas para o cálculo de curvaturas e eixos de simetria.
- USING POINT BASED TECHNIQUES FOR SEISMIC HORIZONS VISUALIZATION