Research Interests

(Last update: March 2, 2004)

  Abstract Non-Interference: We are studyng how to use abstract interpretation in order to model the notion of parametric non-interference relatively to an observation [GM03Sec]. Our aim is to model the power of the attackes by using abstract domains and to characterize the released information (robust declassification). More recently we defined a compositional proof system for proving abstract non-interference in a syntax directed way [GM04Sec].

  Abstract interpretation theory and applications: Actually we are studying the transformations of formal and constructive systematic methods for domain design in abstract interpretation, seen as closure operators in a Galois connection. Moreover we studied a systematic method for simplifying abstract domains in order to isolate the most abstract domain, when it exists, whose refinement toward completeness for a given semantic function returns a given domain [GM02Ref].

  Semantics: We applied systematic methods, in particular combination operations to semantics. This work is based on the semantics representation, given by Cousot, as abstraction of maximal trace (operational) semantics. In this way we have been able to design systematically symmetric [GM00, GMagp00] or compositional semantics [GM02]. We put together these works in order to characterize properties of semantics in terms of the properties of the operators used to design them. In this way we are able to design semantics as solutions of simple domain equations [GMjo]. We generalized the notion of compositional semantics to cope with transfinite reductions of a transition system. This generalization is necessary to deal with program manipulation techniques modifying the termination status of programs, such as program slicing [gm02hosc]. Moreover we enriched the hierarchy of semantics with the safety observable and we obtained it, such as one of its abstractions, as fix-point semantics [GMsafe].

  Static program analysis: We studied a numerical power domain for the analysis of properties of numerical variables. This domain allows to characterize varibles that, in a program, are numerical (integer or rational) powers of natural or integer values [M01,M01jo]. Moreover we generalized this kind of analysis in order to characterize invariant properties of the prime factorization of integer variables, i.e. we are able to find the prime factors of integer variables characterizing the properties of their exponents. We use this kind of analysis in watermarking process of software products [M01jo].

  The Formal method group in Verona.

  Semantics and Abstract Interpretation at ENS (P. Cousot)