Keeping local types local?

Keeping local types local?

[oleg]

David Rajchenbach-Teller wrote:

> One way of doing so would be to use monads but my idea is to use local
> modules and local types and take advantage of the fact that values of
> that type cannot escape the scope of the local module. Unfortunately,
> as it turns out, sometimes, values with a local type can escape their
> scope -- and I'm looking for an idea on how to plug the leak.

I don't think there is much hope. Without monads (or, better,
parameterized monads) and without the effect type system, there is
nothing to prevent the `escape'. The type system of OCaml is
powerless: it can prevent the value 'v' of some type to be used
outside the local module that declares that local type. However,
nothing prevents us from forming a closure
	fun () -> consumer v; ()
and using that closure anywhere we see fit. The closure has the
`effect' of consuming the value, regardless of any bracketing
boundaries. And yet its type is unit->unit. The problem with ML in
general is precisely that the type of the function says absolutely
nothing about the function's effects. It gets worse: there is a
similar way to consume the value 'v' of a `local' type
inappropriately: via an assignment. The consumer code may include the
following:

	let thunk = ref (fun () -> ())

	let process () =
	     !thunk ();
	     thunk := fun () -> ignore (set v);
	     ...

The next invocation of the the process function of the consumer will
execute set v, probably outside of the transaction
boundaries. One should also worry about returning thunks via
exceptions... 

Section 4.3 of
	http://okmij.org/ftp/Computation/resource-aware-prog/region-io.pdf
as well as the accompanying code shows several attempts to break out
of the region boundaries. As far as the Region-IO paper is concerned,
all attempts failed. Because we do use monads, rank-2 polymorphism and
because the type of the monad specifically reflects its effects. For
fancier guarantees, one needs parameterized monads (which aren't
actually monads), see Section 6 of the paper.

Rank-2 polymorphism is available in OCaml too. In fact, MetaOCaml uses
this technique to prevent `escaping' of free variables, to make sure
that only closed code could be run. Mutations and exceptions still
pose the problem however.

Perhaps the best approach in OCaml now is sand-boxing. Although
it is not advertised much, OCaml system is quite `reflective'. One can
trivially adapt the main compiler driver so to compile a source code
file in a `reduced' environment -- the environment that does not have
the ref type, for example. By controlling the available operations and
available types, we can restrict the effects; we should also define an
appropriate variant (Int, Bool, pair, array -- but not a closure) and
insist the return value be of that variant type. The return value
must be serializable, and we should only permit assignments of
serializable values. That may be sufficient for safety.

Re: Keeping local types local?

[David Rajchenbach-Teller]

Thanks for the answer.

My hope is that, since OCaml does already perform some scope escape
analysis, this analysis could be hijacked into something more
restrictive with the help of some simple rewriting/staged compilation.

Now, I realise that monads (I'm unfamiliar with parametrised monads,
although I have the intuition that they are what I call "indexed
families of monads" in my own work -- I'll be sure to read your paper)
are a solution to the problem, possibly the only solution. My issue with
this is that monads are a quite un-ocamlish solution, which requires
rewriting every single line of code, largely losing the ability to
compose functions and affecting performances too much for my taste, not
to mention the problem of monad transformers.

So I'm looking for another way out. As far as both your examples and my
experiments seem to indicate, the only way of escaping scope is to
return a continuation which calls one of the protected functions and
ignores the result. So there is a relatively simple way of preventing
escapes, which can probably be done syntactically: forbidding
continuations. Now, that's a harsh measure so perhaps we can alleviate
it. Assuming we allow rewriting, we can possibly replace every single
function definition inside the scope with something a tad more drastic
-- I don't know what yet, but there may be a way.

Now, I have the feeling that this may require also modifying the
language, to introduce something which, to my intuition, looks like
implicit parameters. I'm not sure how deep such a modification should
run (perhaps Camlp4 is sufficient) but I have the feeling that such a
modification would also prove quite useful for adding type-classes to
OCaml, so if the depth is limited, it may be a good idea to achieve both
changes with one stroke.

What do you think?

Cheers,
 David

P.S.: I'll be sure to read your paper -- we seem to have many common
preoccupations of late.
P.P.S.: Sandboxing? Interesting idea. I was planning to get a few
students to implement dynamic  evaluation in OCaml but I hadn't thought
of using that for the purpose of sandboxing.

On Tue, 2008-09-16 at 03:12 -0700, oleg@okmij.org wrote:
> David Rajchenbach-Teller wrote:
> 
> > One way of doing so would be to use monads but my idea is to use local
> > modules and local types and take advantage of the fact that values of
> > that type cannot escape the scope of the local module. Unfortunately,
> > as it turns out, sometimes, values with a local type can escape their
> > scope -- and I'm looking for an idea on how to plug the leak.
> 
> I don't think there is much hope. Without monads (or, better,
> parameterized monads) and without the effect type system, there is
> nothing to prevent the `escape'. The type system of OCaml is
> powerless: it can prevent the value 'v' of some type to be used
> outside the local module that declares that local type. However,
> nothing prevents us from forming a closure
> 	fun () -> consumer v; ()
> and using that closure anywhere we see fit. The closure has the
> `effect' of consuming the value, regardless of any bracketing
> boundaries. And yet its type is unit->unit. The problem with ML in
> general is precisely that the type of the function says absolutely
> nothing about the function's effects. It gets worse: there is a
> similar way to consume the value 'v' of a `local' type
> inappropriately: via an assignment. The consumer code may include the
> following:
> 
> 	let thunk = ref (fun () -> ())
> 
> 	let process () =
> 	     !thunk ();
> 	     thunk := fun () -> ignore (set v);
> 	     ...
> 
> The next invocation of the the process function of the consumer will
> execute set v, probably outside of the transaction
> boundaries. One should also worry about returning thunks via
> exceptions... 
> 
> Section 4.3 of
> 	http://okmij.org/ftp/Computation/resource-aware-prog/region-io.pdf
> as well as the accompanying code shows several attempts to break out
> of the region boundaries. As far as the Region-IO paper is concerned,
> all attempts failed. Because we do use monads, rank-2 polymorphism and
> because the type of the monad specifically reflects its effects. For
> fancier guarantees, one needs parameterized monads (which aren't
> actually monads), see Section 6 of the paper.
> 
> Rank-2 polymorphism is available in OCaml too. In fact, MetaOCaml uses
> this technique to prevent `escaping' of free variables, to make sure
> that only closed code could be run. Mutations and exceptions still
> pose the problem however.
> 
> Perhaps the best approach in OCaml now is sand-boxing. Although
> it is not advertised much, OCaml system is quite `reflective'. One can
> trivially adapt the main compiler driver so to compile a source code
> file in a `reduced' environment -- the environment that does not have
> the ref type, for example. By controlling the available operations and
> available types, we can restrict the effects; we should also define an
> appropriate variant (Int, Bool, pair, array -- but not a closure) and
> insist the return value be of that variant type. The return value
> must be serializable, and we should only permit assignments of
> serializable values. That may be sufficient for safety.
> 
> 
-- 
David Teller-Rajchenbach
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act brings liquidations. 

