[cap-talk] Non-safety vs. permission propagation -- HRU and IBAC ACLs

[James A. Donald]

Toby Murray wrote:
 > Its comparable to saying that some programs that a
 > user U might run are known to be safe and hence, these
 > subjects (that represent these programs) should be
 > removed from the model.

I understand you to be pointing out that assuming all
programs are maximally hostile, is in fact assuming that
some programs are maximally hostile, and other programs
(the operating system) are fine.  We can always obtain a
proof that X is secure or a proof that X is insecure, by
implicitly moving X between these categories.
Implementing a system based on this principle is apt to
result in something like the various MLS systems, in
that the "secure" category is apt to contain so much
stuff that it is probably not very secure.

In a useful large secure system, the criterion of
goodness is the size of the attack surface, not a proof
of security, for to prove the system secure, one would
need to reduce the attack surface to zero, which is
impractical. Proofs of security are more useful for
particular small functions and activities, rather than
for a necessarily large working environment.

To design useful secure systems, we have to identify
software functionality that require large authority, and
architect the system so that each such area of
functionality is performed by a single piece of code
which is treated as a separate entity with separate
privileges, in the powerbox software pattern, rather
than large number of entities each containing that
functionality, thereby reducing the attack surface.

That is to say, it is necessary to consider what X in
fact is, and why the user wants X, and what the user is
planning to do with X, so that the user can do X while
needing to trust a smaller amount of code than he does
at present.