Tim, I think the board you want is the PolarFire SoC Icicle board. You can find them on the RISC-V Exchange website: RISC-V Exchange - RISC-V International (riscv.org) <https://riscv.org/exchange/>
We will be offering these as our next round of boards that go out. Your project is a great one so it's simply a matter of when, not if I'll get a board for you. But, I can rest assured that you're "on my list". ;-) -Jeff -- Jeff Scheel (he/him/his) Linux Foundation, RISC-V Technical Program Manager On Mon, Jun 14, 2021 at 2:29 PM Tim Daly <axiom...@gmail.com> wrote: > Program bugs won't go away until we change a few things. > > There is a 25 year old effort in proof technology but it is > divorced from the lower layers. > > Since Axiom is a collection of mathematical algorithms > it, unlike other software, is well specified. That makes it > ideal for proof technology. It is also well-factored so the > various definitions and axioms in proofs can be built up > in an orderly manner. > > Compilers and operating systems lie between the code > and the metal so what the compiler outputs might still > fail by violating the proof. > > Ideally the proof would be carried down to the metal > and checked by a proof checker so that even if the > compiler failed, due to perhaps an optimization, the > failure would be caught during execution before it > got too damaging. > > Proofs also ensure that various "standard" attacks > like buffer over-runs can't exist. > > Schools like CMU are teaching proof techniques in > their CS classes so the next generation will be well > aware of when, how, and why to use them. > > The gap is between the software and the hardware. > I'm doing research to cross that gap. That's where > RISC-V and FPGAs come into play. It allows proofs > "down to the metal". > > RISC-V allows me to extend the instruction set to > support proofs and FPGA interactions. I can > run RISC-V in both hard core (for the code) and > soft-core (for the FPGA) so I'm able to have a common > Instruction Set Architecture that "knows" about proofs. > > FPGAs allow me to have a hardware implementation > of proof technology that can't be manipulated by an > attacker. It also allows the proofs to be checked in > parallel with the execution so there is minimal impact > on performance but still have high assurance code. > > There is still a long way to go. I have to implement > the proof checker in the FPGA, for example. I have > to figure out what the extended ISA needs to be to > "cross-talk" from the hard IP to the soft IP, etc. > > If I'm not chosen for one of the free FPGAs, at least > let me know when they are generally available. > > Tim > > > > On 6/14/21, Jeff Scheel <j...@riscv.org> wrote: > > Thanks for the detailed explanation, Tim. That's very helpful. > > -Jeff > > > > -- > > Jeff Scheel (he/him/his) > > Linux Foundation, RISC-V Technical Program Manager > > > > > > On Thu, Jun 10, 2021 at 7:25 PM Tim Daly <axiom...@gmail.com> wrote: > > > >> I'm the lead developer on Axiom, a computer algebra system. > >> https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system) > >> > >> The current effort involves proving mathematical algorithms > >> "down to the metal". The "metal" target is an FPGA. The > >> proof system is LEAN (open source from Microsoft): > >> https://leanprover.github.io/ > >> > >> The basic idea is to develop a proof of an algorithm. > >> Once a proof exists there is a "proof checker" that can > >> check the proof. It is much easier than creating the proof. > >> > >> Next, the algorithm and the proof are packaged together > >> in the ELF (aka proof-carrying code). The bundle is wrapped > >> in AES to ensure integrity. > >> > >> When the algorithm is run in the CPU, the proof is > >> side-loaded into the FPGA. While the algorithm runs > >> the proof checker algorithm checks the proof. > >> > >> State information from the proofs of algorithms in the > >> program get "flowed" thru the execution so that the > >> whole program is proof-checked. > >> > >> The current effort is focused on several things: (1) creating > >> a soft core RISC-V process (it needs to be a verified soft > >> core), (2) implementing the proof checker in RISC-V, > >> (3) figuring out how to communicate between the main > >> CPU and the RISC-V soft core, and (4) figuring out how > >> to side-load the proof to run in parallel. > >> > >> The proof instructions implementing things like side-load > >> and communication are currently expected to be an > >> extended RISCV instruction set. > >> > >> I have the open source tool chain set up. I've been learning > >> how to use them on an icebreaker fpga. The icebreaker is > >> too small for the whole task but I can construct pieces in > >> verilog for test purposes. > >> > >> Tim Daly > >> http://axiom-developer.org/~daly > >> > > >
