4 ms·

You can do a lot with capabilities at the language level, if the language supports it. It doesn't require effect types: it's extremely boring from a type system

You can do a lot with capabilities at the language level, if the language supports it. It doesn't require effect types: it's extremely boring from a type system perspective, which is an advantage. Imagine these changes to a language, making it "capability safe": - There is a `Network` object, and it's the only way to access the network. Likewise, there's a `Filesystem` object, and it's the only way to access the file system. - Code cannot construct a `Network` or `Filesystem` object. Like, you just can't, there's no constructor. - The `main()` function is passed a `Network` object and a `Filesystem` object. Consider the consequences of this. The log4j vulnerability involved a logging library doing network access. In a capability safe language, this could only happen if you passed a `Network` object to the logger, either in its constructor or in one of its methods. So the vulnerability is still possible. But! Now you can't be surprised that your logger was accessing the network because you gave it the network. And a logger asking for network access is sufficiently sketchy that log4j almost certainly would have made network access optional for the few users that wanted that feature, which would have prevented the vulnerability for everyone else! I talked about there being a single monolithic `Filesystem` object. That is what would be passed into `main()`, but you should also be able to make finer grained capabilities out of it. For example, you should be able to use the `Filesystem` object to construct an object that has read/write access to a directory and its subdirectories. So if a function takes one of these as an argument, you know its not mucking around outside of the directory you gave it. Capability safety within a language is stronger than the sort of capability safety you can get at the process level or at the level of multiple machines. But we want those too!

gnafkcud 2y ago
this was the original approach for Java, and the main idea behind being able to ship untrusted apps directly to the user and run them in the browser tomcat also gave different privilege levels to different parts of the classpath nice idea, but didn't seem to work in practice
- justinpombrio 2y ago
  That's what I'm calling capabilities at the application level (where you say "this .jar can't access the network"), rather than at the language level (where you say "this function wasn't given access to the network as an argument"). I don't think any widely known language has tried capabilities at the language level. (The language not widely known that does it is E.) The real power will come when you can mix them. In one direction, that looks like `main()` not getting passed a `Network` object because the ".jar" wasn't granted network access. In the other direction, that looks like the system C library you invoked failing to access the network because when you invoked it from Java you failed to provide a `Network` object, so it was automatically sandboxed to not be able to access the network.
  - tlavoie 2y ago
    Have you looked at "Emily" language at all? Same person or two, their original paper isn't reachable at their linked URL, but is on the Wayback Machine. "How Emily Tamed the Caml" - https://web.archive.org/web/20221231184748/https://www.hpl.hp.com/techreports/2006/HPL-2006-116.pdf https://web.archive.org/web/20221231184748/https://www.hpl.h... Emily took the approach of restricting a subset of OCaml, which they were running on Windows machines. No idea how tough it would be to get it running on a modern version. Also for OCaml, the MirageOS unikernel is neat - develop on Linux etc., then recompile configured as a virtual machine with only the drivers (network, filesystem) needed by that one app. - https://mirage.io/ https://mirage.io/
  - blibble 2y ago
    > That's what I'm calling capabilities at the application level (where you say "this .jar can't access the network"), rather than at the language level (where you say "this function wasn't given access to the network as an argument") it wasn't, it was done at the type and classloader level have a read about SecurityManager
deleted 2y ago
[deleted]
marcosdumay 2y ago
> this could only happen if you passed a `Network` object to the logger Yeah, this is not only an effects type system, it's a static effects type system.
- justinpombrio 2y ago
  No it's not. I'd guess you're imagining a type signature like this one? void effect:Network my_function_to_connect_to_server() { ... } I mean a type signature like this one: void my_function_to_connect_to_server(Network network) { ... } Where there's absolutely nothing special about the Network type, except that (i) it has no constructor, and (ii) nothing in the Java language lets you talk to a network without it. All of this is expressible with Java's type system today.
  - marcosdumay 2y ago
    > void my_function_to_connect_to_server(Network network) See how there's the Network right there on the type?
    - justinpombrio 2y ago
      That's an ordinary argument type. Like: void my_function_to_connect_to_server( Network network, int port, String server_name ) It's not categorically different than the other arguments, and doesn't require an effect type system. At this point I'm not sure if you're misunderstanding what I'm proposing, or if you don't know what an effect system is. If you care to communicate, you'll need to say something more substantial. Walk me through what you're trying to say.
      - marcosdumay 2y ago
        Make it generic, with some kind of Resource interface that Network is one of the implementations¹, and you get a dynamic effect system. But that thing you wrote is a static effect system. Having a singleton that you need to carry with the type doesn't make it not part of the type system. 1 - Or actually use Resource as a class. But Java wouldn't do this.
