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: [EMAIL PROTECTED] ( Ludovic Court?s ) Subject: On trusting its parent process To: [email protected] Message-ID: <[EMAIL PROTECTED]> 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 _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
