SIRRTL Beta Release Notes (v1)

Secure-Firrtl Release Notes

11/07/2019

Secure Firrtl Purpose:

Secure Firrtl is a version of the original FIRRTL hardware description language
with security types for confidentiality and integrity. Secure Firrtl supports
flexible security type representations and dependent types so that hardware
can be multiplexed across security levels. Secure Firrtl also supports
constrained downgrading (declassification and endorsement) to implement
more practical designs.

Requirements:

• Secure Firrtl is intended to compile code generated by ChiselFlow, a modified frontend
  for the Chisel3 compiler. To use Secure Firrtl, follow the instructions for installing ChiselFlow
  found in that repo's README. Then, you can use Firrtl generated by ChiselFlow as input
  to Secure Firrtl.

Features:

• Built-in Hypercube Representation of Security Labels (https://dl.acm.org/citation.cfm?id=3243743)
  (The compiler supports extending it with other label representations. Just extend
  the Policy trait (src/main/firrtl/Policy.scala); see HypercubePolicy for how to do this.
• Security Label Inferfence - All module interfaces need labels but internal signals only
  sometimes need them, often they can be inferred.
• Nonmalleable downgrading (declassification & endorsement) prevents attackers from
  undermining the downgrade mechanism.

How to Use SecureFirrtl:

• SecureFirrtl assumes you have compiled Chisel3 source code using the secure-chisel compiler.
  Programmers may also write Secure Firrtl directly. See the src/main/antlr4/FIRRTL.g4 file
  for the security label syntax.

• You can use sbt assembly to build an executable jar for Secure Firrtl just as you would
  for normal Firrtl. Below is an example execution of secure firrtl which generates an
  intermediate representation AND a checkable Z3 file.

  ./firrtl -i circuit.fir -o circuit.lbl.fir -z circuit.z3 -X labeled

• The "labeled" compiler (specified with the -X flag) tells the compiler to generate
  labeled MidFirrtl (with inferred labels). The '-z' flag tells the compiler to emit
  a Z3 file which can be used to typecheck the circuit.

• The set of constraints in the Z3 file specify situations under which information
  flow would be violated; therefore, when verifying the file all of the constraints
  should be unsatisfiable in a well-typed circuit. Here is an example script that
  will count the number of IFC violations:

  z3 -smt2 circuit.z3 | grep "^sat" | wc -l

  (note: 1 security error in a circuit may lead to multiple satisfiability errors)

• The secure-firrtl compiler will only run the labelchecking pass when the
  'labeled' compiler is being used. If Verilog is being generated, security labels
  will not be checked. It will also not automatically run z3 to check the dependent
  type constraints.

Version Specific Information:

This version of Secure Firrtl operates on the Chirrtl representation (i.e. the level
of Firrtl closest to Chisel). There are several bugs in typechecking caused by
this fact that result in unsound typechecking. Specifically, the 'last connect' semantics
of Firrtl are not properly inferred and Memories are assumed to be Sequential (such as SRAM).
The former means that some circuits which are incorrectly marked as sound when they
contain implicit label changes. The latter means that labels on non-sequential Mem objects are not checked.

Advantages:

• Can efficiently typecheck a secure version of the Hyperflow processor.
• Does not have Out of Memory or Timeout Errors

Disadvantages:

• Is unsound
• Compiler is not integrated with the unit tests for Firrtl
• Label Checking modifies circuit which cannot be run when generating Verilog
• Vector Labels (where different entries in a bit vector or Memory have different labels)
  are not supported.

Other Versions:

• See version v0.2 for a completely sound typechecker that has problems
  scaling to large designs but is well integrated into Firrtl's test bench