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

[Bill Frantz]

At 10:38 AM -0700 4/19/01, zooko@zooko.com wrote:
>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 am glad you are trying to read and validate the code.  The only way its
security properties can be trusted is if people try to verify them.  You
are one of the first.  If there is anything I can do to make it easier,
please let me know.  (See the comments about IBM below for my preferred
technique.)


>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...

{Repeat after me 5 times, "Threads are good ..."  OK, you still don't
believe it.  :-)  But it is the only way in Java to implement concurency.
You don't have events like OS/360's ECBs, or multi-IO wait like Unix's
select.}

There are some notes about thread usage in
<http://www.erights.org/elib/distrib/vattp/index.html>.  Should I try to
rewrite that section to make it clearer how threads and concurrency are
controlled in VatTP?  (IBM achieved great success in clearly describing the
System/360 architecture by following the policy of not answering questions
about it, but instead rewriting the architectural description and asking,
"Now do you understand?"  I would like to follow that policy in this case.)

>
>
>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).

I believe the most of the logic you are interested in here is in
ConnectionsManager.java.


Cheers - Bill


-------------------------------------------------------------------------
Bill Frantz       | Microsoft Outlook, the     | Periwinkle -- Consulting
(408)356-8506     | hacker's path to your      | 16345 Englewood Ave.
frantz@netcom.com | hard disk.                 | Los Gatos, CA 95032, USA