VeriFast Linux Kernel Module Verification Kit README
====================================================

The VeriFast Linux Kernel Module Verification Kit enables you to write verified
Linux kernel modules using VeriFast,
http://people.cs.kuleuven.be/~bart.jacobs/verifast/

The VeriFast Linux Kernel Module Verification Kit currently consists of:
-   A documented wrapper with formal specifications which wraps around the Linux
    API.  Verified kernel modules use this wrapper instead of the Linux API.
-   A buildsystem which takes care of both compiling and verifying the kernel
    module.  This buildsystem is integrated with Linux' buildsystem.

There is also an example verified kernel module, see helloproc_README.txt


Files
=====

Files: Use but do not edit
--------------------------

-   vf_*.h, except vf_*_impl.h
    The wrapper API specifications and documentation.
    You can #include them in your kernel module.

-   bool.h and limits.h
    Special cases.  You can #include these files in your kernel module
    too.


-   vf_README.txt
    This file.


Files: Edit
-----------

-   Makefile_template.make
    An example configuration file to get your kernel module compiled and
    verified.  Just fill in a few fields and rename to "Makefile".


Files: Implementation
---------------------
You don't have to look at the implementation in order to use it, the
API is documented.

-   vf_*.c and vf_*_impl.h
    Implementation of the wrapper API.  You need these files to get your kernel
    module compiled.
    Also contains motivation why the wrapper API specifications hold when
    the API implementation calls the Linux API.

-   vf_buildsystem.make
    Makes sure your kernel can be compiled and verified, integrated
    with Linux' build system, kbuild.
    
-   vf_*.vfmanifest
    Files telling verifast which procedures, ... from the vf_*.h files
    are implemented.
    
-   vf_autogenerated_initexit_proxy_*
    These are autogenerated files by the verify&build system, you can
    safely remove them.



How to make initialisation of a kernel module both work and be verified?
========================================================================

The initialisation and cleanup of the kernel module must be implemented
in the same C file.  Let's say that file is called xyz.c.
Write init and exit functions, with the following constraints:
- init and exit must be called xyz_module_init and xyz_module_exit.
  "xyz" must be the part of the filename before ".c".
- init and exit must implement the typedefs module_setup_t and
  module_cleanup_t, and be annotated as such.
- The init and exit procedures are not allowed to be static.

The result looks like this:

	void xyz_module_exit() //@ : module_cleanup_t(xyz)
		//@ requires module_state();
		//@ ensures module(xyz, _) &*& vf_cleanup_debt(0);
	{
		// ... implementation here
	}

	int xyz_module_init() //@ : module_setup_t(xyz)
		//@ requires module(xyz, true) &*& vf_cleanup_debt(0);
		/*@ ensures
			result == 0 ? module_state() : module(xyz, _)
			&*& result == -1 &*& vf_cleanup_debt(0);
		@*/
	{
		// ... implementation here
	}

Note that the only part you can actually choose in the above snippet
is the implementation and "xyz", which must be the filename (without
".c").

The predicate module_state() has to be defined by yourself (you can
put it in the same xyz.c file or in a .h file included by xyz.c).
Note that module_state must be produced by xyz_module_init and
consumed by xyz_module_exit.  Global data and predicates generated by
functions that create callbacks can be described in module_state(),
such that it is not leaked and xyz_module_exit can free it.

Next, the verify and build system needs to be configured for your
kernel module.  Copy Makefile_template.make to a file called Makefile,
and fill in the fields.

That's all.  The build and verify system (executed with "make",
"make verify_only" or invoked by kbuild) takes care of all the rest.




Code guidelines for VeriFast Linux Kernel Module Verification Kit developers
============================================================================
The wrapper API and implementation should be conform the Linux code and
documentation guidelines, see Documentation/CodingStyle and
Documentation/kernel-doc-nano-HOWTO.txt in the Linux kernel source tree.
But in first place, just make sure it's readable, documented,
with names that make sense (no "int tsbbn"), and secure.

There are a few extras:
-   VeriFast annotations are currently also documented like Linux'
    documentation guidelines, but are prefixed with "/*#" instead of
    "/**".
    
-   Functions, groups of global variable declarations, and other such
    "blocks" are currently separated by two newlines.
    
-   Motivation why the specs are conform the way Linux works, are
    written in the implementation (the .c files), not in the
    specifications (the .h files).
    
-   Write documentation in such a way that users can use the wrapper
    without looking at its implementation.  Users should never need to
    look at vf_*.c files.  This one is important.

-   Motivation why the specifications are the way they are, can be
    written outside the specification if you think it would be confusing
    or too much information for the user.  You can write them in a
    "/* ... */" block (instead of "/** ... */"), except when it's about
    the way Linux works, these things should be inside the vf_*.c files.