[nv-vn]

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]

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]

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