Formal Analysis of Security Data Paths in RTL Design Ziyad Hanna, PhD, Chief Architect, VP of Research Jamil R. Mazzawi, Consulting Services Manager HVC 2012 - Haifa Verification Conference, November 8, 2012 Introduction Introduction (Cont.) Source: Constructive and Destructive Aspects of Hardware Security for the Internet of Things. Prof. Christof Paar, presented at Intel’s Symposium: Computer Security: Modeling and Validation, 5 Nov 2012 Introduction (Cont.) Agenda Why security path verification Security path verification overview Usage examples Conclusion Why Security Path Verification Why do people care • Many systems (cell phones, game console etc.) contains secure information • Vulnerability will likely lead to unauthorized access of secure data • The potential loss (direct or indirect) is very large Where is the vulnerability • Software encryption algorithm • Hardware where secured areas can be accessed without going through the proper encryption paths Why is there hardware vulnerability • Integrating IP’s create an unexpected paths to access secure areas • Addition of test-logic creates paths to the outputs What Do People Do Today System Architecture • Moving secured areas in to isolation • Analyzing data-flow on the whole system • Manually identify potential structural paths and insert blocking conditions System integration • Investigate (often with a structural analysis tool) each structural path to ensure that they are false path Very tedious and ad hoc • Only be able to look at a small subset of trace • Rather subjective and no clear checking mechanism • Difficult to get real sense of completeness Security Path Verification overview Identify any unintentional path to/from secured areas • Use of Path sensitization technology (see next) • User specifies secure area and illegal sources and destinations for the data inside this area – Optional: User can specify blocks through which data is allowed to propagate • Waveforms show illegal propagations found Secure Area Potential Savings • Time savings – weeks vs months • Verify all paths and able to understand progress • Completeness, not just subjective determination of correctness Usage example 1 Verify that data in secure register does not propagate to AXI interface without going through encryption block Secure Register Encryption Block AXI Secure Interface Usage example 1 (cont’d) Verify that data in secure register does not get overwritten by any data on AXI interface Secure Register Encryption Block AXI Secure Interface Path sensitization technology Path sensitization technology: • This technology introduces a new type of property: path cover, which has a source signal and a destination signal – • No SVA equivalent for this property! By proving this property, data at the source of the path is tainted. Then, Jasper formally verifies if it is possible to cover tainted data at the destination • When the property is covered, a waveform displays how data can propagate from source to destination • The property can also be determined to be unreachable, which means that it is not possible for data to propagate from source to destination Example: Path cover from B to C Data at B is tainted Can tainted data show up at C? Waveforms Taint generated at the source Red highlighting: Data reached destination Black-Box with Connectivity abstraction During Security Verification, blocks can be black-boxed with a special qualification about whether tainted data is allowed to go through the black-box or not This allows the user to selective black-box modules and tune the verification so only meaningful paths are found This feature is important to guarantee the scalability of this verification while still keeping results sound Standard black-boxes: Tainted data does not go through Black-box with connectivity abstraction: Tainted data is allowed to go through Usage example 2 Verify that data read from ROM does not propagate to some key points of the design top Master 0 Master 1 Interconnect Slave 0 RAM Slave 1 Slave 2 ROM Slave 3 Usage example 3 Verify that data from secure area never propagates to CPU register memory if “protected mode” is set to 0 Slave CPU Protected Mode =0 Secure Area Register Memory Usage example 4 The design is a small network, consisting of external memory, external secure ROM, two CPUs and some internal elements. The Encrypt/Decrypt slaves receive cryptography keys from the Key Manager (a master) and encrypts/decrypts data written to some of its memory locations The Key Manager reads the keys from the ROM and transfers it to the slaves after reset The goal is to verify that there is no undesired leak of this key to other parts of the system, such as CPU and external memory Bus protocol is simple request/acknowledge Design Overview top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface ROM Slave 1: Encrypt Slave 2: Decrypt Slave 3: RAM Interface External RAM Reading the keys from the ROM to the slaves top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface ROM DK EK Slave 1: Encrypt Slave 2: Decrypt EK DK Slave 3: RAM Interface External RAM Valid encryption or decryption top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface DK EK ROM EK DK Slave 3: RAM Interface External RAM Check 1: ROM leak top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface ROM DK EK Slave 1: Encrypt Slave 2: Decrypt Slave 3: RAM Interface External RAM Check 2: Illegal key overwrite top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface ROM EK DK Slave 3: RAM Interface External RAM Check 2: Illegal key overwrite top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface ROM EK DK Slave 3: RAM Interface External RAM Check 2: Illegal key overwrite from wrong ROM address top Master 0: CPU0 Master 1: CPU1 Master 2: Key Mgr Interconnect Slave 0: ROM Interface EK DK Slave 3: RAM Interface address!=0 ROM External RAM Conclusion: Security Path Verification Verify the lack of functional paths to/from secure areas of a design Based on path sensitization technology Requirements are not expressible by regular SVA assertions, therefore not possible with standard FV tools Special black-boxing to allow scalability to bigger designs Easy debug with special highlighting in the waveform