[Haskell-cafe] Well typed OS

[Alexander Kjeldaas]

You could consider the compiler for the IO type part of the TCB and execute
source code with caching, like nix. Every process could be wrapped in an IO
sandbox that is enforcing the types for all IO operations.

  That just requires being able to implement a->Maybe b i.e. have a fixed
binary representation for the data in and out of the inner program.

Something like rudimentary programmable scripts that run on kernel system
call invocations already exists in Linux, so it could be possible to
compile down to that.

Alexander

 2018, 17:04 Barak A. Pearlmutter <barak at pearlmutter.net> wrote:

> At a high level, you seem to be proposing encoding and enforcing
> safety properties of executables using a type system. One
> instantiation of this idea is proof-carrying-code (Necula and Lee,
> 1996, see https://en.wikipedia.org/wiki/Proof-carrying_code), which
> ensures safety properties of machine code. The spin-off Cedilla
> Systems built a mobile OS (intended for phones) around this, with the
> idea that third-party apps would run unprotected with safety
> guaranteed solely by sophisticated use of types. The Fox Project,
> http://www.cs.cmu.edu/~fox/, was philosophically similar, and their
> web page contains a bunch of interesting pointers to relevant work.
>
> For whatever reason, this stuff never got much penetration. But in
> today's Internet of Things, with malware being injected into mobile
> phones and cars and light bulbs and toothbrushes and smart dust, it
> may deserve another look.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181006/3a20d678/attachment.html>