The source of trust

[Guy Bormann]

Jonathan,

I find your comments on the list very interesting! (But : see below)
When I try to reason about trust (or eavesdrop on a discussion involving
trust in this case ;-) I tend to reread this article by Ken Thompson
over and over :
http://cm.bell-labs.com/who/ken/trust.html

So, what you are basically saying is that the goal of EROS-OS/Coyotos
(and Hot Potatoes-OS; sorry, couldn't resist the urge) is to provide the
primitives so that the grandmothers of the world can chat over the
Internet without having to write their own compiler (well, extend this
to Ludovic-OS) in order to be able to rebuild their favorite (open
source by necessity) Instant Messanger app? And in addition, I have the
feeling you also strongly believe that the team is almost there. Is this
a correct assessment of the status (or your estimate of the status) of
EROS-OS/CoyotOS?
  What also interests me is the verification part. I happen to have come
into contact with the Esterel language through my work in Space
Robotics. This is a synchronous language for specification of reactive
systems that has formal semantics. But even then formal verification is
extremely hard (but luckily not impossible, leading to a successful
completion of a project at our company :-).
  So, if building the kernel (or 'seed' for the sake of disambiguation)
of trust is founded on the behavioural verification of the minimal set
of primitives, how did you proceed in this verification process? Is it a
design time activity, a compile-time one or do you instrument code to
provide hooks for runtime-verification? Some claim you can never reach
verification if you don't do the latter (as we painfully found out in
the final stages of that project, although we suspected it was necessary
from the beginning)!


Guy Bormann

PS: I think your prayers are heard, Ludovic (see at the bottom).
"Date: Tue, 12 Jul 2005 15:05:44 +0200
From: address@hidden ( Ludovic Court?s )
Subject: On trusting its parent process
To: address@hidden
Message-ID: <address@hidden>
Content-Type: text/plain; charset=us-ascii

Hi,

LSM talks by Shapiro (on EROS and Coyotos) and Forsyth (on Plan 9) were
quite insightful.  I just found this followup:
http://www.coyotos.org/pipermail/coyotos-dev/2005-July/000138.html .

What strikes me in this message is this:

  1. The *only* way that a process in plan-9 can obtain a capability is
  from its parent. This is a problem if the capability refers to
important
  state and the parent is untrusted. Consider, for example, that the
  "passwd" program can no longer trust the content of /etc/passwd,
because
  it has no way to know if it is receiving an authentic copy of the
file.

  [...]

  This differs very strongly from the status in EROS/Coyotos, where
  *authentication* capabilities are not considered to be "holes" for
  purposes of confinement. An implication of this is that the capability
  which answers the question "Is this capability a capability to an
  authentic X object" can be widely distributed, and can come to the
user
  in a way that the parent process cannot interfere with.

In the Hurd, processes get capabilities to the root filesystem, to
`auth' and friends from their parent process.  This is very convenient
because it allows to run processes in a "sandbox".  OTOH, this makes it
impossible for a process to make sure it is talking to "authentic"
servers, as in the Plan 9 case above.

Now, what does "authentic" mean in a system designed in such a way that
most system services can be replaced by the user?  Should programs be
allowed to rely on a specific implementation of a given service?

Just a few random thoughts...  Hopefully this will lead to a pleasant
discussion!  ;-)

Ludovic."
-- 
  --------------------------------+-------------------------------
dr. Guy Bormann, physicist        |
C and C++ programming             o smail : Boomsesteenweg 171 b3
UNIX/GNU/Linux enthusiast         |         2610 Wilrijk
                                  |         Belgium