Formal Verification of RISC-V cores with riscv-formal

Learn how to use formal Assertion Based Verification (ABV) and open-source tools to formally verify HDL designs, and how to use the properties and formal test benches in the riscv-formal framework to formally verify RISC-V cores with ease. This tutorial is aimed specifically at HDL design engineers without in-depth knowledge of formal methods who want to add formal ABV to their verification toolbox.

http://www.clifford.at/papers/2018/riscv-formal/

https://tmt.knect365.com/risc-v-summit/agenda/1#track-1_formal-verification-of-risc-v-processor-implementations-space-limited

https://github.com/SymbioticEDA/riscv-formal

SiFive open sources RISC-V Freedom U540-C000’s Bootloader

It is good to see SiFive open-source their stack. RISC-V is Free as in Beer, not Freedom, so an implementor may make a closed-source implementation, and we need to encourage implementors to make open-source implementations. 😉

https://www.sifive.com/blog/2018/09/06/an-open-source-release-of-the-freedom-u540-c000s-bootloader/

ARM pulls RISC-V web site?

Re: https://firmwaresecurity.com/2018/07/10/arm-basics-com-arm-architecture-understand-the-facts/

and https://firmwaresecurity.com/2018/07/09/arm-on-risc-v-five-things-to-consider-before-designing-a-system-on-chip/

it appears ARM pulled the site. I can’t see this site anymore:

https://www.riscv-basics.com/

But the Wayback Machine appears to have made a snapshot:

https://web.archive.org/web/20180710134510/https://riscv-basics.com/

https://www.theregister.co.uk/2018/07/10/arm_riscv_website/

SiFive: DDR controller configuration register values unleashed!

Re: https://firmwaresecurity.com/2018/06/25/risc-v-implementations-filled-with-blobs/

https://forums.sifive.com/t/ddr-controller-configuration-register-values-for-hifive-unleashed/1334/8

Comment from SiFive:

SiFive is committed to supporting the open-source community. We are pleased to report that after discussions with our IP partners, we are now able to make available all the source code required to initialize the HiFive Unleashed board. The board’s boot sequence is described in the manual. The assembly code in the initial reset ROM is listed in the manual Chapter 6.1 “Reset Vector”. The firmware in the ZSBL mask ROM is directly readable by software on the chip, and we will be making the full source code available shortly. The source code for FSBL including the DDR initialization will also be available shortly. We can attest there is no other firmware run by the system during boot.

RISC-V: Secure Boot and Remote Attestation in the Sanctum Processor

Cryptology ePrint Archive: Report 2018/427

Secure Boot and Remote Attestation in the Sanctum Processor

During the secure boot process for a trusted execution environment, the processor must provide a chain of certificates to the remote client demonstrating that their secure container was established as specified. This certificate chain is rooted at the hardware manufacturer who is responsible for constructing chips according to the correct specification and provisioning them with key material. We consider a semi-honest manufacturer who is assumed to construct chips correctly, but may attempt to obtain knowledge of client private keys during the process. Using the RISC-V Rocket chip architecture as a base, we design, document, and implement an attested execution processor that does not require secure non-volatile memory, nor a private key explicitly assigned by the manufacturer. Instead, the processor derives its cryptographic identity from manufacturing variation measured by a Physical Unclonable Function (PUF). Software executed by a bootloader built into the processor transforms the PUF output into an elliptic curve key pair. The (re)generated private key is used to sign trusted portions of the boot image, and is immediately destroyed. The platform can therefore provide attestations about its state to remote clients. Reliability and security of PUF keys are ensured through the use of a trapdoor computational fuzzy extractor.

We present detailed evaluation results for secure boot and attestation by a client of a Rocket chip implementation on a Xilinx Zynq 7000 FPGA.

https://eprint.iacr.org/2018/427

https://eprint.iacr.org/2018/427.pdf

On the Path to a Secure Boot Solution for RISC-V

On the Path to a Secure Boot Solution for RISC-V
By SecureRF | April 26, 2018 | 0

As the RISC-V ISA gains in popularity and more industries proceed with plans to build and deploy systems based on RISC-V technologies, the security requirements of those systems will grow. One avenue that hackers have used to exploit systems has been to modify the firmware and cause it to misbehave. For example, one of the recent vehicle hacks involved corrupting firmware in order to jump from an infotainment center to the CAN-BUS. The solution to this style of attack is a secure boot, and with minimal additions to the ISA, RISC-V can provide secure boot hooks directly. Secure boot is a self-hosted root of trust that uses a digital signature and a known, trusted, public key to protect the firmware before it loads. The RISC-V system validates the signature over the firmware using the trusted public key and will run the code only if the signature verifies correctly. If the firmware has been modified in any way, the signature validation will fail. Once this initial trusted load completes, subsequent loads can use the same process to chain the trust to additional loads.[…]

