1. Inicio
  2. Atrás
Título: CCMini: a prototype of certifying compiler based on annotated abstract syntax trees
Autores: Bavera, Francisco
Nordio, Martín
Medel, Ricardo
Aguirre, Jorge
Baum, Gabriel Alfredo
Fecha: 2012-10-26
2005-10
2005-10
Publicador: Unversidad Nacional de La Plata
Fuente:

Tipo: Objeto de conferencia
Objeto de conferencia
Tema: Verification
Compilers
Security
Ciencias Informáticas
Lenguajes de Programación
Descripción: 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.
II Workshop de Ingeniería de Software y Bases de Datos (WISBD)
Idioma: Inglés