Formal verification of taint-propagation security properties in a commercial SoC design

SoCs embedded in mobile phones, tablets and other smart devices come equipped with numerous features that impose specific security requirements on their hardware and firmware. Many security requirements can be formulated as taint-propagation properties that verify information flow between a set of signals in the design. In this work, we take a tablet SoC design, formulate its critical security requirements as taint-propagation properties, and prove them using a formal verification flow. We describe the properties targeted, techniques to help the verifier scale, and security bugs uncovered in the process.