Uso de LOTOS na gerência de segurança de aplicações distribuídas em JAVA

Abstract

Apesar de possuir características que a tornam mais flexível que outras linguagens de programação, existem fragilidades que podem facilitar a construção de ataques usando a linguagem Java. Um componente de extrema importância, no Modelo de Segurança da plataforma Java é o Carregador de Applets, responsável, entre outras ações, pela associação dinâmica de uma classe remota (inclusa em alguma applet) e seu respectivo código. A adição de classes a um ambiente de execução Java pode ser danosa quando se tratar, por exemplo, de uma applet com intenções maliciosas. Neste caso, a possibilidade de existirem classes com métodos perigosos que podem, por exemplo, sobrepor­se à definição original de classes predefinidas, pode ser impedida pelo trabalho do Carregador de Classes (CCA). Neste trabalho, a Técnica de Descrição Formal LOTOS e a ferramenta Eucalyptus são usadas com a intenção de testar e validar a implementação de uma extensão à especificação original do Carregador de Applets. Abaixo é apresentado a especificação da proposta utilizando­se LOTOS.