[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: needing an fpga...
From: |
Camm Maguire |
Subject: |
Re: needing an fpga... |
Date: |
Thu, 17 Jun 2021 12:58:55 -0400 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/26.1 (gnu/linux) |
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