[E-Lang] a casual attempt to audit implementation details of VatTP security

[zooko@zooko.com]

I poked around in 0.8.4 source code a bit trying to ascertain whether it was
really impossible for an active attacker to cause you to process a message from
a previous VatTP connection after you have already processed messages from a new
VatTP connection.

I wasn't really able to convince myself one way or the other of this.  I don't
think this is any bad reflection on Bill's programming skills -- indeed the
consistent style and the clear in-line comments were a great help -- but there
are two architectural conditions which make auditing the security code
difficult.

The first is threading.  You apparently can't do asynchronous I/O (i.e.
event-based programming of your comms code) in Java at *all* without resorting
to native code.[1]

I'm sure I don't have to convince E aficionados of the difficulty of auditing
code for trans-thread consistency guarantees...


The second is the fact that the security properties I was seeking to verify are
implemented in terms of the state of the underlying comms system.  It isn't the
case that there is one function which takes a message and some state as input,
and outputs a decision of whether the message is proved fresh or not.  Instead
the security properties are implemented -- or not as the case may be -- by a
non-obvious causal interaction between crypto state (like
`DataPath.myProtocolParms' and `RecvThread.myIsDoingMac') and TCP connection
state (presumably in the causal dependencies in the creation and destruction of
`DataPaths' or `DataConnections' or something -- this was the part I wasn't able
to follow due to the tangles caused by threading).

Again, this is no ill reflection on Bill -- threading was forced upon him, and
defining security in terms of connections instead of messages is the state of
the art.

I'm sure given more time and perhaps an introduction to the designed causal
relationships I could convince myself that the connection non-replaying property
is guaranteed by this implementation.



It is not my intent in writing this message to argue that VatTP is bad, that
connection-based security is bad, or that threading is bad (although I do happen
to hold the latter two value judgements).


By the way, I noticed that `{Send,Recv}Thread.computeMAC()' is doing "envelope
style" MACs -- MAC(K, M) = H(K, M, K).  This has some theoretical problems as
described in the HMAC paper by Bellare, Canetti, Krawzcyck[2].  If VatTP is to
continue with conservative crypto design, it would be well to switch to HMAC.
(In a related story see this thread [3] on mojonation-devel, where it is
revealed that Mojo Nation uses an even less defensible MAC, and where some
discussion of conservative versus aggressive crypto design for the next version
is discussed.)


Regards,

Zooko

P.S.  It seems appropriate to point out at this time that the Evil Geniuses
Transport Layer, as currently implemented in Mojo Nation, is susceptible to
easy replay attacks (for all even-numbered messages), and also that it offers no
ordering guarantees whatsoever.

[1] http://www.cs.berkeley.edu/~mdw/proj/java-nbio/

[2] "Keying Hash Functions for Message Authentication"
    http://citeseer.nj.nec.com/bellare96keying.html

[3] http://www.geocrawler.com/mail/thread.php3?subject=%5BMojonation-devel%5D+AES&list=5026