Indexado en

UPV Enlace externo

Licencia y uso

Citaciones

Altmetrics

Análisis de autorías institucional

Escobar, SAutor o CoautorRomero, DAutor o Coautor

Compartir

A Tool for Automated Certification of Java Source Code in Maude

Publicado en:Electronic Notes In Theoretical Computer Science. 248 19-29 - 2009-08-04 248(), DOI: 10.1016/j.entcs.2009.07.056

Autores: Alba-Castro, M; Alpuente, M; Escobar, S; Ojeda, P; Romero, D

Afiliaciones

Resumen

In previous work, an abstract certification technique for Java source code was proposed based on rewriting logic, which is a semantic framework that has been efficiently implemented in the rule-based programming language Maude. Starting from a specification of a (generic) Java abstract semantics written in Maude, we develop an abstract verification technique that essentially consists of a reachability analysis using the Java abstract semantics. We provide facilities to associate abstract domains to the variables of the considered Java program so that the resulting state-space is finite. As a by-product of the abstract verification, a safety certificate is delivered that contains a set of (abstract) rewriting proofs that can be checked by the code consumer using a standard rewriting logic engine. The main advantage is that the amount of code that must be explicitly trusted is very small. This paper presents a Web tool that implements the abstract certification technique by providing appropriate abstract domains for different safety properties while hiding the technical details of the method from the user. The tool has been devised to be easily extendable to other properties and domains. It currently supports the certification of two kinds of safety properties that are not handled by standard Java compilers: secure integer arithmetic rules and non-interference policies.

Palabras clave