[Haskell-cafe] Well typed OS

[William Yager]

On Sat, Oct 6, 2018 at 11:03 PM 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.


I would guess a factor that prevented something like PCC from taking off is
the fact that proofs over binaries are relatively pretty challenging to
express and verify, and ISA semantics tend to be really complicated.

I think an intermediate approach that might be a lot cheaper to implement
is to ship some sort of IR (rather than machine code) that is A) relatively
cheap to check and compile and B) carries some variety of safety guarantee.

As I recall, A) is already in use. Apple requires developers to submit
applications as LLVM IR rather than machine code.

LLVM IR definitely isn't designed with B) in mind, however. I could imagine
something like Core being useful here. A fully annotated type-checked
language with semantics amenable to formal analysis.

You could add some sort of effects system to the type system of the IR, as
a basis for enforcing security policies. E.g. network access could be an
effect.

The advantage of doing this over PCC is that we don't have to retrofit the
proof system to match the ISA, but instead can design the IR specifically
to make the proof system easy. A downside is that you have to compile the
application once upon downloading it, but this doesn't seem to cause too
much of an issue in practice.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181007/585db1a0/attachment.html>