Libre-SOC Formal Correctness Proofs
Mathematical unit tests for open hardware System-on-Chip
Hardware projects like the Libre-SOC Project involve writing an inordinate amount of comprehensive unit tests to make sure everything functions the way it should. This is a critical and expensive part of the overall design process. Formal Mathematical Proofs (already quite popular in secure software development) provide an interesting alternative for several reasons: they're mathematically inviolate, which we believe makes them more trustworthy. And they are simpler to read and much more comprehensive (100% coverage), saving hugely on development and maintenance. From a security and trust perspective, both aspects are extremely important. 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. The project aims to provide proofs for every module of the Libre RISC-V SoC, and therefore contributes significantly with the larger goal of developing a privacy-respecting processor in a way that is independently verifiable.
- The project's own website: https://libre-riscv.org/nlnet_2019_formal
Why does this actually matter to end users?
When you go to a store to buy a laptop or mobile phone, you may see different brands on the outside but choice in terms of what is inside the box (in particular the most expensive component, the processor technology) is pretty much limited to the same core technologies and large vendors that have been in the market for decades. This has a much bigger effect on the users than just the hefty price tag of the hardware, because the technologies at that level impact all other technologies and insecurity at that level break security across the board.
In the field of software, open source has already become the default option in the market for any new setup. In hardware, the situation is different. Users - even very big users such as governments - have very little control over the actual hardware security of the technology they critically depend on every day. Security experts continue to uncover major security issues, and users are rightly concerned about the security of their private data as well as the continuity of their operations. But in a locked-down market there is little anyone can do, because the lack of alternatives. European companies are locked out of the possibility to contribute solutions and start new businesses that can change the status quo.
This ambitious project wants to deliver the first completely open computer processor in history - one you don' t have to merely trust, because you can verify and modify everything about it. All of the technology included, from top to bottom, will become available for inspection, and can be tuned by anyone technically capable enough. This will significantly contribute to the creation a new generation of computer technologies, as well as more energy efficient and cheaper devices. NGI Zero funds several important building blocks of this project, like this effort to provide so-called mathematical correctness proofs, which test every little part of a hardware design for possible logic flaws a human would not be able to spot. Ultimately these building blocks will come together in a transparent computer processor that can make our computing devices more trustworthy.
This project was funded through the NGI0 PET Fund, a fund established by NLnet with financial support from the European Commission's Next Generation Internet programme, under the aegis of DG Communications Networks, Content and Technology under grant agreement No 825310.
