Higher-Order and Symbolic Computation, 17(4)
Algebraic Power Analysis by Abstract Interpretation
Isabella Mastroeni, Dipartimento di Informatica,
Universita di Verona, Italy
Abstract: In this paper we design abstract domains for power analysis. These
domains are conceived to discover properties of the following type:
"The variable 'X' at a given program point is the power of 'c' with
the exponent having a given property 'pi'", where 'c' and 'pi' are
automatically determined. This construction is general and includes
different algebraic entities, such as numerical and polynomial (with
rational coefficients), as bases. Several families of domains are
presented, some of these consider that the exponent can be any natural
or integer value, the others also include the analysis of properties
of the exponent set. Relevant lattice-theoretic properties of these
domains are proved such as the absence of infinite ascending chain
and the structure of their meet-irreducible elements. The numerical
domains are applied in the analysis of integer powers of imperative
programs and in the analysis of probabilistic concurrent programming,
with probabilistic non-deterministic choice. Moreover we use the
numerical power domains in order to analyze the factorization of
integer variables, i.e., invariant properties of factors and of their
exponents. In this way we are able to statically detect information
hidden in prime factorization, which can be used in software
watermarking.
Keywords: Abstract interpretation, static program analysis,
algebraic power analysis, abstract domains, software watermarking.
|
This article is not yet available online.
|
|