Automated Assertion Checker Generator and Information Flow Tracking for Security Verification

被引:0
|
作者
Zapata, Miguel Angel Alfaro [1 ]
Shahshahani, Amirhossein [1 ]
Zilic, Zeljko [1 ]
机构
[1] McGill Univ, Elect & Comp Engn, Montreal, PQ, Canada
关键词
Automated Assertion Checker Generator; Information Leakage; Information Flow Tracking; Security Validation;
D O I
10.1109/ISQED60706.2024.10528770
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
The increasing complexity of designs and the emergence of hardware security vulnerabilities pose challenges to efficient verification. This paper presents an automated tool that integrates Information Flow Tracking (IFT), automated assertion generation, and hardware assertion checkers to detect information leakage vulnerabilities on hardware designs. The tool generates tagged RTL models using IFT techniques and automatically generates security assertions based on specified secure assets. The security assertions are then converted into hardware assertion checkers. The tool was evaluated on various RTL designs, and the impact on FPGA resource utilization was measured. The results show that our tool successfully generates security assertions and assertion checkers, providing a systematic approach to security verification in hardware designs.
引用
收藏
页数:6
相关论文
共 50 条
  • [21] Challenges in the automated verification of security protocols
    Comon-Lundh, Hubert
    AUTOMATED REASONING, PROCEEDINGS, 2008, 5195 : 396 - 409
  • [22] Automated verification of security pattern compositions
    Dong, Jing
    Peng, Tu
    Zhao, Yajing
    INFORMATION AND SOFTWARE TECHNOLOGY, 2010, 52 (03) : 274 - 295
  • [24] VERICA-Verification of Combined Attacks: Automated formal verification of security against simultaneous information leakage and tampering
    Richter-Brockmann J.
    Feldtkeller J.
    Sasdrich P.
    Güneysu T.
    IACR Transactions on Cryptographic Hardware and Embedded Systems, 2022, 2022 (04): : 255 - 284
  • [25] AGILE: Automated Assertion Generation to Detect Information Leakage Vulnerabilities
    Dipu, Nusrat Farzana
    Ayalasomayajula, Avinash
    Tehranipoor, Mark M.
    Farahmandi, Farimah
    IEEE TRANSACTIONS ON INFORMATION FORENSICS AND SECURITY, 2024, 19 : 1794 - 1809
  • [26] Imprecise Security: Quality and Complexity Tradeoffs for Hardware Information Flow Tracking
    Hu, Wei
    Becker, Andrew
    Ardeshiricham, Armita
    Tai, Yu
    Lenne, Paolo
    Mu, Dejun
    Kastner, Ryan
    2016 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2016,
  • [27] Security and Fault Diagnosis-Based Assertion-Based Verification for FPGA
    Zhang, Shasha
    Cao, Liang
    2019 COMPANION OF THE 19TH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY (QRS-C 2019), 2019, : 478 - 481
  • [28] Security Analysis of a System-on-Chip Using Assertion-Based Verification
    Bhamidipati, Padmaja
    Achyutha, Shanmukha Murali
    Vemur, Ranga
    2021 IEEE INTERNATIONAL MIDWEST SYMPOSIUM ON CIRCUITS AND SYSTEMS (MWSCAS), 2021, : 826 - 831
  • [29] Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis
    Ferraiuolo, Andrew
    Xu, Rui
    Zhang, Danfeng
    Myers, Andrew C.
    Suh, G. Edward
    ACM SIGPLAN NOTICES, 2017, 52 (04) : 555 - 568
  • [30] An information flow security policy verification methodology and its application in operating systems
    Yi, XD
    Yang, XJ
    Proceedings of the 11th Joint International Computer Conference, 2005, : 700 - 703