https://www.securerf.com/path-secure-boot-solution-risc-v/

QEMU has RISC-V support

part 2:https://www.sifive.com/blog/2018/04/25/risc-v-qemu-part-2-the-risc-v-qemu-port-is-up stream/

part 1: https://www.sifive.com/blog/2017/12/20/risc-v-qemu-part-1-privileged-isa-hifive1-virtio/

see-also Sifive’s statement on Spectre/Meltdown:

https://www.sifive.com/blog/2018/01/05/sifive-statement-on-meltdown-and-spectre/

seL ported to RISC-V

seL, in addition to Intel and ARM, now supports RISC-V!

https://github.com/seL4/seL4/tree/master/include/arch/riscv/arch
https://sel4.systems/pipermail/devel/2018-April/001928.html
https://docs.sel4.systems/Hardware/RISCV
https://sel4.systems/About/seL4/
https://riscv.org/

 

PS: seL is not the only OS porting to RISC-V, here’s the Debian port:
https://groups.google.com/a/groups.riscv.org/forum/#!topic/sw-dev/u4VcUtB9r94

PS: RISC-V is getting active, and has had lots of newsworthy events that I’ve not covered:
https://riscv.org/news/

RISC-V dev boards: early access limited pre-order

https://www.crowdsupply.com/sifive/hifive-unleashed

https://abopen.com/news/multi-core-64-bit-linux-capable-risc-v-board-unveiled-available-pre-order/

 

Western Digital embraces RISC-V

[…]Western Digital’s leadership role in the RISC-V initiative is significant in that it aims to accelerate the advancement of the technology and the surrounding ecosystem by transitioning its own consumption of processors – over one billion cores per year – to RISC-V.[…]

https://www.wdc.com/about-wd/newsroom/press-room/2017-11-28-western-digital-to-accelerate-the-future-of-next-generation-computing-architectures-for-big-data-and-fast-data-environments.html

SiFive appoints new CEO

SiFive Appoints Naveed Sherwani as CEO

SAN FRANCISCO – August 15, 2017 – SiFive, the first fabless provider of customized, open-source-enabled semiconductors, today announced that industry veteran Naveed Sherwani has joined the company as CEO to lead it through its next phase of growth. Stefan Dyckerhoff, who had held the top spot at the company since its inception, will remain a member of the SiFive board of directors. “Naveed brings a lifetime of experience not only in the semiconductor and open source sectors, but also in growing successful startups into industry leaders,” Dyckerhoff said. “SiFive has achieved significant industry milestones since its founding, and we continue to drive innovations that are leveling the playing field for those priced out of the traditional silicon market. We are excited to have Naveed join the team, and look forward to further growth under his leadership.” Sherwani joins SiFive with more than 25 years of experience in the industry at companies including Intel, Brite Semiconductor and Open Silicon. Over the course of his career, Sherwani has been involved in the development of more than 300 chips, and, through his work as founder and CEO of Open Silicon, was instrumental in leading the development of ASIC technologies, which offered lower cost alternatives to traditional, less reliable legacy offerings.[…]

https://www.sifive.com/posts/2017/08/15/sifive-appoints-naveed-sherwani-as-ceo/

https://riscv.org/

HiFive1

Call for Papers: 7th RISC-V Workshop

7th RISC-V Workshop November 28-30, 2017

We’re seeking proposals for talks and poster presentations conveying recent activity in the RISC-V community at the upcoming 7th RISC-V workshop hosted by Western Digital in Milpitas California on November 28-30, 2017.[…]

https://riscv.org/2017/06/7th-risc-v-workshop-call-for-papers/

https://riscv.org/

SiFive Coreplex IP for RISC-V

RISC-V is a free and open instruction set architecture based on modern design techniques and decades of computer architecture research. With over 60 member companies and a robust software ecosystem, RISC-V is set to be the standard architecture in all modern computing devices, from 32-bit embedded microcontrollers to 64-bit application processors and datacenter accelerators and beyond. SiFive Coreplex IP are the most widely deployed RISC-V cores in the world and are the lowest risk, easiest path to RISC-V. SiFive Coreplex IP are fully synthesizable and verified soft IP implementations that scale across multiple design nodes, making them ideal for your next SoC design.

https://www.sifive.com/products/coreplex-risc-v-ip/

 

RISC-V edition of Computer Organization and Design

Computer Organization and Design RISC-V Edition
1st Edition
The Hardware Software Interface
Authors: David Patterson John Hennessy
Paperback ISBN: 9780128122754
Imprint: Morgan Kaufmann
Published Date: 13th April 2017
Page Count: 696

https://www.elsevier.com/books/computer-organization-and-design-risc-v-edition/patterson/978-0-12-812275-4
https://www.elsevier.com/books-and-journals/book-companion/9780128122754
https://textbooks.elsevier.com/web/product_details.aspx?isbn=9780128122754