Tim, I think the board you want is the PolarFire SoC Icicl=
e board.=C2=A0 You can find them on the RISC-V Exchange website:=C2=A0
RISC-V Exchange - RISC-V Internatio=
nal (riscv.org)=C2=A0

We will be offering these as o=
ur 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.=C2=A0 But, =
I can rest assured that you're "on my list".=C2=A0 ;-)

<=
div>-Jeff--

Jeff Scheel (he/him/his)Linux Foundation, RIS=
C-V Technical Program Manager

On Mon=
, Jun 14, 2021 at 2:29 PM Tim Daly <axiomcas@gmail.com> wrote:

Program bugs won't go away until we change a few th= ings.

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.=C2=A0 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 <jeff@riscv.org> wrote:

> Thanks for the detailed explanation, Tim.=C2=A0 That's very helpfu= l.

> -Jeff

>

> --

> Jeff Scheel (he/him/his)

> Linux Foundation, RISC-V Technical Program Manager

>

>

> On Thu, Jun 10, 2021 at 7:25 PM Tim Daly <axiomcas@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<= br> >> 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),=C2=A0 (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

>>

>

In Synaptic, here is a version of Axiom that hangs when I try to use the Hyper Doc.

In Debian I get the same faulty version.

I have also many times, tried to download the program, the last one from Sourceforge and after a long time, the same result.

My very last attempt, a bin file, very fast but no results.

I also got a permission denied to an echo, etc.

*It seems that the Linux (four of them) do not have the necessary staff.

My actual Linux is:

Linux Mint 20.1 Cinnamon

It is a Debian-Ubuntu Linux that can be defined as an Ubuntu.

My request is an Axiom that works properly in Ubuntu.

Please consider *, because it is a fact.