CellIFT: Leveraging Cells for Scalable and Precise Dynamic Information Flow Tracking in RTL

Recent work has shown that hardware is plagued with safety and security-critical architectural and microarchitectural bugs that are very difficult to detect. As we show in our paper, RTL-level dynamic Information Flow Tracking (IFT) can detect these complex bugs with relatively little effort. The problem is that existing IFT mechanisms do not scale to complex designs such as state-of-the-art CPUs.

Our new IFT solution, called CellIFT, scales to the most complex microprocessor microarchitectures publicly available. We designed CellIFT based on a new level of abstraction, already commonly used by synthesizers and simulators which we call the cell level. Cells represent simple synthesizable mathematical operations such as adders, multiplexers or comparators.

Our results show improved precision and vastly improved scalability. CellIFT instruments hardware designs faster and with fewer resources than any existing mechanism. For designs that were already supported by existing mechanisms, CellIFT speeds up the simulation by 21 to 61 times, and typically reduces resource usage and critical path for FPGA emulation. Furthermore, CellIFT is the first hardware dynamic IFT mechanism to instrument the most complex open-source RISC-V microprocessors and SoCs.

Hardware dynamic information flow tracking

Dynamic information flow tracking is a mechanism that, for a given set of input signals (taint sources), reveals which internal and output signals (taint sinks) can be affected by changing values at these inputs, as illustrated in the figure below.

Applications

Hardware dynamic information flow tracking can dynamically check confidentiality and integrity properties. For example, for confidentiality, you taint the secret data, and you check if some observable signals are affected by the value of the secret data. For integrity, taint some input and check whether it alters some internal data or state unexpectedly.

We showed various concrete applications of CellIFT in our paper, including detecting microarchitectural elements that could leak information, detecting Spectre vulnerabilities and Meltdown-type bugs, and detecting architectural bugs such as address space non-conformities, reachability bugs, reset bugs and privilege violations.

The applications of CellIFT have not yet been exhaustively explored, and this is an exciting area for future research.

More information

CellIFT is released as open source. Instructions on how to use CellIFT and examples using five different RISC-V CPUs can be found on our GitHub page.

A paper about CellIFT is accepted for publication at USENIX Security 2022.

Frequently Asked Questions

How is CellIFT implemented?
CellIFT is implemented as a pass in the Yosys synthesizer. CellIFT is written in C++.

Is CellIFT scalable to any design complexity?
We instrumented arguably among the most complex open-source RISC-V designs with CellIFT. One known limitation is the size of memories, such as caches, which have an impact on CellIFT performance. However, these memories can generally be reduced for running the CellIFT experiments fast, or they can be replaced by models as we do in our experiments.

How is the mechanism integrated into the design?
CellIFT adds new logic to follow the taint flows around the original design without modifying the original logic.

Is my design compatible with CellIFT?
Any purely digital design should be compatible with CellIFT. If your design contains a technology-specific part such as an oscillator, you should replace it with a model and instrument the result with CellIFT.

Can I use CellIFT with another synthesizer than Yosys?
We implemented CellIFT in Yosys only: it is a popular and mature synthesizer under constant evolution, that is convenient to work with. However, the properties that we exploit are not Yosys-dependent. Therefore, it is certainly possible to port CellIFT to another synthesizer.

Can I use CellIFT on an FPGA?
Yes, CellIFT is fully synthesizable.

Acknowledgements

This work was supported in part by a Microsoft Swiss JRC grant and by the Swiss State Secretariat for Education, Research and Innovation under contract number MB22.00057 (ERC-StG PROMISE).