research-article

Property Specific Information Flow Analysis for Hardware Security Verification

Authors:

Armaiti Ardeshiricham,

Mustafa S Gobulukoglu,

Ryan KastnerAuthors Info & Claims

2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Pages 1 - 8

https://doi.org/10.1145/3240765.3240839

Published: 05 November 2018 Publication History

Abstract

Hardware information flow analysis detects security vulnerabilities resulting from unintended design flaws, timing channels, and hardware Trojans. These information flow models are typically generated in a general way, which includes a significant amount of redundancy that is irrelevant to the specified security properties. In this work, we propose a property specific approach for information flow security. We create information flow models tailored to the properties to be verified by performing a property specific search to identify security critical paths. This helps find suspicious signals that require closer inspection and quickly eliminates portions of the design that are free of security violations. Our property specific trimming technique reduces the complexity of the security model; this accelerates security verification and restricts potential security violations to a smaller region which helps quickly pinpoint hardware security vulnerabilities.

References

[1]

Alexandres Andreou, Andrey Bogdanov, and Elmar Tischhauser. 2017. Cache timing attacks on recent microarchitectures. In 2017 IEEE International Symposium on Hardware Oriented Security and Trust. 155–155. https://doi.org/10.1109/HST.2017.7951819

[2]

Armaiti Ardeshiricham, Wei Hu, and Ryan Kastner. 2017. Clepsydra: Modeling timing flows in hardware designs. In International Conference on Computer-Aided Design. 147–154. https://doi.org/10.1109/ICCAD.2017.8203772

[3]

Armaiti Ardeshiricham, Wei Hu, Joshua Marxen, and Ryan Kastner. 2017. Register transfer level information flow tracking for provably secure hardware design. In Design, Automation & Test in Europe Conference & Exhibition. 1695–1700. https://doi.org/10.23919/DATE.2017.7927266

[4]

Shuwen Deng, Doğuhan Gümüşoğlu, Wenjie Xiong, Y. Serhan Gener, Onur Demir, and Jakub Szefer. 2017. SecChisel: Language and Tool for Practical and Scalable Security Verification of Security-Aware Hardware Architectures. Cryptology ePrint Archive, Report. (2017).

[5]

Nicole Fern, Ismail San, and Kwang Ting Tim Cheng. 2017. Detecting hardware Trojans in unspecified functionality through solving satisfiability problems. In Asia and South Pacific Design Automation Conference. 598–504.

[6]

Joseph A. Goguen and Jose Meseguer. 1982. Security Policies and Security Models. In IEEE Symposium on Security & Privacy. 11–20.

[7]

Matthew Hicks, Murph Finnicum, Samuel T. King, Milo M. K. Martin, and Jonathan M. Smith. 2010. Overcoming an Untrusted Computing Base: Detecting and Removing Malicious Hardware Automatically. In IEEE Symposium on Security and Privacy. 159–172. 201018https://doi.org/10.1109/Sp.2010.18

[8]

Wei Hu, Alric Althoff, Armaiti Ardeshiricham, and Ryan Kastner. 2016. Towards Property Driven Hardware Security. In 17th International Workshop on Microprocessor and SOC Test and Verification (MTV). 51–56.

[9]

Wei Hu, Baolei Mao, Jason Oberg, and Ryan Kastner. 2016. Detecting Hardware Trojans with Gate-Level Information-Flow Tracking. Computer 49, 8 (Aug 2016), 44–52. https://doi.org/10.1109/MC.2016.225

Digital Library

[10]

Wei Hu, Jason Oberg, Dejun Mu, and Ryan Kastner. 2012. Simultaneous information flow security and circuit redundancy in Boolean gates. In International Conference on Computer-Aided Design. 585–590.

[11]

Yier Jin and Yiorgos Makris. 2012. Proof carrying-based information flow tracking for data secrecy protection and hardware trust. In the 30th IEEE VLSI Test Symposium (VTS). 252–257. https://doi.org/10.1109/VTS.2012.6231062

[12]

Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2018. Spectre Attacks: Exploiting Speculative Execution. ArXiv e-prints (Jan. 2018). arXiv:.

[13]

Xun Li, Vineeth Kashyap, Jason K. Oberg, Mohit Tiwari, Vasanth Ram Rajarathinam, Ryan Kastner, Timothy Sherwood, Ben Hardekopf, and Frederic T. Chong. 2014. Sapper: A Language for Hardware-level Security Policy Enforcement. In Architectural Support for Programming Languages and Operating Systems. 97–112.

[14]

Xun Li, Mohit Tiwari, Jason K. Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, and Ben Hardekopf. 2011. Caisson:a hardware description language for secure information flow. In Acm Sigplan Conference on Programming Language Design & Implementation. 109–120.

