5 ms·

I find the explanation for the sequencing rule rather unsatisfying. Why shouldn't the following be true? b : lb d : ld -----------------------

by nv-vn 5y ago

I find the explanation for the sequencing rule rather unsatisfying. Why shouldn't the following be true? b : lb d : ld ------------------------------- a := b :>> c := d : max lb ld Otherwise, it seems like you could leak info by just assigning two variables, where one is always public. E.g. x = user.firstName; y = random() would be "safe." (It's very likely that I'm missing something here)

mathetic 5y ago
Let's say we have `a, b, d : 0` and `c : 999`. Then `a := b :>> c := d` according to your rule is well-typed and has a security level `999`. Now let's say I have a conditional expression `private : 999`. The following program typechecks according to the rest of the restrictions. In particular, `999` from `private` is less than or equal to the `999` from the sequenced command. ITE private $ a := b :>> c := d But we just leaked data because if the value of `a` (which we can observe) is not `b`, then we know that `private` was 0 (aka. false). This should never happen because `a` is public and `private` is private. The intuition here is that the lower the security level a command has the more public the conditional has to be. Otherwise, private data would *influence* public data which we can then observe to deduce something about the private data. > it seems like you could leak info by just assigning two variables, where one is always public. I didn't quite follow this bit. But if you elaborate, I'm happy to discuss.
- nv-vn 5y ago
  I think maybe the key idea I was missing here is that the type of a variable is not always the same as the type of the scope it was defined in? If I'm understanding correctly, there's an implicit rule that's missing: a : la b : lb a := b -------------------------- a : lb So for example if `b : lb`: a := b :>> doSomething() need not have a type `>= lb`. Does that sound vaguely correct? Btw thanks for clarifying

by nv-vn 5y ago

mathetic 5y ago

Let's say we have `a, b, d : 0` and `c : 999`. Then `a := b :>> c := d` according to your rule is well-typed and has a security level `999`. Now let's say I have a conditional expression `private : 999`. The following program typechecks according to the rest of the restrictions. In particular, `999` from `private` is less than or equal to the `999` from the sequenced command. ITE private $ a := b :>> c := d But we just leaked data because if the value of `a` (which we can observe) is not `b`, then we know that `private` was 0 (aka. false). This should never happen because `a` is public and `private` is private. The intuition here is that the lower the security level a command has the more public the conditional has to be. Otherwise, private data would *influence* public data which we can then observe to deduce something about the private data. > it seems like you could leak info by just assigning two variables, where one is always public. I didn't quite follow this bit. But if you elaborate, I'm happy to discuss.

nv-vn 5y ago
I think maybe the key idea I was missing here is that the type of a variable is not always the same as the type of the scope it was defined in? If I'm understanding correctly, there's an implicit rule that's missing: a : la b : lb a := b -------------------------- a : lb So for example if `b : lb`: a := b :>> doSomething() need not have a type `>= lb`. Does that sound vaguely correct? Btw thanks for clarifying