search

panrg / path-properties

A Vocabulary of Path Properties
Other
1 stars 3 forks source link

Extend transparency definition to discuss evaluation of the property #57

Closed cyrill-k closed 3 years ago

cyrill-k commented 3 years ago

This pull request extends the definition of the transparency property based on the discussion mentioned in #25.

My own opinion on this PR:

So, I would suggest to merge it but I'm also fine with leaving out the implementation details.

renghardt commented 3 years ago

I agree it's useful here to have the definition a bit more formalized. Having read up on what a "taint analysis" is, it seems a little odd to me to apply this concept to Transparency in this document, as the (meta-)information M is not really the same as "insecure user input". But if it helps others understand the property, I'm all for it.

I have to admit I don't understand this part of Richard's comment though:

In your original doc (e.g., IP vs NAT example), it is the no-taint requirement, in that the function f does not access the metric. In PL/security, it is no taint.

Isn't this one and the same thing, i.e., "no-taint" vs "no taint" in both parts of the sentence? Or is the difference that, with the updated definition, it doesn't matter if the node actually accesses M, as long as the result of f doesn't change?

cyrill-k commented 3 years ago

Isn't this one and the same thing, i.e., "no-taint" vs "no taint" in both parts of the sentence? Or is the difference that, with the updated definition, it doesn't matter if the node actually accesses M, as long as the result of f doesn't change?

I'm also not 100% sure what he meant but I think it is the same and he just wanted to say that this is called no taint requirement in the context of PL/security...

I think the difference is meant with regards to my suggestion in the chat of having a constant function to model transparency.