CCMini: a prototype of certifying compiler based on annotated abstract syntax trees

Certifying compilers use static information of a program to verify that it complies with certain security properties and to generate certified code. To do so, those compilers translate the source program into an annotated program written in some intermediate language. These annotations are used to v...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Bavera, Francisco, Nordio, Martín, Medel, Ricardo, Aguirre, Jorge, Baum, Gabriel Alfredo
Formato: Objeto de conferencia
Lenguaje:Inglés
Publicado: 2005
Materias:
Ciencias Informáticas
Verification
Lenguajes de Programación
Compilers
Security
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/23081
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-23081
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
Verification
Lenguajes de Programación
Compilers
Security
spellingShingle Ciencias Informáticas
Verification
Lenguajes de Programación
Compilers
Security
Bavera, Francisco
Nordio, Martín
Medel, Ricardo
Aguirre, Jorge
Baum, Gabriel Alfredo
CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
topic_facet Ciencias Informáticas
Verification
Lenguajes de Programación
Compilers
Security
description Certifying compilers use static information of a program to verify that it complies with certain security properties and to generate certified code. To do so, those compilers translate the source program into an annotated program written in some intermediate language. These annotations are used to verify the generated code. Given a source program, a certifying compiler will produce object code, annotations, and a proof that the code comply with the customer’s security specifications. Thus, certifying compilers can automatically produce the security evidence required to establish a Proof-Carrying Code (PCC) setting. In this work we present CCMini, a certifying compiler for a simple subset of the language C. This compiler guarantees that compiled programs do not read uninitialized variables and do not access to undefined array positions. The verification process is carried on abstract syntactic trees by using static analysis techniques; in particular, control analysis and data analysis are used.
format Objeto de conferencia
Objeto de conferencia
author Bavera, Francisco
Nordio, Martín
Medel, Ricardo
Aguirre, Jorge
Baum, Gabriel Alfredo
author_facet Bavera, Francisco
Nordio, Martín
Medel, Ricardo
Aguirre, Jorge
Baum, Gabriel Alfredo
author_sort Bavera, Francisco
title CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
title_short CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
title_full CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
title_fullStr CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
title_full_unstemmed CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
title_sort ccmini: a prototype of certifying compiler based on annotated abstract syntax trees
publishDate 2005
url http://sedici.unlp.edu.ar/handle/10915/23081
work_keys_str_mv AT baverafrancisco ccminiaprototypeofcertifyingcompilerbasedonannotatedabstractsyntaxtrees
AT nordiomartin ccminiaprototypeofcertifyingcompilerbasedonannotatedabstractsyntaxtrees
AT medelricardo ccminiaprototypeofcertifyingcompilerbasedonannotatedabstractsyntaxtrees
AT aguirrejorge ccminiaprototypeofcertifyingcompilerbasedonannotatedabstractsyntaxtrees
AT baumgabrielalfredo ccminiaprototypeofcertifyingcompilerbasedonannotatedabstractsyntaxtrees
bdutipo_str Repositorios
_version_ 1764820468103118850

Ejemplares similares