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

dc.creatorBavera, Francisco
dc.creatorNordio, Martín
dc.creatorMedel, Ricardo
dc.creatorAguirre, Jorge
dc.creatorBaum, Gabriel Alfredo
dc.date2005-10
dc.date2005-10
dc.date2012-10-26T18:37:58Z
dc.identifierhttp://sedici.unlp.edu.ar/handle/10915/23081
dc.descriptionCertifying 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.
dc.descriptionII Workshop de Ingeniería de Software y Bases de Datos (WISBD)
dc.descriptionRed de Universidades con Carreras en Informática (RedUNCI)
dc.formatapplication/pdf
dc.languageen
dc.relationXI Congreso Argentino de Ciencias de la Computación
dc.rightshttp://creativecommons.org/licenses/by-nc-sa/2.5/ar/
dc.rightsCreative Commons Attribution-NonCommercial-ShareAlike 2.5 Argentina (CC BY-NC-SA 2.5)
dc.subjectCiencias Informáticas
dc.titleCCMini: a prototype of certifying compiler based on annotated abstract syntax trees
dc.typeObjeto de conferencia
dc.typeObjeto de conferencia


Este ítem pertenece a la siguiente institución