[cap-talk] Language and/or multi process/IPC security (prev: Windows Vista: security by admonition)

[David Wagner]

Rob <rmeijer at xs4all.nl> writes:
>You state 'memory-safe, and preferably capability-secure'
>and I do believe it should be exactly the other way around, if a system is
>designed and implemented capability secure using capability secure IPC and
>the memory safety features offered by OS with the use of multiple
>processes,
>this would be more essential than memory safe language usage.
>In fact, I do believe that with a proper capability design and an
>implementation based on multiple process and IPC, the usage of language
>based memory security would not actualy add any level of security.

Memory safety makes it easier to look at the source code of an
application, reason about its security properties, and convince
yourself that it will work as it ought to.

If I have an application that runs on a capability-secure OS but is
written in a non-memory-safe language (like C), then I might be able to
upper-bound the set of capabilities that the application can get access to
(and thus upper-bound the amount of harm it could cause to my system),
but it's very hard to be sure that it will handle those capabilities the
way I want.  For instance, I might be able to convince myself that the
application can only write to the file "foo.txt", but for an app of any
non-trivial complexity, it will be very hard to convince myself that it
writes the right thing to "foo.txt" (as opposed to, say, total garbage).

The reason that memory safety makes it easier to reason about program
behavior is that it enables modular reasoning.  Modular reasoning means
that can look at part of the program (e.g., the implementation of one
module, along with the specification and types for the modules it calls or
is called by) and draw some conclusions about how that module will behave,
without having to look at the rest of the program.  Modular reasoning is
not possible in a non-memory-language, because it is always possible that
the part of the code you didn't look at could tamper with the private
state (or even modify the running code) of the part you did look at.

Examples (in Java):

- If class Foo declares a local variable of "private" scope, I can
  be sure that only the code of Foo can directly access that variable.
  I may be able to establish some invariants regarding that variable
  just by looking at the code of Foo, without needing to look at the
  whole program.

  In contrast, in a non-memory-safe language like C, I could never
  be sure that my invariant was preserved without looking at the whole
  program.  If I only look at the code of Foo, for all I know some
  wild pointer or buffer overrun flaw elsewhere in the code might
  modify the private variable out from under me.

- If class Foo allocates a Bar object, and if I can see from the code
  of Foo that the Bar-reference never escapes, then I can safely identify
  all the messages that might ever be sent to that Bar, without looking at
  anything other than the code of Foo.
  
  In contrast, in a non-memory-safe language like C, I could never be
  sure I've identified all the messages that might be sent to the Bar
  (without examining the entire program).  For all I know, some other
  place in the code might forge a pointer to this Bar and send it messages.

Modular reasoning seems pretty important to reasoning about the security
properties of programs of non-trivial size.  For that reason, memory-safe
and type-safe languages seem useful.