Formal Verification of Security Properties in RTL Hardware Designs

Once more, the entire topic of embedded systems security is awfully under-represented at the otherwise excellent¹ Embedded Systems Week. Only the fairly small but highly interesting WESS Workshop addressed the topic properly; one of the most interesting papers presented at WESS is "Automatized High-Level Evaluation of Security Properties for RTL Hardware Designs" by Andrea Höller (who also gave the talk), Christopher Preschern, Christian Steger, Christian Kreiner, Armin Krieg, Holger Bock and Josef Haid.

Let me start by quickly explaining what "RTL Hardware Designs" are. "RTL" stands for "Register-Transfer Level" and basically defines the logic design phase within the circuit (or system) design process. At the register-transfer level, hardware description languages such as Verilog or VHDL are used to describe the logic circuits that operate on data flows between registers. That means, the RTL phase comes after the functional description of a circuit/system has been developed and after the system components and their interfaces have been specified; at the RTL level, the system components get "implemented" and the finished RTL design gets then translated into a netlist using a specific hardware library, placed and routed.

Formal Verification is in some sense the holy grail of security researchers and engineers: Ideally, we would like to have formal proofs and assurances all the way from the theoretic foundations down to the most obscure implementation detail of security-relevant products. In other words, we would like to have an exhaustive model of the product based on which we can check that all required security properties are provided by the product at all times and under all circumstances. This requires two steps:

1. Extraction of an accurate model from the implementation.
2. Model checking, i.e. verification whether the model maintains the specified security properties.

In one way this is nice because it can be automated to a large degree and thus removes the human error factor from the security equation but: Exhaustive formal verification is extremely difficult at best and, quite often, absolutely infeasible. So it will never replace implementation-specific and experimental security verification. But we can use formal verification to cut down on development costs and time-to-market; the sooner security problems are identified during the design stage the easier (and cheaper) they are to fix. With each fixed security problem the chance that your prototype manages to pass (e.g. Common Criteria) security evaluation increases.

In some points the Common Criteria security evaluation process already requires formal verification techniques to be employed. For example, each product needs to come with a model extracted from its functional specification and a proof that the model (and therefore the functional specification) indeed maintains all required security properties. But as far as formal verification of hardware design is concerned, this is all that is required by Common Criteria, leaving a large gap towards exhaustive formal verification of the finished product. This is where Höller et al.'s work comes into play. They show a possible extension to the Common Criteria verification process by extracting a verifiable model from the RTL specification and using conventional model checkers such as NuSMV (http://nusmv.fbk.eu/) together with the LTL (linear temporal logic) property specifications to verify whether the RTL implementation still meets the security requirements. It should be noted that the LTL property specifications are already required within the existing Common Criteria process and can be reused for Höller et al.'s additional verification step. In the second part of their paper Höller et al. show how to use the RTL model checking to check whether an implementation is resistant against certain types of faults.

My personal best paper award for WESS definitely goes to Höller et al.

---
¹) Disclaimer: The mainline conferences haven't actually started yet. My assessment of ESWeek's excellency is based on past experience.