You don’t need this existential GADT, it is equivalent to the simply defined type sink = [sink_ty] Std.r. The type that will indeed be used if we get rid of row-polymorphism to favor explicit casting at call site.
module type Doublable = sig
module type S = sig
type t
val double : t -> t
end
(* the super type of all doublable values *)
type doublable
(* a generic, and only real way to produce a doublable *)
val make : (module D : S) -> D.t -> doublable
module Top : S with type t = doublable
(* then any generic methods on doublable go there *)
val foo : (module D : S) -> D.t -> ...
val bar : (module D : S) -> D.t -> ...
val baz : (module D : S) -> D.t -> ...
end
And you can implements the doublable type with an object and even expose it publicly. To be honest, what I really miss in Eio API is this generic make constructor for all the kinds of resources it propose.
In fact when you do OOP, you systematically apply the generic functions foo, bar and baz with the same first class module, namely Top, the one that states that all doublable are doublable (a real truism, I know). And that’s what I usually dislike in OOP idiom: in order to use generically a value as doublable, you first have to upcast it in the supertype that represents the object, which most of the time is a complete non sense and an insult to human mind.
When you do subtyping between two objects types, it really amounts to do subtyping between their corresponding module signatures. That’s why I proposed the & module type operator, to be on par with the object type language. If you have two signatures S1 and S2 you will have <S1.top; S2.top> = <(S1&S2).top> (where the type top denotes the supertype of all values satisfying these signatures, seen as an OOP object and that Rust call a trait object).
I would qualify this as a fundamental security bug of the current Eio implementation: downcasting must be forbidden in a capability system, otherwise there is no more guaranty of any kind.
Edit: one thing that’s missing in OCaml is the possibility to use first-class module with classes (because they are indeed deeply related).
class doublable (module M : S with type t = 'a) (x : 'a) = object end;;
Error: Modules are not allowed in this pattern
I may change my mind upon learning more, but I don’t see eye-to-eye to this as of yet. Here is my current reasoning: before reading this discuss thread, I didn’t have the idea of mixing the idea of capabilities in eio with the resource module as a single topic. The part of Eio that I thought to be about capability is the pieces contained in a Stdenv, and this part still uses a regular Object so doesn’t have this security bug (e.g. your program won’t do Net stuff if you don’t give it the env#net part, etc.). The dynamic dispatch implemented by Eio.Resource to me is more of an implementation detail - you probably need of form of this to deal with the multi-backend part of the library, but I don’t see a priori how this must be necessarily thought as part of the Capability approach. Is there a framing by which both can be discussed separately?
Maybe I had misunderstood something in my reading of Eio API, but as far as I understand it any resource is a _ Std.r. And this type is an object-like type where its object system is implemented by the Resource module (and I still don’t understand why Eio reimplements an object system since there is already an existing one in OCaml). This system allows dynamic downcasting, which I consider as a security issue in a capability object system.
For instance, nothing can guaranty, from its type, that the function File.pread : _ ro -> file_offset:Optint.Int63.t -> Cstruct.t list -> int doesn’t write to the file given if it is a _ rw one. Maybe, under the hood, pread try a downcasting and does a write if it succeeds, which defeats the whole purpose of a capability system: I have to read the code to convince me that pread doesn’t perform forbidden writes.
Honestly, as I said just above, I don’t really understand why the Resource module implements an unsafe object system, since we already have a perfectly valid and well thought one in OCaml.
The Stdenv, which contains what you could maybe call the toplevel or main capabilities is a regular OCaml Object as of eio.1.2, not a _ Std.r.
That being said, I am still going through the code and your argument about forbidding downcasting won me over. I should refine my reserve, perhaps by acknowledging the issue, but saying that I am not yet sure how much of a big deal this is in practice (a.k.a “a fundamental security bug”). I agree in principle, and I am thankful for your explanations, from which I feel I already learned a lot!
I am doing some exploration based on feedback from this thread, and as part of on-going work I started in Eio.Resource and Type-Safety · Issue #774 · ocaml-multicore/eio · GitHub. I have many questions I would love to ask the eio-devs, but this is going to be a end-of-year break for me. If we could have this topic be a agenda item in one of the next eio meetings, I’d love to attend and discuss more! Happy end-of-year, and talk soon!
Maybe but it gives you access to resources that are all _Std.r. So even if its an OCaml object, as soon as the main entry point of a program delegates some of its works to auxiliary functions, those can bypass the restricted right they have (by trying to downcast the resources they consume).
Finally, I think I find my answer to the reason of the Resource module on Eio issue tracker. It is on an issue you open Eio.Resource and Type-Safety and @talex5 gave you this response:
And now I feel very disappointed. Eio implements its own object system instead of using the built-in one, just to avoid annoying people. But it is necessary to have an object system to implement capabilities ! It seems clear to me from the paper Capability Myths Demolished that a capability is a pair maid up of an authority and a resource (to follow the article’s terminology). For instance, in the brief design of your doublable example the two components (authority and resource) could not be more explicit in the API:
val foo : (module D : S) -> D.t -> ...
The first-class module is the authority (and so the module type language is the access policy language) and D.t is the resource. The OCaml type system ensure that foo can not use more right with the resource that what the authority give to it.
With such an API, we get implicit subtyping for free on authorities (you can give to foo a module with more right, i.e. a subtype of S, it can still only use the right given by the S signature).
But I guess that this API with an explicit authority argument will not scale very well in a library like Eio. So the solution is to switch to an OOP API like this one:
val foo : #doublable -> ...
val bar : #doublable -> ...
val baz : #doublable -> ...
It was the original design of @talex5 and I find it was a very ingenious use of OCaml object system. This choice of API makes even more sense in a capability framework since, at some point, resources are not only consume but also produce. But, for safety reason, the pair (authority, resource), when produced, have to be hidden behind an existential (that would be the GADT implementation of an object) in order to avoid privilege escalation. Therefore, since, most of the time, resources will appear in the form of an object, you might as well stick with an object-oriented API (and it’s still the case, _ Std.ris an object).
I’ve just been catching up on this thread. I’d like to clear up a bit of confusion: the polymorphic types (whether variants or objects) are unrelated to capabilities. The types are to catch errors at compile time rather than run time. Capabilities do not require a static type system, and many existing capability systems don’t have one.
Consider this function:
let f () =
let w, r = Unix.pipe () in
Unix.write_substring w "Hello" 0 5
This compiles fine, but raises Unix_error when run, because I mixed up w and r, which both have type Unix.file_descr. To avoid this, Eio adds types. If you do this with Eio, you get:
let f () =
Switch.run @@ fun sw ->
let w, r = Eio_unix.pipe sw in
Eio.Flow.copy_string "Hello" w
This expression has type Eio_unix.source_ty r
but an expression was expected of type [> Eio.Flow.sink_ty ] r
However, the errors are not ideal and if it’s causing more confusion than benefit then we should consider removing the types.
Capabilities solve a different problem. Consider:
let f () =
let r, w = Unix.pipe () in
Unix.close w;
Unix.sleep 1;
Unix.write_substring w "Hello" 0 5
On its own, this fails with Unix.EBADF because w is no longer valid. However, if another domain meanwhile opened an Sqlite database (e.g. with Sqlite3.db_open "./my_db") then the database will get corrupted.
Capabilities solve this spooky-action-at-a-distance problem.
If you try this in Eio, you get:
let f () =
Switch.run @@ fun sw ->
let r, w = Eio_unix.pipe sw in
Eio.Flow.close w;
Eio_unix.sleep 1.0;
Eio.Flow.copy_string "Hello" w
Fatal error: exception Invalid_argument("write: file descriptor used after calling close!")
Only code that is given access to the database can access it, and this code was never passed a reference to it.
I would say rather “The purpose of a capability system is to prevent code without a reference to the bytes value from accessing it”. Since bytes values only exist in memory, capability safety here is just memory safety, and the API is already capability safe (assuming you ignore the explicitly “unsafe” functions, as we always have to do in OCaml).
You could use polymorphic types to provide further control. @dinosaure did that with cstruct_cap.mli (which also uses the word “capability”, but not in the way I use it).
But this isn’t the main point. It would be quite reasonable to have a program like this:
Code needing read and write access to the bytes : 5 lines
Code needing read-only access: 20 lines
Code not needing access: 1 million lines
The main value of memory safety / capabilities is protecting against (3). Protecting against (2) is relatively minor.
But we already know this for memory; it’s why writing secure C code is so hard. If we did Sqlite3.db_open ":memory:" above then no corruption would occur, because OCaml’s memory safety doesn’t allow it, but you need capabilities if you want to generalise this idea to other mutable state, such as files.
Anything that provides private state would do, such as a function closure (the blog used functions rather than objects). In general, functions and objects are equivalent for this purpose.
Note that the paper’s first author, Mark Miller, was a developer of the E language. There, a function is just an object with a run method. f(x) is syntactic sugar for f.run(x) and def square(x) {return x*x} is sugar for:
def square {
to run(x) {return x*x}
}
(which is nice, because you can start by writing everything with plain functions and then upgrade them to objects if you want additional features, without breaking the API)
The policy is the code. The web-server example in the blog gave full read/write access to htdocs to the handler, with let handler = static_files htdocs. Here’s how static_files converted the read/write access to htdocs into read-only access for the HTTP library:
let static_files dir request =
Path.load (dir / request.path)
Here, it just happens as a side-effect of writing the HTTP handler, since it only uses the load function. This is typical. It is possible to wrap one resource in similar but more restricted one (as the Attenuation section shows), but this is relatively uncommon. I probably will add an Eio.Path.read_only function at some point, though.
In some cases, you may be able to restrict the static type of a resource (e.g. casting away write access) rather than wrapping it, but capabilities don’t require that.
This is also true for Java, and for Eio resources (especially since switching from objects).
I guess that you miss my point. According to you, if I have a function with this signature:
foo : _ read -> foo
(this is not the type you will get with Eio, but the idea is here) foo is supposed to consumed a value it can only read.
But If foo is using Resouce.get_opt under the hood then, sometimes, it can can write to its arguments. And, at this this point, it defeats all the purpose of the capability system. Hence, your supposed capability system is broken by design (it was not the case when you used OCaml built-in object).
Here is the problem: you add a broken capability layer (that what not the case when you used OCaml object classes) on top of concurrency layer. But OCaml users only want the latter. So my advise to OCaml programmers is, from a logical and mli reading audit point of view, to stay away from Eio until they solve this problem. Since now, Eio adds you burden without any benefit.
To be honest, I don’t mind the problem with Java. Behind this language there is the gang of four that I personally call the gang of four idiiot. So, what is the purpose to be like an idiot? i’m not an adept of OOP, but when it is a good solution, especially with OCaml implementation, why not use it?
For sure, that’s absolutly not what is said in the articles that you linked in your blog post. If you have a text editor, at some point you want to open a file. But, to do so, for sure you need a reference (resources) to that file, but the articles you linked not only say that you need such a reference but that you also must only have the right to read it (and not write to it, if the only thing you have is a reference to the resource).
Putting this in stdlib terms, I think you’re suggesting that a function such as this shouldn’t be able to write to its argument:
val foo : in_channel -> unit
Normally this will be the case, because the channel will be opened in read-only mode. And it would be considered rude to write to it. However, the type here is not a security feature. foo can easily write to the channel if it wants:
let foo x =
let fd = Unix.descr_of_in_channel x in
ignore (Unix.write_substring fd "Hello" 0 5 : int)
let () =
let fd = Unix.openfile "/tmp/out" [O_RDWR; O_CREAT; O_EXCL] 0o600 in
let ch = Unix.in_channel_of_descr fd in
foo ch
What I wrote was:
The capability solution to this is to create a new resource that proxies only read requests to the underlying read/write resource. Typically this happens as in the HTTP example, where the request handler only uses the load function on the htdocs directory.
I think you are suggesting that in Eio you want to be able to make a read/write flow into a read-only one securely using type casting. This is an interesting idea, but not a capabilities thing. At least for Unix flows it wouldn’t work, because a two-way flow should give up its underlying file descriptor on demand when used as read/write, but refuse to do so when read only, but it can’t know its type at runtime.
Yes, to be clear: I personally prefer using objects (polymorphic records) for this. However, some parts of the OCaml community strongly dislike them, so to avoid splitting the community we removed them.
I didn’t say such a thing. And I am perfectly aware of the problem with Stdblib regards capabaility.
What I want to say is simpler:Eio is a very good piece of code. When you used object classes it was the right thing to do. Implementation of an object system via the Resource module only add thid consequence: you have a working capability system and now it is broken.
Hence, my advise is the following: do what you did at first because it was the right thing to do.