[prev in list] [next in list] [prev in thread] [next in thread] 

List:       cap-talk
Subject:    Re: [cap-talk] TCB in safe language system was Security by safe
From:       "Ben Kloosterman" <bklooste () gmail ! com>
Date:       2009-09-09 1:17:01
Message-ID: 002201ca30eb$3ee25ab0$bca71010$ () com
[Download RAW message or body]

> I guess you are assuming that there is one agreed upon
>language for such a language protected system?  Is there universal
>agreement
>on intermediate code these days?  
>
>Does everybody agree on Java byte code?
>How would interpreters like Perl and Python work?
>
Note the language restriction applies only to user apps the trusted base can
be written in any language .

The 4 projects I know use Common Intermediate Language  ( based on MISL)
from .NET . Other people are/have played with Java byte code. 

Microsoft , Borland , LVVM and Mono and many others provided compiler to CIL
for  Dephi , C# , F# , Cobol , VB ,  , Java , Iron Python , Ruby ,C  ,
Perl.NET , Java script and more .

Either way  you can write a compiler for any language or an interpreter if
it is needed. 

>We seem to be agreeing on the above essence of this approach.  As noted
>earlier in this message there are some costs.  Perhaps that's a good
>place to leave this discussion - unless you have something to add
>about defining the "TCB".

I don't see the performance issue except for a once of cost. Yes these
systems are less flexible but they will be more reliable as the all user
code (including device drivers and services) is type safe.

And with regard to the TCB 

>I need to hear how the TCB is defined in such a system.

The TCB is just native x86 code mostly compiled from C#, it also contains
some assembler code. So pretty similar to a traditional OS.  The whole TCB
could in fact be compiled from C like any OS but it's better to use a type
safe language and Microsoft is even using Sing# ( an extension of c#) so it
can be proved more easily.

I think a good way to visualise these systems is Minix v1 but all user
applications ( including services and device drivers) are restricted to type
safe languages such as .NET or Java and compiled by a trusted compiler.

There are many ways of building such a TCB , I envisage the OS loader just
putting these assemblies together and not exposing them in the Dynamic
Loader , the Assembler(compiler) will prevent  direct access to addresses in
far Jmp and Calls ( they need to be named for the loader to patch them when
loaded)


>Right, because it seems to any executable is in the TCB.  If not, please
>describe how not.

No this is not the case user programs executables are stored in a protected
area but are not trusted to do special things such as hardware access (
which the HAL does)  ,though they are trusted to behave properly in terms of
memory access.

And 

>1.  How to insure that only safe code is accepted at this
>intermediate level, and

The Intermediate to binary compiler will check this. The following checks
are needed
- The 4-5 things mentioned earlier eg a Bool value of 2
- That all  Code access is relative to the program  eg branches are fine ,
far calls and jmps are made to a named method.  The system can check whether
user code is allowed access to this method. ( This is not an issue for CIL)
- Check data access is to valid static locations or via the heap references.

>
>2.  How to protect and safely generate the necessarily unsafe code that
>is >needed for things like drivers and handling module to module
transitions

Drivers are user code and contain no unsafe code. To access the hardware
they need to make a kernel call . The actually hardware PIO , DMA and the
handling of the interrupt is done by the HAL. 
Module to Module transitions are done by the Dynamic loader a piece of
trusted code , at load it can check whether the access is allowed eg a call
to a method not in the loader will prevent the Assembly from loading. 

Regards, 

Ben

_______________________________________________
cap-talk mailing list
cap-talk@mail.eros-os.org
http://www.eros-os.org/mailman/listinfo/cap-talk
[prev in list] [next in list] [prev in thread] [next in thread]