[Haskell-cafe] Well typed OS

[Vanessa McHale]

The problem with an IR is that some languages would inevitably suffer -
LLVM in particular was designed as a backend for a C compiler, and so it
is not necessarily well-suited for lazy languages, immutable languages,
etc. (not to mention self-modifying assembly and other such pathological
beasts...)


On 10/06/2018 08:31 PM, William Yager wrote:
>
>
> On Sat, Oct 6, 2018 at 11:03 PM Barak A. Pearlmutter
> <barak at pearlmutter.net <mailto: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.
>
>
>   
>
>
> _______________________________________________
> 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/20181007/a3ecb5d7/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20181007/a3ecb5d7/attachment.sig>