Secure mobile code and control flow analysis

The interaction between software systems by means of mobile code is a powerful and truly effective method, particularly useful for installing and executing code dynamically. However, for this mechanism to be applicable safely, especially in industrial or critical applications, techniques that guaran...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Bavera, Francisco, Aguirre, Jorge, Nordio, Martín
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2006
Materias:
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/22802
Aporte de:
id I19-R120-10915-22802
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Inglés
topic Ciencias Informáticas
Program verification
mobile code
certifying compilation
static analysis
proof-carrying code
spellingShingle Ciencias Informáticas
Program verification
mobile code
certifying compilation
static analysis
proof-carrying code
Bavera, Francisco
Aguirre, Jorge
Nordio, Martín
Secure mobile code and control flow analysis
topic_facet Ciencias Informáticas
Program verification
mobile code
certifying compilation
static analysis
proof-carrying code
description The interaction between software systems by means of mobile code is a powerful and truly effective method, particularly useful for installing and executing code dynamically. However, for this mechanism to be applicable safely, especially in industrial or critical applications, techniques that guarantee foreign code execution safety for the consumer or host will be necessary. Of course, tool support for automating, at least partially, the application of these techniques is essential. The importance of guarantee code execution safety originates numerous active research lines, among which Proof-Carrying Code (PCC) is one of the most successful. One of the problems to overcome for the PCC industrial use is to obtain lineal methods of safeness certification and verification. A framework for the generation and execution of safe mobile code based on PCC together with techniques for static analysis of control and data-flow, called PCC-SA, was developed later by the authors. The results of the group that allowed proving the hypothesis that the PCC-SA complexity in practice is lineal respect to the input programs length, as for certification as for verification processes are also presented. To achieve this, a C-program family, whose elements are referred to as lineally annotative, is defined. Parameters statically measured over their source code determine whether a program belongs to this family or not. Different properties of this family are demonstrated in this work, which allows formally showing that for all the programs of this family, the PCC-SA presents a lineal behavior. The parameters required for a large sample of programs keeping of standard packages, are calculated. This calculation finally determines that all the programs of the sample are lineally annotative, which validates the hypothesis previously stated.
format Objeto de conferencia
Objeto de conferencia
author Bavera, Francisco
Aguirre, Jorge
Nordio, Martín
author_facet Bavera, Francisco
Aguirre, Jorge
Nordio, Martín
author_sort Bavera, Francisco
title Secure mobile code and control flow analysis
title_short Secure mobile code and control flow analysis
title_full Secure mobile code and control flow analysis
title_fullStr Secure mobile code and control flow analysis
title_full_unstemmed Secure mobile code and control flow analysis
title_sort secure mobile code and control flow analysis
publishDate 2006
url http://sedici.unlp.edu.ar/handle/10915/22802
work_keys_str_mv AT baverafrancisco securemobilecodeandcontrolflowanalysis
AT aguirrejorge securemobilecodeandcontrolflowanalysis
AT nordiomartin securemobilecodeandcontrolflowanalysis
bdutipo_str Repositorios
_version_ 1764820467730874369