[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
10.1145/3240765.3240839guideproceedingsArticle/Chapter ViewAbstractPublication PagesConference Proceedingsacm-pubtype
research-article

Property Specific Information Flow Analysis for Hardware Security Verification

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
[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
[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
[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

Cited By

View all
  • (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
  • (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
  • (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
  • Show More Cited By

Index Terms

  1. Property Specific Information Flow Analysis for Hardware Security Verification
        Index terms have been assigned to the content through auto-classification.

        Recommendations

        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

        Publisher

        IEEE Press

        Publication History

        Published: 05 November 2018

        Permissions

        Request permissions for this article.

        Qualifiers

        • Research-article

        Contributors

        Other Metrics

        Bibliometrics & Citations

        Bibliometrics

        Article Metrics

        • Downloads (Last 12 months)0
        • Downloads (Last 6 weeks)0
        Reflects downloads up to 11 Dec 2024

        Other Metrics

        Citations

        Cited By

        View all
        • (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
        • (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
        • (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
        • (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
        • (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
        • (2023)JinnProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620627(6965-6982)Online publication date: 9-Aug-2023
        • (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
        • (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
        • (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
        • (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
        • Show More Cited By

        View Options

        View options

        Login options

        Media

        Figures

        Other

        Tables

        Share

        Share

        Share this Publication link

        Share on social media