Leakage Traces

[OwenConoly]

Adds leakage traces to the semantics.

I'm unsure whether the leakage trace semantics actually belong in this repository; maybe they should go in riscv-semantics instead. But this PR should be a fine place to discuss whether these changes belong here.

Another basic question about this PR, which I don't know the answer to: should we associate leakage with assembly instructions (as it currently is in this branch), or should we associate leakage with basic operations that the machine does? To elaborate: currently, I've modified the definition of a cycle so that, before executing each instruction, we first leak (the appropriate function of) the instruction. Alternatively, taking the 'associate leakage with basic operations' approach, we could just say that the appropriate things are leaked while the instruction is being executed. For example, we would modify the definition of the loadByte function (wherever it's defined) so that it leaks whatever address it loads.

A downside of the leak-instructions approach is that the instruction fetch locations (program counter values) aren't explicitly leaked. (Arguably this doesn't matter at all, since we do leak branches.) But we could further modify the definition of a cycle so that they are leaked.

I think Andres mentioned to me that there exists an official RISC-V specification saying what should be leaked by different instructions? If we stick with the leak-instructions approach, then I expect we could have a line-to-line-ish correspondence between our leakage spec in Haskell/Coq and the spec in English. This would be nice.

The code in this branch is a bit of a mess, and the semantics of some instructions (e.g., CSR instructions, which I am not very familiar with) are probably wrong. I figured I'd try to answer questions like "should I rewrite this in Haskell" before taking the time to clean it up.

[samuelgruetter]

I'm unsure whether the leakage trace semantics actually belong in this repository; maybe they should go in riscv-semantics instead. But this PR should be a fine place to discuss whether these changes belong here.

One could say that leakage is something you only need for reasoning, not in simulation, and that therefore it's fine to write it directly in Coq. On the other hand, if you believe that other use cases could benefit from your definitions as well, you could also write them in Haskell, but then it would be good to follow some official spec as closely as possible.

Another basic question about this PR, which I don't know the answer to: should we associate leakage with assembly instructions (as it currently is in this branch), or should we associate leakage with basic operations that the machine does? To elaborate: currently, I've modified the definition of a cycle so that, before executing each instruction, we first leak (the appropriate function of) the instruction. Alternatively, taking the 'associate leakage with basic operations' approach, we could just say that the appropriate things are leaked while the instruction is being executed. For example, we would modify the definition of the loadByte function (wherever it's defined) so that it leaks whatever address it loads.

I'm not sure if the 'associate leakage with basic operations' approach would work: There is currently no basic operation in the typeclass to record branching, and adding one that gets called in ExecuteI seems too invasive because most users of that file are not interested in leakage.

A downside of the leak-instructions approach is that the instruction fetch locations (program counter values) aren't explicitly leaked. (Arguably this doesn't matter at all, since we do leak branches.) But we could further modify the definition of a cycle so that they are leaked.

Leaking fetch addresses would make sense, imho.

I think Andres mentioned to me that there exists an official RISC-V specification saying what should be leaked by different instructions? If we stick with the leak-instructions approach, then I expect we could have a line-to-line-ish correspondence between our leakage spec in Haskell/Coq and the spec in English. This would be nice.

Would be nice indeed. (but also, don't aim for a would-be-nice that you can't finish before leaving for your next career step -- I don't know your schedule but I'd rather have your current code merged than halfway improved towards something better but unmerged)

The code in this branch is a bit of a mess, and the semantics of some instructions (e.g., CSR instructions, which I am not very familiar with) are probably wrong. I figured I'd try to answer questions like "should I rewrite this in Haskell" before taking the time to clean it up.

I'd be fine with either merging almost-as-is or with doing it in Haskell.
If you decide not do write Haskell, I'd request the following changes to the current code:

• Move the changes of Decode.v into a separate file, because that's a file automatically translated with hs-to-coq
• Cleanup, including: I'm not sure whether the additions to MetricMinimalMMIO.v are actually needed, and MetricMinimalNoMul.v/MinimalNoMul.v were deleted (moved to softmul) at some point, so you shouldn't add them back, no Print/Search etc commands

[OwenConoly]

OK, I'll stick with Coq and the leak-instructions approach, and I'll change things so that we leak fetch addresses.

Would be nice indeed.

I'll try to find some RISC-V spec saying what is leaked by instructions. Section 32.6 of this document says that instructions like or should have data-independent timing. I couldn't find anything about branches, loads, or stores, though.

[samuelgruetter]

I'll try to find some RISC-V spec saying what is leaked by instructions. Section 32.6 of this document says that instructions like or should have data-independent timing. I couldn't find anything about branches, loads, or stores, though.

This section 32.6, aka the Zkt extension, only says which instructions must be constant-time if an implementation wants to claim to comply to Zkt, but doesn't list everything that should be considered "leaked" like you'd need it for your spec. @andres-erbsen is "the Zkt extension" what you had in mind when suggesting to follow the official spec more closely, or is there something else?

[OwenConoly]

Aside from further comments y'all might have, I think this is ready to be merged.

[andres-erbsen]

This looks really good. I suggest we merge before more perfectionism kicks in.

[OwenConoly]

Merging sounds good to me, as soon as I move option_map2 to where it belongs! I’m waiting on somebody to merge mit-plv/coqutil#120 before I update this branch to import option_map2 from coqutil.

[samuelgruetter]

LGTM as well, and I agree that we're already in perfectionism territory here 😉
Regarding merging: This PR beaks bedrock2, right? So maybe it would be safer to just agree that this is what we will merge once the bedrock2 PR is also available? Just imagining a scenario where a coqdev makes a PR against riscv-coq's master and would like to get bedrock2 updated to incorporate that soon to get their coq PR done. But if you want to merge now, @andres-erbsen, and are ready to deal with such scenarios, that's fine with me as well.

[OwenConoly]

Oops, I suddenly disagree that this is about ready to merge. I have been running make without errors and thinking things are fine, but apparently I should've been running make all instead. Running make all shows that a good number of things are still broken in the Examples directory.

[OwenConoly]

Never mind, fixing Examples was not much work at all. Should be good now.

[andres-erbsen]

@samuelgruetter I am fine with holding this change until bedrock2 is ready for it.

[OwenConoly]

The bedrock2 leakage PR is about ready to be merged, so can we go ahead and merge this one?

[andres-erbsen]

ci run again

[andres-erbsen]

CI passed at https://github.com/mit-plv/bedrock2/actions/runs/12846436787/job/35951920895#step:3:111