An abstract interpretation-based approach to mobile code safety

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

Description

Title: An abstract interpretation-based approach to mobile code safety
Author/s:
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: 3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004)
Event Dates: 3 April 2004
Event Location: Barcelona, Spain
Title of Book: roceedings of the 3rd International Workshop on Compiler Optimization Meets Compiler Verification (COCV 2004)
Date: 30 May 2005
Volume: 132
Subjects:
Freetext Keywords: 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.
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview

Abstract

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.

More information

Item ID: 14613
DC Identifier: http://oa.upm.es/14613/
OAI Identifier: oai:oa.upm.es:14613
Official URL: http://www.sciencedirect.com/science/article/pii/S1571066105050085
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 09 Mar 2013 08:24
Last Modified: 21 Apr 2016 14:21
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM