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 条
  • [1] The compositional security checker: A tool for the verification of information flow security properties
    Focardi, R
    Gorrieri, R
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1997, 23 (09) : 550 - 571
  • [2] Isadora: automated information-flow property generation for hardware security verification
    Deutschbein, Calvin
    Meza, Andres
    Restuccia, Francesco
    Kastner, Ryan
    Sturton, Cynthia
    JOURNAL OF CRYPTOGRAPHIC ENGINEERING, 2023, 13 (04) : 391 - 407
  • [3] Isadora: automated information-flow property generation for hardware security verification
    Calvin Deutschbein
    Andres Meza
    Francesco Restuccia
    Ryan Kastner
    Cynthia Sturton
    Journal of Cryptographic Engineering, 2023, 13 : 391 - 407
  • [4] On Automated Generation of Checker Units from Hardware Assertion Languages
    Fibich, Christian
    Wenzl, Matthias
    Roessler, Peter
    2014 MICROELECTRONIC SYSTEMS SYMPOSIUM (MESS), 2014,
  • [5] Theorem proof based gate level information flow tracking for hardware security verification
    Qin, Maoyuan
    Hu, Wei
    Wang, Xinmu
    Mu, Dejun
    Mao, Baolei
    COMPUTERS & SECURITY, 2019, 85 : 225 - 239
  • [6] Security Verification of RISC-V System Based on ISA Level Information Flow Tracking
    Wu, Lingjuan
    Gao, Yifei
    Zhu, Jiacheng
    Tai, Yu
    Hu, Wei
    2023 IEEE 32ND ASIAN TEST SYMPOSIUM, ATS, 2023, : 195 - 200
  • [7] The invariant checker: Automated deductive verification of reactive systems
    Saidi, H
    COMPUTER AIDED VERIFICATION, 1997, 1254 : 436 - 439
  • [8] SVA Checker Generator for FPGA-Based Verification Platform
    Mohamad, Nurita
    Ooi, Chia Yee
    Ismail, Nordinah
    Teh, Jwing
    2016 IEEE INTERNATIONAL SYMPOSIUM ON CIRCUITS AND SYSTEMS (ISCAS), 2016, : 1750 - 1753
  • [9] Security policy checker and generator for Java']Java mobile codes
    Kaiya, H
    Furukawa, H
    Kaijiri, K
    ENGINEERING INFORMATION SYSTEMS IN THE INTERNET CONTEXT, 2002, 103 : 255 - 264
  • [10] Information flow query and verification for security policy of Security-Enhanced Linux
    Chen, Yi-Ming
    Kao, Yung-Wei
    ADVANCES IN INFORMATION AND COMPUTER SECURITY, PROCEEDINGS, 2006, 4266 : 389 - 404