Presentation
Leveraging Invariants for Scalable Verification of RISC-V Cryptography Extensions
DescriptionRISC-V has recently ratified a vector cryptography extension. Ex-
haustive formal verification of hardware designs that implement
this extension is crucial for security. However, scaling verification
for designs with such large bit-widths is challenging. We present
the first formal verification of Marian, an open-source implementa-
tion of the RISC-V vector cryptography extensions. We show that
proof modularization enables us to obtain an unbounded proof for
Marian. Together with our systematic invariant identification, we
reach an additional speedup of 174%. Our evaluation shows that
invariants that assert properties of counters, such as bounds or
directions, or handshakes are particularly effective in improving
the verification times. We show the generalizability and reusability
of our invariant identification methodology by formally verifying
another custom implementation of RISC-V vector cryptography
extensions. During verification, we found a violation that turned
out to be a flaw in the specification, which is now being updated.
haustive formal verification of hardware designs that implement
this extension is crucial for security. However, scaling verification
for designs with such large bit-widths is challenging. We present
the first formal verification of Marian, an open-source implementa-
tion of the RISC-V vector cryptography extensions. We show that
proof modularization enables us to obtain an unbounded proof for
Marian. Together with our systematic invariant identification, we
reach an additional speedup of 174%. Our evaluation shows that
invariants that assert properties of counters, such as bounds or
directions, or handshakes are particularly effective in improving
the verification times. We show the generalizability and reusability
of our invariant identification methodology by formally verifying
another custom implementation of RISC-V vector cryptography
extensions. During verification, we found a violation that turned
out to be a flaw in the specification, which is now being updated.
Event Type
Research Manuscript
TimeWednesday, July 2912:06pm - 12:18pm PDT
LocationMtg Room 202AB