Leakage traces #431
Leakage traces #431
Conversation
|
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? |
There was a problem hiding this comment.
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.
Proving the appropriate relationship between Semantics.v and LeakageSemantics.v will only be trivial if we modify Semantics.v so that So, should I modify Semantics and MetricSemantics |
|
However, the Semantics- |
|
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" 🚀😂🙄 |
Sounds good!
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). |
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:
I'd probably keep IO calls though, since the nondeterminism there seems to add an interesting dimension. |
|
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 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 |
|
👍 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
force-pushed
the
leakage_traces
branch
from
bc1fcb2 to
cff166c
Compare
|
The existence of (Metric)LeakageSemantics.v implies the existence of: (Metric)LeakageLoops.v, (Metric)LeakageProgramLogic.v, (Metric)LeakageWeakestPreconditionProperties.v, and (Metric)LeakageWeakestPrecondition.v, right? |
|
Yes. At some point I may try to share more code, but for new these are just copied I think. |
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
|
|
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. |
|
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? |
|
Separate PRs sounds good to me. (There is some possibility that we will want to review them together, though.) |
OwenConoly
force-pushed
the
leakage_traces
branch
from
55105b1 to
989d21b
Compare
OwenConoly
force-pushed
the
leakage_traces
branch
from
0b8e3d6 to
bd1bc4b
Compare
OwenConoly
force-pushed
the
leakage_traces
branch
from
3e87198 to
df2698e
Compare
|
As discussed in person, this branch is in overall good shape and it seems desirable to merge it soon rather than to wait for perfection. @samuelgruetter do you have any concerns? |
| @@ -1,6 +1,6 @@ | |||
| [submodule "deps/riscv-coq"] | |||
| path = deps/riscv-coq | |||
| url = https://github.com/mit-plv/riscv-coq.git | |||
| url = https://github.com/OwenConoly/riscv-coq.git | |||
There was a problem hiding this comment.
This git-config change should not be merged, instead the relevant riscv-coq changes should be merged to its upstream.
| r0 closed binder, rn closed binder, | ||
| tr name, tr' name, mem name, mem' name, | ||
| pre at level 200, | ||
| post at level 200). |
There was a problem hiding this comment.
@OwenConoly There are some leakage-fnspec notations here; should I interpret you talking about the lack of such notations as a signal that the ones here don't work? If so, probably best to remove.
There was a problem hiding this comment.
Yes, I believe they did not work. But now I think I have fixed them.
There are now two notations in LeakageWeakestPrecondition. There is the fnspec! notation, which is just like the fnspec! in WeakestPrecondition.
There is also the fnspec_ex! notation, which is just like fnspec! except that an existential quantifier has been inserted in the appropriate place for stating that a program is constant-time. Do you like this notation? There are now many examples of it being used in bedrock2Examples/ct.v.
There was a problem hiding this comment.
Hmm, they sure seem better than no notation. How about fnspec! exists f ... g, "getline" x y z ~> v, { ...? I believe "exists" is already a keyword, and perhaps this way a user familiar with fnspec! will guess the meaning of the new notation correctly more often.
There was a problem hiding this comment.
That seems nice and intuitive. I changed the notations to look like that instead.
| @@ -0,0 +1,452 @@ | |||
| Require Import Coq.ZArith.ZArith coqutil.Z.div_mod_to_equations. | |||
compiler/src/compiler/Pipeline.v
Outdated
| Call(pick_sp: list Leakage -> word)(p: Program)(s: Settings)(funcname: string) | ||
| (k: list Leakage)(t: trace)(m: mem)(argvals: list word)(mc: MetricLog) | ||
| (post: list Leakage -> trace -> mem -> list word -> MetricLog -> Prop): Prop; | ||
| WeakenCall: forall pick_sp p s funcname k t m mc argvals (post1: _ -> _ -> _ -> _ -> _ -> Prop), |
There was a problem hiding this comment.
@samuelgruetter do properties of Call belong here?
There was a problem hiding this comment.
@samuelgruetter do properties of Call belong here?
They don't. This is a record that's supposed to contain only "data", no proofs. But what happens if we just delete this WeakenCall field here? Then compose_phases doesn't work any more, because it needs L3.(WeakenCall). And why does compose_phases, which did not need weakening, now suddenly need weakening? My guess is that it's because you introduced a language-dependent argument to post (namely Leakage, which can be instantiated differently for each language), which is against the design that I had in mind for the phase composition (see chapter 3.5 of my thesis): The idea is that before composing the phases, you identify a common state data type over which to write the postconditions, and it's the responsibility of each Call definition to transform from the language-specific format into the common state datatype. So I'd expect that if you remove WeakenCall and Leakage from the record, and replace Leakage by some CommonLeakage, it should all work.
There was a problem hiding this comment.
The reason I had used WeakenCall where it was not needed before is that I had adopted a default behaviour of axiom-avoidance. There is a choice between carrying around WeakenCall and using functional/propositional extensionality. I've just noticed that the previous version of compose_phases (before I touched it) used functional/propositional extensionality, so I assume that's the way to go here, and I've updated the compose_phases proof to use axioms instead of WeakenCall.
Keeping the Leakage parameter around works fine. I could still replace this by some CommonLeakage, but it would be kind of ugly: CommonLeakage would just have to be the union/sum of the two different types of Leakage.
| rewrite app_nil_r. reflexivity. } | ||
| Qed.*) | ||
|
|
||
| Check (@compiler_correct_wp _ _ Words32Naive.word mem _ ext_spec _ _ _ ext_spec_ok _ _ _ _ _ word_ok _ _ RV32I _ compile_ext_call leak_ext_call compile_ext_call_correct compile_ext_call_length fs_swap instrs_swap finfo_swap req_stack_size_swap fname_swap _ _ _ _). |
There was a problem hiding this comment.
Either remove this or turn it into a lemma.
compiler/src/compiler/Pipeline.v
Outdated
| Check @MetricLeakageSemantics.exec. Print mem. | ||
| Check locals_based_call_spec_weaken. Print env. | ||
| Print string_keyed_map. |
There was a problem hiding this comment.
(nitpick: please clean up all such output before asking to merge)
compiler/src/compiler/Pipeline.v
Outdated
| Call(pick_sp: list Leakage -> word)(p: Program)(s: Settings)(funcname: string) | ||
| (k: list Leakage)(t: trace)(m: mem)(argvals: list word)(mc: MetricLog) | ||
| (post: list Leakage -> trace -> mem -> list word -> MetricLog -> Prop): Prop; | ||
| WeakenCall: forall pick_sp p s funcname k t m mc argvals (post1: _ -> _ -> _ -> _ -> _ -> Prop), |
There was a problem hiding this comment.
@samuelgruetter do properties of Call belong here?
They don't. This is a record that's supposed to contain only "data", no proofs. But what happens if we just delete this WeakenCall field here? Then compose_phases doesn't work any more, because it needs L3.(WeakenCall). And why does compose_phases, which did not need weakening, now suddenly need weakening? My guess is that it's because you introduced a language-dependent argument to post (namely Leakage, which can be instantiated differently for each language), which is against the design that I had in mind for the phase composition (see chapter 3.5 of my thesis): The idea is that before composing the phases, you identify a common state data type over which to write the postconditions, and it's the responsibility of each Call definition to transform from the language-specific format into the common state datatype. So I'd expect that if you remove WeakenCall and Leakage from the record, and replace Leakage by some CommonLeakage, it should all work.
Co-authored-by: Andres Erbsen <[email protected]>
OwenConoly
force-pushed
the
leakage_traces
branch
from
0252627 to
21d12fa
Compare
apparently SPI will be a bit of work
SPI was easy to fix once straightline worked properly
fancy new notations!)
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.