[plt-dev] certificates, #%module-begin, and typed-scheme's soundness

On Wed, Dec 16, 2009 at 6:46 PM, Jon Rafkind <rafkind at cs.utah.edu> wrote:
> On 12/16/2009 04:37 PM, Sam TH wrote:
>>
>> On Wed, Dec 16, 2009 at 6:05 PM, Carl Eastlund<carl.eastlund at gmail.com>
>>  wrote:
>>
>>>
>>> On Wed, Dec 16, 2009 at 5:19 PM, Sam TH<samth at ccs.neu.edu>  wrote:
>>>
>>>>
>>>> The program at the end of this message behaves in arbitrary ways.  In
>>>> particular, it segfaults on my system.  However, this should be safe:
>>>> Typed Scheme is checking that only vectors are passed to `f'.  But the
>>>> `cheater' macro uses `local-expand' to extract a reference to `f', and
>>>> use it in arbitrary ways.
>>>>
>>>
>>> You provided 'f'.  Certificates do not protect identifiers that are
>>> provided from the module that defines them.
>>>
>>
>> As Jay points out, I didn't really provide `f'.  I provided a
>> rename-transformer that points to `f'.  Here's a more explicit version
>> of the original module:
>>
>> (module m typed/scheme
>>   (require scheme/unsafe/ops (for-syntax scheme/base))
>>   (: f ((Vectorof (U)) ->  Any))
>>   (define (f x) (unsafe-vector-length x))
>>   (define-syntax f*
>>     (make-rename-transformer #'f))
>>   (provide (rename-out [f* f])))
>>
>> This suggests to me that this is a bug in the interaction of
>> rename-transformers and certificates.
>>
>>
>
> I don't have an answer, but it seems to me that since you are providing
> *something* that the thing you provided can be inspected by destructing the
> syntax. Whether the syntax-case gets the original f or f* won't the result
> be the same? (the result being applying the function `f' to 3).

This is exactly what the certificate system should prevent -
destructuring the syntax.

> Or are you saying that since `f' was not provided that
> `make-rename-transformer' should not certify access to the syntax being
> renamed?

Exactly.

-- 
sam th
samth at ccs.neu.edu