Initial support for the Scalar Cryptography Extension, v0.9.2 #80
Conversation
|
|
||
| /* | ||
| * Dummy function representing an entropy samping. | ||
| * TODO: Examine how best to support this in SAIL? |
There was a problem hiding this comment.
You'll likely need a Platform.get_random_bits for OCaml and a wrapper around getrandom for C that this then exposes.
There was a problem hiding this comment.
Is this process documented somewhere? Or is there an example in another architecture I can use as a reference? It might be a bit beyond my OCaml abilities at the moment.
For context - there is a lot of worry/discussion about how a mechanism like this gets tested, particularly for the architectural compliance tests. E.g., changing exactly what the tests check, or switching in a deterministic PRNG for testing etc.
Would it be okay to leave this as a TODO for the purposes of getting the rest of this PR merged (once I've fixed the various other issues) and coming back to it? I'll understand if not.
There was a problem hiding this comment.
Search for ocaml: in model/ to find all the existing "FFI bindings" and pick one that looks close to what you need this to do. I can see the value in determinism, but it probably should be configurable.
There was a problem hiding this comment.
Thanks for the pointer, I'll give it a whirl.
I agree it should be configurable. I expect it will end up being modified as the standardisation / compliance processes are discussed more. The aim at the moment I guess is just to get something minimally functional in there.
model/riscv_insts_crypto.sail
Outdated
| mapping clause assembly = SHA256SUM1 (rs1,rd) <-> "sha256sum1" ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) | ||
|
|
||
| val crypto_sha256 : (sha256_op, regidx, regidx) -> Retired effect {escape,rreg,wreg} | ||
| /* --- specification snippet begin --- */ |
There was a problem hiding this comment.
I'm sorry, I'm guessing at what you are asking about here. Did you mean what are these instructions for? Or why have I written the code this way? I hope the former...
These instructions are lightweight accelerators for the SHA2 hash function. They wrap up the single operand sigma0/1 and sum0/1 functions described in the SHA2 specs into a single instruction. They're explained more in section 3.3 of the draft spec.
There was a problem hiding this comment.
The specification snippet comments, not the valspecs or function definitions.
There was a problem hiding this comment.
Oh! Sorry. They make/made it easier to track which parts of the SAIL code would be in-lined into the specification. I can remove them if they're not the done thing / there is another accepted method for it.
There was a problem hiding this comment.
If you need LaTeX, sail can already produce that as output (and we use that in our CHERI ISA specification). I don't know if there's a way to extract the raw sail snippets out, but matching on ^function and the following ^} in a simple shell/awk/sed/etc script should be easy enough.
There was a problem hiding this comment.
Well, there is an ongoing issue about RISC-V documentation all being moved into asciidoc, rather than LaTeX, as the base ISA, priv ISA, crypto and Bitmanip specs currently use. So, while I hope the SAIL tooling can be used for this, it's a bit of a TBD right now.
There was a problem hiding this comment.
awk '/^function\>/{f=$2; b=1} b{print>f".sail"} /^}/{b=0}' model/riscv_insts_crypto.sail
(requires GNU awk, so will need gawk if running on *BSD) will produce a .sail file containing the source for each function, provided you keep the whitespace sane. Or you can rewrite such a trivial script in your favourite language.
The main value add of saildoc is not so much extracting source code but its ability to insert LaTeX hyperlinks everywhere and to permit the use of markdown to document functions (like doxygen/javadoc/etc); for CHERI-RISC-V, all our instruction semantics documentation is done on the associated execute function clauses (so it's there in the model and stays in sync) and then pulled into our ISA spec as LaTeX. If you want that then you'll need to use LaTeX (or use something that lets you mix LaTeX with other markups) or write a separate saildoc backend for asciidoc.
|
Also somehow you've managed to get your commit messages to include information that is normally commented-out in the generated message for your editor. |
|
Hi @jrtc27 - Thanks a lot for taking the time to review, it's much appreciated. I've replied to some of your comments just to be absolutely sure. If what I've understood is correct, I'll make those changes as add them to this PR. Many thanks, |
|
Thanks for your clarifications to everything - I'll work on this and push an update. |
|
Hi @jrtc27 About the Entropy Source specifically:
My assumption is that when the handling of non-determinism is decided upon between the crypto TG and architectural tests SIG, a switch can be added that changes the behaviour of these platform level functions, and the SAIL code won't need touching. Does that sound okay? Like I say, let me know if there's anything concerning, and thanks again for looking at all of this. Many thanks, |
|
Could you please rebase to remove the .gitignore commits from the history entirely and squash all the commits into one? |
|
Okay, done, I hope that's what you were expecting? |
|
Hi there - is there any update on this? No hurry, just making sure I have something to report at the next weekly meeting. |
|
Regarding randomness/entropy sources, as far as I know this is the first Sail ISA model that attempts to include one. Our general approach for side effects is to have external functions declared with an appropriate effect so that the tooling knows that they might do something strange, and then to implement it differently for different situations. For example, memory accesses are all done through external functions and external implementations can include simple sequential memory and complex concurrent memory models. From a quick look it seems like all you're missing here are the effect annotations, although I'm not entirely certain what the best choice of effect would be. |
|
Hi @bacam Practically, would it be possible to merge the current implementation and iterate on it? To be clear, I absolutely don't want to rush you to merge this in. If it makes more sense or is easer for you and the sail-riscv owners to think on this and fix it first, then let's do that. I'm just trying to avoid SAIL becoming a blocker for scalar crypto, because we are moving on to things like architectural compliance testing. |
Unfortunately the set of effects is fixed at the moment and the existing ones aren't ideal for this. We would like to revisit the effect system at some point, especially because some of the original uses of it have disappeared or never happened, but we don't have any concrete plans.
I think it would be OK so long as you don't intend to use the theorem prover backends of Sail in the near future. Please do put a warning in that there really should be an effect there, though. Alternatively you could put a similar effect in, perhaps |
Okay, great, that sounds like a path forward. I'll do as you say, adding the If people want to use the theorem prover backends and ignore the entropy source, then presumably they can also omit the file Thanks, |
|
Hi, I realise I misread your message slightly. I've just added warning comment to the relevant entropy source function. I hope that's okay? |
That's fine, but |
|
Ah! Yes, my mistake. Duly added. |
|
You still have a bunch of weird whitespace scattered around. Please go through and review everything to be uniform and match the current style. |
I'm sorry this is a repeated issue with this PR. I will be honest, I don't always know what one person or another means by "weird", but sure, I'll go back over and get everything as consistent as I can. Is there an actual style guide for the Sail/C/OCaml code? |
|
Thanks for all of these, it's much clearer now. Apologies for being a bit slow! |
|
Okay, I really hope that's everything. I'm getting very change blind now. Thank you for your patience. Thanks, |
| register mnoise : Mnoise | ||
|
|
||
| /* mnoise is defined in machine mode only */ | ||
| function clause ext_is_CSR_defined (0x7A9, Machine) = { |
There was a problem hiding this comment.
| function clause ext_is_CSR_defined (0x7A9, Machine) = { | |
| function clause ext_is_CSR_defined(0x7A9, Machine) = { |
is the right style. Also repeated below for mentropy and some of your other functions. The exception in the style seems to be execute, for whatever reason that one consistently does have the space (though there are a fair number of cases for other functions too... 😞).
There was a problem hiding this comment.
Okay, I think I've caught all the non-execute clause cases of this. I've left execute clauses with a space.
model/riscv_types_crypto.sail
Outdated
|
|
||
|
|
There was a problem hiding this comment.
Still a fair number of these in this file
Makefile
Outdated
| @@ -22,8 +22,12 @@ endif | |||
| SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail | |||
| SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail riscv_insts_hints.sail | |||
| SAIL_DEFAULT_INST += riscv_insts_fext.sail riscv_insts_cfext.sail | |||
| SAIL_DEFAULT_INST += riscv_insts_crypto.sail | |||
There was a problem hiding this comment.
Hm, thinking this through a bit, this probably should be named riscv_insts_zcrypto.sail or whatever your ISA string is. Do you have one proposed yet?
There was a problem hiding this comment.
Thats a good point. Yes, we are the K extension. I'll change "crypto" in the file names to kext in keeping with the others.
|
Okay, renamed and de/re-whitespaced. I've just noticed that the offical "RISC-V" org has forked riscv-sail here. I'm not privy to the organisation around that - but is my PR now open against the wrong repository? |
|
Hi there |
ben-marshall
changed the title
Previously we were always sending the fields in a fixed order, but we have to omit optional data that is not set. This refactors the logic and adds new getters for the optional data. This code will become a lot simpler once we support the -c2 backend of sail.
Homebrew on Arm-based Macs installs in /opt/homebrew, and hard-coding /opt/local was the wrong solution for MacPorts anyway. Instead, use pkg-config to query the right compiler and linker flags for gmp and zlib.
Add workaround for ubuntu 18.04 lack of pkg-config for libgmp.
This was broken by #76
I have used this locally to build using a command like: docker run -v $PWD:/sail-riscv -w /sail-riscv <docker-image> make csim Thanks to @jameyhicks in #28 for showing how. Next step is to integrate this into github workflow somehow.
This function was inconsistent in its use of arguments vs. globals. However, in all existing cases, the arguments are fed as the values of these globals, so this has no observable impacts in the current model, but hopefully prevents confusion later.
Previously we were erroneously passing the instruction's memory access to lower layers of the memory machinery. For example, a store instruction still should be attempting reads of PTEs, not stores.
- Expose "just below the periphery" functions that allow bypassing effectivePermission and instead take a Permission explicitly (as well as an AccessType, in the case of reads, to distinguish Read from Execute; for writes, just an ext_access_type that will be wrapped in Write).
Using the new riscv_mem functions to elide the Privilege level computation
It's possible that we might want to do page table walks at Privilege levels other than the default value (e.g., under the explicit direction of the instruction stream). Split translateAddr into a thin wrapper of the same name and a new translateAddr_priv that takes the Privilege as an argument.
This is required for implementing memory version support for CHERI.
Brief: - This commit adds initial support for the scalar cryptography extension to RISC-V, synced with version v0.9.2 of the draft proposals. - The riscv-crypto repository (https://github.com/riscv/riscv-crypto) contains all of the work so far on the extension. See the releases tab for the latest spec release. - The code in this commit is based off a patch maintained locally in the riscv-crypto repository under the `sail/` directory. Now that the scalar-crypto extension is nearing the freeze milestone, we are aiming to upstream our experimental work to make future engineering tasks easier for everyone involved. Details: - There are two main classes of functionality being added. The instructions and the entropy source. - The instructions all work off the general purpose registers. Instructions common to RV32 and RV64 live in `model/riscv_insts_kext.sail`. RV32 and RV64 specific instructions live in the corresponding `model/riscv_insts_kext_rv[32/64].sail` files. - There is a considerable amount of common code (which will eventually also be used by the vector crypto extension) which lives in `model/riscv_types_kext.sail`. This consists of things like SBox definitions, block cipher operations and common structs/enums. - The entropy source lives entirely within `model/riscv_kext_entropy_source.sail`. It is a CSR based interface to an Entropy Source (note this is *not* the same as a "random number generator") which can be used to _seed_ a DRBG. There is a warning noting that the platform function to get entropy is lacking a side effect at present. - Implement platform support for the entropy source. - For the C simulator, this is a wrapper around reading /dev/urandom. - For the OCaml simulator, thisis a wrapper around `Random.int`. I couldn't tell if this is suitable as a cryptographic randomness source. However, given people don't use SAIL as a virtual machine (like, say QEMU) this shouldn't be a problem. - These platform functions are what can be overridden/changed in the future when a policy for determinism and testing is settled on. Changes to be committed: modified: Makefile modified: c_emulator/riscv_platform.c modified: c_emulator/riscv_platform.h modified: c_emulator/riscv_platform_impl.c modified: c_emulator/riscv_platform_impl.h new file: model/riscv_insts_kext.sail new file: model/riscv_insts_kext_rv32.sail new file: model/riscv_insts_kext_rv64.sail new file: model/riscv_kext_entropy_source.sail modified: model/riscv_platform.sail new file: model/riscv_types_kext.sail modified: ocaml_emulator/platform.ml
On branch scalar-crypto Your branch is up-to-date with 'origin/scalar-crypto'. Changes to be committed: modified: model/riscv_insts_kext_rv64.sail Untracked files: c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/softfloat.a c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 model/riscv_insts_zbk.sail ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 z3_problems
On branch scalar-crypto Your branch is up-to-date with 'origin/scalar-crypto'. Changes to be committed: modified: model/riscv_insts_kext_rv64.sail Changes not staged for commit: modified: model/riscv_insts_kext.sail Untracked files: c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/softfloat.a c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 model/riscv_insts_zbk.sail ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 z3_problems
On branch scalar-crypto Your branch is ahead of 'origin/scalar-crypto' by 1 commit. (use "git push" to publish your local commits) Changes to be committed: modified: model/riscv_insts_kext.sail Untracked files: c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/softfloat.a c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 model/riscv_insts_zbk.sail ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 z3_problems
SHA512, AES32, SM3, SM4. Made the AES32 instrucitons more consistent / easier to understand. On branch scalar-crypto Your branch is ahead of 'origin/scalar-crypto' by 2 commits. (use "git push" to publish your local commits) Changes to be committed: modified: model/riscv_insts_kext.sail modified: model/riscv_insts_kext_rv32.sail Untracked files: c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/softfloat.a c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 model/riscv_insts_zbk.sail ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 z3_problems
Conflicts: model/riscv_types_ext.sail
|
Hello - so as you can see I have absolutely ruined my pull request by fudging up a merge and rebase from the original repository. Scalar crypto recently passed architectural review with some changes which require Sail clean up anyway. So, my plan is to close this PR and open a new, clean one with all the up to date changes. I won't close this one until I'm ready to open a new one though, just in case people come looking and wonder what's happened. I hope this makes sense and apologies for my awful git-fu. |
Brief: (PR information duplicated from commit message)
This commit adds initial support for the scalar cryptography extension to RISC-V, synced with version v0.8.1 of the draft proposals.
The riscv-crypto repository (https://github.com/riscv/riscv-crypto) contains all of the work so far on the extension. See the releases tab for the latest spec release.
The code in this commit is based off a patch maintained locally in the riscv-crypto repository under the
sail/directory. Now that the scalar-crypto extension is nearing the freeze milestone, we are aiming to upstream our experimental work to make future engineering tasks easier for everyone involved.Details:
There are two main classes of functionality being added. The instructions and the entropy source.
The instructions all work off the general purpose registers. Instructions common to RV32 and RV64 live in
model/riscv_insts_crypto.sail. RV32 and RV64 specific instructions live in the correspondingmodel/riscv_insts_crypto_rv[32/64].sailfiles.There is a considerable amount of common code (which will eventually also be used by the vector crypto extension) which lives in
model/riscv_types_crypto.sail. This consists of things like SBox definitions, block cipher operations and common structs/enums.The entropy source lives entirely within
model/riscv_crypto_entropy_source.sail. It is a CSR based interface to an Entropy Source (note this is not the same as a "random number generator") which can be used to seed a DRBG. Given the lack of SAIL support for entropy sources or randomness (to my knowledge), this is mostly a stub implementation at the moment. I expect there to be a long discussion of how best to support this going forward, particularly with regard to the architectural tests (i.e. riscv-compliance).This code has been tested using a very basic set of WiP compliance tests, also found in the riscv-crypto repository. Re-building these tests for the latest version of the riscv-compliance framework is high on the priority list for the crypto TG, and having upstream SAIL model support is part of that process. We have a PR open with the upstream Spike repository at the moment too. Our hope is to enable future development of the architectural tests using upstream versions of Spike and the SAIL model.
Additional:
I'm new to SAIL, so any and all comments/criticism and suggestions for improving this patch are very welcome. I've tried to use the existing RISC-V and ARM models as a guide, but obviously might have fallen short of best practice in places. I'm very happy iterating on this pull request until it is suitable for merging.
I wasn't entirely clear on the Makefile structure. I hope I have added all the files in the right places and order?
I'm sorry this is such an enormous PR, and so hard to review. I didn't see a better way to break it down into smaller incremental pieces, but am of course happy to help explain things as needed. I'm also happy maintaining this code (with the help of the repo owners) during the rest of the standardisation process.
The scalar cryptography extension is unique in that it borrows instructions from the Bit-manipulation extension. Since there is not yet any support for Bitmanip within
sail-riscv, I have only included instructions unique to the scalar crypto extension. As and when Bitmanip support is added, I/we can work to make sure the right instructions are available to both extensions. Details of the relevant instructions are found in the scalar crypto specification.In terms of compiler support for these new instructions - we are using an experimental patch in the riscv-crypto repository at the moment, others are working on an upstream appropriate version. For now, the experimental toolchain is usable by anyone who needs it.
Like I say, I'm sure there will be a certain amount of iteration before this can be merged. Please let me know what I can do to help or make things clearer.
Many thanks,
Ben