Compile-time checks

The two FPL compilers are able to generate `resource safe' code, i.e., it is possible to check at compile time how many resources can be consumed by an expression, how many loop iterations may be incurred, etc. Neither FPL language supports pointers and interaction with the rest of the kernel is limited to the explicitly registered external functions. Also, while it is not possible to determine the resource consumption of external functions statically, we are able to check (and control) which functions may be called from a filter. As a result, a simple authorisation check rejects filter expressions that do not agree with the local safety policy and no runtime checks for resource consumption are necessary. This is explained in the next section. At runtime the code only checks for array bound violations, divide by zero, etc. By configuring the size of all buffers and slots as a power-of-2, bounds checking involves no more than a bitwise AND.

In an approach modelled after the OKE (see Section 3.5), the (trusted) FPL-2 compiler takes the filter expression, checks whether it is safe and if so, compiles it to a Linux kernel module which is subsequently compiled by gcc. It also generates a compilation record, which proves that this module was generated by the local (trusted) FPL-2 compiler. The proof contains the MD5 of the object code and is signed by the compiler (Figure 8). We check at load time whether the code was generated by a trusted compiler and whether the MD5 matches the code [8].

Figure 8: User compiles kernel module