Jonathan S. Shapiro wrote:
All:
Mr. Fortaine has been running around stirring up trouble among several
senior researchers recently, sharing quotes and statements back and
forth without context and wasting a great deal of time.
Concerning his latest post here, he has offered two links:
[1] http://www-1.ibm.com/linux/news/semiconductor.shtml
[2] http://www.computationallogic.com/reports/files/028.pdf
The first was offered in response to my statement that there are zero
example of high-robustness or high-security monolithic systems today. I
think his point is that the Linux systems have been running there for 5
months. Just for the record, 5 months of uptime is not considered "high
robustness", and the article says absolutely nothing about security.
The second link is a reference to Bill Bevier's dissertation, which is
entitled "Kit: A Study in Operating System Verification". Matt Kaufmann
suggested this link to Fortaine at about 4pm EST yesterday, but Fortaine
obviously hasn't read it.
First, let me say that the Kit work is brilliant. It was a major step
forward in the state of the art in operating systems work, and it
remains an excellent piece of work today. In fact, I spent a bunch of
time speaking with Bill Bevier about the work about two years ago.
While Kit is a terrific piece of work, Bevier is very straightforward
about acknowledging that the Kit system is a long way from anything that
could be considered a "production capable" kernel. Kit shows that
verification on a more capable operating system kernel may be possible
with a lot of work. It does not show that it has been done.
Yesterday, Fortaine sent a note to Matt Kaufmann that quoted me out of
context and created a serious miscommunication. As a result of this and
other actions, I have asked him NOT to forward any other mail of mine
(which request, please note, he has just ignored). One day later,
without waiting for my response to Kaufmann, Fortaine is now attacking
me here.
Fortaine closes with:
For me, this man and his project are only a bad joke ... Be more
serious, guys :-) !
Yes, in fact, I believe if you want to see the HURDNG boot one day, we
will need to build our microkernel and choose our language ....
As I have said in a previous, extensive note, building a kernel may in
fact be the right thing for the HurdNG team to do. I've also given some
ideas about how this should be decided.
But please keep in mind that Fortaine has no idea what he is talking
about, and that his "conclusions" are established by a series of
discussions involving out-of-context quotes on topics that he doesn't
really understand.
Also, keep in mind that Fortaine has absolutely no knowledge of the
financial investment that is going into Coyotos and the progress that
has been made on its implementation. In fact, he hasn't even *asked*
about this!
Regards,
Jonathan Shapiro
Hello all :-),
Let's go for war :-) :
Shapiro wrote :
The first was offered in response to my statement that there are zero
example of high-robustness or high-security monolithic systems today. I
think his point is that the Linux systems have been running there for 5
months. Just for the record, 5 months of uptime is not considered "high
robustness", and the article says absolutely nothing about security.
5 months are not considered as "high robustness". Ok, so you want to test
10 years an OS and say 10 years later, it's production ready ... I don't
believe that IBM would have invest *2,5 billion dollars* just for fun ...
Let me joke ... :-) : I am currently working in the automotive industry
and in the industrial world, 1 penny is 1 penny ....
All right about security :-)
Nmap ( http://insecure.org/nmap/ ) this :
http://www.lanl.gov/
( Linux + Kerberos : http://web.mit.edu/Kerberos/ )
Did you speak about high security ?
Shapiro wrote :
But please keep in mind that Fortaine has no idea what he is talking
about, and that his "conclusions" are established by a series of
discussions involving out-of-context quotes on topics that he doesn't
really understand.
For sure, I don't understand these topics, so I ask for the opinions of
*many* ( maybe to many :-) ) experts ...
You are one of those experts that nobody understand (even Matt Kaufmann,
note : winner of the ACM Software Award 2005 with ACL2, see below...) To
my knowledge, this kind of "experts" does not go very far ... => maybe
it's time for us to put you back in your "black box"...
Shapiro wrote :
Also, keep in mind that Fortaine has absolutely no knowledge of the
financial investment that is going into Coyotos and the progress that
has been made on its implementation. In fact, he hasn't even *asked*
about this!
The time-to-market : an American vulgarity moreover... ( DOS Forever ...
:-) )
http://symbolx.org/ddf_news.html
Plan B -- 2006/06/14: 15:40 CDT
*Coyotos is not going to be used for the duration of this project for two
reasons:
It does not build in BSD or Linux without considerable work.*
Hurd-L4 has been abandoned, and no official plans have been made by the
Hurd team to use Coyotos.
For the above reasons, I'm a bit disappointed, but I do have a backup
plan. I'm going to do work on the Minix 3 operating system. I need to get
familiar with that OS and write abstraction libraries for my framework.
For the time being, I will be doing all this under FreeBSD using QEMU
virtualization.
As time progresses and the abstraction libraries stabilize on one or two
operating systems, I plan to take a look at Minix 3's main driver
framework and try to improve on it. I can't remember what problems I
thought it had, but I did note them in my paper.
Maybe it's time to update your cvs ... :-)
Final words :
A simple mail that is not *out of context* - Requirements : to know to
read English :
Hi --
Thanks. OK, I've looked at those two emails from Jonathan Shapiro.
Regarding
the first message, I appreciate the nice words about ACL2, but I didn't
completely understand this statement:
The problem with ACL2 is that it's based on a language that does not
provide either mutation or representation, and has no static type
system.
Certainly he's right about there being no static type system. I don't
know
what he means by "mutation" or "representation"; I'll just say that ACL2
is
written primarily in itself, so it seems to be a sufficiently rich
language for
a non-trivial application. For example, we define a macro, defrec, that
we use
extensively in the ACL2 source code (which you're welcome to browse),
which
makes it convenient to specify and use record structures.
I like the sentiment in the second message about a desire to do proofs.
I'm a
little surprised at the comment that "the number of systems that can prove
useful properties about things like operating system kernels is zero",
since
Bill Bevier did something like that about 20 years ago, and Rockwell
Collins
has, I believe, been doing this sort of work recently.
The following passage from the second email also surprised me (it's not
included in your email):
Our goal is to get something that is structured
similarly to ACL2, but with static types and state in the programming
language.
ACL2 has a notion of state, and more generally, a notion of
single-threaded
objects (stobjs). I think these are much simpler than Haskell's monads
but
supply some of the same functionality (e.g., I/O). You can read about
stobjs
in ACL2's documentation, or by following the "Books and Papers" link from
the
ACL2 home page and then searching for "Single-Threaded".
-- Matt
X-ME-UUID: address@hidden
Date: Tue, 08 Aug 2006 22:34:55 +0200
From: Guillaume FORTAINE <address@hidden>
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-162 required=200
Matt Kaufmann wrote:
> Hi --
>
> I may take a look, but realistically, I'll be more likely to do so if
you tell
> me specific areas in which you seek my advice.
>
> Regards,
> Matt
> X-ME-UUID: address@hidden
> Date: Tue, 08 Aug 2006 21:54:40 +0200
> From: Guillaume FORTAINE <address@hidden>
> X-SpamAssassin-Status: No, hits=-0.2 required=5.0
> X-UTCS-Spam-Status: No, hits=16 required=200
>
> Hello,
>
> As you are experts in Formal Methods / Verified Software /
Programming
> languages, I would want to have your advice about this programmign
> langage ( BitC ) :
>
> http://www.coyotos.org/docs/bitc/spec.html
>
> Best Regards,
>
> Guillaume FORTAINE
>
>
>
> Hello Mr Kaufmann,
The bitc programming langage aims to implement formal verification
directly in the langage to prove Operating System design ( unlike Coq,
Isabelle, ACL2 which are *externals* proof provers).
It could very interesting that formal experts as you give your advices
to better develop this langage.
Here are two interesting points for you :
What do you think of this idea ? :
http://www.coyotos.org/pipermail/bitc-dev/2006-August/000768.html
"> What are you suggestions to enhance BitC in describing sophisticated
> invariants ( some links, info to have a start point).
>From a developer perspective, the best existing technology for this is
probably ACL2. There are provers that use theoretically more advanced
technologies, but none of these have good integration with the
programming environment. ACL2 is the clear leader from the perspective
of *programmers* (as opposed to verification researchers).
The problem with ACL2 is that it's based on a language that does not
provide either mutation or representation, and has no static type
system.
So, I would like to achieve two things:
1. An ACL2-like environment with a production-capable programming
language, and
2. Some "intermediate" steps. Full verification is a big thing to jump
in to. Intermediate techniques like model checking are very powerful and
have a smaller cost of entry for the programmer. There is no reason why
*all* of these techniques cannot be integrated into a single
environment."
And this proposition ? :
http://www.coyotos.org/pipermail/bitc-dev/2006-August/000770.html
"> Unlike Hume, it includes imperative operations (I'd be interested in
> seeing what effect this has on verification -- this may weaken the
> proofs that can be constructed?)
The main impact is that our basis for discharge will need to be theorems
about the evolution of the state space rather than approaching the
problem through term substitution. This is, of course, a larger search
problem and we expect to hit many challenges.
We have been careful to preserve a pure subset language so that we can
switch back and forth between term-based and state-based reasoning as a
way to slice the search. I'm actually about to strengthen this aspect of
the language explicitly.
But I think that there is another thing to say here: it is better to
have weak proofs than no proofs. Right now, the number of systems that
can prove useful properties about things like operating system kernels
is zero. Jones' work on House is terrific, but everybody involved admits
that House is a toy (and that this was the right thing to do first). We
are approaching from the perspective of OS builders. Our objectives are
more aggressive and may not be realistic.
Perhaps our approach will not work, but if it does not we will learn
something about why not."
*Nothing to add, judge by yourself...*
Best Regards,
Guillaume FORTAINE
_______________________________________________
L4-hurd mailing list
address@hidden
http://lists.gnu.org/mailman/listinfo/l4-hurd
__________ NOD32 1.1701 (20060810) Information __________
This message was checked by NOD32 antivirus system.
http://www.eset.com