Skip to Main content Skip to Navigation

Proof preservation and program compilation

Abstract : Software applications have gained a notable role in our everyday activities, mobile code applications being a significant portion of these software agents. The mobile code paradigm entails the distribution of applications from the code producer to heterogeneous client environments in which they are executed. An extended practice of this paradigm consists in the development of third party components, that are transferred across an untrusted network such as Internet and finally integrated in a host execution environment such as a PC or a cellular phone. Naturally, this computational environment opens the door to the deployment of malicious code in client workstations. In some cases a potential misbehavior of the mobile code does not constitute a serious risk, for example when the integrity of the data affected by the execution is irrelevant, or when the execution architecture imposes strong constraints on the computational capabilities of the foreign application. There still are, however, situations in which it is essential to verify the functional correctness of the code before executing it, for instance when the confidentiality of critical data such as credit card information could be compromised, or when the execution environment does not have a special mechanism to monitor excessive resource consumption. George Necula proposed a technique to provide trust to code consumers about the program correctness without trusting the code producer side. The technique, Proof Carrying Code (PCC), consists in deploying code together with a formal proof of its correctness. Correctness is an inherent property of the received code that cannot be inferred from the identity of the code producer. That naturally puts PCC in advantage with respect to methods based on trusting a third party authority. Indeed, a signature from a trusted authority it is not sufficient to provide absolute trust on the execution of the received code. From its origins, the typical mechanism of PCC to generate certificates relies on a certifying compiler, an extension of a standard compiler that automatically produces certificates for decidable safety policies. Extending the set of enforceable properties is challenging and in the most general case it requires human interaction. One possibility, is to verify the final executable code from scratch. However, the lack of structure makes low level code verification a less natural, and hence more daunting, task. This, together with the fact that verification environments target mostly high level code, makes more appropriate the idea of moving the generation of certificates at the source code level. The main drawback of producing certificates ensuring source code correctness is that they do not entail correctness of the final compiled code. Several techniques may be proposed to transfer evidence of program correctness from the source code to the executable counterpart. That includes, for instance, deploying the source program and original certificates in addition to the executable code and certifying the correctness of the compilation process. However, this approach is not satisfactory, since in addition to require availability of the source code, a certificate ensuring compiler correctness can be prohibitively large. A more viable alternative is to provide a mechanism to generate certificates for compiled code from certificates of the original source program. Compilers are complex procedures composed of several steps, in which the original program is progressively transformed into intermediate lower level representations. Barthe et al. and Pavlova have shown that original certificates are preserved, up to minor differences, along with the first compiler phase: a nonoptimizing compilation from source level to an unstructured intermediate representation. However, compiler optimizations applied to the intermediate representations represent a challenge since a priori certificates cannot be reused. In this thesis, we analyze how optimizations affect the validity of certificates and propose a mechanism, Certificate Translation, to transform certificates in order to overcome the effects of program transformations, rendering feasible the generation of certificates for executable mobile code at the source level. Chapter 2 introduces certificate translation for common compiler optimizations applied in the context of an intermediate RTL language. The main difficulties are presented, and a classification of program transformations is given in terms of the effort required to transform the original certificates. A general scheme is provided to cover transformations that performs arithmetic simplifications such as constant propagation and common subexpression elimination. In addition, ad-hoc techniques are proposed for other standard optimizations that do not correspond to this classification. Chapter 3 studies the existence of certificate translators in a mild extension of an abstract interpretation framework that includes a notion of certificates. This abstract setting provides considerable advantages with respect to the approach of Chapter 2 since it allows us to extend certificate translation to diverse programming languages and several analysis environments. Certificate transformation is studied in this abstract setting for simple program transformations which can be composed to represent a wide variety of program optimizations, for instance those considered in Chapter 2. In a second part of the thesis, we extend certificate translation to less typical settings, that can be of interest in PCC scenarios. More precisely, the chapters in the second part consider the aspect oriented paradigm, hybrid verification methods and parallel programs executing in memory hierarchies. For each setting, appropriate analysis and verification settings are provided. Then, the effect of common transformations over verification results are studied.
Document type :
Complete list of metadata

Cited literature [71 references]  Display  Hide  Download
Contributor : Ecole Mines ParisTech Connect in order to contact the contributor
Submitted on : Friday, April 17, 2009 - 8:00:00 AM
Last modification on : Tuesday, July 21, 2020 - 3:21:51 AM
Long-term archiving on: : Friday, October 19, 2012 - 12:35:09 PM


  • HAL Id : pastel-00004940, version 1



César Kunz. Proof preservation and program compilation. Mathematics [math]. École Nationale Supérieure des Mines de Paris, 2009. English. ⟨NNT : 2009ENMP1591⟩. ⟨pastel-00004940⟩



Record views


Files downloads