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
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
SIDAN is written in OCaml, and is implemented as a Frama-C plugin.