[cap-talk] "Package-scoped" Confused Deputy in OCaml (was Re: Toby's Confused deputy statement)

[Sandro Magi]

Karp, Alan H wrote:
> To do that we need to identify the patterns that lead to amplification.  We have unsealers (and decryption by analogy) for the explicit case.  For the implicit case, we have the Java mixed scoping example and the firewall crossing example.  I believe Jed's Horton example falls into the latter category.  Sandro also pointed out an issue with modules in languages like ML that my reply showed I don't understand. 

Took me a bit to brush off the OCaml skills, but here's the equivalent 
of the package scoping "confused deputy" in OCaml:

(* Bob's signature: this hides the Confused.O.write function from
  * external clients.
  *)
module type Bob =
sig
  module O :
  sig
   type t
   val read : t -> string
   val make : unit -> t
  end

  module B :
  sig
   type t
   val make : O.t -> t
   val compile : t -> string -> O.t -> unit
  end
end;;

(* provides both O and B which can both see each other's full
  * definition.
  *)
module Confused : Bob =
struct
  module O =
  struct
   type t = out_channel
   let make u = stdout
   let read x = "dummy string"
   let write x s = output_string x s
  end

  module B =
  struct
   type t = O.t
   let make x = x
   let compile log source output =
    O.write log "compiling log"; (* can access O's write function *)
    O.write output "writing cc output"
  end
end;;

(* corresponds to Alan's Alice class *)
# let o = Confused.O.make () in
   let b = Confused.B.make o in
     Confused.B.compile b "foo" o;;
compiling logwriting cc output- : unit = ()


If you type this into OCaml's REPL, the output is displayed on that last 
line. I don't think this module structure is too common, but the style 
is very natural and the mistake is easy to make.

My suggestion in an earlier reply was to restrict even O and B from 
seeing each other's implementation. Most would consider this approach 
overly-aggressive, as modules that are not explicitly sealed by a 
signature have a default signature generated from the definition which 
exposes all internals, but Alan's example shows that the aggressiveness 
just might be warranted.

Sandro