nlnet_2019_formal.mdwn

   1 # NL.net proposal 2019-10-032
   2
   3 * NLNet Project Page <https://nlnet.nl/project/LibreSoC-Proofs/>
   4
   5 ## Project name
   6
   7 The Libre RISC-V SoC, Formal Correctness Proofs
   8
   9 ## Website / wiki
  10
  11 <https://libre-riscv.org/nlnet_2019_formal>
  12
  13 Please be short and to the point in your answers; focus primarily on
  14 the what and how, not so much on the why. Add longer descriptions as
  15 attachments (see below). If English isn't your first language, don't
  16 worry - our reviewers don't care about spelling errors, only about
  17 great ideas. We apologise for the inconvenience of having to submit in
  18 English. On the up side, you can be as technical as you need to be (but
  19 you don't have to). Do stay concrete. Use plain text in your reply only,
  20 if you need any HTML to make your point please include this as attachment.
  21
  22 ## Abstract: Can you explain the whole project and its expected outcome(s).
  23
  24 The Libre RISCV SoC is being developed to provide a privacy-respecting
  25 modern processor, developed transparently and as libre to the bedrock
  26 as possible.
  27
  28 The entire hardware design is libre licensed so that independent third
  29 party audits may be carried out, in order for endusers to have a degree of
  30 confidence that their privacy is not being violated through the addition
  31 of spying backdoor coprocessors or simply through hardware implementation
  32 oversights (SPECTRE, Meltdown, Intel Pentium FPU Divide Bug and so on)
  33
  34 However: not only is that an extremely daunting task, but "quis custodiet
  35 custodiens?" Who guards the guards?
  36
  37 A solution to this problem is to provide formal mathematical correctness
  38 proofs at every level of the hardware design. With mathematically
  39 inviolate proofs, even an enduser can run the tests for themselves.
  40
  41 # Have you been involved with projects or organisations relevant to this project before? And if so, can you tell us a bit about your contributions?
  42
  43 Luke Leighton is an ethical technology specialist who has a consistent
  44 24-year track record of developing code in a real-time transparent
  45 (fully libre) fashion, and in managing Software Libre teams.  He is the
  46 lead developer on the Libre RISC-V SoC.
  47
  48 Dan Leighton is a software entrepreneur and experienced tech leader. He
  49 has worked on delivering innovative open source software projects for
  50 over 25 years in education, publishing and internet infrastructure. He
  51 specialises in bridging the gap between engineering and commercial teams.
  52
  53 # Requested Amount
  54
  55 EUR 50,000.
  56
  57 # Explain what the requested budget will be used for?
  58
  59 Working with mathematically-minded Software Engineers, every module in
  60 the Libre RISC-V SoC will have a "formal proof unit test written". This
  61 is an unusual design choice: most hardware designs will have monte carlo
  62 and corner case unit tests etc. written which, unfortunately, are both
  63 complex (and a distraction) and often incomplete.
  64
  65 Examples include the IEEE754 Floating Point Unit, where in the 1990s
  66 Intel managed to introduce an actual hardware division bug. We seek to
  67 formally *prove* that the output from the FP Divide unit outputs the
  68 correct answer, for all possible inputs.
  69
  70 There are other areas which can benefit from correctness proofs,
  71 at the low level: pipelines, FIFOs, the basic building blocks of a
  72 processor. nmigen, interestingly, already has a formal correctness
  73 proof for its FIFO library due to the complexity of testing FIFOs.
  74 On this stable foundation the higher level capabilities will then also
  75 get their own proofs.
  76
  77 Finally a high level formal proof will be run, which already exists in
  78 the form of "official" RISC-V Conformance Tests (if it does not depend
  79 on proprietary software), as well as the unofficial formal correctness
  80 test suite from SymbioticEDA.
  81
  82 Throughout this process, bugs will be found, including in code
  83 already written. These will require fixing, where previously, with
  84 non-mathematical unit tests, it was believed that the work was completed.
  85
  86 # Does the project have other funding sources, both past and present?
  87
  88 The overall project has sponsorship from Purism as well as a prior grant
  89 from NLNet.  However that is for specifically covering the development
  90 of the RTL (the hardware source code).
  91
  92 The formal correctness testing requires specialist expertise involving
  93 formal logic mathematical training, which is a different skillset from
  94 hardware design. Our initial proposal does not cover this scope.
  95
  96 Also not covered in the initial funding is the bugfixing that will be
  97 required should the more rigorous formal proofs discover any issues.
  98
  99 # Compare your own project with existing or historical efforts.
 100
 101 There do exist high level formal RISC-V Correctness proofs in various
 102 forms. One of these is the SymbioticEDA formal RISC-V proof which can
 103 for example test the Register File, and test that the integer operation
 104 is correct and so on, working its way through all operations one by one.
 105 This however is at a high level.
 106
 107 The Kestrel 53000 Series of embedded controllers have some formal unit
 108 tests written in verilog, at the lowest level. We are following their
 109 development and porting to nmigen closely, and consulting with their
 110 part time developer.
 111
 112 A massive comprehensive suite of formal correctness proofs for a
 113 processor of the scope and size of the Libre RISC-V SoC is just not
 114 normally done. The only reason we are considering it is because of the
 115 dramatic simplification of unit tests that the approach brings, and the
 116 mathematically inviolate guarantees it brings for endusers and developers.
 117
 118 ## What are significant technical challenges you expect to solve during the project, if any?
 119
 120 This project is critically dependent on having software engineers that
 121 have the mathematical acumen for formal logic correctness proofs. This
 122 is quite a rare combination.
 123
 124 In addition, we are using an unusual choice of HDL: a python based tool
 125 called nmigen. Fortunately its backend is yosys, which has well known
 126 industry recognised links to formal proof libraries, through symbiyosys.
 127
 128 We will need to train engineers to adapt to the unique mathematics,
 129 or train mathematicians to the unique software quirks.
 130
 131 Luckily we have several examples already, in the form of the work carried
 132 out by the developer of the Kestrel 53000 series of CPUs.
 133
 134 The other main challenge is that as the size of the code being tested
 135 goes up, the CPU resources required go up exponentially. At the low level
 136 it is fine: tests can take several hours on a standard high end desktop.
 137 However as things progress to larger levels we may actually need access
 138 to Beowulf Clusters or other supercomputing resources.
 139
 140 ## Describe the ecosystem of the project, and how you will engage with relevant actors and promote the outcomes?
 141
 142 As mentioned in the 2018 submission, the Libre RISC-V
 143 SoC has a full set of resources for Libre Project Management and development:
 144 mailing list, bugtracker, git repository and wiki - all listed here:
 145 <https://libre-riscv.org/>
 146
 147 In addition, we have a Crowdsupply page
 148 <https://www.crowdsupply.com/libre-risc-v/m-class> which provides a public
 149 gateway, and heise.de, reddit, phoronix, slashdot and other locations have
 150 all picked up the story.  The list is updated and maintained here:
 151 <https://libre-riscv.org/3d_gpu/>
 152
 153 # Extra info to be submitted
 154
 155 * <http://libre-riscv.org/3d_gpu/>
 156 * <https://nlnet.nl/project/Libre-RISCV/>
 157 * <https://symbiyosys.readthedocs.io>
 158
 159 # Management Summary
 160
 161 The Libre RISC-V SoC Project, https://nlnet.nl/project/Libre-RISCV/, is
 162 funded by NLNet to reach ASIC-proven status.  As of Dec 2019 It has been
 163 in development for a year, and writing comprehensive unit tests has been
 164 both a critical part of that process and a major part of the time taken.
 165 Formal Mathematical Proofs turn out to be critical for several reasons:
 166 firstly, they are simpler to read and much more comprehensive (100%
 167 coverage), saving hugely on development and maintenance; secondly,
 168 they're mathematically inviolate.  From a security and trust perspective,
 169 both aspects are extremely important.  Firstly: security mistakes are
 170 often accidental due to complexity: a reduction in complexity helps
 171 avoid mistakes.  Secondly: independent auditing of the processor is a
 172 matter of running the formal proofs.  This proposal therefore not only
 173 saves on development time, it helps us meet the goal of developing a
 174 privacy-respecting processor in a way that is *independently* verifiable.