[plt-scheme] module security, part 2'

Ignore part 2 in last month's two-part series on module security:

  http://list.cs.brown.edu/pipermail/plt-scheme/2004-August/006473.html

The problem wasn't a lack of security, but a lack of flexibility. With
the given rules, Errortrace could not provide enough information in a
stack trace to be useful.

Meanwhile, the given rules offered no real guarantee in terms of
additional security, because they could be circumvented through
bytecode. With this in mind, we changed `syntax-recertify' to move
certificates whenever someone could accomplish the same result by using
bytecode. Specifically, `syntax-recertify' now moves a certificate
given the certificate's inspector or a superior (as opposed to
accepting only a superior).

So, which messages should you believe now?

 - Part 1 on module security,
     http://list.cs.brown.edu/pipermail/plt-scheme/2004-August/006355.html
   is still fine, but below is a replacement for the ending.

 - Part 2 contained a useful bit that was not related to recertifying.
   I've revised it and included it below, too.

Matthew

----------------------------------------

Program-Processing Tools
------------------------

Program-processing tools, such as Errortrace, pull apart macro
expansions and assemble them in a different way. These
program-processing programs break in v299.13, because certificates get
lost by re-assembly.

However, Errortrace can use `syntax-recertify' to transfer an arbitrary
certificate from an old expression to one that it constructs.

Errortrace can do this as long as it is loaded while the original code
inspector is installed. Otherwise, it will trip over expansions of
MzScheme macros that introduce references to exported identifiers. More
generally, a code inspector that supports bytecode loading also
supports program processing.

Thus, Errrotrace can rearrange the expansion of, say, `send' to abuse a
private identifier from `(lib "class.ss")', but this is the same risk
as loading a bytecode that refers to `(lib "class.ss")'. Changing the
code inspector prevents anyone from abusing private identifiers in
processing a program.

Is It Really Secure?
--------------------

I don't know. Nothing that takes several messages (with corrections) to
explain is as simple as anyone would like, and there is an awful lot of
room for error. So far, though, it seems secure, and I'm optimistic.
We'll have to try it for a while longer before we can draw any
meaningful conclusions.

One source of insecurity is that MzScheme will have bugs, but I'd like
to draw out the other possible source: the new constructs might not
provide enough security, even when they work as defined.

For example, in the module

  (module m mzscheme
    (provide t)
    (define hidden 5)
    (define t 
      (syntax-rules ()
        [(_ f) (f 17)])))

the `hidden' binding is accessible because the `t' macro expands to an
application of the given `f'. The `f' provided to `t' might be a macro,
in which case it is given a `17' that has the lexical context of `m'.
Also, the result from `f' will be certified as if it came from `m',
since `t' is in `m'. Thus, `f' can use `datum->syntax-object' to get at
`hidden'.

In general, a macro must not expand to a use of another macro that it
doesn't trust. If a macro's intent is to expand to a function
application using a given function expression, the result must be
constructed to ensure that a macro identifier isn't given in place of
a function expression. For example, the above could be changed to

  (module m mzscheme
    (provide t)
    (define hidden 5)
    (define t 
      (syntax-rules ()
        [(_ f) (let ([the-func f]) (the-func 17))])))

to ensure that `hidden' stays hidden.

Fortunately, it appears that few macros place parts of their input into
application positions, or otherwise expand into uses of untrusted
macros. The only case that I can find is in the `match' macro for
patterns that use `?', and this case could be easily changed in the
same way as `t'. Another mitigating factor is that the `match' module
doesn't seem to have anything to hide, so the problem doesn't matter.
Still, there may be more cases like `match', and maybe --- just maybe
--- one of the them matters.

That's the main problem that I see, and there may well be more. Even
with these caveats, I think that MzScheme might now provide a practical
level of security for module bindings. We'll see.