Re: Safety and security

[James Mastros]

[EMAIL PROTECTED] wrote:
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.
Oh.  In that case, the fact that it's "proof carrying" is just a 
particular case of signed code.  I think that's a solved problem in 
parrot, at least from a design-of-bytecode perspective.  It may have 
become unsolved recently, though.

I thought proof-carrying code contained a proof, not a certificate. 
(The difference is that a proof is verifiably true -- that is, it's 
givens match reality, and each step is valid.  OTOH, a certificate is 
something that we have to use judgment to decide of we want to trust or 
not.)

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.
I think we're done with step 3, but not 1 and 2.

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.
Note that in the common case, there are no eval STRINGs (at runtime), 
and thus all you have to do is prove that you don't eval STRING, which 
should be a much easier proposition.

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.
I suspect most code that wants to be provable will attempt to prove that 
it does not use those features, rather then prove that it uses them safely.

(As pointed out in a deleted bit of the grandparent post, this may 
consist of proving that it has a bit set in the header that says that it 
shouldn't be allowed to eval string, which is easy to prove, since it's 
a verifiable given.)

	-=- James Mastros