From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.2 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id F0960BBAF for ; Tue, 16 Sep 2008 18:47:20 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoICAON/z0jAXQIniGdsb2JhbACTCwEBAQ8gpiaBZw X-IronPort-AV: E=Sophos;i="4.32,409,1217800800"; d="scan'208";a="15010232" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 16 Sep 2008 18:47:03 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m8GGl3U7017049 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Tue, 16 Sep 2008 18:47:03 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgoDAON/z0jCpx6vamdsb2JhbACTCw0FCAYSpiaBZw X-IronPort-AV: E=Sophos;i="4.32,409,1217800800"; d="scan'208";a="17010998" Received: from smtpka.univ-orleans.fr (HELO ka.univ-orleans.fr) ([194.167.30.175]) by mail3-smtp-sop.national.inria.fr with ESMTP; 16 Sep 2008 18:47:02 +0200 Received: from smtps.univ-orleans.fr (localhost [127.0.0.1]) by ka.univ-orleans.fr (Postfix) with ESMTP id 5E24412AD4C; Tue, 16 Sep 2008 18:47:02 +0200 (CEST) Received: from [192.168.0.12] (ras75-4-82-235-58-110.fbx.proxad.net [82.235.58.110]) by smtps.univ-orleans.fr (Postfix) with ESMTP id F3B9336E60; Tue, 16 Sep 2008 18:47:04 +0200 (CEST) Subject: Re: Keeping local types local? From: David Rajchenbach-Teller To: oleg@okmij.org Cc: caml-list@inria.fr In-Reply-To: <20080916101241.E4E51AE53@Adric.metnet.fnmoc.navy.mil> References: <20080916101241.E4E51AE53@Adric.metnet.fnmoc.navy.mil> Content-Type: text/plain Date: Tue, 16 Sep 2008 18:47:02 +0200 Message-Id: <1221583622.6350.178.camel@Blefuscu> Mime-Version: 1.0 X-Mailer: Evolution 2.12.1 Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 48CFE307.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ens-lyon:01 ocaml:01 restrictive:01 rewriting:01 staged:01 compilation:01 monads:01 monads:01 rewriting:01 transformers:01 escapes:01 camlp:01 ocaml:01 cheers:01 oleg:01 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.