Metacircular Interpretation

(* Buster Testacles and his infeasibly large Monad ... or is it
   Testacles Monad and his infeasibly large Buster ... or is it
   Monad Buster and his infeasibly large Testicles ... ?

   You see, it's worth taking some trouble to get the arguments in the
   right order, so that we can use currying and type-directed partial
   evaluation to compose monadic representations at the same time as
   we compose parsers for those types. And, if we can compose the
   types, then we should be able to compose the semantics too.

   There are also "fringe benefits" to be had --- decidable
   Higher-Order Unification, for example. That sounds useful. ["Higher
   Order Unification Revisited: Complete Sets of Transformations", by
   Wayne Snyder and Jean H. Gallier] It might make HOU decidable for
   any language we interpret in a monad. If so, then that ought to
   make quite a lot of stuff decidable. Peano Arithmetic (PA) for
   example. Then Ladies will be able to understand the proofs in the
   Arithmetica of Diophantus.

   The Arithmetica of Diophantus was written by a Woman. The reason I
   think I know this is that little men, e.g. Heath, don't seem to
   understand it. I know this because Heath asserts as a fact, some
   statement to the effect that ``Diophantus only used a single
   variable in his problems because he couldn't conceive of the notion
   "more than one variable"''.  _Even though_ he observes that
   Diophantus takes great pains to cast problems in two or more
   unknowns into monadic form.

   Heath apparently sees no reason to explain to his readers this
   utterly incredible discovery he has made: which is, how it is that
   the "man" who had apparently invented the notion of using a
   non-numerical symbol, i.e., a _variable,_ to represent an unknown,
   and who had proved dozens and dozens of theorems in arithmetic and
   whose examples frequently used six digit numbers, couldn't
   _conceive_ of the notion of "one variable" generalisng to "two
   variables" or "three variables".

   Heath thus seems to think Diophantus stupid. Yet Heath knows at the
   same time that he (Heath, I mean!) doesn't know how Diophantus
   proved "the porisms" which are referred to throughout the text. It
   doesn't seem to occur to Heath that the author might have had a
   _reason_ for not using more than one unknown value in the
   equations, and that that reason might have something to do with the
   unknown (to Heath) proof methods in the porisms. Maybe the machine,
   "for technical reasons", couldn't automatically generate proofs for
   propositions with more than one hypothetical?

   This is what I see as typical of how little men treat the thought
   of Women when it is so far advanced of their own that they cannot
   even recognise it as thought. They are at best patronising (see
   e.g. Babbage's comments on the work of Ada Augusta Lovelace), or
   they ridicule it. Perhaps that's better than them recognising that
   it _is_ thought, but not being able to understand it, because then
   they get angry and all they can think of doing is trying to insult
   her.

   Now if there is any reader who is scoffing "... and of course both
   Diophantus and Heath would have been completely familiar with
   Eilenberg and Moore, not to mention Moggi!" Well, I won't complain.
   At least you're not insulting me. But if you want to learn
   something, perhaps for the first time in your life, then look up
   what Aristotle writes on the theory of proportionals, in particular
   on the proposition Proportionals Alternate (PA) which is Euclid's
   Prop. V.16. It seems to be about using translations between
   languages to apply the same proof in three different domains:
   logic, arithmetic and geometry.

   But I have to agree with Wadler on one thing: I'm also a fan of
   John Reynolds. What I love about the man is that he writes to
   explain things, not just because he thinks he can make himself look
   clever. And he doesn't make himself look clever, because he
   explains things so well that he makes what he's writing about seem
   utterly trivial. Perhaps that's why so few seem to have heard of
   him, and also why hardly anyone seems to have really read anything
   he's written.

   This is a bit of a problem, because it's _systemic_. There's a
   mechanism in "academia" which consistently acts against anyone who
   thinks and writes clearly, and that means _anyone_ who does work of
   any real lasting value. As Leonard Cohen never dared to say,
   everybody knows that the mediocre is the enemy of the best, but how
   can they know that, really, when even the mediocre is perpetually
   swamped by the utterly useless?

   It doesn't take an academic "genius" to explain what is the
   mechanism either. The problem is _trade_. Human reason is not a
   least-fixedpoint, so it's not effective reason: it's co-effective
   reason, and a greatest-fixedpoint. So actual Human knowledge is
   inherently, necessarily, co-operative. Therefore, if you take
   people whose responsibility is the acquisition and dissemination of
   knowledge, and you force them to compete against each other in "the
   race whose prize is `Daily Bread'" then they are unable to
   co-operate without losing "the prize". Consequently, the good ones,
   who co-operate, and who actually know something, drop out, and the
   winners are ... can you guess?

   Well, by a truly remarkable co-incidence, they all turn out to be
   men who don't have time to read what other men write because
   they're far too busy writing things for those other men to not read
   ...  Now how long can this sort of thing go on before somebody
   cottons on to the fact that what's being published is, well, less
   than mediocre, shall we say? And what's going to happen then? I
   daresay there are a lot of very clever schemes that have been
   thought up to deal with it, so we needn't worry about anything,
   need we ...?

*)

signature Monad =
sig
   type 'a M
   val unit : ('a -> 'b) -> 'a -> 'b M
   val bind : 'a M -> ('a -> 'b M) -> 'b M
   val show : ('a -> 'b) -> 'a M -> 'b
end

signature Interpreter =
sig
   type term
   type result
   val eval : term -> result
end

signature Value =
sig
   type value
   type result
   val showval : value -> result
   val errval : string * string -> value
end

signature Evaluator =
sig
   type environment
   type term
   type value
   type 'a M
   val interp : term -> environment -> value M
end

signature Environment =
sig
   eqtype name
   type value
   type environment
   val lookup : environment -> name -> value
   val bind : environment -> name * value -> environment
   val null : environment
end

functor ListEnvironment
   (eqtype name
    type value
    val error : name -> value)
   :> Environment
      where type name = name
        and type value = value =
struct
   type name = name
   type value = value
   type environment = (name * value) list
   local fun lookup e n =
            case List.find (fn (n',_) => n' = n) e
              of NONE => error n
               | SOME (_,v) => v
         fun bind e p = p::e
   in
      val lookup : environment -> name -> value =
           lookup
      val bind : environment -> name * value -> environment =
           bind
      val null = []
   end
end

structure InterpI =
struct
   type name = string
   structure MonadI :> Monad =
   struct (* This way you see more clearly that the Monad is just a type function *)
      type 'a M = 'a
      val unit : ('a -> 'b) -> 'a -> 'b M
          = fn f => fn x => f x
      val bind : 'a M -> ('a -> 'b M) -> 'b M
          = fn x => fn f => f x
      val show : ('a -> 'b) -> 'a M -> 'b
          = fn f => fn x => f x
   end
   datatype value =
       Wrong
     | Num of int
     | Fun of value -> value MonadI.M
   datatype term =
       Var of name
     | Con of int
     | Add of term * term
     | Lam of name * term
     | App of term * term
   structure Value
      :> Value
          where type value = value
            and type result = string =
   struct
      local
         fun showval Wrong = "<wrong>"
           | showval (Num i) = Int.toString i
           | showval (Fun _) = "<fn>"
         fun errval (_,_) = Wrong
      in
         type value = value
         type result = string
         val showval : value -> result =
            showval
         val errval : string * string -> value =
            errval
      end
   end
   structure Env : Environment =
      ListEnvironment (type name = name
                       type value = Value.value
                       val error : name -> value =
                          fn n => Value.errval ("bind",n))
   structure Evaluator
      :> Evaluator
            where type value = value
              and type 'a M = 'a MonadI.M
              and type environment = Env.environment
              and type term = term =
   struct
      type environment = Env.environment
      type term = term
      type value = value
      type 'a M = 'a MonadI.M
      local
         open MonadI
         fun add (Num i) (Num j) = Num (i + j)
           | add _ _ = Value.errval ("Add","wrong type(s)")
         fun app (Fun k) a = k a
           | app _ _ = unit Value.errval ("App","wrong type")
         fun interp (Var x) e = unit (Env.lookup e) x
           | interp (Con i) e = unit Num i
           | interp (Add (u,v)) e =
                         bind (interp u e) (fn a =>
                         bind (interp v e) (fn b =>
                         unit (add a) b))
           | interp (Lam (x,v)) e =
                          unit Fun (fn a =>
                                      interp v (Env.bind e (x,a)))
           | interp (App (u,v)) e =
                          bind (interp u e) (fn a =>
                          bind (interp v e) (fn b =>
                          app a b))
      in
         val interp : term -> environment -> value M
            = interp
      end
   end
   fun eval t =
      let val env = Env.null
          val m = Evaluator.interp t  env
      in MonadI.show  Value.showval m
      end
end

(*             Wadler calls this "the standard meta-circular
               interpreter". But Reynolds, who coined the phrase, might
               not agree, because this interpreter doesn't
               interpret itself. This is because it doesn't
               represent the abstract syntax and deconstruct it.

               It might be argued that this is merely a nicety, but
               consider the questions Wadler asks, such as "How do we
               compose interpreters in a monad?" And "Can we interpret
               a call-by-need interpreter in a monad?" If the
               interpreters really were meta-circular then the answers
               to these questions would obviously be positive.

               And Wadlers interpreters aren't modular, as he
               claims. They're all one big amorphous blob.

               If you now go and carefully read Reynolds' paper
               "Definitional Interpreters for Higher-Order Programming
               Languages" in Higher-Order and Symbolic Computation, 11,
               363–397 (1998), you will see that the treatment he
               gives there is far, far superior to the one Wadler
               gives, some twenty years later.

               Note, for example, how Reynolds uses recursive symbolic
               _environments_ to implement fixedpoint combinators, and
               how they dissolve in the first-order translation (p.
               381).  The resulting first-order meta-circular
               interpreter is one of the most beautiful 20 lines of
               code I've ever seen: it is just three lambda
               expressions (excluding the trivial wrapper function
               interpret) and one pair of these---eval and apply---are
               mutually recursive. The function eval also calls the
               function get, which is (simply) recursive. One final
               interesting point to note is that eval takes _two_
               arguments: a value, and an environment, which is a kind
               of _state._

               If anyone can show me more recent work that uses this
               idea, with or without attribution, I would be very
               interested to hear about it. I have never come across
               the idea mentioned anywhere else, and it is what a
               mathematician might call "highly non-obvious".

               Another notable feature of Reynolds' treatment is that
               he uses abstract syntax as an informal type
               discipline. All the values used in definitional
               interpreters are for all practical purposes,
               typed. This is from "Definitional Interpreters
               Revisited" in Higher-Order and Symbolic Computation,
               11, 355–361 (1998):

                  In “Definitional Interpreters”, however, closures do
                  not contain lambda expressions, but merely unique
                  tags that are in one-to-one correspondence with
                  occurrences of lambda expressions in the program
                  being defunctionalized. The computations described
                  by these occurrences are moved to interpretive
                  functions associated with the points where closures
                  are applied to arguments. Moreover, within each
                  interpretive function the case selection on tags of
                  closures is limited to those tags that might be seen
                  at the point of application

            .     I’ve been told that this was an early example of
                  control flow analysis in a functional setting, which
                  has inspired some of the extensive development of
                  this area [23]. In fact, however, the limiting of
                  the case selections was not determined by control
                  flow analysis, but by the informal abstract type
                  declarations (called abstract syntax equations) that
                  guided the construction of the original interpreter.

               Something which any reader of the full paper will find
               curious is the fact that Reynolds' for some reason
               implements the successor function and the equality
               relation as bound values in the first four
               interpreters, even though none of the interpreters
               actually use these functions. The answer is perhaps
               that in the last interpreter, which implements
               memories: which are essentially lists of references,
               the successor and equality are the only two primitive
               constants that are needed, And coincidentally this is
               also enough to bootstrap PA.

               So why would anyone want to implement the last
               interpreter in the first one? Perhaps because the first
               one can be implemented pretty easily in any language.

               And that leads to the question "Why would anyone want
               memories in the first interpreter?" Well, memories are
               essentially lists of references to values
               (cf. Reynold's comment quoted above, regarding how
               closures are implemented, and the role of abstract
               syntax as an informal type discipline). So memories
               allow one to implement abstract syntax in the
               interpreter. And that, I think, is why the first
               interpreter is called meta-circular: because it can
               interpret the last interpreter, which can interpret the
               first one. So those first 20 lines of code are enough
               to bootstrap any language which can be described by a
               grammar, i.e. in terms of abstract syntax equations on
               records, and a formal semantics described in terms of
               untyped lambda calculus.

               That would make quite a neat API for the LLVM JIT
               engine, wouldn't it? There's not much that one would
               have to write ad-hoc, and then from any scripting
               language, one could interpret interpreters with a
               full-on assembler, capable of optimising tail-recursive
               calls, and handling and throwing exceptions, and all
               this running in native machine code on half a dozen
               different processor architectures. And an API like that
               would be an awful lot easier to use than all that macho
               hairy stuff with templates and abstract classes and
               what-not. Are there _really_ no simpler ways to
               implement abstract syntax in c++?

               Now if we have memories representing abstract syntax,
               then we have (informally) typed values, one of which is
               the type of memories. And those memories can hold any
               sort of object that could be described by a recursive
               set of abstract syntax equations.

               Now take a look at the type system that MacQueen,
               Plotkin and Sethi describe in "An ideal model for
               recursive polymorphic types" (1983) The ideal model is
               just such a set of recursive equations. Note that they
               define a least-fixedpoint type variable binder, and a
               pair of rules that can be included in a type inference
               algorithm W, with a circular unification algorithm. As
               MacQueen et al. point out, type checking is undecidable
               in general, but this can be used in practice, and the
               denotational semantics handle the possibility, because
               there is the error value W for _dynamic_ type errors. So
               much for mu, the least fixedpoint. There is also the
               type nu, of type environments, which are functions from
               variables to ... well, memory values, I suppose. Like
               the algorithm W would be, implemented meta-circularly:
               a function from lambda expressions to memory values,
               i.e. abstract syntax representing types.

               Now look at the 1982 paper "Principal Typeschemes for
               Functional Programs" by Damas and Milner, and see the
               curious comment they make in the section describing the
               denotational semantics, to the effect that "A free type
               variable is implicitly universally quantified across
               the _whole_ of the expression in which it appears, and
               so it is sufficient to verify just the instantiation of
               type variables by any monotype ... " The whole
               expression in this case includes the "modelled by"
               turnstile, so they seem to be referring to some sort of
               inner model of the type system ... one that could be
               described in terms of memories, perhaps?

               And since untyped lambda expressions can be represented
               by abstract syntax, and since the successor and an
               equality predicate can be implemented in untyped lambda
               calculus, there you have it: operational semantics from
               hot aehr! (This Aristotle's term, meaning
               "information", as far as I can tell.)

               Which brings us to "Proofs and Bloody Types" by Girard
               et al. Perhaps the missing intuition (all of it is
               missing, from that book!) is to be found in this
               "operational denotational semantics" idea. Look perhaps
               at their "denotational" model of system-T expressions
               as untyped lambda expressions implemented as an
               operator algebra and written in the language of ZF set
               theory, then at their reducibility proofs for System F,
               and then at the proofs in MacQueen et al. on the
               contractive/non-expansiveness of the type operators
               when they are under least-fixedpoints: these have an
               eerie familiarity (so much so that it makes me feel bit
               sick to think about it, but I hope that I'll soon be
               able to face opening that book again, and enjoying it
               --- once I have some idea what it's about.)
 *)

local
   open InterpI
   val term0 = (App (Lam ("x", Add (Var "x", Var "x")),
                     Add (Con 10, Con 11)))
in
   val rI = eval term0
end

Lewis Carroll´s Sylvie and Bruno

https://drive.google.com/file/d/0B9MgWvi9mywhbjZCblQzYWQ5RWx0SkN0NklrRzgtRllOYWVB/view?usp=sharing

Representing Data

This is what was really the idea behind Red October a general data representation for any interpreted language.  It includes a section on some potentially interesting applications to cryptography, and an explanation on pages 14-15 as to why I am not yet convinced of any claims that the security of any cryptographic protocol is based on mathematics.

https://drive.google.com/file/d/0B9MgWvi9mywhX0tlbldHSjYzR0NkWGMwaGxPeVlTWVpLdkg0/view?usp=sharing

Process Synchronisation by Communication

This is about using inter-process communication to implement process synchronisation primitives which can be used in distributed multi-programming systems: computation "in the cloud" where the particular machines which carry out the steps of a computation are nondeterministically chosen as the computation progresses. Computation distributed in this way is secure, because no one physical system has a complete representation of the state of the computation.

https://drive.google.com/file/d/0B9MgWvi9mywhN01WTHF2RmpTOWtGYlR4VjdQaWhEQlBFWHJN/view?usp=sharing

The T.H.E. Multiprogramming System Mk II

I have reformatted Dijkstra´s original as it appeared in the 1968 Communications of the ACM paper which includes an appendix not in the typewritten manuscript. The appendix gives more details of the methodology for verifying the design.:

   https://drive.google.com/file/d/0B9MgWvi9mywhTkxJQzFoTFppZ3dwNHk4TjJUbjA3LTFhT2dV/view?usp=sharing

And Dijkstra´s notes on Multiprogramming go into yet more detail, giving a nice example of how to work through a problem of devising a mechanism which is more or less GNU Screen:

   https://www.cs.utexas.edu/users/EWD/ewd01xx/EWD123.PDF

Here is an outline for another version of the system, with real-time performance guarantees. I was moved to write this by the very impressive way that my Standard ML mock-up of the system works.

    https://drive.google.com/file/d/0B9MgWvi9mywhbjg0Q0dYOVFkTmVyR0F1YUJDTjAtUTlENnBr/view?usp=sharing

Shadow TCP stacks in OpenBSD

This design outline concerns the implementation of a protocol for
dynamic routing by port-knocking in the OpenBSD packet filter
pf(4). This protocol is intended for the purpose of protecting virtual
private networks against denial of service (DoS) attacks from without.

This design is intended solely to enhance _availability_ of services
which would otherwise be open to DoS attacks; it is a dynamic routing
protocol and makes _no_ claims to do anything for the _privacy,
integrity_ or _authenticity_ of the traffic payloads. These issues are
properly addressed by transport protocols such as IPSEC and TLS.

The idea is to provide a means by which the existence of any TCP
service may be rendered undetectable by active port-scans and/or
passive traffic flow analyses of TCP/IP routing information in the
headers of packets passing over physical (as opposed to virtual,
i.e. tunnelled) networks.

Only those with a certain specific "need to know" will be able to
direct traffic to those IP addresses which are the ingress points of
protected VPNs. This need-to-know will be conferred by the device of a
one-time, time-limited pre-shared key transmitted in the 32 bit ISN
field of SYN packets used to initiate one or more TCP/IP connections
between certain combinations of host/port.

This design should make possible the implementation of e.g., proxy
servers which automatically track VPN ingress point routing changes
and manage the creation, distribution and use of pre-shared keys on
behalf of clients and servers behind pf(4) "firewalls", and
furthermore, to do this transparently; i.e. without imposing any
procedural requirements on the users, and without modification of the
client/server operating-system or application programs on either side
of the interface.

This in turn will make possible the implementation of services to
dynamically (and non-deterministically, from the point-of-view of
anyone without a VPN connection) change the physical network addresses
of the VPNs' points of ingress, and to do this rapidly and frequently,
whilst automatically distributing the necessary routing changes to
enable the subsequent key generation and distribution described in the
preceeding paragraph.

The design presented here owes a great to the TCP Stealth design of
Julian Kirsch[1]. The difference is only that instead of making the
one-time use of keys dependent on the varying TCP timestamp, which is
not universally implemented, we make the pre-shared key itself
one-time, and we extend the protocol to arbitrarily long sequences of
knocks which may be from more than source address, directed to more
than destination, and may be either synchronous or asynchronous. We
also implement the protocol as a routing mechanism, so making the
existence of services invisible to probes of active attackers as well
as passive ones who merely observe traffic flows (c.f.[1] Sec 3.2,
p10). Another reason for not using the TCP timestamp as a key
modulator is that an attacker who can block the SYN/ACK responses of a
server knock can identify TCP Stealth knocks by the fact that the
retransmissitted SYN packets have the same TCP timestamp.

One good feature of Kirch's design we have not implemented is the
prevention of session hijacking by a man-in-the-middle. This is
achieved by the device of varying the isn-key according to the first
bytes of the payload of the first packet received after the connection
is established. The benefit of this is significant because an attacker
who can intercept TCP handshakes can effect a DoS attack on the client
by hijacking successful knocks, but with TCP Stealth payload
protection the server can safely reject or divert the hijacking
attempts and still allow the genuine client to connect, possibly
through the pfsync peer.

We do not implement this because it requires further changes to the
pf(4) modulate state code path, which would significantly complicate
testing. We have however made the key_type a parameter so this feature
should be added as a second phase development once the basic
functionalty has been well-tested.

The following is an attempt to specify precisely what changes to the
existing pf(4) and related programs are required to implement the
desired functionality. Constructive comments would be much
appreciated.

Objections that this is so-called "security by obscurity" are simply
not valid because the isn-keys have time-limited validity, are
one-time use only, may be made arbitrarily complex and may be chosen
non-deterministically from the point of view of anyone who does not
have access to the protected VPNs, which already implies the required
need-to-know. We are in effect encrypting the destination addresses of
IP traffic with a one-time pad. Using a synchronous four key knock
sequence, for example, even knowing the exact length of the knock
sequence and all of the m possible source addresses and n possible
destination addresses, any would-be attacker will have a chance of far
less than one in 2^128 of correctly guessing the key.

[1] Julian Kirsh, "Improved Kernel-based Port-knocking in Linux",
    Munich, 15 August 2014.

          =========================================

The implementation will be maintained as a patch to the standard
OpenBSD source tree, affecting the pf(4), pfsync(4), tcpdump(8) and
pfctl(8) programs.

We require the implementation to satisfy the following conditions:

   1. The code changes should be _trivially_ proven to not affect
      potential security in _any_ way, if the features provided are
      not in fact explicitly enabled in the pf(4) configuration.

   2. When the features it provides _are_ used, it should be stated
      exactly (and verifiably, so with explicitly stated reasons) what
      negative security effects they potentially have on the operation
      of pf(4).

   3. Changes to existing code should be the minimum required to
      implement the required functionality, and they should be such
      that (a) their operational effects can be easily verified to be
      conditional on the explicit enabling of the feature, and (b)
      they are absolutely necessary for the implementation of that
      feature.

   4. A strategy for exhaustively testing _all_ significant conditions
      on _all_ the modified code-paths must be laid out in advance of
      implementation, and an exhaustive list of test cases developed
      as the modifications are added.

The following design satisfies condition (1) because the default
maximum no of isn-keys in the isn_key tree is 0, hence it must be
explicitly set to a value > 0 by an ioctl(2) call, or the appearence
of "set limit isn-keys n" in the ruleset. But the first line of the
rule match testing (see step 9. below) requires the ISN appear in the
isn-keys tree, otherwise the packet is passed by that rule. Hence
unless explicitly enabled, this feature has no effect whatsoever on
any packet routing: all packets are passed as if the rule did not
exist.

Likewise any ioctl(2) operations will fail (see step 6. below) if the
isn-keys table size is found to be zero. Also, since no
isn-key-related pfsync(4) operations will occur if isn-keys is zero
(see step 12. below) and since all new pfctl(8) operations are via
ioctl(2) calls, (see steps 2. & 3. below) there will be no change to
the operation of either pfctl(8) or tcpdump(8), which will not receive
isn-key-related packets from the pfsync i/f. In addition, since the
default maxisnkeytmo timeout is 30s, no keys will affect routing
decisions, or use pf(4) resources for more than 30 seconds, unless
explicitly enabled.

The following design satisfies condition (2) because the first line of
the rule match testing (see step 9. below) requires the keys must all
have dst/src address in the anchor-local isn_key_{dst,src}
table. Therefore the only effect the isn-key rule option can have is
on packets where addresses of both endpoints have been explicitly
added to the respective tables.

Furthermore, since every isn-key is removed from the isn_keys table on
first use, and since connections are deferred until the pfsync(4) peer
ACKs these removals, in normal operation (i.e. with an congestion-free
pfsync(4) physical i/f between the peers), no isn-key will effect the
establishment of more than one TCP connection.

To show that condition (3) is also satisfied, the satisfaction of each
of the requirements 3a and 3b will be noted for each change in turn in
the steps below.

Condition (4) will be satisfied by a testing framework based on qemu
emulations of one or more systems (the test machines) "instrumented"
by debug log messages redirected by syslogd(8) to a pipe program which
writes them to a serial device /dev/cuaXX, from whence they will be
read by the test framework running on the test host monitoring the
associated qdev pipe. The test frame workwill match a certain "test"
prefix with an event code to a particular test event. The test
framework will be able to respond to events by executing programs as
root as necessary to set up configurations, configure interfaces etc,
by writing commands to, and reading output from, a pipe which will
correspond to the stdin/stdout of a root shell on the test
machines. The test framework will also be able to communicate with
arbitrary other programs on the test machines to make certain ioctl(2)
calls, etc, based on input from serial devices via qemu ipies on the
test host. The test framework will also have access to tunnels via
which it can send and receive raw packets on the test network. The
test framework will be scripted by a command language allowing the
specification of stte machines which respond to events and timeouts by
actions and state-change changes. Actions will include the ability to
schedule timeouts, send packets, log test results etc.

The details of the test framework have yet to be specified. For now we
will simply note the facilities that will be required to test the
changes below.

1. Add a new pool and RB trees, in sys/net/pf.c, for isn keys, if and
   only if PF_LIMIT_IKS > 0. Fields are:

      keyid, proto,
      src_add, src_port, dst_add, dst_port, anchor,
      keyseq, async, seqno,
      isn_key, key_type, timeout, uid, gid

      Where src_add and/or dst_add may be specified as addresses are
      specified in pf rules, i.e. as table names, route labels, etc.

      If keyseq == keyid then
          If seqno == 1 then this is a simple key.
          Otherwise it's the last in a sequence of seqno knocks

      A synchronous knock sequence is made in reverse order of seqno,
          Otherwise it's asynchronous and the knocks can be
             made in any order, except the last must have
             keyseq == keyid

      Add pf_isn_key_insert
      Add pf_find_isn_key_byid etc.

      Add pf_status.isn_keys          - pfvar.h line 1415
      Add pf_status.maxisnkeytmo       - pfvar.h around line 1406
      Add pf_status.isnkeyid

      Also add ioctls for setting/getting maxisnkeytmo, see step 6
      below.

   Implementation conditions:
  
   (3a) the allocation of the new pool and RB trees are conditional on
        the explicit enabling of the service by setting the
        PF_LIMIT_IKS to a non-zero value.

   (3b) It is absolutely necessary to store the pre-shared keys in the
        pf(4) address space if it is to check for their existence in
        filtered packets.

    (4) Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test1.X referring
        to this step.

2. Add pfctl.c functions:

      Add pfctl.maxisnkeytmo - pfctl_parser.h line 92
      Add syntax for maxisnkeytmo at parse.y, around line 678
      Add pfctl_{set,load}_maxisnkeytmo to pfctl.c line 1890

      void pfctl_set_maxisnkeytmo(struct pfctl *pf, u_int32_t seconds)
      int pfctl_load_maxisnkeytmo(struct pfctl *pf, u_int32_t seconds)

   Implementation conditions:

   (3a) pfctl implements the change via iocrl(2) calls, so by the
        condition on step 6. below, the timeout can only be extended
        if the limit[PF_LIMIT_IKS] > 0

   (3b) The ability to extend the maximum key timeout is a necessary
        contingency for the case where exposed transport networks are
        congested, possibly because of an ongoing DoS attack flooding
        one or more links.

    (4) Test framework for running pfctl with arbitrary commands to
        load rulesets and test for errors.

3. Add a new limit (pfctl_set_limit) counter:

#define PFIKS_HIWAT        0    /* default isn-key tree max size */
    { "isn-keys",        PF_LIMIT_IKS }, /* sbin/pfctl/pfctl.c line 143 */

   Implementation conditions:
  
   (3a) This requirement dropped due to circularity.

   (3b) It is self-evident that this feature is absolutely necessary.

    (4) Test framework for running arbitrary isn-key related ioctl(2) commands to
        load rulesets and report results and errors.

4. Add isn-key keyword for matching rules

   sbin/pfctl/parse.y line 2395
       "  "   "            1834

   Add post-parse checks for:
        no multiple use,
        only with IPPROTO_TCP,
        only with keep-state outgoing rules if SYN_PROXY is used

   Add filter_opts.isn_key flag        - sbin/pfctl/parse.y line 250
   Add pf_rules.isn_key flag           - pfvar.h, line 625

     u_int8_t         isn_key;

   Implementation conditions:
  
   (3a) Although rules may be introduced without having explicitly
        enabled the feature by setting limit[PF_LIMIT_IKS] > 0, the
        setting of the flag has no effect on routing if the feature is
        not enabled, as per the first match-test condition of step
        9. below.

   (3b) It is self-evident that this feature is absolutely necessary.

    (4) Test framework for running pfctl with arbitrary commands to
        load rulesets and test for errors.

5. Add purge_thread function for clearing isn key tree:

    pf_unlink_isn_key pf.c line 1273
    pf_free_isn_key
    pf_purge_expired_isn_keys

   The above functions should either panic, or return immediately if
   limit[PF_LIMIT_IKS] == 0.

   Implementation conditions:
  
   (3a) If there are no keys in the isn-keys table, then these
        functions will return immediately.

   (3b) This feature is absolutely necessary because isn-keys are
        time-limited, and must be removed from the tree when timed
        out to free the limited tree space.

    (4) Test framework for running pfctl with arbitrary commands to
        load rulesets and test for errors.

        Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test5.X referring
        to this step.

6. Add ioctl(2) calls to get/set/clear entries, in groups

   In sys/net/pf_ioctl.c:

#define DIOCCLRIKS    _IOWR('D', 97, struct pfioc_ik_kill)
#define DIOCGETIK    _IOWR('D', 98, struct pfioc_ik)
#define DIOCGETIKS    _IOWR('D', 99, struct pfioc_iks)
#define DIOCADDIKS    _IOWR('D', 100, struct pfioc_iks)
#define DIOCSETMAXISNKEYTMO    _IOWR('D', 101, u_int32_t)
#define DIOCGETMAXISNKEYTMO    _IOWR('D', 102, u_int32_t)

   Or can we use 51--56?

   Always fail any of the above ioctl(2) calls whenever
   limit[PF_LIMIT_IKS] == 0

   In DIOCADDIKS: the timeouts must be >0 and <= maxisnkeytmo
                  a simple key shall have seqno == 1 and async == 0
                  if seqno > 1 then there must be at least seqno - 1
                      following keys in the input structure and if
                      the seqno of each of this set are in strictly
                      descending order from seqno ... 1, then those n
                      keys will form a single compound knock.
                  in either case, the keyseq values must all be 0,
                      and will be filled in and set equal to the keyid
                      of the first key in the sequence.
                  async should be 0 or 1 and must be the same for all
                      keys in a sequence.

        If any of the above checks fail, EINVAL is returned without
        altering the key tree in any way: i.e. all keys must be
        correct, or none will be added.
                  the keyseq values must all be 0, and will be filled
                      in and set equal to the keyid of the first key.

   Add EACCESS permission checks for new ioctls

   Add ioctls for maxisnkeytmo

       Add pf_trans_set.maxisnkeytmo around pf_ioctl.c line 130

    u_int32_t    maxisnkeytmo;

 #define    PF_TSET_MAXISNKEYTMO        0x10

       Add PF_TSET_* case for pf_trans_set_commit() around line 2733

   If real uid is non-zero, then only get/add/clr isn-keys with that
      particular real uid/gid.  Get ruid, rgid from
      p_cred->p_r{uid,gid} thus:

       uid_t ruid = p->p_cred->p_ruid;
       gid_t rgid = p->p_cred->p_rgid;

       isn_key->uid = ruid == 0 ? pfik->pfsync_ik->uid : ruid;
       isn_key->gid = ruid == 0 ? pfik->pfsync_ik->gid : rgid;

   sbin/pfctl/pfctl.c option changes:
  
   Add -F option modifier 'Keys' to flush isn-keys table

   Add -s option modifier 'Keys' to show isn keys, line 2376:
   Add isn-keys show on 'show all' option.

   Implementation conditions:

   (3a) The ioctl(2) calls fail if limit[PF_LIMIT_IKS] == 0, and the
        extra pfctl(8) options are implemented by these ioctl(2)
        calls.

   (3b) The ADDIKS ioctl is self-evidently necessary and the CLRIKS
        ioctl is necessary to disable the feature. The GETIKS/GETIK
        are necessary to find out what keys are currently enabled. The
        GET/SETMAXISNKEYTMO ioctls are necessary to allow this to be
        changed at run-time without flushing and reloading the entire
        pf(4) ruleset.

        We do not use the existing mechanism for setting default
        timeouts because this is not a default timeout, it is the
        _maximum_ timeout.

        The -s and -F modifiers are necessary to allow the key table to
        be examined and/or flushed quickly and easily.

    (4) Test framework for running pfctl with arbitrary commands under
        arbitrary real uids/gids (via sudo) to load rulesets and test
        for errors.

        Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test6.X referring
        to this step.

7. Add reason codes for dropping packets

   #define PFRES_PRE_ISN_KEY    16        /* isn-key */
   #define PFRES_BAD_ISN_KEY    17        /* bad isn-key */

   Implementation conditions (3a) and (3b) and (4) are satisfied where
   these codes are used in steps 9. and 10. below.

8. Add field pf_desc.isn_key to keep the ISN of the incoming SYN packet.

   Implementation conditions:

   (3a) Has no effect in itself, regardless of whether or not the
        feature is enabled.

   (3b) required for step 10. below.

9. Add isn-key rule matching/key dropping code around pf_test_rule pf.c line 3245

   This only works for outgoing TCP connections if they are matched by
     isn-key rules which specify SYN_PROXY keep_state, which must then
     use exactly this isn-key for the ISN on the server-side of the
     connection.

   To test packets, look up all isn-keys matching anchor/proto and
     where {dst,src}_add are each in the anchor-local
     isn_key_{dst,src} table (resp.) Then test each one for detals:
     address/uid/gid/etc as follows:

 (*) If nothing then
       pass
     Otherwise
       Match incoming connects on dst_add/port and isn_key
       Match outgoing connects on dst_add/port and
         src_add/port(0 is wildcard) and test that if non-zero,
         the uid/gid of the isn-key entry match those of the
         src_add/port sockets.
 
       The result of this will be a single key, or nothing
       If nothing then
         pass
       Otherwise
         If the matching isn-key has keyid == keyseq then
           If either seqno == 1 or this is the only key with this keyseq then
              set pf_desc.isn_key to the matching isn_key
              match
           Otherwise
              DEL the entire sequence keyseq == this_keyseq && keyid != this_keyid
              log BAD_NOCK
              pass PFRES_BAD_ISN_KEY
    
         Otherwise
           If async == 1 then
              pass PFRES_PRE_ISN_KEY
           Otherwise
              If this_keyid is first in a list of isn-keys with
                        keyseq == this_keyid sorted by descending order of seqno then
                 pass PFRES_PRE_ISN_KEY
              Otherwise
                 DEL the entire sequence keyseq == this_keyseq && keyid != this_keyid
                 log BAD_NOCK
                 pass PFRES_BAD_ISN_KEY

         DEL the key with keyid == this_keyid

    On receipt of a valid SYN/ACK with a final matching ISN key, wait
      for pfsync to DEL_ACK this before making the connection.

    Other protocols (currently there are none): hold the first packet
      until the pfsync DEL_ACK arrives.

      This prevents a race with another firewall. For this to work,
      the interface must have been set up for pfsync(4) deferral using
      ifconfig(4), and the pfsync physical i/f must be congestion-free
      so that deferrals are not timed out (at present, this means they
      must be ACKed by pfsync within 20 ms. which is hard-coded.)

   Implementation conditions:

   (3a) The first step (*) of the match test requires the isn-key
        table to be non-empty, so that if the feature is not enabled
        by setting limit[PF_LIMIT_IKS] > 0 then the candidate key list
        will be empty and no packet routing changes will be made.

   (3b) It self-evident that this is absolutely necessary to implement
        the required functionality.

    (4) Test framework for running pfctl with arbitrary commands under
        arbitrary real uids/gids (via sudo) to load rulesets and test
        for errors.

        Test framework actions to send TCP packets

        Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test9.X referring
        to this step.

        Test framework events corresponding to receipt of TCP packets
        with certain matching SEQ and ACK fields, flags, src and
        destination addresses:ports. These could be implemented using
        a bpf(4) filter attached to the test machine tunnel i/f on the
        test host.

10. Modify SYN_PROXY and MODULATE_STATE to preserve ISN for outgoing
    isn-keyed connections pf.c lines 3547 and 3652 (We want the SYN flood
    protection, but we need to be able to choose the ISN)

    Always make changes to the existing routing code conditional on
    both pf_desc.r->isn_key and pf_desc.isn_key being non-zero, so
    that it is easy to show there are no changes to the routing of any
    packet which is _not_ matched by some isn-key rule and some
    particular key in the isn-key tree.

   Implementation conditions:

   (3a) The pf_desc.isn_key is only non-zero when a match with some
        entry in the isn-key tree has occurred, and this can only
        happen when the feature has been explicitly enabled.

   (3b) These changes are absolutely necessary to implement the
        feature because the SYN_PROXY code would otherwise change the
        ISN of outgoing TCP SYN packets thus preventing the feature
        from working for outgoing connections.

    (4) As for step 9 above.

        Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test9.X referring
        to this step.

11. Add pfsync structures and packets for isn keys

#define PFSYNC_ACT_INS_IK    16    /* insert isn key */
#define PFSYNC_ACT_DEL_IK    17    /* delete isn key */
#define PFSYNC_ACT_DEL_IK_ACK    18    /* delete isn key ACK */
#define PFSYNC_ACT_CLR_IK    19    /* clear all isn keys */

Add to if_pfsync.h line 285:

#define PFSYNC_S_IKDACK    0x06

// One hopes there is some administrative mechanism to reserve numbers
// in this space so that patches can be applied to consecutive OpenBSD
// releases without prejudicing the compatibility of patched pfsync(4)
// implementations in consecutive releases.

struct pfsync_isn_key {
    u_int64_t     keyid;
    u_int64_t     keyseq;
    u_int32_t     anchor;
    u_int8_t     seqno;
    u_int32_t     isn_key;
    u_int32_t     timeout;
    u_int32_t     keytype;
    u_int8_t     async;
    struct pf_rule_addr     src;
    struct pf_rule_addr     dst;
    uid_t           uid;
    gid_t         gid;
    u_int8_t     proto;
    u_int32_t     creation;
    u_int32_t     expire;
    u_int32_t     creatorid;
    u_int8_t     sync_flags;
};

struct pfsync_clr_ik {
       char                anchor[MAXPATHLEN];
       u_int32_t            creatorid;
} __packed;

struct pfsync_del_ik {
    u_int64_t            keyid;
    u_int64_t            keyseq;
    u_int32_t            creatorid;
} __packed;

struct pfsync_del_ik_ack {
    u_int64_t            id;
    u_int32_t            creatorid;
} __packed;

   Implementation conditions:

   (3a) These changes only have operational effects when code in steps
        12. and 13. below uses them.

   (3b) Ditto.

    (4) Ditto

12. Add pfsync(4) glue fns in if_pfsync.c:

   (*) The following should immediately test limit[PF_LIMIT_IKS] > 0
       and log and return an error otherwise, eg:

       log(LOG_ERR, "if_pfsync: pfsync_isn_key_xx: isn-key tree is empty.");
       return (EINVAL);

   pfsync_isn_key_import
   pfsync_isn_key_export
   pfsync_in_isn_key_clr
   pfsync_in_isn_key_del
   pfsync_in_isn_key_del_ack(caddr_t buf, int len, int count, int flags)
   pfsync_in_isn_key_ins
   pf_unlink_isn_key
   pf_isn_key_copyin

   Implementation conditions:

   (3a) Satisified by the condition (*)

   (3b) This is absolutely necessary if the feature is to operate in
        fail-over configurations where routing is effected by more than
        one pfsync peer. Without this facility dynamic routing
        protocols such OSPF could not be used to route around VPN
        points of ingress which were under DoS attacks, for example.

    (4) Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test12.X referring
        to this step.

        Test framework events corresponding to receipt of TCP packets
        from pfsync(4) interfaces. These could be implemented using
        a bpf(4) filter attached to the test machine tunnel i/f on the
        test host.

13. Add sbin/tcpdump/print-pfsync.c functions:

    pfsync_print_isn_key_ins
    pfsync_print_isn_key_del
    pfsync_print_isn_key_del_ack
    pfsync_print_isn_key_clr

    Add sbin/tcpdump/pf_print_isn_key.c

    print_isn_key(struct pf_sync_isn_key *isn_key, int flags)

   Implementation conditions:

   (3a) These functions will only be called when pfsync packets with
        isn-key specific subheaders are received, which is conditional on
        the explicit enabling of the feature as ensured by the
        relevant conditions on step 12. above.

   (3b) These changes are absolutely necessary if the operation of the
        pfsync features is to be observable by tcpdump(8).

    (4) Test framework events corresponding to LOG messages at level
        DEBUG with an event identifier. TEST:EVENT:test13.X referring
        to this step.

        Instrumenting tcpdump(8) with appropriate TEST:EVENT logging.

        Test framework events corresponding to receipt of messages
        from tcpdump(8)

Security Engineering for Linux Users

This is one way die-hard Linux users can find out what the word "engineering" really means. They can learn about OpenBSD without rebooting either their machines, or their minds.

First read the man pages. OpenBSD man pages aren't documentation, they're literature, so you need to see them nicely formatted. Get the source from a mirror, e.g.

mkdir ~/openbsd && cd ~/openbsd

wget http://mirrors.ucr.ac.cr/OpenBSD/5.5/src.tar.gz

wget http://mirrors.ucr.ac.cr/OpenBSD/5.5/sys.tar.gz

tar xzf src.tar.gz &&  tar xzf sys.tar.gz

Then put this shell script in a place where it's runnable:

#! /bin/sh
MP=$HOME/openbsd
FP=$(find $MP/. -name $2.$1)
if test -n "$FP" -a -f $FP ; then
   if test -f /tmp/$2.$1.pdf ; then
      echo "Done!"
   else
      man -Tps $FP | ps2pdf - /tmp/$2.$1.pdf 2> /dev/null
   fi
   evince /tmp/$2.$1.pdf &
else
   echo "error: file $2.$1 does not exist."
fi

Now when you want to see a page, type something like

bsdman 5 pf.conf

Use QEMU to run OpenBSD virtual machines.  You can download QEMU source and build it with commads like:

wget http://wiki.qemu-project.org/download/qemu-2.1.2.tar.bz2

tar xjf qemu-2.1.2.tar.bz2 && cd qemu-2.1.2

./configure --enable-gtk --with-gtkabi=3.0 --prefix=$HOME/usr --extra-ldflags=-Wl,-R,$HOME/usr/lib --extra-cflags=-I$HOME/usr/include

make && make install

This assumes you have things like gtk-3.0 and glib-3.0 installed in ~/usr, and that this is where you want qemu installed too.

If you're doing this on a machine or user account you care about, then you will want to check the signatures, and you will want to try and find out what they should be. Obviously there's no point checking the signatures if you got them from the same place as the code!

Get an install ISO image from one of the mirrors, e.g.:

wget ftp://mirrors.ucr.ac.cr/OpenBSD/5.5/i386/install55.iso

The same point we made above about checking signatures applies here too, of course. Now make a disk image to install onto:

qemu-img create -f qcow2 openbsd.img 4G

Now create some ifup scripts to start and stop the tunnel devices. The first is to handle the general case. Put this in /etc/qemu-ifup

#! /bin/sh

addr=192.168.$2.1
mask=255.255.255.0

if test -z "$1" ; then
   echo qemu-ifup: error: no interface given
   exit 1
fi

ifconfig $1 inet $addr netmask $mask

And the second is the one to take the i/f down, put it in /etc/qemu-ifdown:

#! /bin/sh
exit 0

Then do special cases, I have three, change the final n to one of 1..N for N guest VMs, call them /etc/qemun-ifup where n is one of 1...N:

#! /bin/sh
/etc/qemu-ifup $1 n

Then make them executable (assuming they're the only files in /etc that are called qemu*

chmod +x /etc/qemu*

Now install a standard OpenBSD on the image:

$HOME/usr/bin/qemu-system-i386 -hda openbsd.img -boot d -m 128 -cdrom install55.iso -net tap,vlan=0,script=/etc/qemu1-ifup -net nic

Set up the i/f em0 as 192.168.1.0/24 and give it IP address (fixed) 192.168.1.2

Then shut down the VM properly (using /sbin/halt) and make N copies of the openbsd.img file called openbsdn.img, where n is one of 1...N.

Now make a script startbsd with this in it:

#! /bin/sh
if test ! -p $HOME/.cua01.$1 ; then
   mkfifo -m u=rw,go= $HOME/.cua01.$1
fi
sudo /bin/sh -c "echo 1 >/proc/sys/net/ipv4/ip_forward"
sudo $HOME/usr/bin/qemu-system-i386 \
   -runas $USER -hda openbsd$1.img -boot c -m 128 -name guest$1 \
   -net tap,vlan=0,script=/etc/qemu$1-ifup \
   -net nic \
   -chardev pipe,id=com1,path=$HOME/.cua01.$1 \
   -device isa-serial,chardev=com1,irq=3,iobase=0x2f8 \
   -daemonize

Now you should be able to launch N instances with

./startbsd n

and customize them by setting the interfaces to be started with /etc/hostname.em0 containing

inet 192.168.n.2 255.255.255.0

where again n is one of 1...N.