[pt] 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. / [en] Nowdays most computer programs are obtained from the
WEB. Since their source is usually unknown, it is necessary
to be sure that the code of the program behaves as
expected.The ideal solution would be verify the code
against a specification of safety policies.However, this
can take too much time.Another approach is making the code
itself prove that it is safe. The concept os proof-carryng
code (PCC) is based on this idea: a program carries a proof
of its conformity with certain safety policies. That is ,
it carries a proof cencerning properties related to the
code itself. Therefore, the same formal methods employed in
formal verification of programs can be used in this
tecnology. Due to this fact, in this work it is studied how
Hoare logic applied to source codes written in an
imperative programming language, which is a formal methods
are researched to generate proofs of program correctness
using the method explained, so that it can be possible to
generate PCC safety programs with Hoare logic.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:4428 |
| Date | 22 January 2004 |
| Creators | JULIANA CARPES IMPERIAL |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | TEXTO |
Page generated in 0.0028 seconds