On Mar-24, Dan Sugalski wrote:At 12:36 PM +1100 3/24/04, [EMAIL PROTECTED] wrote:On 24/03/2004, at 6:38 AM, Dan Sugalski wrote:
This is a question without a simple answer, but does Parrot provide an infrastructure so that it would be possible to have proof-carrying[1] Parrot bytecode?
In the general sense, no. The presence of eval and the dynamic nature of the languages we're looking at pretty much shoots down most of the provable bytecode work. Unfortunately.
? I'm not sure if I understand why. (Though I should warn that I did not read the referenced paper; my concept of PCC comes from reading a single CMU paper on it a couple of years ago.) My understanding of PCC is that it freely allows any arbitrarily complex code to be run, as long as you provide a machine-interpretable (and valid) proof of its safety along with it.
Clearly, eval'ing arbitrary strings cannot be proved to be safe,
It can be safe. Normally, PCC works by certifying the code during compilation, and attaching the machine-checkable certificate with the resulting compiled code (be that bytecode, machine code or whatever). During runtime, a certificate checker then validates the certificate against the provided compiled code, to assure that what the certificate says it's true.
If you eval an arbitrary string, the compile/evaluate stages are more closely linked: you effectively run the code (and thus check the certificate) immediately after compilation.
The main requirement is that Parrot permits some sort of 'hooks', so that
1. during compilation, a certificate of proof can be generated and attached with the bytecode, and
2. before evaluation of the code, a certificate checker has to validate the certificate against the code, and also that
3. Parrot's bytecode format must allow such a certificate to be stored with the bytecode.
Eval'ing a specific string *might* be provably safe, which means that we should have a way for an external (untrusted) compiler to not only produce bytecode, but also proofs of the safety of that bytecode. We'd also need, of course, the trusted PCC-equipped bytecode loader to verify the proof before executing the bytecode. (And we'd need that anyway to load in and prove the initial bytecode anyway.)
This would largely eliminate one of the main advantages of PCC, namely that the expensive construction of a proof need not be paid at runtime, only the relatively cheap proof verification.
If you are directly eval'ing an arbitrary string, then yes, you have to generate the proof when you compile that string to PBC. But you can also provide a program/subroutine/etc as PBC with a certificate already attached.
Back to reality. I understand that many of Parrot's features would be difficult to prove, but I'm not sure it's fundamentally any more difficult than most OO languages.
AFAIK (although I don't know that much :), the Java VM has been proved secure to a large extent.
-- % Andre Pang : trust.in.love.to.save
