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.
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.
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.