About SIDAN

SIDAN is an experimental tool for hardening C programs. It uses static analyses based on abstract interpretation to build a model of normal behaviour for a program, and then generates executable assertions checking at runtime the adequacy of the execution to the model. As such, it belongs to the family of behavioural intrusion detection systems.
More precisely, the model built by SIDAN defines invariant properties on the values taken by variables influencing function and system calls before &/or after the calls (those variables including —but not being restricted to— the functions arguments).

SIDAN is written in OCaml, and is implemented as a Frama-C plugin.