[cap-talk] Memory access based OS security

[Ben Kloosterman]

>bklooste at gmail.com (Ben Kloosterman) on Monday, August 3, 2009 wrote:
>
>>Hardware-level security through address management was introduced as a
>way to work around failures of
>>the application languages (:shudder:, remembering early implementations
>of Windows). But if you force
>>applications to compile to a particular language (or bytecode), you can
>enforce security at the
>>software level and achieve security without the sacrifices to
>performance that come from partitioning
>>the address space.
>
>The idea of depending on the compiler or byte code verifier in a
>"language
>based system" (LBS) is quite attractive since it might result in a higher
>performance system. However it does impact the assurance aspect of secure
>systems.
>
>With systems like KeyKOS, EROS, CapROS, Coyotos, VM/370, etc. the
>security
>assertion is that no sequence of machine language instructions is able to
>subvert the security of the system. The only compiler that needs
>verification is the one used to compile the system, and it only needs to
>be
>verified for the features used by the source code of the system. Since
>only
>a limited amount of programming needs to be verified, auditing the output
>of the compiler is a feasible, if tedious, possibility.
>
>In contrast, LBS system compilers and/or byte code verifiers must be
>verified against all possible inputs, which seems to me to be a harder
>problem.

This is true but there are a wide range of things that need to be verified
eg in  KeyKOS and EROS  you have more application faults due to pointers , c
errors and not being strongly typed.  A strongly typed OS doesn't have to
deal with them . 

Im also against the current obsession with formally verified kernels not for
the goal itself but because the focus is just on the 6-7000 lines of
research Micro Kernel ( which takes like 40 man years)  , they forget the
asm parts , shared memory , the compiler(which compiles user
services/drivers) and the services.  Nearly all failures and security issues
in a fully tested system are drivers or trusted services ( especially user
written services) not doing the right thing.  How many errors have occurred
due to the micro kernel in a mature OS which is most cases is just the
message parsing API and some assembly stubs ?  The end result is it crashes
or is breached and the consumer will be annoyed his mathematically proven
kernel just failed.

You are also making functional changes more difficult eg Windows 7 made a
change to improve multiple core performance that changed 200 code files ( I
can't remember the details but it was a lot) . Changes like these are
described as suicide hence we get little OS change . Verification will make
it worse. 

I think a better approach is to use TDD automated tests and build it up as
issues are found  for the same work of verifying a kernel you could have
tests covering the compiler ,key device drivers , key services , key apps ,
shared memory and the kernel. Even better is you can make frequent changes
to the OS with some confidence as its strongly typed and tested and changing
the appropriate tests is much easier than a proof.

 
Regards,

Ben