Re: Keeping local types local?

[oleg]

> So I'm looking for another way out. As far as both your examples and my
> experiments seem to indicate, the only way of escaping scope is to
> return a continuation which calls one of the protected functions and
> ignores the result.

I'm afraid this is worse than it seems. Returning any closure (not
necessarily a continuation) can defeat the security. To summarize, the
security of the framework is defeated if

	-- one returns a closure that calls a protected function
	-- one returns an object whose method calls a protected function
	-- one returns a polymorphic record that `abstracts'
	over the abstract type guarding the protected function

	-- one assigns to the mutable variable: a closure, an object,
or a polymorphic record

	-- one throws or returns an exception that contains a closure,
an object, or a polymorphic record

Here is the illustrating code. We start with the baseline
let f0 () =
  let result =
    let module A =
        struct
          type 'a t = Guard of 'a (*Used only to prevent scope escape.*)
                  (** Local primitives, usage guarded by [Guard] *)
          let set v =
            print_endline "set has been called"; Guard ()
          let return x = Guard x
          let result =
	    print_endline "Initialization";
            match
	      (* Good client *)
	      set 1
            with Guard x -> print_endline "Clean-up"; x
        end in A.result
  in result
;;
let test1 = f0 ();;

We see that set has been called after initialization and _before_ the
clean-up. In the code below, we replace the client line (which above
was just `set 1') with something else. The stupid bad client

let f1 () = ...
	return (fun () -> set 1)
	...

is easily caught. The type checker rejects the code with the message
  This `let module' expression has type unit -> unit A.t
  In this type, the locally bound module name A escapes its scope

Alas, a bit more cunning client, as you have observed,

let f2 () = ...
	      return (fun () -> ignore (set 1); ())
	...
let test2 = f2 () ();;

manages to call the setter _after_ the clean-up. But that is not the
only cunning client. Here is another one

let f3 () = ...
	      return (object val mutable guarded = return ()
		            method call_setter = guarded <- set ()
		     end)
	...
let test3 = (f3 ())#call_setter;;

and another one

exception Foo of (unit -> unit);;
let f4 () = ...
	      return (Foo (fun () -> ignore (set 1); ()))
let test4 = try raise (f4 ()) with Foo e -> e ();;

and another one

let cunning_ref = ref (fun () -> ())
let f5 () = ...
	      cunning_ref := (fun () -> ignore (set 1); ()); return ()
	...
let test5 = f5 (); !cunning_ref ();;


To ensure security, one should prohibit returning, assigning or
throwing any values other than the values of simple types: numbers,
strings, pairs, arrays and lists of those. In short, only easily
serializable values may be returned, assigned and thrown.

I fully agree with your assessment of monads. I should remark that
type-based assurances work well for data dependencies, but not so for
control dependencies (that's why we need a so-called type-state).
Monads convert control dependency into data dependency.

You do know of FlowCaml, right? It doesn't seem to be actively
maintained though...

Re: [Caml-list] Re: Keeping local types local?

[David Rajchenbach-Teller]

On Wed, 2008-09-17 at 01:07 -0700, oleg@okmij.org wrote: 
> > So I'm looking for another way out. As far as both your examples and my
> > experiments seem to indicate, the only way of escaping scope is to
> > return a continuation which calls one of the protected functions and
> > ignores the result.
> 
> I'm afraid this is worse than it seems. Returning any closure (not
> necessarily a continuation) can defeat the security. To summarize, the
> security of the framework is defeated if

You're right, I actually meant "closure" rather than "continuation". 

> I fully agree with your assessment of monads. I should remark that
> type-based assurances work well for data dependencies, but not so for
> control dependencies (that's why we need a so-called type-state).
> Monads convert control dependency into data dependency.

"Type-state"? I'm not familiar with the term although it sounds exactly
like what I have in mind (and which I hoped to be able to emulate with
OCaml-compatible dynamic scoping, i.e. implicit arguments).

> You do know of FlowCaml, right? It doesn't seem to be actively
> maintained though...
Yes, FlowCaml is my plan C (plan A was monads).
> 
Thanks,
 David
> 
-- 
David Teller-Rajchenbach
 Security of Distributed Systems
  http://www.univ-orleans.fr/lifo/Members/David.Teller
 Angry researcher: French Universities need reforms, but the LRU act
brings liquidations.