Re: The source of trust

[Jonathan S. Shapiro]

On Tue, 2005-10-11 at 02:07 +0200, Guy Bormann wrote:
> 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

It turns out that this attack has a straightforward workaround, and that
it is not possible if suitable verification techniques are employed. Ken
is aware of this, and agrees.

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

Indeed. First comment: this is big-R research, and we plan to get a
prototype done in C first.  On to verification:


The main reason that I think we will *eventually* make progress on
Coyotos is the fact that we do atomic system calls. We inherited this
property from EROS, which got it from KeyKOS, which got it from GNOSIS,
which got it from System/360 and the IBM 801. Norm Hardy, who was the
primary architect of KeyKOS, was a member of IBM's "Advanced Computing
Systems" group, which brought you both of those processors.

Atomic system calls have two consequences that reduce the verification
challenge significantly:

1. If a process sleeps, no kernel stack for that process is retained.
   This means that the kernel really is a state machine. It is *not*
   a concurrent pushdown automata. This brings us back into the realm
   that in principle we know how to verify. The issue now is capturing
   verification objectives and dealing with issues of scale.

2. In any case where alias analysis might force us to check for a
   problem, the kernel path will have been restarted from scratch.
   This tremendously reduces the complexity of aliasing-induced
   analysis by the prover. It probably buys us a factor of two
   in feasible scale of analysis, which should turn out to be enough.

   This property must itself be proved, but we have already shown for
   EROS that proving this property is a straightforward control flow
   model checking exercise.

So I think it's a matter of time and funding, not feasibility.
Basically, we got very lucky with this design and stumbled into a sweet
spot for verification. But you now see why I think these techniques
won't generalize. We may be able to extend them into transactional
systems, which would be a useful thing. They aren't going to help us
with large-scale general purpose programs.

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

I think there are two questions here:

  1. What was the original methodology (which did *not* involve
     verification)?
  2. Now that we are verifying, what are the proof objectives and
     how do we plan to integrate the tools?

The original method was simply paranoia and careful design. Restricting
ourselves to an atomic action design makes things much simpler -- all
paths, for example, have bounded length and are guaranteed to terminate.
Transactional programming discipline also tends to limit interactions
between paths because there is no logical concurrency to worry about it.
Finally, it's a fixed-resource kernel. We build a startup time partition
of memory based on how much we have and then we leave it the hell alone.
Malloc is the path to the devil. Free() actually *is* the devil. :-)

A second factor is that most of the kernel complexity is dealing with
caching and translation issues. Caching may be complicated in the
details, but it is idiomatically a very straightforward design pattern
and the details are readily captured as semi-formal invariants (which we
did). Translation kinds of things are mathematically specifiable, and
again it is possible to capture semi-formal invariants and we did. I
would say that the greatest weaknesses in this approach at the time
were:

  1) Inability to check the actual C code automatically

  2) There is always a question about whether the small invariants
     actually succeed in collectively enforcing the big invariants.
     The argument that they do is usually a semi-formal argument.

In the course of the kernel effort, we were mostly concerned about
permissions checks and authorization. The paths are short enough to do
by hand.

A bit later, we hand-verified the confinement mechanism that was built
on *top* of these primitives. This verification implies that we can
easily do mandatory controls, but also that we have a very powerful
field-leveling hammer to use on hostile code:

  http://www.eros-os.org/papers/oakland2000.ps

Scott Doerrie (one of my students) is now automating this proof in
Twelf. He has found a small error in the statement of transitive access
composition, but it does not alter the outcome. We are learning a lot
about Twelf, not all of it pleasant.

Later still, I did some control flow model checking work with Hao Chen
on the EROS kernel:

  http://www.eros-os.org/papers/ccs04.pdf

This is the work the convinced me of the importance and relevance of the
"atomic action" property, and led us to start more deeply into a more
complete verification effort.


As to our current verification objectives and techniques:

We will certainly formalize the existing invariants and check them.
  These include state and temporal isolation invariants.
We will attempt to integrate prover technology and support into the
  programming language. My conceptual model for usability here is ACL2,
  but with a prover that works and a strong type system.
We will *then* attempt to capture the global operational semantic
  invariants that sit under the confinement verification.
We will attempt to do a correspondence proof on address
  translation.
Finally, we will attempt to do a global liveness proof (if we live
  long enough to try it). The rest of these are just ridiculously
  hard. The global liveness check is actually interesting.


These, of course, do not constitute total correctness, but they
represent a substantially broader effort than has previously been done
for a general-purpose nucleus. Fortunately, we don't have to succeed at
all of them to move the ball substantially forward.

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

Our belief, based on our own experience and discussions with several
high-assurance evaluators, is that the marginal confidence achieved by
going from semi-formal to full-formal isn't really that big if the
semi-formal stuff is done right. However:

Current high assurance evaluations are prohibitively expensive exactly
because the *code* is not verified. If verification can be extended to
code, then the first round evaluation checks the verification
objectives, and subsequent re-evaluations only need to check that those
are still being satisfied. A mechanical proof system applied in this way
could cut this part of the re-evaluation cost from millions of dollars
to hundreds of dollars. This is the difference between engineerable high
assurance and no high assurance at all.

So: we're definitely going for code.

And we actually think that evaluating the code is silly -- this should
be a process similar to open source. We call it "open proofs". What *is*
important is to have a group of very talented and knowledgeable people
look at the proof objectives and confirm that they are reasonable and
useful. In our view, the proof objectives should be published too, and
we welcome open source style review, but you really do need a certifying
body if you want to tackle software liability. We want to.


shap