Hi Holger, On Thu, Jul 13, 2006 at 08:02:29AM +0200, holger krekel wrote:
def enter_bid(n): if n > highest_bid.value: highest_bid.value = n enter_bid = secure(enter_bid)
Here the annotator analysis is supposed to prevent a leak of information from the secret value. But if the if-branch additionally contains:
num_bids += 1
don't you run into a branching/code-dependent-on-secret-condition problem again? Would the annotator prevent the manipulation of the global 'num_bids'? Would it need to be a public value?
You can't modify global values in RPython anyway. But more generally, yes, the annotator would follow all mutations and propagate security levels.
Moreover, i have practical concerns: your proposed scheme requires RPython annotator analysis which implies to have the PyPy tool chain available and accessible at programming time. Not impossible but also not a use case that we went for so far.
Well, we haven't considered much at all. This is just one approach, which we didn't think of earlier, but there are of course others.
Also it is not clear to which target "secure" would compile functions to, C or bytecode or ...?
I don't know. That's not too important for the security aspect; anything would work, maybe even to the point of not actually compiling at all but just using the annotator for the security proof (although I'd regard this as less secure somehow, given the subtle differences between RPython and full Python). A bientot, Armin