Seminário de Teoria da Computação


                Algebraic Formal Methods I 
    Invariant Generation for Program Verification and Security


                      Rachid Rebiha

             Sexta-feira, 7 de novembro de 2008
                     Sala 85  16:00hs


Resumo:

We are interested in the development of new mathematical approaches
and concepts that would generalize recent formal methods for
verification and security.  In this talk, we would like to illustrate
the kind of problems that are in our research agenda.

We will present new methods that addresses the various deficiencies of
state-of-the-art invariant generation methods. An invariant at a
location in a program is an assertion true of any reachable program
state associated to this location. It is well-known that the
automation and efectiveness of formal verification of programs depend
on the ease with which strong invariants can be automatically
generated (e.g. safety properties can be reduced to invariant
properties).

- First we will provide mathematical techniques and design efficient
algorithms to automate the discovery and strengthening of non-linear
interrelationships among the variables of a program containing
non-linear loops, branching and initiation conditions ... . We will
also see how we extend this work to hybrid systems (program with
discrete structure and differential state evolution).

- Then we would extend the Logic of the program semantic by handling
uninterpreted function (suitable to deal with).  Here we propose
concept from Abstract Interpretation (fix point and abstraction theory
for static analysis) and unification theory (from theorem proving...).

- Using, these computed invariants, we will see how we could build
Host-Based Intrusion Detection System.  We will introduce
"Quasi-static analysis" and our "guarded model", a Host-based
intrusion detection systems that monitor an application execution and
report any deviation from its statically built model.  We will see how
this kind of automatically build model detect "mimicry attacks", the
even increasingly threatening "non-control-data flow attacks" and
"application logic bugs" (attacks beyond recent intrusion detection
systems).