Re: Keeping local types local?

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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs