Exploring the Abyss? Unveiling Systems-on-Chip Hardware Vulnerabilities Beneath Software

被引:1
作者
Rajendran, Sree Ranjani [1 ]
Dipu, Nusrat Farzana [1 ]
Tarek, Shams [1 ]
Kamali, Hadi Mardani [1 ]
Farahmandi, Farimah [1 ]
Tehranipoor, Mark [1 ]
机构
[1] Univ Florida, Dept Elect & Comp Engn, Gainesville, FL 32611 USA
关键词
Security; Hardware; Testing; Software; Databases; Fuzzing; Codes; System-on-chip (SoC); security verification; security properties; SW-exploitable hardware vulnerabilities; COST;
D O I
10.1109/TIFS.2024.3372800
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Due to the increasing size and complexity of system-on-chips (SoCs), new threats and vulnerabilities are emerging, mainly related to flaws at the system level. Due to the lack of decisive security requirements and properties from the perspective of the SoC designer, the system-level verification process, whose violation may lead to exploiting a hardware vulnerability, is not studied comprehensively. To enable more comprehensive verification of system-level properties, this paper presents a framework known as HUnTer (Hardware Underath Trigger) for identifying sets of instructions (sequences) at the processor unit (PU) that reveal the underlying hardware vulnerabilities. HUnTer automates (i) threat modeling, (ii) threat-based formal verification, (iii) generating counterexamples, and (iv) generating snippet code to exploit the vulnerability. Furthermore, the HUnTer framework defines a unique security coverage metric (HUnT_Coverage) to measure the performance and effectiveness of vulnerability exploits. To demonstrate the high effectiveness of the proposed framework, we conduct a wide variety of case studies using the HUnTer framework on RISC-V-based open-source SoC architecture and attains the security coverage of 86% as an average for 11 benchmarks of the Trust-Hub database.
引用
收藏
页码:3914 / 3926
页数:13
相关论文
共 46 条
[1]  
Ahmed Alif, Scalable Hardware Trojan Activation by Interleaving Concrete Simulation and Symbolic Execution
[2]   SHarPen: SoC Security Verification by Hardware Penetration Test [J].
Al-Shaikh, Hasan ;
Vafaei, Arash ;
Rahman, Mridha Md Mashahedur ;
Azar, Kimia Zamiri ;
Rahman, Fahim ;
Farahmandi, Farimah ;
Tehranipoor, Mark .
2023 28TH ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, ASP-DAC, 2023, :579-584
[3]  
Ardeshiricham A, 2017, DES AUT TEST EUROPE, P1691, DOI 10.23919/DATE.2017.7927266
[4]  
Asanovic K., 2016, Tech. Rep. UCB/EECS-2016-17, V4
[5]  
Asanovicet K, 2014, Tech. Rep. UCB/EECS-2014-146
[6]  
Azar Kimia Zamiri, 2022, Cryptology ePrint Archive, V2022, P1
[7]  
Barnum Sean., 2008, Common attack pattern enumeration and classification (capec) schema description
[8]   Security Analysis of a System-on-Chip Using Assertion-Based Verification [J].
Bhamidipati, Padmaja ;
Achyutha, Shanmukha Murali ;
Vemur, Ranga .
2021 IEEE INTERNATIONAL MIDWEST SYMPOSIUM ON CIRCUITS AND SYSTEMS (MWSCAS), 2021, :826-831
[9]  
Bhunia S., 2018, HARDWARE SECURITY HA
[10]   Automata-based assertion-checker synthesis of PSL properties [J].
Boule, Marc ;
Zilic, Zeljko .
ACM TRANSACTIONS ON DESIGN AUTOMATION OF ELECTRONIC SYSTEMS, 2008, 13 (01)