Dear Jacob Lifshay,
A proposal for a grant application was sent to NLnet Foundation
(https://nlnet.nl) using this email address. Your project has received
code 2024-12-324. The text of the proposal is shown below for your
records. If you want to make changes to this proposal before the
deadline, feel free to resubmit. We will send you a follow-up email
after the deadline has passed to provide more information regarding
the review process.
Important: if this request did NOT originate from you (and you are
unaware of others that could have made this application on your
behalf), do NOT CLICK on any links in this message nor open
attachments. Please notify us if this is the case, otherwise you can
expect at least two other emails from us. If that is not a problem,
feel free to discard immediately.
Best regards,
the NLnet team
Code : 2024-12-324
Requestor : Jacob Lifshay
Email : programmerjake@gmail.com
Phone : 12089070040
Organization: Libre-Chip
Country : USA
Consent : You may keep my data on record
Call : Commons_Fund
Project : Libre-Chip's First CPU Architecture And Formal Proof of
No Spectre bugs
Website : https://libre-chip.org/
Abstract : Modern CPUs suffer from a constant stream of new
speculative-execution security
flaws
(Spectre-style bugs). Because of that,
software has to constantly add more convoluted and slow mitigations to
properly enforce security boundaries, such as a WebAssembly VM needing
to add code to prevent leaking data from outside the VM to whatever
programs are running inside the VM, or a web browser needing to stop
JavaScript code from seeing memory that it should not have access to.
To address this major category of CPU flaws, Jacob Lifshay formulated
a way to formally prove that a CPU with speculative execution doesn't
suffer from any speculative-execution data leaks -- this should work
for nearly any kind of CPU design.
We are working towards building a high-performance superscalar CPU
with speculative execution and working on proving that it doesn't
suffer from any speculative-execution data leaks, thereby
demonstrating that this major category of CPU flaws can be fixed once
and for all without crippling CPU performance.
Experience : * Jacob Lifshay -- Worked on designing PowerISA CPUs
with Libre-SOC for 5yr, built a simple OoO Superscalar CPU simulator
https://salsa.debian.org/Kazan-team/power-cpu-sim, built a RV32I CPU
with VGA output in a few weeks that runs a 2.5D maze game
https://github.com/programmerjake/rv32. Also is the main author of
the Fayalite HDL
library
- Cesar Strauss - Contributed to the Libre-SOC project, mostly on digital
design and formal verification. Presented the talk "An introduction to
Formal Verification of Digital Circuits" on FOSDEM 2024
(https://archive.fosdem.org/2024/schedule/event/fosdem-2024-2215-an-introduction-to-formal-verification-of-digital-circuits/).
Amount : € 50000
Use : Nearly all of the cost is for labor, with some amount
set aside for general project management (e.g. tracking funding,
server maintenance, etc.), and for hardware costs such as buying
bigger FPGAs so the CPU design will fit.
We're aiming for a rate of somewhere around $69305.60/yr per person
which is the minimum salary for small employers for 2025 in Washington
State USA (where Jacob Lifshay lives at the time).
https://www.lni.wa.gov/forms-publications/f700-207-000.pdf
Estimated Budget:
General Project Management
€2000
For tracking funding, server maintenance, and similar.
Hardware Costs
€3000
For buying bigger FPGAs, CI server hardware improvements,
Oscilloscopes (if necessary), and similar.
Improvements to Fayalite
€10000
For adding the code for translation to Coq, adding tooling for
generating FPGA bitstreams, as well as other improvements to Fayalite
as necessary.
Building enough of the CPU to execute multiple instructions
€10000
This covers getting register renaming and ALU and/or branch
instructions working, as well as other portions of the CPU design as
necessary. This may or may not include actually fetching those
instructions from memory, instead the instructions may be supplied by
a testing harness.
Implementing Memory Subsystem
€15000
This covers the rest needed for the CPU to be able to fetch
instructions from memory and execute them as well as implementing
Load/Store instructions.
Work towards the Formal Proof of No Spectre bugs
€10000
This covers working on the Formal Proof of No Spectre bugs as well as
improvements to other software/hardware needed for that.
Comparison : ### UPEC, as described in "An Exhaustive Approach to
Detecting Transient Execution Side Channels in RTL Designs of
Processors"
https://arxiv.org/pdf/2108.01979
According to https://arxiv.org/pdf/2407.12232, UPEC is limited in
that it only works on a specific conservative mechanism (preventing
speculative load instructions from executing until all prior branches
are resolved). by contrast our formal proof method should work even if
the CPU runs speculative loads before resolving branches, with much
less stringent conditions on those loads.
"RTL Verification for Secure Speculation Using Contract Shadow Logic"
https://arxiv.org/pdf/2407.12232
Contract Shadow Logic works by assuming that memory is partitioned
into secret and non-secret regions, by contrast our formal proof
method is based on verifying that no data processed by transient
instructions (instructions that were speculatively executed and then
canceled) can affect any digital signals that leave the processor.
Challenges : We expect to solve 2 technical challenges:
- To create a working OoO Superscalar CPU with Speculative Execution,
trying to design it such that it doesn't have any Spectre-style
vulnerabilities (mostly by doing a better job of tracking any state
whatsoever that has speculative modifications). The CPU probably will
not yet support some of the features required for high performance
(e.g. a complex cache hierarchy) and/or supporting running an
operating system and/or floating-point. The plan is to add those
features later if they are not completed as part of this grant. - To make substantial progress on creating a formal proof that the CPU
doesn't have any Spectre-style vulnerabilities. This is complex enough
and has enough potential problems we may run into that we may not
finish by the end of this grant, and may need additional grants
afterward to finish, hence why the goal is making substantial progress
instead of having the proof 100% complete and working.
To address this general category of CPU flaws, Jacob Lifshay
formulated a way to formally prove that a CPU with speculative
execution doesn't suffer from any speculative-execution data leaks:
- Assume that to leak data, you must be able to observe some change
in the digital signals going from/to the CPU core that depends on the
results (defined to include any side-effects that change any state,
such as cache state changes or branch predictor changes) of some
transient instructions (instructions that were speculatively executed
and then canceled). - Take the concrete cycle-accurate CPU design, and construct a
theoretical equivalent that has the additional feature of looking into
the future to determine which instructions will be canceled and
preemptively forces their results to be zeros (or any other value that
doesn't depend on transient instructions' data; since we're doing math
here, we don't have to limit ourselves to physically possible designs
that respect time flow). The reasoning is that if all transient
instructions' results are always zeros, they can't possibly be leaking
any useful data, therefore the theoretical equivalent CPU design
doesn't have any speculative-execution data leaks. - Formally prove that all digital signals from/to the concrete CPU
core always exactly match the timing and data in all respects of the
theoretical equivalent CPU design. This proves that the concrete CPU
core can't have any speculative-execution data leaks.
It is expected that automated formal proof software (like SMT solvers
such as Z3) will probably be too slow to be usable for the formal
correctness proof, therefore the plan is to use Fayalite to generate a
translation of the CPU design to Coq or some other similar language
for writing formal proofs.
Fayalite is a HDL
library written in Rust that we have been developing since around
April 2024 that targets the
FIRRTL intermediate
language (used by the Chisel ecosystem
for generating Verilog; firtool, the FIRRTL to Verilog translator, is
part of LLVM Circt, so is well maintained).
A WIP high-level design of our CPU:
https://libre-chip.org/first_arch/index.html
Ecosystem : We plan on working with the OpenPower Foundation for any
custom ISA extensions we may need. We are already working with the
FIRRTL specification GitHub repo to resolve problems we encounter, as
well as with LLVM Circt, and with the Rust Language.
This project benefits Europeans (as well as everyone else) by
providing a CPU with good performance that doesn't suffer from
Spectre-style flaws, as well as working on providing a method of
formally proving if any particular CPU design doesn't suffer from
Spectre-style flaws, hopefully encouraging CPU designers everywhere to
formally prove their CPU designs to not have Spectre-style flaws
instead of the reactionary fixes that they have been using that only
covers known Spectre-style flaws and has a constant stream of
failures.
Attachments :