fill out most sections of NLNet grant proposal

src/grants/nlnet-first.md

@@ -6,7 +6,7 @@ Website/Wiki: <https://libre-chip.org/>
 
 # Abstract
 
-Modern CPUs suffer from a [constant stream of new speculative-execution security flaws](https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline) ([Spectre](https://meltdownattack.com/)-style bugs), additionally software has to constantly add more convoluted and slow mitigations to properly inforce 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.
+Modern CPUs suffer from a [constant stream of new speculative-execution security flaws](https://en.wikipedia.org/wiki/Transient_execution_CPU_vulnerability#Timeline) ([Spectre](https://meltdownattack.com/)-style bugs), additionally 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 invented 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.
 
@@ -14,7 +14,7 @@ We are working towards building a high-performance superscalar CPU with speculat
 
 ## Relevant Previous Involvement
 
-* Jacob Lifshay -- TODO
+* 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](https://git.libre-chip.org/libre-chip/fayalite) HDL library
 
 * Others... TODO
 
@@ -34,19 +34,19 @@ TODO, come up with estimated budgets.
 
 <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 untill all prior branches are resolved). Jacob Lifshay's idea, by contrast, should work even if the CPU runs speculative loads before resolving branches, with much less stringient conditions on those loads.
+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>
 
-TODO
+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.
 
 ## Technical challenges we expect to solve during the project
 
 We expect to solve 2 technical challenges:
 
-* To create a working OoO Superscalar CPU with Speculative Execution.
+* 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).
 * 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, I (Jacob Lifshay) invented a way to formally prove that a CPU with speculative execution doesn't suffer from any speculative-execution data leaks:
@@ -55,10 +55,10 @@ To address this general category of CPU flaws, I (Jacob Lifshay) invented a way
 2. 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.
 3. 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 (stuff 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 software library 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).
+It is expected that automated formal proof software (stuff 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](https://git.libre-chip.org/libre-chip/fayalite) is a HDL library written in Rust that we have been developing since around April 2024 that targets the [FIRRTL](https://github.com/chipsalliance/firrtl-spec) intermediate language (used by the [Chisel](https://www.chisel-lang.org/) ecosystem for generating Verilog; firtool, the FIRRTL to Verilog translator, is part of [LLVM Circt](https://circt.llvm.org/), so is well maintained):
 
 ## Ecosystem
 
-TODO
+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.
 
-TODO European dimension? benefits people everywhere by having CPUs with better security, including Europeans.
+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.