Well typed OS

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
24 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Well typed OS

Yotam Ohad
Hi,
In the last couple of days, I've been toying with the thought of an operating system in which programs (or more accurately, any process) has a distinct type which limits
its use of the machine. For example, `echo` (String -> String) won't be able to print an output without a second program which would handle changing stdout.

I think it could "break down" the IO monad into other structures that are better at specifying what is changing: A file is read / memory written / etc.
I do, however, not sure how to incorporate drivers (which handles IO and external devices) into this. Giving them an `IO a` type feels like cheating. I would be much cooler if there was a way
to treat them like the `echo` function from earlier.

What are your thoughts/suggestions? I'll be happy to hear them.

Yotam

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
Am 05.10.2018 um 06:36 schrieb Yotam Ohad:

> Hi,
> In the last couple of days, I've been toying with the thought of an
> operating system in which programs (or more accurately, any process) has
> a distinct type which limits
> its use of the machine. For example, `echo` (String -> String) won't be
> able to print an output without a second program which would handle
> changing stdout.
>
> I think it could "break down" the IO monad into other structures that
> are better at specifying what is changing: A file is read / memory
> written / etc.
> I do, however, not sure how to incorporate drivers (which handles IO and
> external devices) into this. Giving them an `IO a` type feels like
> cheating. I would be much cooler if there was a way
> to treat them like the `echo` function from earlier.
>
> What are your thoughts/suggestions? I'll be happy to hear them.

An OS needs to work for any programming language, so I'm not sure how to
get from an IO-based approach to a working OS. Unless you plan to write
the OS itself in Haskell and make it so that all programs are Haskell
modules, but that's a huge task.

The design approach you're after is called "Capabilities". It's not
ordinarily described as a type system, and I'm not sure whether it's a
good idea to use static types in the first place because there are
situations where you want to grant or revoke them dynamically.
See https://en.wikipedia.org/wiki/Capability-based_security . This
article also has a link to other security models; capabilities are
pretty famous, but it's quite possible that a different one would be a
better fit.

HTH
Jo
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Ivan Perez


On Fri, 5 Oct 2018 at 01:41, Joachim Durchholz <[hidden email]> wrote:
Am 05.10.2018 um 06:36 schrieb Yotam Ohad:
> Hi,
> In the last couple of days, I've been toying with the thought of an
> operating system in which programs (or more accurately, any process) has
> a distinct type which limits
> its use of the machine. For example, `echo` (String -> String) won't be
> able to print an output without a second program which would handle
> changing stdout.
>
> I think it could "break down" the IO monad into other structures that
> are better at specifying what is changing: A file is read / memory
> written / etc.
> I do, however, not sure how to incorporate drivers (which handles IO and
> external devices) into this. Giving them an `IO a` type feels like
> cheating. I would be much cooler if there was a way
> to treat them like the `echo` function from earlier.
>
> What are your thoughts/suggestions? I'll be happy to hear them.

An OS needs to work for any programming language, so I'm not sure how to
get from an IO-based approach to a working OS. Unless you plan to write
the OS itself in Haskell and make it so that all programs are Haskell
modules, but that's a huge task.

He seems to suggest that he is playing around with the idea, more than proposing to write a whole OS.

For the sake of the exercise, it makes sense to assume that all programs will carry a type specification.
 

The design approach you're after is called "Capabilities". It's not
ordinarily described as a type system, and I'm not sure whether it's a
good idea to use static types in the first place because there are
situations where you want to grant or revoke them dynamically.

In part, isn't specifying this up-front what iOS and Android do with permissions, or docker with capabilities?

As an exercise, I think this could be nice. And my intuition would be to use specific effects/monads as well, both to provide the capabilities themselves and to encode the idea that that permission or effect is needed. Type inference might be able to tell you whether a permission may be needed at all or not, so this seems like a potentially good idea.

The idea of using a less-than-IO monad to limit possible IO effects is not uncommon. We briefly used it in [1, Section 7.3 - Limiting the Impact of IO] and I seem to recall Thorsten Altenkirsch talking about this (I don't remember if there's a paper and could not find one right now).

There's two parts to this problem: can I write Haskell programs with limited-IO type specifications, and I think the answer is yes, and can I ensure that programs will not use resources not declared in their type, and I think the answer depends on kernel and, possibly, hardware support (even if you restrict this to Haskell).

Because the type is not included in the program, it would not be included with the executable. It would be interesting to output that too in some form during compilation. This would seem also useful for DSLs.

Best wishes,

Ivan


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

MarLinn
In reply to this post by Yotam Ohad
Hi Yotam,

