These wouldn't be general proofs of just anything - they would
naturally refer to the subject of the proof (i.e. the code), so that
altering the code automatically invalidates the proof.
Cosider type systems for example. Type checking a program amounts to
proving the type of each expression. How could a program carry a proof
about the types of its expressions? Simple, the "proof" just
annotates every expression with its type. The "proof verifier" just
goes through the program and makes sure the types are valid. (For C,
this example may seem a bit trivial - it has a first-order type
system, so it is easy to type check without the annotations; it's more
convincing for languages with higher-order type systems such as ML.)
Most of the work the Java bytecode verifier does is basically type
checking (e.g. it makes sure that the bytecode doesn't do things like
turn an integer into a pointer). So imagine a typed assembly
language, with things like
movl (%edx) : int*, %eax : int
If all the types are there, making sure they are correct is fairly
easy. This kind of approach could work well for machine code produced
by a Java compiler.
(I suspect the same is true of the BPF code, but I know next to
nothing about it.)
The problem is that kernels tend to be programmed in nice to-the-metal
languages like C, in which one can write perfectly type correct
programs that do nasty stuff, for example writing to deallocated
memory (which meanwhile may been allocated to an object with a
different type...). In general you can't prove that C programs don't
do dangerous things (hello Mr. Turing). So I doubt that proof-carrying
code would be useful for traditional kernel programming.
-- Dave Wragg- To unsubscribe from this list: send the line "unsubscribe linux-kernel" in the body of a message to majordomo@vger.rutgers.edu Please read the FAQ at http://www.altern.org/andrebalsa/doc/lkml-faq.html