Re: [MirageOS-devel] Type enforced security

[Anil Madhavapeddy <anil@xxxxxxxxxx>]

On 16 Sep 2015, at 12:35, Hannes Mehnert <hannes@xxxxxxxxxxx> wrote:
> 
> Hey,
> 
> On 09/16/2015 11:12, Garrett Smith wrote:
>> Is there an example in the Mirage codebase where the OCaml type system
>> is used explicitly to enforce a security policy or behavior? This is a
>> bit of a weird question, sorry, I'll explain.
>> 
>> I'm putting together a presentation on unikernels and I'm looking over
>> the various vulnerability patches in OpenSSL and thinking a) yeah, the
>> underlying  C code make it pretty tough to spot edge cases and bugs
>> but b) the patches themselves aren't obviously correct (to me).
>> 
>> I'm wondering if the OCaml type systems is (or could be) used to
>> enforce a various security baselines to help maintainers guard against
>> errant patches, features, etc. Is there a specific example I can point
>> to that highlights the advantages of using the OCaml type system
>> vis-a-vis C's along this line?
> 
> my take on this is if you stick to purely functional programming (no
> shared mutable state, no exceptions), you can understand code locally
> (the behaviour of a function is only influenced by its arguments).  Once
> you have that, understanding (security-critical) things is pretty
> straightforward:
> https://berlin.ccc.de/~hannes/oob.diff (slightly modified (to not
> include the removal of 'open Cstruct) from
> https://github.com/mirleft/ocaml-tls/commit/80117871679d57dde8c8e3b73392024ef4b42c38)
> is a commit where previously an out of bounds access to the underlying
> buffer was possible (since the 4 byte header were not properly accounted
> for in line 323), which lead to an exception thrown by Cstruct.
> 
> From the diff you can see what exactly changed (size -> size+4); no
> other behaviour changed.  To contrast I cannot understand from the diff
> the impact/commit in go's ssl implementation:
> https://code.google.com/p/go/source/detail?r=eae0457c101512f59296538f0162749eba325892&name=release-branch.go1.3
> 
> Unfortunately, not all MirageOS code base is in a purely functional
> style (yet! ;).

There's also a broader set of examples in the nqsb-TLS Usenix Security
paper from this summer:

http://anil.recoil.org/papers/2015-usenixsec-nqsb.pdf

In particular, the use of the OCaml module system to repurpose the
TLS stack to act as both a trace checker and an executable library
is something that's extremely hard to do safely from OpenSSL (where
everything is intertwined).

Hannes, is there an example of how to run the nqsb-TLS trace checker
command-line tool anywhere?

-anil


_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel