X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=nlnet_2019_formal.mdwn;h=1d3cbb4072a86211fb505290e9f3fcf370e5f5dd;hb=3019c1e3a12f7c8135a6a417655b0ec2d4fa5b6e;hp=8b4368d142031429f71ecd1725c7ee905c3b8951;hpb=314aa4b1c38b3a4a03662aef5c9f231a2ff3fa6e;p=libreriscv.git diff --git a/nlnet_2019_formal.mdwn b/nlnet_2019_formal.mdwn index 8b4368d14..1d3cbb407 100644 --- a/nlnet_2019_formal.mdwn +++ b/nlnet_2019_formal.mdwn @@ -1,5 +1,7 @@ # NL.net proposal 2019-10-032 +* NLNet Project Page + ## Project name The Libre RISC-V SoC, Formal Correctness Proofs @@ -156,4 +158,17 @@ all picked up the story. The list is updated and maintained here: # Management Summary -The Libre RISC-V SoC Project, https://nlnet.nl/project/Libre-RISCV/, is funded by NLNet to reach ASIC-proven status. As of Dec 2019 It has been in development for a year, and writing comprehensive unit tests has been both a critical part of that process and a major part of the time taken. Formal Mathematical Proofs turn out to be critical for several reasons: firstly, they are simpler to read and much more comprehensive (100% coverage), saving hugely on development and maintenance; secondly, they're mathematically inviolate. From a security and trust perspective, both aspects are extremely important. Firstly: security mistakes are often accidental due to complexity: a reduction in complexity helps avoid mistakes. Secondly: independent auditing of the processor is a matter of running the formal proofs. This proposal therefore not only saves on development time, it helps us meet the goal of developing a privacy-respecting processor in a way that is *independently* verifiable. +The Libre RISC-V SoC Project, https://nlnet.nl/project/Libre-RISCV/, is +funded by NLNet to reach ASIC-proven status. As of Dec 2019 It has been +in development for a year, and writing comprehensive unit tests has been +both a critical part of that process and a major part of the time taken. +Formal Mathematical Proofs turn out to be critical for several reasons: +firstly, they are simpler to read and much more comprehensive (100% +coverage), saving hugely on development and maintenance; secondly, +they're mathematically inviolate. From a security and trust perspective, +both aspects are extremely important. Firstly: security mistakes are +often accidental due to complexity: a reduction in complexity helps +avoid mistakes. Secondly: independent auditing of the processor is a +matter of running the formal proofs. This proposal therefore not only +saves on development time, it helps us meet the goal of developing a +privacy-respecting processor in a way that is *independently* verifiable.