[15]

Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown. ArXiv e-prints (Jan. 2018). arXiv:.

[16]

Baolei Mao, Wei Hu, Alric Althoff, Janarbek Matai, Jason Oberg, Dejun Mu, Timothy Sherwood, and Ryan Kastner. 2015. Quantifying Timing-Based Information Flow in Cryptographic Hardware. In International Conference on Computer Aided Design. 552–559. https://doi.org/10.1109/ICCAD.2015.7372618

[17]

Bits Please. 2016. Extracting Qualcomm's KeyMaster Keys - Breaking Android Full Disk Encryption. In http://bits-please.blogspot.com/2016/06/extracting-qualcomms-keymaster-keys.html

[18]

Seetharam Narasimhan, Dongdong Du, Rajat Subhra Chakraborty, Somnath Paul, Francis G. Wolff, Christos A. Papachristou, Kaushik Roy, and Swarup Bhunia. 2013. Hardware Trojan Detection by Multiple-Parameter Side-Channel Analysis. IEEE Transactions on Computers 62, 11 (Nov 2013), 2183–2195. https://doi.org/10.1109/TC.2012.200

Digital Library

[19]

Jason Oberg, Wei Hu, Ali Irturk, Mohit Tiwari, Timothy Sherwood, and Ryan Kastner. 2011. Information flow isolation in I2C and USB. In Proceedings of the 48th Design Automation Conference. ACM, 254–259.

[20]

Jason Oberg, Sarah Meiklejohn, Timothy Sherwood, and Ryan Kastner. 2014. Leveraging gate-level properties to identify hardware timing channels. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 33, 9 (2014), 1288–1301.

[21]

Hassan Salmani, Mohammad Tehranipoor, and Jim Plusquellic. 2012. A Novel Technique for Improving Hardware Trojan Detection and Reducing Trojan Activation Time. IEEE Transactions on Very Large Scale Integration Systems 20, 1 (Jan 2012), 112–125. https://doi.org/10.1109/TVLSI.2010.2093547

Digital Library

[22]

Sergei Skorobogatov and Christopher Woods. 2012. Breakthrough Silicon Scanning Discovers Backdoor in Military Chip. Springer-Heidelberg, 23–40.

[23]

Mohit Tiwari, Jason K Oberg, Xun Li, Jonathan Valamehr, Timothy Levin, Ben Hardekopf, Ryan Kastner, Frederic T Chong, and Timothy Sherwood. 2011. Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security. In International Symposium on Computer Architecture (ISCA). 189–199. https://doi.org/10.1145/2000064.2000087

[24]

Mohit Tiwari, Hassan M.G. Wassel, Bita Mazloom, Shashidhar Mysore, Frederic T. Chong, and Timothy Sherwood. 2009. Complete Information Flow Tracking from the Gates Up. In the 14th International Conference on Architectural Support for Programming Languages and Operating Systems. 109–120.

[25]

Joakim Urdahl, Shrinidhi Udupi, Tobias Ludwig, Dominik Stoffel, and Wolfgang Kunz. 2016. Properties First? A New Design Methodology for Hardware, and Its Perspectives in Safety Analysis. In the 35th International Conference on Computer-Aided Design. Article, 8 pages. https://doi.org/10.1145/2966986.2980086

[26]

Adam Waksman, Matthew Suozzo, and Simha Sethumadhavan. 2013. FANCI: Identification of Stealthy Malicious Logic Using Boolean Functional Analysis. In Conference on Computer; Communications Security. 697–708.

[27]

Danfeng Zhang, Yao Wang, G. Edward Suh, and Andrew C. Myers. 2015. A Hardware Design Language for Timing-Sensitive Information-Flow Security. In International Conference on Architectural Support for Programming Languages and Operating Systems. 503–516. https://doi.org/10.1145/2694344.2694372

[28]

Jie Zhang, Feng Yuan, Lingxiao Wei, Zelong Sun, and Qiang Xu. 2015. VeriTrust: Verification for Hardware Trust. IEEE Trans. Comput.-Aided Design Integr. Circuits Syst. 34, 7 (July 2015), 1148–1161. https://doi.org/10.1109/TCAD.2015.2422836

Digital Library

Cited By

