An abstract interpretation-based approach to mobile code safety

Albert Albiol, Elvira; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2005). An abstract interpretation-based approach to mobile code safety. En: "3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004)", 3 April 2004, Barcelona, Spain.

Descripción

Título: An abstract interpretation-based approach to mobile code safety
Autor/es:
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004)
Fechas del Evento: 3 April 2004
Lugar del Evento: Barcelona, Spain
Título del Libro: roceedings of the 3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004)
Fecha: 30 Mayo 2005
Volumen: 132
Materias:
Palabras Clave Informales: Mobile code safety, Certifying compilation, Proof-carrying code, Abstract interpretation, Static analysis, Código móvil de seguridad, Recopilación de certificados, Código con demostración, Intepretación de resúmenes, Analisis estadístico.
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
Pdf - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa

Resumen

Recent approaches to mobile code safety, like proof- arrying code, involve associating safety information to programs. The code supplier provides a program and also includes with it a certifícate (or proof) whose validity entails compliance with a predefined safety policy. The intended benefit is that the program consumer can locally validate the certifícate w.r.t. the "untrusted" program by means of a certifícate checker—a process which should be much simpler, eflicient, and automatic than generating the original proof. We herein introduce a novel approach to mobile code safety which follows a similar scheme, but which is based throughout on the use of abstract interpretation techniques. In our framework the safety policy is specified by using an expressive assertion language defined over abstract domains. We identify a particular slice of the abstract interpretation-based static analysis results which is especially useful as a certifícate. We propose an algorithm for checking the validity of the certifícate on the consumer side which is itself in fact a very simplified and eflicient specialized abstract-interpreter. Our ideas are illustrated through an example implemented in the CiaoPP system. Though further experimentation is still required, we believe the proposed approach is of interest for bringing the automation and expressiveness which is inherent in the abstract interpretation techniques to the área of mobile code safety.

Más información

ID de Registro: 14613
Identificador DC: http://oa.upm.es/14613/
Identificador OAI: oai:oa.upm.es:14613
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 09 Mar 2013 08:24
Ultima Modificación: 21 Abr 2016 14:21
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM