Re: needing an fpga...

[Tim Daly]

Camm,

Greetings, as you say...

That would save me a lot of effort. At the moment I've been
targeting FORTH because I have a verilog implementation.

I'm hoping for a "Lisp all the way to the metal". That way I can
move freely between Axiom's SANE implementation, to the RISC-V
hard processor and the soft processor running on the FPGA. Coding
the proof checker in a primitive lisp that compiles directly to RISC-V
would be sweet.

The lower level Lisps only need to be enough to support the
compiled forms, such as goto, rather than full lisp with macros.
Essentially it only needs to support a thin layer over the RISC-V
instruction set.

I hadn't thought of it until now but I'm expecting to develop a
special set of extended instructions for RISC-V (an "L" extension?)
that will support the "side-loading" of proofs into the FPGA from
the main CPU. It might be interesting to think about having some
of those instructions support primitive Lisp operations, such as
CONS, CAR, CDR, etc.

I've never heard of porterbox before. I'll have to look at it.

Hope you and the family are well.

Tim

On 6/17/21, Camm Maguire <camm@maguirefamily.org> wrote:
> 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
>