Re: [MirageOS-devel] Type enforced security

[Hannes Mehnert <hannes@xxxxxxxxxxx>]

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! ;).

hannes

Attachment: signature.asc
Description: OpenPGP digital signature

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