Hook DSL

This project provides a very lightweight plugin for creating hooks to modify existing C programs. It is not so much a Doman Specific Language, as it is a method for modifying code.

The idea is that one way to modify existing software is by replacing specific functions with a "hook" function that may replace an existing function altogether, or may make changes to the parameters to the old function before calling it, or post-process the output of the old function.

For example, suppose you have a component that communicates with other components via messages, and you want to introduce encryption into the message passing. Just to make it interesting, suppose you don't have the source code to the original program, but you do know the semantics of the calls to send and receive messages. You can rename the old functions, e.g. changing send_message to send_message_hooked, and receive_message to receive_message hooked. Then, you create a new send_message that first encrypts the message content before passing it to send_message_hooked, and create a new receive_message that reads a message using receive_message_hooked and then decrypts it.

Because your new functions have the same name as the original functions, you shouldn't have to change any of the calls to the original functions, you just have to patch the names of the old functions. This does rely on still having to go through a linker, so that this may work best with dynamically loaded libraries.

The Hook DSL is not strictly necessary for creating hook functions. The reason it exists is just to facilitate the use of Frama-C in creating hooks.

The input to the Hook DSL is a C file that declares the functions that are to be hooked. It should contain Frama-C declarations that give the specification for each function, in terms of expected inputs and outputs. For each function prototype, include the annotation hook in the Frama-C ACSL specification.

For each function for which there is a hook specification, HookDSL will create an extern function declaration whose name is the original function name with _hook appended to it. For example:

/*@ requires b != \null;
 @ hook;
 */
void origfunc (float a, int *b);

The generated file includes the hooked function and the hook function, each with the Frama-C function specification, since the new hook function should conform to the same requirements, and if it calls the original function, the Frama-C can use the specification for the original function in proving properties of the new hook function.

The above declaration results in this file:

/*@ requires b ≢ \null;
    hook ; */
extern void origfunc_hook(float a, int *b);

/*@ requires b ≢ \null;
    hook ; */
void bar(float a, int *b);

void bar(float a, int *b)
{

}

To use a custom hooked function name, the hook specification can take function name prepended with a backslash. For example:

/*@ ensures \result > 1 && \result < 10;
 @ hook \calc_special;
 */
int calculate(int a, char b);

The generated file would look like this:

/* Generated by Frama-C */
/*@ ensures \result > 1 ∧ \result < 10;
    hook "calc_special"; */
extern int calc_special(int a, char b);

/*@ ensures \result > 1 ∧ \result < 10;
    hook "calc_special"; */
int calculate(int a, char b);

int calculate(int a, char b)
{

}

Building the Plugin

The plugin uses the Dune build system for Ocaml, which is available at https://dune.build/install The easiest way to install Dune is to use the Ocaml package manager Opam:

opam install dune
opam install frama-c

Then, build and install the plugin:

dune build
dune install

Running the Plugin

Use Dune to run the plugin. Use the -hook-output option to specify the name of the file that the plugin writes the new declarations to.

frama-c -hook-output hooked.c hookme.c