one rather small and abstract comment:

Permissions and capabilities feel like they are something contravariant.
Intuitively it should be easy to "get out" of permissions but hard to
"get into" them. (compare 'pure' and 'extract')

Resulting actions are probably covariant just like the more general IO.

Therefore I conclude that programs in your OS will probably be a
profunctor, an arrow, or something similar. I wouldn't even be surprised
if one could build an OS on nothing but Optics into the RealWorld.

Cheers,
MarLinn

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Vanessa McHale
In reply to this post by Joachim Durchholz
You'd probably want an ABI for types, no? You'd need a new executable
format (among many other things!).

The question is: would it be worth it? Types are wonderful in Haskell
because they allow us to structure our programs. What would structuring
processes via types accomplish? It would improve the situation with
shell scripting/pipes as you allude, but that's still an immense amount
of effort.

As for effect types - the IO monad in Haskell exists primarily to allow
side effects in a lazy language, so there's no reason I see to keep it
in an operating system.


On 10/05/2018 12:40 AM, Joachim Durchholz wrote:

> Am 05.10.2018 um 06:36 schrieb Yotam Ohad:
>> Hi,
>> In the last couple of days, I've been toying with the thought of an
>> operating system in which programs (or more accurately, any process)
>> has a distinct type which limits
>> its use of the machine. For example, `echo` (String -> String) won't
>> be able to print an output without a second program which would
>> handle changing stdout.
>>
>> I think it could "break down" the IO monad into other structures that
>> are better at specifying what is changing: A file is read / memory
>> written / etc.
>> I do, however, not sure how to incorporate drivers (which handles IO
>> and external devices) into this. Giving them an `IO a` type feels
>> like cheating. I would be much cooler if there was a way
>> to treat them like the `echo` function from earlier.
>>
>> What are your thoughts/suggestions? I'll be happy to hear them.
>
> An OS needs to work for any programming language, so I'm not sure how
> to get from an IO-based approach to a working OS. Unless you plan to
> write the OS itself in Haskell and make it so that all programs are
> Haskell modules, but that's a huge task.
>
> The design approach you're after is called "Capabilities". It's not
> ordinarily described as a type system, and I'm not sure whether it's a
> good idea to use static types in the first place because there are
> situations where you want to grant or revoke them dynamically.
> See https://en.wikipedia.org/wiki/Capability-based_security . This
> article also has a link to other security models; capabilities are
> pretty famous, but it's quite possible that a different one would be a
> better fit.
>
> HTH
> Jo
> _______________________________________________
> 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.

_______________________________________________
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.

