Tesis doctoral de Mauricio Fernando Alba Castro
In this thesis we propose an abstraction based certification technique for java programs which is based on rewriting logic, a very general logical and semantic framework efficiently implemented in the functional programming language maude. We focus on safety properties, i.E. Properties of a system that are defined in terms of certain events not happening, which we characterize as unreachability problems in rewriting logic. The safety policy is expressed in the style of jml, a standard property specification language for java modules. in order to provide a decision procedure, we enforce finite-state models of programs by using abstract interpretation. starting from a specification of the java semantics written in maude, we develop an abstraction based, finite-state operational semantics also written in maude which is appropriate for program verification. as a by-product of the verification based on abstraction, a dependable safety certificate is delivered which consists of a set of rewriting proofs that can be easily checked by the code consumer by using a standard rewriting logic engine. The abstraction based proof-carrying code technique, called javapcc, has been implemented and successfully tested on several examples, which demonstrate the feasibility of our approach. we analyse local properties of java methods: i.E. Properties of methods regarding their parameters and results. We also study global confidentiality properties of complete java classes, by initially considering non–interference and, then, erasure with and without non–interference. Non–interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this thesis, we present a novel security model for global non–interference which approximates non–interference as a safety property. Erasure is a way of strengthening confidentiality by upgrading data confidentiality levels, up to the extreme of demanding the removal of secret data from the system. in this thesis, we also propose a certification technique for confidentiality of complete java classes that includes non–interference and erasure policies.
Datos académicos de la tesis doctoral «Abstract certification of java programs in rewriting logic«
- Título de la tesis: Abstract certification of java programs in rewriting logic
- Autor: Mauricio Fernando Alba Castro
- Universidad: Politécnica de Valencia
- Fecha de lectura de la tesis: 24/11/2011
Dirección y tribunal
- Director de la tesis
- María Alpuente Frasnedo
- Tribunal
- Presidente del tribunal: salvador Lucas alba
- ricardo Peña marí (vocal)
- Francisco Javier Duran muñoz (vocal)
- claude Marché (vocal)