COMVERS:
Verifiable and Resource-Aware Mobile Computing
(COmputación Móvil VErificable y consciente de los RecursoS)
- COMVERS (UPM-CLIP) Subproject Summary (See also
MERIT):
One of the fundamental problems that Computer Science faces today is
the issue of when we can safely execute (possibly untrusted) code.
This problem is further exacerbated in the context of mobile
computing. One of the most promising solutions to this problem is
Proof-Carrying Code (PCC). The basic idea behind PCC is the
inclusion of a certificate along with the code which can be used to
check, in a simple and efficient manner, that the code satisfies
certain security requirements. One of the advantages of this approach
is that it does not assume the existence of a centralized trust
entity. In this subproject we are proposing the use of
abstraction carrying code (ACC), an instance of PCC where
abstract interpretation serves as the enabling technology. Abstract
interpretation allows the determination of safe approximations of many
properties of a program including, amongst others, the computational
cost. COMVERS will provide advances in the field of the static
analysis that will permit the acquisition of precise information
regarding resource consumption. This will allow the extension of the
framework of PCC to include certificates containing information
regarding computational costs. This information, gathered through a
process of static analysis, will be used in the software development
phase, as it allows the detection of errors at compile time and the
verification that the program is correct with respect to a certain
security policy. Furthermore, it will also be used in the compiler
thereby allowing the generation of code with reduced resource
requirements. In COMVERS we will study rigorous procedures that will
allow performing platform-specific optimizations according to the
resources available in a particular platform. We will call this kind
of compiling resource-aware. The techniques of analysis,
debugging, optimization, and ACC mentioned will be implemented in a
prototype which will be distributed as free software.
- Keywords: Program Specialization, Program Optimization,
Pervasive Computing, Cost Analysis, Resource Consumption Analysis,
Abstract Interpretation, Global Analysis, Parallelization,
Visualization, Logic and Constraint Programming, Multi-Paradigm
Programming, Declarative Programming.
- CLIP-Group Research Personnel Involved:
<webmaster at clip.dia.fi.upm.es>
Last modified: Sun Jul 9 18:31:02 2006