Leakage traces

[OwenConoly]

This PR will add leakage traces to the source and intermediate semantics, augment the compiler-correctness statement and proof to talk about leakage traces, and add some examples involving leakage traces.

[OwenConoly]

For now, this branch only has some edits to Semantics.v. Before I add anything else, I wanted to ask whether I should be making these edits (i.e., adding leakage traces) in Semantics.v, MetricSemantics.v, or both? Also, why are Semantics.v and MetricSemantics.v separate, and are there plans to merge them eventually?

[andres-erbsen]

Semantics.v, MetricSemantics.v, or both?

IMO the best option is to create additional semantics files. We want to have only one compiler proof, so that would use LeakageMetricSemantics. Some program proofs may be done with that one as well, but the examples for our current manuscript probably shouldn't be, so there we'd probably want want LeakageSemantics as well. In an unverified software project, this kind of duplication would be asking for inconsistency bugs, but I hope it won't be too hard to state and prove the appropriate relationships between these variants.

[OwenConoly]

I hope it won't be too hard to state and prove the appropriate relationships between these variants.

Proving the appropriate relationship between Semantics.v and LeakageSemantics.v will only be trivial if we modify Semantics.v so that exec takes the pick_sp parameter. If LeakageSemantics exec takes pick_sp as a parameter but Semantics exec stays as is, then proving any sort of equivalence between them is equally as nontrivial as that semantics-equivalence statement we put in the paper, the one that I wrote a ~3000-line proof of.

So, should I modify Semantics and MetricSemantics execs to take pick_sp as a parameter, and then prove the appropriate relationships between Semantics vs. MetricLeakageSemantics, MetricSemantics vs. MetricLeakageSemantics, and LeakageSemantics vs MetricLeakageSemantics?

[OwenConoly]

However, the Semantics-exec-implies-LeakageSemantics-exec direction is trivial even if LeakageSemantics takes pick_sp as a parameter and Semantics doesn't. So if that direction of the equivalence is all we care about, then potentially I could just leave Semantics and MetricSemantics alone.

[andres-erbsen]

Ah, indeed. I was only thinking of the easy direction, Semantics implies LeakageSemantics. I don't think we should add pick_sp to current semantics. @samuelgruetter do you think it would be acceptable to carry both copies in the repo, but only the half of the equivalence proof that allows program proofs without leakage to be used with a compiler proof that preserves everything they say about leakage?

However, the other direction of this relationship might be a good opportunity to drill down on the difficulty in the equivalence proof and perhaps simplify it. We don't have to do this, but I'm thinking that if you could state the desired equivalence with a minimized version of semantics that is just complicated enough to illustrate the challenge (without abstract traces, predictors, or even function calls and etc), then I would give it a try. "How hard can pushing a quantifier into an inductive be" 🚀😂🙄

[samuelgruetter]

Ah, indeed. I was only thinking of the easy direction, Semantics implies LeakageSemantics. I don't think we should add pick_sp to current semantics. @samuelgruetter do you think it would be acceptable to carry both copies in the repo, but only the half of the equivalence proof that allows program proofs without leakage to be used with a compiler proof that preserves everything they say about leakage?

Sounds good!

However, the other direction of this relationship might be a good opportunity to drill down on the difficulty in the equivalence proof and perhaps simplify it. We don't have to do this, but I'm thinking that if you could state the desired equivalence with a minimized version of semantics that is just complicated enough to illustrate the challenge (without abstract traces, predictors, or even function calls and etc), then I would give it a try "How hard can pushing a quantifier into an inductive be" 🚀😂🙄

This kind of proof would be interesting as a minimal standalone file that might accompany a paper as "supplemental material", where the focus is really to make it as simple as possible, but without simplifying away the core difficulty. (And if at some point, we actually need this direction of the equivalence for real, we can again scale it up to the whole language).

[OwenConoly]

"How hard can pushing a quantifier into an inductive be"

This could be nice, yeah! To make it as academic as possible (and remove the coqutil/bedrock2 dependency and get a standalone file) I'd probably make the following simplifications to the equivalence proof I currently have:

• no memory, only locals
• no leakage traces or metrics either
• locals are nats instead of words (in addition to removing a dependency, this makes me happy because proofs seem less trivial when they're written about Turing-complete languages)
• no ifs, since you can write them with whiles anyway
• instead of stack allocation, the quantifier is just an RNG construct
• no function calls

I'd probably keep IO calls though, since the nondeterminism there seems to add an interesting dimension.

[OwenConoly]

Oh, bedrock2 is Turing-complete! I forgot that you can store and retrieve as much information as you want in the IO trace (with an appropriate choice of ext_spec). That's kinda cool.

I had thought that it was just a finite-state machine, so in principle, you could prove some absolute upper bound (depending only on word size and source program) on the size of an exec proof tree (and then this sort of equivalence theorem becomes trivial).

[andres-erbsen]

👍 You can store a turing-machine tape in a nat, so I think all options here are turing-complete. And I'd even remove I/O at first, we can add it back later if we want.

[OwenConoly]

The existence of (Metric)LeakageSemantics.v implies the existence of:

(Metric)LeakageLoops.v, (Metric)LeakageProgramLogic.v, (Metric)LeakageWeakestPreconditionProperties.v, and (Metric)LeakageWeakestPrecondition.v,

right?

[andres-erbsen]

Yes. At some point I may try to share more code, but for new these are just copied I think.

[samuelgruetter]

The existence of (Metric)LeakageSemantics.v implies the existence of:

(Metric)LeakageLoops.v, (Metric)LeakageProgramLogic.v, (Metric)LeakageWeakestPreconditionProperties.v, and (Metric)LeakageWeakestPrecondition.v,

right?

Will we ever need a program logic that does both metrics and leakage at the same time? If not, the needed files should probably just be

• MetricLeakageSemantics.v (because in the compiler, we want both at the same time)
• (non-metric) LeakageLoops.v, LeakageProgramLogic.v, LeakageWeakestPreconditionProperties.v, and LeakageWeakestPrecondition.v

[andres-erbsen]

I don't have specific code planned where this would be needed, but I imagine basic library functions like memset could end up being used by callers that need either kind of spec. I'm fine with procrastinating on building support for this, though.

[OwenConoly]

Ok. I can just do the MetricLeakage files while I'm at it, if they'll be needed eventually anyway. (Probably I'll end up making some errors in MetricLeakageProgramLogic, since there won't be any test cases for it.)

Unrelatedly, since I am adding the separate files for Leakage stuff instead of changing what was already there, my changes to the source language shouldn't break the compiler proof. So it seems natural to split this PR into two: in this PR I can just change the source language and add some examples, and then I can make a separate PR for compiler proof things. Does that sound good?

[andres-erbsen]

Separate PRs sounds good to me. (There is some possibility that we will want to review them together, though.)