Verifying OpenTitan

OpenTitan is an open source silicon Root of Trust (RoT) project, which includes a firmware design and implementation of a secure boot process. This repository contains two experimental verified implementations of an RSA signature verification routine used in the OpenTitan Mask ROM, one in RISC-V and the other in the OpenTitan Big Number Accelerator (OTBN) ISA for OpenTitan's cryptographic hardware accelerator.

We are motivated by the following observation: formal proofs are often employed to show correctness of cryptographic routines at the assembly level, and while the same cryptographic routines are often implemented on different ISAs, the current cost of verification effort scales poorly with the number of architectures. This project aims to learn, through verifying two implementations of the same procedure in two different architectures, how to automate the process of proving the same routine for future architectures.

Verified Implemenations in Vale

Our verified implementations are slightly adapted from the current machine code implementations from the OpenTitan project, in instances where instruction reordering simplified verification but did not semantically alter the code.

The implementations are verified using a customized development of the Dafny variant of Vale, which is described in:

Vale: Verifying High-Performance Cryptographic Assembly Code
Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, Laure Thompson.
In Proceedings of the USENIX Security Symposium, 2017.
Distinguished Paper Award

The otbn-custom branch builds directly on top of the dafny-legacy branch, and exposes additional Dafny language features within Vale procedures.

Repository Organization

The arch directory contains the code describing the machine models for OTBN and RISC-V. In particular, for each architecture:

1. A machine.s.dfy file describes the machine model, which describes the architecture's maintained machine state (registers, flags, and instruction format). It also contains the executable semantics for the architecture.
2. A decls.i.dfy file describes the semantics for each instruction in the form of a Hoare triple. These definitions are untrusted, and implemented using the trusted operations defined in machine.s.dfy.
3. A 'vale.s.dfy' file that contains architecture-specific, user-defined types, functions, and lemmas which are used in generated Dafny files.

The impl directory contains the Vale implementations for the RSA signature verification routines. The OTBN implementation is based off of the code here and the RISC-V implementation is based off of the code here.

Note that one central convention is that all trusted specification files end in .s.dfy. Everything else should be a .i.dfy file and will be verified for correctness.

Build Instructions

We assume the following packages are installed by the user:

ninja (1.10.+)

dotnet (5.0)

nuget

python (3.+)

We assume some otbn tools are available:

otbn_as.py

otbn_ld.py

We also assume the Singular tool is installed, which is used by the custom version of the Dafny language installed by our builds script.

Finally, you will need all the Vale dependencies listed here. This is because a custom version of Vale will be compiled from source during setup.

To prepare for the build process, run:

python3 build.py setup

The setup will install custom versions of dafny and vale, and download a version of Dafny standard library. The setup should only need to be ran once.

We rely on ninja for building the project. To generate a build.ninja file for this project, run:

python3 build.py

Then run:

ninja -v -j4

This will start the build using 4 threads. The build output are all in the gen directory. gen/arch/otbn/printer.s.dll.out contains the printer output assembly code form the project. gen/impl/otbn/run_modexp.elf is currently the linked elf file assembled from the printer output.

Research Potentials:

Making Assembly Proofs Easier

1. proof generation
2. width independent proofs
3. algebra solvers

Building a Verified Hardware Root of Trust

Closing the Hardware/Software Gap