Restrictions on side-effectful functions
Sandro Magi
wanted to make a suggestion for future consideration: side-effectful
functions should be encapsulated by closures which must be explicitly
passed to any code that wishes to make use of them.
For instance:
read_line : () ~> (variant)
write_line : (A:any) ~> (A)
would not be global functions invokable anywhere, but are only
invokable in the entry "main ()" function.
Why is this useful? It eliminates *ambient* authority/side-effects.
This aids in auditing as the authority-bearing code (only effectful
functions), are centralized in "main", and all possible side-effects
flow from there. This is the "powerbox" pattern (Taming OCaml:
http://www.hpl.hp.com/techreports/2006/HPL-2006-116.pdf#search=%22%22powerbox%22%20pattern%22).
Any code which wishes to perform I/O, would then have to be passed
read and/or write closures on an underlying stream type. This may seem
like a pain, but at least then you know exactly what authorities
you're passing around, and what external side-effects a function may
have, and functions which are not given these authorities are
automatically "clean".
This approach also dramatically increases flexibility, as
read_line/write_line could then be implemented over any underlying
stream type (console, network, file, etc.), or could implement
logging, filtering, etc. on the data, so it's just a good abstraction
anyway. :-)
Sandro
Christopher Diggins
> This aids in auditing as the authority-bearing code (only effectful
> functions), are centralized in "main", and all possible side-effects
> flow from there. This is the "powerbox" pattern (Taming OCaml:
> http://www.hpl.hp.com/techreports/2006/HPL-2006-116.pdf#search=%22%22powerbox%22%20pattern%22).
>
> Any code which wishes to perform I/O, would then have to be passed
> read and/or write closures on an underlying stream type. This may seem
> like a pain, but at least then you know exactly what authorities
> you're passing around, and what external side-effects a function may
> have, and functions which are not given these authorities are
> automatically "clean".
>
> This approach also dramatically increases flexibility, as
> read_line/write_line could then be implemented over any underlying
> stream type (console, network, file, etc.), or could implement
> logging, filtering, etc. on the data, so it's just a good abstraction
> anyway. :-)
Sorry for the long delay in responding to this post. This sounds like a
very good programming pattern, but a somewhat draconian rule for a
language to enforce (unless it is specifically concerned with authority
bearing code). I think this kind of rule would be too strict for the
general purpose version of Cat to enforce at the top level. I believe
there needs to be some degree of flexibility given to the programmer.
Perhaps a good compromise is to formally identify programs which do
model this pattern as being "clean" and offer tools and utitilites for
identifying and rewriting to this form. I believe this might be a nice
compromise to enforcing the rule under all circumstances.
Any thoughts on this?
Christopher Diggins
Sandro Magi
>
> Sorry for the long delay in responding to this post. This sounds like a
> very good programming pattern, but a somewhat draconian rule for a
> language to enforce (unless it is specifically concerned with authority
> bearing code).
Unfortunately, every language eventually becomes concerned with
authority bearing code, and it's much harder to retrofit security than
it is to leave out the insecure elements in the first place.
What do you find draconian about it precisely? I think the more you
ponder it, the more you'll realize that this design integrates
security more cleanly into the language than any other method you
could ever devise on your own. Quite a few other languages are using
this approach to good effect.
> I think this kind of rule would be too strict for the
> general purpose version of Cat to enforce at the top level.
If by "toplevel" you mean the interactive interpreter loop, then I
agree, as the interactive is not really where serious development
occurs. I was concerned more for when Cat eventually supported
separate compilation from files, or dynamically loaded modules.
> I believe there needs to be some degree of flexibility given to the programmer.
>
> Perhaps a good compromise is to formally identify programs which do
> model this pattern as being "clean" and offer tools and utitilites for
> identifying and rewriting to this form. I believe this might be a nice
> compromise to enforcing the rule under all circumstances.
While it sounds nice, I think it would be a bad idea: the secure
design might seem painful at first, but it "encourages" the programmer
to create smaller functions in order to pass around fewer parameters.
This makes functions more fine-grained, easier to audit, and easier to
reuse; it's just good design.
The fact that this design makes it hard to pass around numerous,
coarse-grained authorities is a good thing. Automating the conversion
means there's no disincentive to passing 100 different authorities to
a large unwieldy function which if compromised, would expose 100
authorities instead of the 1 or 2 the developer would have passed in
manually.
In our discussion on Lambda The Ultimate
(http://lambda-the-ultimate.org/node/1847#comment-22632), I've pointed
out a number of papers. Perhaps the most relevant to Cat are:
1. "How Emily Tamed the Caml", or defining a capability-secure subset of OCaml:
http://www.hpl.hp.com/techreports/2006/HPL-2006-116.html
2. The rationale that convinced the python devs to make python
capability-secure:
http://svn.python.org/view/python/branches/bcannon-sandboxing/securing_python.txt?rev=50717&view=log
Oz-E, the effort to secure the multi-paradigm language Oz, might also
interest you: http://www.info.ucl.ac.be/~pvr/oze.pdf. This one is not
in the list of links on LTU.
Sandro
Christopher Diggins
> http://www.hpl.hp.com/techreports/2006/HPL-2006-116.html
>
> 2. The rationale that convinced the python devs to make python
> capability-secure:
> http://svn.python.org/view/python/branches/bcannon-sandboxing/securing_python.txt?rev=50717&view=log
Thank you very much for sharing this information and links with me.
Christopher