Qin MLi JYan JHao ZHu WLiu B(2024)HT-PGFV: Security-Aware Hardware Trojan Security Property Generation and Formal Security Verification SchemeElectronics10.3390/electronics1321428613:21(4286)Online publication date: 31-Oct-2024
https://doi.org/10.3390/electronics13214286
Duque Antón AMüller JDeutschmann LFadiheh MStoffel DKunz W(2024)A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators2024 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE58400.2024.10546664(1-6)Online publication date: 25-Mar-2024
https://doi.org/10.23919/DATE58400.2024.10546664
Dipu NAyalasomayajula ATehranipoor MFarahmandi F(2024)AGILE: Automated Assertion Generation to Detect Information Leakage VulnerabilitiesIEEE Transactions on Information Forensics and Security10.1109/TIFS.2023.334397019(1794-1809)Online publication date: 2024
https://doi.org/10.1109/TIFS.2023.3343970
Show More Cited By

Index Terms

Property Specific Information Flow Analysis for Hardware Security Verification

Index terms have been assigned to the content through auto-classification.

Recommendations

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis
ASPLOS '17: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems

Hardware-based mechanisms for software isolation are becoming increasingly popular, but implementing these mechanisms correctly has proved difficult, undermining the root of security. This work introduces an effective way to formally verify important ...
Theorem proof based gate level information flow tracking for hardware security verification
Abstract
Digital hardware lies in the heart of systems deployed in finance, medical care, basic infrastructure and national defense systems. However, due to the lack of effective security verification tools, hardware designs may contain ...
Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis
ASPLOS '17

Hardware-based mechanisms for software isolation are becoming increasingly popular, but implementing these mechanisms correctly has proved difficult, undermining the root of security. This work introduces an effective way to formally verify important ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

2018 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Nov 2018

939 pages

Copyright © 2018.

Publisher

IEEE Press

Publication History

Published: 05 November 2018

Permissions

Request permissions for this article.

Request Permissions

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

27
Total Citations
View Citations
249
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Qin MLi JYan JHao ZHu WLiu B(2024)HT-PGFV: Security-Aware Hardware Trojan Security Property Generation and Formal Security Verification SchemeElectronics10.3390/electronics1321428613:21(4286)Online publication date: 31-Oct-2024
https://doi.org/10.3390/electronics13214286
Duque Antón AMüller JDeutschmann LFadiheh MStoffel DKunz W(2024)A Golden-Free Formal Method for Trojan Detection in Non-Interfering Accelerators2024 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE58400.2024.10546664(1-6)Online publication date: 25-Mar-2024
https://doi.org/10.23919/DATE58400.2024.10546664
Dipu NAyalasomayajula ATehranipoor MFarahmandi F(2024)AGILE: Automated Assertion Generation to Detect Information Leakage VulnerabilitiesIEEE Transactions on Information Forensics and Security10.1109/TIFS.2023.334397019(1794-1809)Online publication date: 2024
https://doi.org/10.1109/TIFS.2023.3343970
Paria SDasgupta ABhunia S(2024)DiSPEL: A Framework for SoC Security Policy Synthesis and Distributed Enforcement2024 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)10.1109/HOST55342.2024.10545407(271-281)Online publication date: 6-May-2024
https://doi.org/10.1109/HOST55342.2024.10545407
Ayalasomayajula AFarzana NPal DFarahmandi F(2024)Prioritizing Information Flow Violations: Generation of Ranked Security Assertions for Hardware Designs2024 IEEE International Symposium on Hardware Oriented Security and Trust (HOST)10.1109/HOST55342.2024.10545352(128-138)Online publication date: 6-May-2024
https://doi.org/10.1109/HOST55342.2024.10545352
Dharsee KCriswell JCalandrino JTroncoso C(2023)JinnProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620627(6965-6982)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620627
Meng XRaj KRay SBasu K(2023)SeVNoC: Security Validation of System-on-Chip Designs With NoC FabricsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2022.317930742:2(672-682)Online publication date: Feb-2023
https://doi.org/10.1109/TCAD.2022.3179307
Restuccia FMeza AKastner ROberg J(2023)A Framework for Design, Verification, and Management of SoC Access Control SystemsIEEE Transactions on Computers10.1109/TC.2022.320992372:2(386-400)Online publication date: 1-Feb-2023
https://doi.org/10.1109/TC.2022.3209923
Lai XJenihhin M(2023)Analyzing Side-Channel Attack Vulnerabilities at RTL2023 IEEE 24th Latin American Test Symposium (LATS)10.1109/LATS58125.2023.10154497(1-2)Online publication date: 21-Mar-2023
https://doi.org/10.1109/LATS58125.2023.10154497
Duque Antón AMüller JFadiheh MStoffel DKunz W(2023)Fault Attacks on Access Control in Processors: Threat, Formal Analysis and Microarchitectural MitigationIEEE Access10.1109/ACCESS.2023.3280804(1-1)Online publication date: 2023
https://doi.org/10.1109/ACCESS.2023.3280804
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents