IAISON (LearnIng and self-AdaptIng abStract interpretatiON) project aims
at investigating the synergies that can be obtained by combining Abstract
Interpretation (AbsInt) with other approaches and techniques, with a
special focus on Machine Learning (ML).
The project is composed of three lines of research, corresponding to
different interactions between Abstract Interpretation and
Machine Learning:
* AbsInt for (helping) AbsInt
* ML for (helping) AbsInt
* AbsInt for (helping) ML
AbsInt for AbsInt.
The starting point is the observation that the traditional approach to
implementing static analyses based on AbsInt, while being of general
applicability, may easily incur issues (e.g., intrinsic inefficiencies when
choosing the more precise abstract domains). This is mainly due to a
rigidity in the abstract computation process, which is usually driven by a
fixed configuration computed before starting the analysis of the program.
We thus propose the adoption of a more dynamic approach, where the
abstract interpreter is enhanced with self-monitoring capabilities and is
allowed to change its own configuration during the analysis: for instance,
the analyzer will be able to switch between different abstract domains in
different portions of the code being analyzed. We also plan to revisit the
abstract compilation approach to static analysis, by proposing the
application of just-in-time (i.e., dynamic) abstract optimizations that are
able to correctly specialize the code being analyzed, trying to obtain the
specific precision/efficiency tradeoff which is desired for the considered
context. An important requirement for this more dynamic approach to static
analysis is that it will be driven by lightweight heuristics (e.g., simple code
metrics) computed automatically, so as to obtain a self-adjusting static
analysis tool.
ML for AbsInt.
Since the selection of an appropriate set of heuristics for a class of target
programs is far from being trivial, we will experiment with the use of ML
methodologies and tools to automatically distill appropriate heuristics for
the self-adapting static analyzer described above. Later, we will become
more ambitious, and try to use ML (in particular, deep learning) as an
oracle, in an attempt to directly generate candidate semantic properties or
even full blown invariant properties for the program under investigation;
being potentially unsound, these guesses need to be checked for validity by
the static analyzer.
AbsInt for ML.
Here we reverse the direction of the interaction between AbsInt and ML
and study how AbsInt approaches may help in the quality assessment of
ML applications. In particular, we propose to study if and how AbsInt
techniques can be exploited (and maybe adapted) for understanding and
verifying neural network robustness to adversarial attacks