Abstract
Security of a system on chip (SoC) can be weakened by exploiting the inherent and potential vulnerabilities of the intellectual property (IP) cores used to implement the design as well as the interaction among the IPs. These vulnerabilities not only increase the security verification effort but also can increase design complexity and time to market. If the design and verification engineers are equipped with a comprehensive set of security properties at the early stage of a design process, SoC security validation effort can be greatly reduced. This chapter explains how one can use property-based verification for security validation of designs. We describe in detail how to identify the security assets and threat models needed to build security attributes and describe how security attributes are developed to protect against security vulnerabilities. Finally, we provide a step-by-step process on how to validate the generated assertions with design examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ahmed, A., Farahmandi, F., Iskander, Y., Mishra, P.: Scalable hardware Trojan activation by interleaving concrete simulation and symbolic execution. In: 2018 IEEE International Test Conference (ITC), pp. 1–10. IEEE (2018)
Anandakumar, N.N., Dillibabu, S.: Correlation power analysis attack of AES on FPGA using customized communication protocol. In: Proceedings of the Second International Conference on Computational Science, Engineering and Information Technology, CCSEIT ’12, pp. 683–688 (2012)
Anandakumar, N.N., Sanadhya, S.K., Hashmi, M.S.: FPGA-based true random number generation using programmable delays in oscillator-rings. IEEE Trans. Circuits Syst. Express Briefs 67(3), 570–574 (2020). https://doi.org/10.1109/TCSII.2019.2919891
ARM, L.: Arm security technology-building a secure system using trustzone technology. Tech. rep., PRD-GENC-C. ARM Ltd. Apr.(cit. on p.), Tech. Rep (2009)
Biswas, L.K., Lavdas, L., Rahman, M.T., Tehranipoor, M., Asadizanjani, N.: On backside probing techniques and their emerging security threats. IEEE Des. Test 39(6), 172–179 (2022). https://doi.org/10.1109/MDAT.2022.3185797
Cadence: JasperGold Formal Propert Verification. URL https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform/formal-property-verification-app.html
Cadence: JasperGold Security Path Verification. URL https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform/security-path-verification-app.html
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transfer 2(4), 410–425 (2000)
Cycuity: Cycuity Radix Solutions
Eslami, M., Ghavami, B., Raji, M., Mahani, A.: A survey on fault injection methods of digital integrated circuits. Integration 71, 154–163 (2020). https://doi.org/10.1016/j.vlsi.2019.11.006. URL https://www.sciencedirect.com/science/article/pii/S016792601930402X
Farahmandi, F., Morad, R., Ziv, A., Nevo, Z., Mishra, P.: Cost-effective analysis of post-silicon functional coverage events. In: Design, Automation & Test in Europe Conference & Exhibition (DATE), 2017, pp. 392–397. IEEE (2017)
Farzana, N., Ayalasomayajula, A., Rahman, F., Farahmandi, F., Tehranipoor, M.: SAIF: Automated asset identification for security verification at the register transfer level. In: 2021 IEEE 39th VLSI Test Symposium (VTS), pp. 1–7. IEEE (2021)
Farzana, N., Rahman, F., Tehranipoor, M., Farahmandi, F.: SoC Security verification using property checking. In: 2019 IEEE International Test Conference (ITC), pp. 1–10. IEEE (2019)
Foster, H.D.: Property specification: the key to an assertion-based verification platform. In: Proceedings of Electronic Design Processes (EDP) Workshop (2003)
Gomina, K., Rigaud, J.B., Gendrier, P., Candelier, P., Tria, A.: Power supply glitch attacks: design and evaluation of detection circuits. In: 2014 IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), pp. 136–141 (2014). https://doi.org/10.1109/HST.2014.6855584
Gruninger, M., Menzel, C.: The process specification language (PSL) theory and applications. AI Mag. 24(3), 63–63 (2003)
Guo, X., Dutta, R.G., Jin, Y., Farahmandi, F., Mishra, P.: Pre-silicon security verification and validation: a formal perspective. In: 2015 52nd ACM/EDAC/IEEE Design Automation Conference (DAC), pp. 1–6 (2015). https://doi.org/10.1145/2744769.2747939
JasperGold Formal Fundamentals Cadence . URL https://www.cadence.com/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform.html
Kim, Y., Daly, R., Kim, J., Fallin, C., Lee, J.H., Lee, D., Wilkerson, C., Lai, K., Mutlu, O.: Flipping bits in memory without accessing them: an experimental study of dram disturbance errors. SIGARCH Comput. Archit. News 42(3), 361–372 (2014). https://doi.org/10.1145/2678373.2665726. URL https://doi.org/10.1145/2678373.2665726
Kocher, P., Horn, J., Fogh, A., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: exploiting speculative execution. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 1–19 (2019). https://doi.org/10.1109/SP.2019.00002
Lipp, M., Schwarz, M., Gruss, D., Prescher, T., Haas, W., Fogh, A., Horn, J., Mangard, S., Kocher, P., Genkin, D., Yarom, Y., Hamburg, M.: Meltdown: reading kernel memory from user space. In: 27th USENIX Security Symposium (USENIX Security 18) (2018)
Nahiyan, A., Sadi, M., Vittal, R., Contreras, G., Forte, D., Tehranipoor, M.: Hardware Trojan detection through information flow security verification. In: 2017 IEEE International Test Conference (ITC), pp. 1–10. IEEE (2017)
Nahiyan, A., Xiao, K., Yang, K., Jin, Y., Forte, D., Tehranipoor, M.: AVFSM: a framework for identifying and mitigating vulnerabilities in FSMs. In: Proceedings of the 53rd Annual Design Automation Conference, pp. 1–6 (2016)
Ning, B., Liu, Q.: Modeling and efficiency analysis of clock glitch fault injection attack. In: 2018 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pp. 13–18 (2018). https://doi.org/10.1109/AsianHOST.2018.8607175
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46–57. IEEE (1977)
Ray, S., Peeters, E., Tehranipoor, M.M., Bhunia, S.: System-on-chip platform security assurance: architecture and validation. Proc. IEEE 106(1), 21–37 (2018). https://doi.org/10.1109/JPROC.2017.2714641
Synopsys: Synopsys VC Formal
Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for SystemVerilog Assertions. Springer Science & Business Media, Berlin (2005)
Wang, H., Forte, D., Tehranipoor, M.M., Shi, Q.: Probing attacks on integrated circuits: challenges and research opportunities. IEEE Des. Test 34(5), 63–71 (2017). https://doi.org/10.1109/MDAT.2017.2729398
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Tehranipoor, M., Nalla Anandakumar, N., Farahmandi, F. (2023). Security Verification. In: Hardware Security Training, Hands-on!. Springer, Cham. https://doi.org/10.1007/978-3-031-31034-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-31034-8_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-31033-1
Online ISBN: 978-3-031-31034-8
eBook Packages: EngineeringEngineering (R0)