Gate-Level Information Flow Tracking for Security Lattices

被引:26
|
作者
Hu, Wei [1 ]
Mu, Dejun [1 ]
Oberg, Jason [2 ]
Mao, Baolei [3 ]
Tiwari, Mohit [4 ]
Sherwood, Timothy [5 ]
Kastner, Ryan [6 ]
机构
[1] Northwestern Polytech Univ, Sch Automat, Xian, Shaanxi, Peoples R China
[2] Univ Calif San Diego, Dept Comp Sci & Engn, La Jolla, CA 92093 USA
[3] Northwestern Polytech Univ, Sch Automat, Xian, Shaanxi, Peoples R China
[4] Univ Texas Austin, Dept Elect & Comp Engn, Austin, TX 78712 USA
[5] Univ Calif Santa Barbara, Dept Comp Sci, Santa Barbara, CA 93106 USA
[6] Univ Calif San Diego, Dept Comp Sci & Engn, La Jolla, CA 92093 USA
基金
美国国家科学基金会;
关键词
Security; Design; Verification; High-assurance system; hardware security; gate-level information flow tracking; multilevel security; security lattice; formal method;
D O I
10.1145/2676548
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
High-assurance systems found in safety-critical infrastructures are facing steadily increasing cyber threats. These critical systems require rigorous guarantees in information flow security to prevent confidential information from leaking to an unclassified domain and the root of trust from being violated by an untrusted party. To enforce bit-tight information flow control, gate-level information flow tracking (GLIFT) has recently been proposed to precisely measure and manage all digital information flows in the underlying hardware, including implicit flows through hardware-specific timing channels. However, existing work in this realm either restricts to two-level security labels or essentially targets two-input primitive gates and several simple multilevel security lattices. This article provides a general way to expand the GLIFT method for multilevel security. Specifically, it formalizes tracking logic for an arbitrary Boolean gate under finite security lattices, presents a precise tracking logic generation method for eliminating false positives in GLIFT logic created in a constructive manner, and illustrates application scenarios of GLIFT for enforcing multilevel information flow security. Experimental results show various trade-offs in precision and performance of GLIFT logic created using different methods. It also reveals the area and performance overheads that should be expected when expanding GLIFT for multilevel security.
引用
收藏
页码:1 / 25
页数:25
相关论文
共 50 条
  • [41] BLOX ELIMINATES GATE-LEVEL DESIGN FOR FPGAS
    TUCK, B
    COMPUTER DESIGN, 1991, 30 (14): : 136 - 136
  • [42] Delay-insensitive gate-level pipelining
    Smith, SC
    DeMara, RF
    Yuan, JS
    Hagedorn, M
    Ferguson, D
    INTEGRATION-THE VLSI JOURNAL, 2001, 30 (02) : 103 - 131
  • [43] A gate-level timing model for SOI circuits
    Shahriari, M
    Naim, FN
    ICECS 2001: 8TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS, VOLS I-III, CONFERENCE PROCEEDINGS, 2001, : 795 - 798
  • [44] Improving Gate-Level Simulation of Quantum Circuits
    George F. Viamontes
    Igor L. Markov
    John P. Hayes
    Quantum Information Processing, 2003, 2 : 347 - 380
  • [45] Formal Verification of Gate-Level Computer Systems
    Hillebrand, Mark
    Tverdyshev, Sergey
    COMPUTER SCIENCE - THEORY AND APPLICATIONS, 2009, 5675 : 322 - +
  • [46] EASILY TESTABLE GATE-LEVEL AND DCVS MULTIPLIERS
    TAKACH, AR
    JHA, NK
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 1991, 10 (07) : 932 - 942
  • [47] A gate-level model for morphogenetic evolvable hardware
    Lee, J
    Sitte, J
    2004 IEEE INTERNATIONAL CONFERENCE ON FIELD-PROGRAMMABLE TECHNOLOGY, PROCEEDINGS, 2004, : 113 - 119
  • [48] FSMx-Ultra: Finite State Machine Extraction From Gate-Level Netlist for Security Assessment
    Kibria, Rasheed
    Farahmandi, Farimah
    Tehranipoor, Mark
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2023, 42 (11) : 3613 - 3627
  • [49] Induction-based gate-level verification of multipliers
    Chang, YT
    Cheng, KTT
    ICCAD 2001: IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, DIGEST OF TECHNICAL PAPERS, 2001, : 190 - 193
  • [50] Optimal Design on Asynchronous System with Gate-level Pipelining
    Tamura, Masato
    Ito, Atsushi
    Ikeda, Makoto
    PROCEEDINGS OF 2015 IEEE 11TH INTERNATIONAL CONFERENCE ON ASIC (ASICON), 2015,