signature.asc (499 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

John Z.
In reply to this post by Yotam Ohad
>  Hi,
> ...
> its use of the machine. For example, `echo` (String -> String) won't be
> able to print an output without a second program which would handle
> changing stdout.

For this specific example, it might be enough to just use something like
Turtle from Gabriel Gonzales:

    http://hackage.haskell.org/package/turtle

which -to me- signals that problem doesn't necessarily have to stretch
so far as to implement a whole OS. Maybe just fixing smaller pieces here
and there would provide much higher bang for the buck.


--
"That gum you like is going to come back in style."
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
In reply to this post by Ivan Perez
Am 05.10.2018 um 12:49 schrieb Ivan Perez:
>
>     The design approach you're after is called "Capabilities". It's not
>     ordinarily described as a type system, and I'm not sure whether it's a
>     good idea to use static types in the first place because there are
>     situations where you want to grant or revoke them dynamically.
>
> In part, isn't specifying this up-front what iOS and Android do with
> permissions, or docker with capabilities?

Even these grant and revoke permissions based on user actions.

What you can describe statically is right relationships - IF the user
has given permission such-and-so, THEN this-and-that activity is allowed.
Maybe that's the way to go. If not: Any alternative should have spent at
least some thought about how to deal with rights being granted and revoked.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

MarLinn
In reply to this post by Vanessa McHale

> You'd probably want an ABI for types, no? You'd need a new executable
> format (among many other things!).
>
> The question is: would it be worth it? Types are wonderful in Haskell
> because they allow us to structure our programs. What would structuring
> processes via types accomplish? It would improve the situation with
> shell scripting/pipes as you allude, but that's still an immense amount
> of effort.

Now that I think about it… having something like an ABI or a "Haskell
binary format" with types in it might indeed be useful in more cases
than this one.

It seems when a Haskell projects gets a bit larger people tend to search
for ways to make it more modular. They try plugin frameworks, OS-level
dynamic linking, on-the-fly compilation etc. But I repeatedly get the
feeling that all these current approaches aren't actually very good. But
what if we had some kind of specialized format for compiled, dynamically
loadable, typed Haskell libraries? Something between a plain OS library
and bytecode. This might help make programs more modular while keeping
them type safe.

One thing that might be useful to add next would be some kind of
centralized registry of types, so that a plugin/library could extend the
ways the system could be extended.

And going along this line of thought even further leads to… uhm… oh.    OH.

Ok, so, it's the month of Halloween, right?

Because… OSGi, but in Haskell.

Well, maybe there's some sane point in between?

Cheers,
MarLinn

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Brandon Allbery
I was thinking typed LLVM.

On Fri, Oct 5, 2018 at 3:46 PM MarLinn <[hidden email]> wrote:

> You'd probably want an ABI for types, no? You'd need a new executable
> format (among many other things!).
>
> The question is: would it be worth it? Types are wonderful in Haskell
> because they allow us to structure our programs. What would structuring
> processes via types accomplish? It would improve the situation with
> shell scripting/pipes as you allude, but that's still an immense amount
> of effort.

Now that I think about it… having something like an ABI or a "Haskell
binary format" with types in it might indeed be useful in more cases
than this one.

It seems when a Haskell projects gets a bit larger people tend to search
for ways to make it more modular. They try plugin frameworks, OS-level
dynamic linking, on-the-fly compilation etc. But I repeatedly get the
feeling that all these current approaches aren't actually very good. But
what if we had some kind of specialized format for compiled, dynamically
loadable, typed Haskell libraries? Something between a plain OS library
and bytecode. This might help make programs more modular while keeping
them type safe.

One thing that might be useful to add next would be some kind of
centralized registry of types, so that a plugin/library could extend the
ways the system could be extended.

And going along this line of thought even further leads to… uhm… oh.    OH.

Ok, so, it's the month of Halloween, right?

Because… OSGi, but in Haskell.

Well, maybe there's some sane point in between?

Cheers,
MarLinn

_______________________________________________
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.


--
brandon s allbery kf8nh

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
In reply to this post by MarLinn
Am 05.10.2018 um 21:46 schrieb MarLinn:
>
> It seems when a Haskell projects gets a bit larger people tend to search
> for ways to make it more modular. They try plugin frameworks, OS-level
> dynamic linking, on-the-fly compilation etc. But I repeatedly get the
> feeling that all these current approaches aren't actually very good. But
> what if we had some kind of specialized format for compiled, dynamically
> loadable, typed Haskell libraries? Something between a plain OS library
> and bytecode. This might help make programs more modular while keeping
> them type safe.

I've been believing that having a strict, universally-understood binary
format was the one thing that enabled Java's library ecosystem. Which is
huge, with a constant evolution of new generations and survival of the
fittest.

The downside is that compatibility with an established binary format is
a pretty restricting design constraint on language evolution - you
cannot evolve the language in ways that require a change to the binary
format, unless you are willing to give up compatibility with all the
precompiled binaries that are around.
I think it's doable, if the binary format has been carefully designed to
allow the kind of extensions that are being tought about.

The other prerequisite is that if a change to the binary format is
unavoidable, old formats stay readable. I.e. the loader needs to be able
to read old format, indefinitely. Alternatively, code repositories could
convert the code at upload time - the compatibility code would then live
in the repositories and not in the loader (which makes the code harder
to write but keeps the runtime smaller).

Well, that's what I can say from the Java and repository perspective.
I'm pretty sure there are other, and more important perspectives :-)

Regards,
JO
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Vanessa McHale
In reply to this post by MarLinn
Another thing that would be different in the OS case would likely be
that one could not have programs/processes of type

a -> a

...which would make any types stored in an ABI a good deal less flexible
than those in Haskell.


On 10/05/2018 02:46 PM, MarLinn wrote:

>
>> You'd probably want an ABI for types, no? You'd need a new executable
>> format (among many other things!).
>>
>> The question is: would it be worth it? Types are wonderful in Haskell
>> because they allow us to structure our programs. What would structuring
>> processes via types accomplish? It would improve the situation with
>> shell scripting/pipes as you allude, but that's still an immense amount
>> of effort.
>
> Now that I think about it… having something like an ABI or a "Haskell
> binary format" with types in it might indeed be useful in more cases
> than this one.
>
> It seems when a Haskell projects gets a bit larger people tend to
> search for ways to make it more modular. They try plugin frameworks,
> OS-level dynamic linking, on-the-fly compilation etc. But I repeatedly
> get the feeling that all these current approaches aren't actually very
> good. But what if we had some kind of specialized format for compiled,
> dynamically loadable, typed Haskell libraries? Something between a
> plain OS library and bytecode. This might help make programs more
> modular while keeping them type safe.
>
> One thing that might be useful to add next would be some kind of
> centralized registry of types, so that a plugin/library could extend
> the ways the system could be extended.
>
> And going along this line of thought even further leads to… uhm…
> oh.    OH.
>
> Ok, so, it's the month of Halloween, right?
>
> Because… OSGi, but in Haskell.
>
> Well, maybe there's some sane point in between?
>
> Cheers,
> MarLinn
>
> _______________________________________________
> 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.

_______________________________________________
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.

signature.asc (499 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Ivan Perez
I sort of see why you might now, but I'm not sure it's what you mean? Could you elaborate?

I think you can if you base this in some sort of indexed monad and have a way to join indices. Your process then become a -> (ioM e) a, where e is the neutral element or index for the index join operation. Perhaps indices could denote sets of permissions or capabilities.

Ivan


On Fri, 5 Oct 2018 at 22:09, Vanessa McHale <[hidden email]> wrote:
Another thing that would be different in the OS case would likely be
that one could not have programs/processes of type

a -> a

...which would make any types stored in an ABI a good deal less flexible
than those in Haskell.


On 10/05/2018 02:46 PM, MarLinn wrote:
>
>> You'd probably want an ABI for types, no? You'd need a new executable
>> format (among many other things!).
>>
>> The question is: would it be worth it? Types are wonderful in Haskell
>> because they allow us to structure our programs. What would structuring
>> processes via types accomplish? It would improve the situation with
>> shell scripting/pipes as you allude, but that's still an immense amount
>> of effort.
>
> Now that I think about it… having something like an ABI or a "Haskell
> binary format" with types in it might indeed be useful in more cases
> than this one.
>
> It seems when a Haskell projects gets a bit larger people tend to
> search for ways to make it more modular. They try plugin frameworks,
> OS-level dynamic linking, on-the-fly compilation etc. But I repeatedly
> get the feeling that all these current approaches aren't actually very
> good. But what if we had some kind of specialized format for compiled,
> dynamically loadable, typed Haskell libraries? Something between a
> plain OS library and bytecode. This might help make programs more
> modular while keeping them type safe.
>
> One thing that might be useful to add next would be some kind of
> centralized registry of types, so that a plugin/library could extend
> the ways the system could be extended.
>
> And going along this line of thought even further leads to… uhm…
> oh.    OH.
>
> Ok, so, it's the month of Halloween, right?
>
> Because… OSGi, but in Haskell.
>
> Well, maybe there's some sane point in between?
>
> Cheers,
> MarLinn
>
> _______________________________________________
> 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.

_______________________________________________
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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Barak A. Pearlmutter-2
In reply to this post by Yotam Ohad
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.
Reply | Threaded
Open this post in threaded view
|

Re: 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 <[hidden email]> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

William Yager
In reply to this post by Barak A. Pearlmutter-2


On Sat, Oct 6, 2018 at 11:03 PM Barak A. Pearlmutter <[hidden email]> 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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Barak A. Pearlmutter-2
> 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.

The Cedilla folks had a pretty clever way of dealing with that issue.
They had a very small proof checker on the embedded device, which used
highly compressed information associated with the binary to basically
guide a theorem prover, where the information helped the prover make
all its choices.

This information was generated from a proof generated by a compiler,
which compiled a high-level language (C in their case) annotated with
extra safety-proof-related information down to both machine code an a
proof of that machine code's safety. So they sort of did what you're
describing, but partially evaluated away the IR.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

"Ionuț G. Stan"
The JVM is also doing something similar. There's a step in the process
of loading the .class files called "bytecode verification". Ιt's
basically a type checker for the stack language used in the bytecode.

This was problematic in Java before version 7, because it was possible
to cause denial-of-service attacks by sending malicious bytecode
payloads. The verifier would spend O(n^2) time verifying that the
bytecode behaves correctly.

As of Java 7, compilers are required to add additional info alongside
the bytecode instructions. This extra info is called a stackmap table
and allows the verifier to complete its verification in O(n) steps,
IIRC. So, a certain instantiation of PPC is already used in the wild.


On 07/10/2018 12:00, Barak A. Pearlmutter wrote:

>> 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.
>
> The Cedilla folks had a pretty clever way of dealing with that issue.
> They had a very small proof checker on the embedded device, which used
> highly compressed information associated with the binary to basically
> guide a theorem prover, where the information helped the prover make
> all its choices.
>
> This information was generated from a proof generated by a compiler,
> which compiled a high-level language (C in their case) annotated with
> extra safety-proof-related information down to both machine code an a
> proof of that machine code's safety. So they sort of did what you're
> describing, but partially evaluated away the IR.
> _______________________________________________
> 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.
>

--
Ionuț G. Stan  |  http://igstan.ro  |  http://bucharestfp.ro
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
Am 07.10.2018 um 12:41 schrieb Ionuț G. Stan:
> The JVM is also doing something similar. There's a step in the process
> of loading the .class files called "bytecode verification". Ιt's
> basically a type checker for the stack language used in the bytecode.

It's checking more than just types:

* Branch target and exception handler address validity.
* Stack offset validity.
* Each code branch ends with a return instruction.
* Local variables initialized before use in each branch of code.
* No stack overflow or underflow along each code path.
* Validation of private and protected access.

I suspect that all of this can be expressed as a type check, but some of
them require that a type be generated for each natural number that's in
the class file, and I have yet to see an approach that gives each of
these types a printable, humanly understandable representation.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

"Ionuț G. Stan"
On 07/10/2018 14:10, Joachim Durchholz wrote:
> Am 07.10.2018 um 12:41 schrieb Ionuț G. Stan:
>> The JVM is also doing something similar. There's a step in the process
>> of loading the .class files called "bytecode verification". Ιt's
>> basically a type checker for the stack language used in the bytecode.
>
> It's checking more than just types:

Sure. I used an informal, hand-wavy sense for "type checker".

> * Branch target and exception handler address validity.
> * Stack offset validity.
> * Each code branch ends with a return instruction.
> * Local variables initialized before use in each branch of code.
> * No stack overflow or underflow along each code path.
> * Validation of private and protected access.
>
> I suspect that all of this can be expressed as a type check, but some of
> them require that a type be generated for each natural number that's in
> the class file, and I have yet to see an approach that gives each of
> these types a printable, humanly understandable representation.

Can you give a bit more detail here? Or a pointer to someone who
elaborated on this? I got a bit lost on the natural number step, which
seems to be some sort of theoretical way to represent those types. On
the other hand you say they're in the class file.

BTW, I'm quite familiar with the class file format and have even started
writing a bytecode verifier for my own compiler pet project. So, be as
specific as you can.

> _______________________________________________
> 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.
>

--
Ionuț G. Stan  |  http://igstan.ro  |  http://bucharestfp.ro
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Well typed OS

Joachim Durchholz
Am 07.10.2018 um 13:47 schrieb Ionuț G. Stan:
>> a type be generated for each natural number that's in
>> the class file, and I have yet to see an approach that gives each of
>> these types a printable, humanly understandable representation.
>
> Can you give a bit more detail here? Or a pointer to someone who
> elaborated on this? I got a bit lost on the natural number step, which
> seems to be some sort of theoretical way to represent those types.

You can make Haskell's type system count, by defining a `Zero` type and
a `Succ a` type - well, I think it's a kind (i.e. a type of types). That
(and equality) is enough to do natural numbers - you have Zero, One =
Succ Zero, Two = Succ Succ Zero, etc.

I don't know enough about this stuff to give a recipe, I just saw
descriptons of what people were doing.
The earliest awesome trick of this kind was somebody who encoded matrix
squareness in the type system. (You cannot even define inversion for a
non-square matrix, so square matrices are pretty different beasts than
non-square ones.)
Somebody else (I think) started doing the natural numbers. You can do
any kinds of cool tricks with that, such as cleanly expressing that to
multiply two matrices, the height of one matrix needs to be the same as
the width of the other.

In theory, you can express any arithmetic relationships within the type
system that way: Addresses, matrix dimension constraints, etc.
In practice, any error messages are going to look like "invalid type
Succ Succ Succ .... Succ Zero", and you have to count the number of
Succs, which sucks (pun intended).

I suspect you can also do fractional numbers with that - you essentially
translate the axioms some type (or kind) declarations.
I'd expect that to be even less usable in practice.
However, it's intriguing what you can do with types.

Now please take this all with a grain of salt. I never used this kind of
stuff in practice, I just saw the reports of people doing this clever
insanity, and didn't want to do it myself.
The approach never took on if this kind of old lore isn't present in
Haskell Café anymore.

> BTW, I'm quite familiar with the class file format and have even started
> writing a bytecode verifier for my own compiler pet project. So, be as
> specific as you can.

I was more like handwaving at the possibility of turning all assertions
over integral numbers into type constraints.
I am definitely not recommending doing this in practice!

Regards,
Jo
_______________________________________________
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.
12