[MirageOS-devel] Type enforced security

[Garrett Smith <g@xxxxxx>]

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?

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