yencabulator 2y ago
In theory Rust where you don't allow unsafe can do that. (Reality is not perfect: https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860) Theseus OS is a research project that created single address space kernel that loads dynamic libraries written in safe-only Rust as "untrusted entities". Compiled with a trusted compiler that forbids unsafe. If they have no access to unsafe, and you're not giving them functions to link to that would hand them these a-capability-if-you-squint objects, they're supposedly sandboxed. https://www.theseus-os.com/ https://www.theseus-os.com/

gnafkcud 2y ago

this was the original approach for Java, and the main idea behind being able to ship untrusted apps directly to the user and run them in the browser tomcat also gave different privilege levels to different parts of the classpath nice idea, but didn't seem to work in practice

justinpombrio 2y ago
That's what I'm calling capabilities at the application level (where you say "this .jar can't access the network"), rather than at the language level (where you say "this function wasn't given access to the network as an argument"). I don't think any widely known language has tried capabilities at the language level. (The language not widely known that does it is E.) The real power will come when you can mix them. In one direction, that looks like `main()` not getting passed a `Network` object because the ".jar" wasn't granted network access. In the other direction, that looks like the system C library you invoked failing to access the network because when you invoked it from Java you failed to provide a `Network` object, so it was automatically sandboxed to not be able to access the network.
- tlavoie 2y ago
  Have you looked at "Emily" language at all? Same person or two, their original paper isn't reachable at their linked URL, but is on the Wayback Machine. "How Emily Tamed the Caml" - https://web.archive.org/web/20221231184748/https://www.hpl.hp.com/techreports/2006/HPL-2006-116.pdf https://web.archive.org/web/20221231184748/https://www.hpl.h... Emily took the approach of restricting a subset of OCaml, which they were running on Windows machines. No idea how tough it would be to get it running on a modern version. Also for OCaml, the MirageOS unikernel is neat - develop on Linux etc., then recompile configured as a virtual machine with only the drivers (network, filesystem) needed by that one app. - https://mirage.io/ https://mirage.io/
- blibble 2y ago
  > That's what I'm calling capabilities at the application level (where you say "this .jar can't access the network"), rather than at the language level (where you say "this function wasn't given access to the network as an argument") it wasn't, it was done at the type and classloader level have a read about SecurityManager

deleted 2y ago

[deleted]

marcosdumay 2y ago

> this could only happen if you passed a `Network` object to the logger Yeah, this is not only an effects type system, it's a static effects type system.

justinpombrio 2y ago
No it's not. I'd guess you're imagining a type signature like this one? void effect:Network my_function_to_connect_to_server() { ... } I mean a type signature like this one: void my_function_to_connect_to_server(Network network) { ... } Where there's absolutely nothing special about the Network type, except that (i) it has no constructor, and (ii) nothing in the Java language lets you talk to a network without it. All of this is expressible with Java's type system today.
- marcosdumay 2y ago
  > void my_function_to_connect_to_server(Network network) See how there's the Network right there on the type?
  - justinpombrio 2y ago
    That's an ordinary argument type. Like: void my_function_to_connect_to_server( Network network, int port, String server_name ) It's not categorically different than the other arguments, and doesn't require an effect type system. At this point I'm not sure if you're misunderstanding what I'm proposing, or if you don't know what an effect system is. If you care to communicate, you'll need to say something more substantial. Walk me through what you're trying to say.
    - marcosdumay 2y ago
      Make it generic, with some kind of Resource interface that Network is one of the implementations¹, and you get a dynamic effect system. But that thing you wrote is a static effect system. Having a singleton that you need to carry with the type doesn't make it not part of the type system. 1 - Or actually use Resource as a class. But Java wouldn't do this.

yencabulator 2y ago

In theory Rust where you don't allow unsafe can do that. (Reality is not perfect: https://github.com/rust-lang/rust/issues/25860 https://github.com/rust-lang/rust/issues/25860) Theseus OS is a research project that created single address space kernel that loads dynamic libraries written in safe-only Rust as "untrusted entities". Compiled with a trusted compiler that forbids unsafe. If they have no access to unsafe, and you're not giving them functions to link to that would hand them these a-capability-if-you-squint objects, they're supposedly sandboxed. https://www.theseus-os.com/ https://www.theseus-os.com/