[coyotos-dev] Couple of potential-someday-user questions

Jonathan S. Shapiro shap at eros-os.org
Thu Jan 27 14:03:46 EST 2005


On Thu, 2005-01-27 at 10:19 -0800, C Y wrote:
> --- "Jonathan S. Shapiro" <shap at eros-os.org> wrote:
> 
> > On Wed, 2005-01-26 at 19:27 -0500, Eric Northup wrote:
> >
> > I think there was a mis-reading here.
> > 
> > We are looking at ACL2, HOL, and Twelf as initial embedding
> > environments where we can validate our ideas about the viability of 
> > this degree of program proof.
> 
> Is that still in doubt?  I thought there were a couple of proofs done
> for EROS that were successful - does Coyotos require a scale of proof
> such that it is unclear whether it's possible?

The verifications done for EROS fell into two categories:

  1. Proofs against a model (the confinement verification). This
     can tell us that the algorithm is right, but it doesn't tell
     us that the code is right.

  2. Model checking against the static control flow (the MOPS work).
     This can tell us that a limited set of constraints on the code
     were satisfied, but it doesn't validate the code in general.

There is a narrow class of programs that falls within the range of what
can potentially be verified today. There is good justification for
expecting a positive outcome, but we don't really know (yet) if Coyotos
falls within that class.

> > Fortunately, it doesn't matter if the proof tool is right -- only if
> > the proof is right. *Checking* a proof produced by an imperfect tool 
> > is actually not that hard. The best way to achieve what C Y is after 
> > is to eventually provide a means for multiple proof *checkers* to be
> > applied to a proof script produced by the BitC prover.
> 
> That's what I ment to say ;-).  Is that planned, or too much work to be
> practical?

I think it's a third phase. Phase one is to have a language and some
reason to believe that building a good proof environment is worth the
effort (i.e. some successful verifications executed in an existing
tool). Phase 2 is to build the proof environment that makes the proving
activity more automated and more efficient. Phase 3 is to develop the
mechanism to spit out a proof script in whatever format is required by
your favorite proof checker.

No matter what you do, you have to *have* the proof before you can check
the proof.

shap



More information about the coyotos-dev mailing list