Re: needing an fpga...

[Camm Maguire]

Greetings!  I take it this discussion pertains to the same platform as
Debian's 'riscv64'.  There are virtual machine images which can be run
in emulation, but I have been waiting for a porterbox to become
available to port gcl.  I anticipate the linker will just take a few
days.

Take care,

Tim Daly <axiomcas@gmail.com> writes:

> 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 <jeff@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 <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
>>> 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
>>>
>>
>
>
>
>

Jeff Scheel <jeff@riscv.org> writes:

> 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) 
>
> 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 <axiomcas@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 <jeff@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 <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
>  >> 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
>  >>
>  >
>

-- 
Camm Maguire                                        camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah