[plt-scheme] 299.106

The exp-tagged code in CVS for MzScheme and MrEd is now version 299.106.

This version adds `only' as a `require' sub-form:

 (require (only mzscheme cons car)) ; imports only `cons' and `car'


This version also adjusts the syntax-certificate model. Ryan discovered
a way to circumvent certificate protection, and a new check is in place
to close that hole. As it turns out, this change tightened certificate
checking just enough to expose a completely different problem, which is
also now fixed. Besides closing security holes, the changes should
affect almost no one. (If you've written your own sub-expander that
uses things like `syntax-local-certifier', you may be an exception.)

At the risk of making certificates sound complicated than they are,
I've included below an explanation of what went two things wrong and
how each is fixed. I'm encouraged that both were fixed with small
adjustments to the certificate model. In any case, the experiment with
syntax certificates continues.

Matthew

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

Certificate change #1:
----------------------

Here's Ryan's exploit in terms of the example from the manual:

 (module m mzscheme
  (provide go)
  (define (unchecked-go n x) 
    ;; to avoid disaster, n must be a number
    (+ n 17))
  (define-syntax (go stx)
    (syntax-case stx ()
     [(_ x)
      #'(unchecked-go 8 x)])))

 (require m)
 (let ([estx (expand-syntax #'(go 9))])
   (syntax-case estx ()
     [(app unchecked-go eight nine)
      (eval #`(let ([app (lambda (u e n) u)])
                #,estx))]))
 => unchecked-go

The key to the exploit is that `estx' is intact in the evaluated
expression, so it keeps its certificates, but we can still extract an
`#%app' that will bind the one in `estx'. In other words, the
expression #'(unchecked-go 8 x) does not use the `#%app' that the macro
implementor intended.

The solution is to disallow a reference to a local binding if the
binding is less certified than the reference. This change ensures that
bindings around an expression cannot meaning something different than
the expression generator expected. The certificate check is sufficient
because the only way to capture an identifier introduced by a macro is
to use an identifier that was introduced at the same time, and getting
such an identifier means pulling it out of a certified context (which
decertifies the identifier).

With the new check, v299.106 produces the following error for the above
program:

 compile: reference is more certified than binding in: #%app


Certificate change #2
---------------------

Previously, a syntax constant

 (quote-syntax datum)

would receive all certificates from its lexical context. In other
words, if a `quote-syntax' expression appeared within an expression
that had some certificate, the certificate was attached (at compile
time) to the syntax constant. This propagation of certificates supports
macro-defining macros.

For example, suppose that the `go' macro above is implemented through
a macro:

 (module m mzscheme
  (provide def-go)
  (define (unchecked-go n x) 
    (+ n 17))
  (define-syntax (def-go stx)
   (syntax-case stx ()
     [(_ go)
      #'(define-syntax (go stx)
          (syntax-case stx ()
           [(_ x)
            #'(unchecked-go 8 x)]))])))

When `def-go' is used inside another module, the generated macro should
legally generate expressions that use `unchecked-go', since `def-go' in
`m' had complete control over the generated macro.

 (module n mzscheme
  (require m)
  (def-go go)
  (go 10)) ; access to \scheme{unchecked-go} is allowed

This example works because the expansion of `(def-go go)' is certified
to access protected identifiers in `m', including `unchecked-go'.
Specifically, the certified expansion is a definition of the macro
`go', which includes a syntax-object constant `unchecked-go'. Since the
enclosing macro declaration is certified, the `unchecked-go' syntax
constant gets a certificate to access protected identifiers of
`m'. Thus, `unchecked-go' in `(unchecked-go 8 10)' is certified.

This is a bit too lose with certificates, however. The problem is that
`unchecked-go' gets certified directly, instead of being certified only
within the application expression. This fact is obscured by the way
that `syntax' expands to use `quote-syntax', so to clarify how this
might happen, it's helpful to write the `def-go' macro as follows:

 (define-syntax (def-go stx)
  (syntax-case stx ()
    [(_ go)
     #'(define-syntax (go stx)
         (syntax-case stx ()
          [(_ x)
           (with-syntax ([ug (quote-syntax unchecked-go)])
             #'(ug 8 x))]))]))

In this case, `unchecked-go' is clearly quoted as an immediate syntax
object in the expansion of `(def-go go)'. If this syntax object is
given a certificate, then it would keep the certificate --- directly on
the identifier `unchecked-go' --- in the result `(unchecked-go 8 10)'.
Consequently, the `unchecked-go' identifier could be extracted and used
with its certificate intact.

The solution is to distinguish "active" certificates from "inactive"
certificates. Active certificates are used for checking certification,
while inactive certificates are attached to syntax-quoted values.
Inactive certificates become active when the macro expander certifies
the result of a macro expansion; at that time, the expander removes all
inactive certificates within the expansion result and attaches active
versions of the certificates to the overall expansion (not to the
sub-datum(s) that had the inactive certificate(s)).

Attaching an inactive certificate to `unchecked-go' and activating it
only for the complete result `(unchecked-go 8 10)' ensures that
`unchecked-go' is used only in the way intended by the implementor of
`def-go.