Re: needing an fpga...

[Tim Daly]

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