ftp://ftp.netbsd.org/pub/Netbsd/misc/proff/launder.tgz

This code intercepts, redirects, and injects network traffic to and
from userland (in other words, it launders it). It has been designed
from the ground up to be *very* fast and resilient in the face of
queue overflows. It can intercept 98Mps sustained on a p100,
transferring the lot to userland, and back. It's low enough level to
intercept and steal, rewrite and inject even ARPs or SNA. It's high
enough level so that IP packets without link level addresses can be
injected, routed, and link-layer encapsulated without direction. It
can be used for creating anything from a full userland protocol stack
to a stateful firewall, to a transparent VPN, to a network extender to
an IDS. It is flexible enough to read from / write to multiple
interfaces via the one device with no additional overhead (unlike
bpf). It has all the timers/high/low water marks and 64 bit counters
that *real world* projects need.

I wrote this code for a commercial project that embargoed release
(the dogs!). I've managed to get a hold of everything but the
kernel hooks and some build glue, which are:

        1) simple hooks ala bpf to specific ethernet driveres to call
           launder.
        2) a generic hook in ether_input. a hook in ip_output, ip_forward
           to grab packets originating at the local host and those packets
           fastforwarded.
        3) standard device ksrc build clue (conf/files etc)
        
Time commitments on my other projects mean I don't have time to bring
this into the tree myself :( but I'm sure it would make some people
happy. If anyone wants to hack on it, please feel free.

Cheers,
Julian.

-- 
Stefan Kahrs in [Kah96] discusses the
   notion of completeness--programs which never go wrong can be
   type-checked--which complements Milner's notion of
   soundness--type-checked programs never go wrong [Mil78].