Abstraction carrying code and resource-awareness

Hermenegildo, Manuel V. and Albert Albiol, Elvira and López García, Pedro and Puebla Sánchez, Alvaro Germán (2005). Abstraction carrying code and resource-awareness. In: "7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming", July 11-13 2005, Lisbon, Portugal. ISBN 1595930906.


Title: Abstraction carrying code and resource-awareness
  • Hermenegildo, Manuel V.
  • Albert Albiol, Elvira
  • López García, Pedro
  • Puebla Sánchez, Alvaro Germán
Item Type: Presentation at Congress or Conference (Article)
Event Title: 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming
Event Dates: July 11-13 2005
Event Location: Lisbon, Portugal
Title of Book: PPDP '05 Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming
Date: 2005
ISBN: 1595930906
Freetext Keywords: Program verification, mobile code certification, resource awareness, program debugging, cost analysis, granularity control, verificación de programas, certificación de código móvil, distributed programming, abstract interpretation, programming languages, recursos comunitarios, depuración de programas, análisis de costes, programación distribuída, interpretación de resúmenes, lenguajes de programación.
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

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


Proof-Carrying Code (PCC) is a general approach to mobile code safety in which the code supplier augments the program with a certifícate (or proof). 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, eíñcient, and automatic than generating the original proof. Abstraction Carrying Code (ACC) is an enabling technology for PCC in which an abstract model of the program plays the role of certifícate. The generation of the certifícate, Le., the abstraction, is automatically carried out by an abstract interpretation-based analysis engine, which is parametric w.r.t. different abstract domains. While the analyzer on the producer side typically has to compute a semantic fixpoint in a complex, iterative process, on the receiver it is only necessary to check that the certifícate is indeed a fixpoint of the abstract semantics equations representing the program. This is done in a single pass in a much more efficient process. ACC addresses the fundamental issues in PCC and opens the door to the applicability of the large body of frameworks and domains based on abstract interpretation as enabling technology for PCC. We present an overview of ACC and we describe in a tutorial fashion an application to the problem of resource-aware security in mobile code. Essentially the information computed by a cost analyzer is used to genérate cost certificates which attest a safe and efficient use of a mobile code. A receiving side can then reject code which brings cost certificates (which it cannot validate or) which have too large cost requirements in terms of computing resources (in time and/or space) and accept mobile code which meets the established requirements.

More information

Item ID: 14539
DC Identifier: http://oa.upm.es/14539/
OAI Identifier: oai:oa.upm.es:14539
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 22 Feb 2013 07:28
Last Modified: 21 Apr 2016 14:15
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM