Re: [Xen-API] Secure design and stub-domains

[Anil Madhavapeddy <anil@xxxxxxxxxx>]

On 30 May 2014, at 14:39, Thomas Sanders <thomas.sanders@xxxxxxxxxx> wrote:

> On 30 May 2014 at 2:27 pm,
> Anil Madhavapeddy [mailto:anil@xxxxxxxxxx] wrote:
>> On 15 May 2014, at 15:56, Thomas Sanders <thomas.sanders@xxxxxxxxxx> wrote:
>>> 
>>> I care about security. I was the tech lead for the work of getting a
>>> slightly customised version of XenServer 6.0.2 through Common Criteria
>>> certification. I'd love a chance to apply a capability-based approach
>>> where it makes sense. We could probably use OCaml's type system to get
>>> more assurances of correctness than we do at present. I look forward to
>>> dom0 services being split out into individual service VMs or stub-
>>> domains.
>> 
>> It's really interesting to hear this.  There is an information-flow variant
>> of OCaml called FlowCaml that could be resurrected fairly easily if
>> a suitable use case came up (like CC cert).
>> This lets the programmer understand how information is travelling across
>> various modules in a complex codebase.
> 
> Thank you: FlowCaml does look interesting.
> 
> Another security-related OCaml variant is Emily[1][2], "a subset of
> OCaml that uses a design rule verifier to enforce object-capability
> principles. It demonstrates how memory-safe languages can be
> transformed into breach-resistant object-capability systems with
> little loss of either expressivity or performance."
> 
> Emily and FlowCaml could even be combined.

Interestingly, many of Emily's design principles are present naturally
in MirageOS OCaml applications:

- MirageOS applications are functorized across all their OS dependencies.
This functor model implies that the need for ambient resources (such as
a giant Unix module) is greatly reduced, and so the enforcement of whether
a particular module should have access to something is a decision that
can be enforced at build-time.  

- We don't do this at the moment, but it's also possible to compile with
-nopervasives to remove even more ambient functions.  The external keyword
can also be banned from user-generated code by using the Ctypes FFI library
in stub-generation mode [1] to completely abstract the process of foreign
binding without writing a single line of C.

- Strings are optionally immutable in the forthcoming OCaml 4.02, with a
transition to the Bytes module for when you really do need mutable strings.

[1] https://github.com/ocamllabs/ocaml-ctypes/releases/tag/ocaml-ctypes-0.3

best,
Anil
_______________________________________________
Xen-api mailing list
Xen-api@xxxxxxxxxxxxx
http://lists.xen.org/cgi-bin/mailman/listinfo/xen-api