Validating NoC Security. Innovation in Verification

Network on Chip (NoC) connectivity is ubiquitous in SoCs, therefore should be an attractive attack vector. Is it possible to prove robustness against a broad and configurable range of threats? Paul Cunningham (Senior VP/GM, Verification at Cadence), Raúl Camposano (Silicon Catalyst, entrepreneur, former Synopsys CTO and now Silvaco CTO) and I continue our series on research ideas. As always, feedback welcome.

The Innovation

This month’s pick is Towards the Formal Verification of Security Properties of a Network-on-Chip Router. The authors presented the paper at the 2018 IEEE ETS and are/were at the Technical University of Munich in Germany.

NoCs are the preferred connectivity fabric for modern SoCs. In mesh form NoCs are fundamental in arrayed processor architectures for many core servers and AI accelerators. Given this, mesh NoCs are a natural target for direct and side-channel software-based attacks. Further supporting recent interest, Google Scholar shows nearly 2k papers on NoC Security for 2022.

Use of formal methods as presented here is appealing since mesh structures are regular and the approach proposed is inductive (or a related algorithm), which should imply scalability. The authors illustrate with a set of properties to check for security against data alteration, denial of service and timing side-channel attacks.

Paul’s view

This is a perfect paper to close out 2022; a tight and crisp read on an important topic. Table II on page 4 is the big highlight for me, where the authors beautifully summarize formal definitions of security attacks on a NOC with a hierarchy of just 21 concise properties covering data modification, denial-of-service, and side-channel (interference, starvation) attacks. These definitions can be pulled out of the table and plugged directly into any commercial model checking tool or implemented as SystemVerilog assertion for a logic simulation or emulation run.

Since the paper was published in 2018 we have seen NOC complexity rise significantly, with almost any SOC from mobile to datacenter to vehicle deploying some form of NOC. At Cadence we are seeing model checking become an industry must-have for security verification. Today, even complex speculative execution attacks like Spectre and Meltdown can be effectively formulated and proven with modern model checking tools.

Raúl’s view

This month’s paper tackles Network on Chip (NoC) vulnerabilities by defining a large set of security related properties of the NoC routers. These are implementation independent. Subsets of these properties provide specific security and correctness checks; for example, avoiding false data in a router comes down to 1) Data that was read from the buffer was at some point in time written into the buffer, and 2) During multiplexing, the output data is equal to the desired input data (properties b5 and m1 in Table II and Fig. 3). Nine such composite effects of the properties are listed, in addition to avoiding false (above) data for example buffer overflow, data overwrite, packet loss, etc.

These 21 properties are formalized – written in Linear Temporal Logic (LTL) and checked using the Phaeton framework [25,26] which uses an unbound model checking solver. The actual model checked is the router synthesized together with a verification module. The latter includes the properties to be verified and acts as a wrapper to read and write the inputs and outputs to the router. All properties could be verified between 142-4185 seconds on a small Intel I5 CPU with 4GB of memory.

To show the effectiveness of the approach, 6 different router implementations were used. Examples include round-robin, time-division-multiplexing… and also trojan versions such as Gatecrasher which issues grants without any request. Time division multiplexing turns out to be the only implementation protected against all threats, i.e., satisfying all 21 properties. Table III summarizes the results.

For someone well versed in formal verification the paper is not difficult to follow, but it is definitely not self-contained or an easy read. It is a nice contribution towards secure NoCs (and router implementations). The correctness and security properties can be verified with “any other verification tool supporting gate-level or LTL model checking”, e.g., commercial model checkers.