Visible to the public Biblio

Filters: Keyword is Hardware design languages  [Clear All Filters]
Mouris, Dimitris, Georgios Tsoutsos, Nektarios.  2020.  Pythia: Intellectual Property Verification in Zero-Knowledge. 2020 57th ACM/IEEE Design Automation Conference (DAC). :1–6.
The contemporary IC supply chain depends heavily on third-party intellectual property (3PIP) that is integrated to in-house designs. As the correctness of such 3PIPs should be verified before integration, one important challenge for 3PIP vendors is proving the functionality of their designs while protecting the privacy of circuit implementations. In this work, we present Pythia that employs zero-knowledge proofs to enable vendors convince integrators about the functionality of a circuit without disclosing its netlist. Pythia automatically encodes netlists into zero knowledge-friendly format, evaluates them on different inputs, and proves correctness of outputs. We evaluate Pythia using the ISCAS'85 benchmark suite.
Guo, Xiaolong, Dutta, Raj Gautam, He, Jiaji, Tehranipoor, Mark M., Jin, Yier.  2019.  QIF-Verilog: Quantitative Information-Flow based Hardware Description Languages for Pre-Silicon Security Assessment. 2019 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). :91—100.
Hardware vulnerabilities are often due to design mistakes because the designer does not sufficiently consider potential security vulnerabilities at the design stage. As a result, various security solutions have been developed to protect ICs, among which the language-based hardware security verification serves as a promising solution. The verification process will be performed while compiling the HDL of the design. However, similar to other formal verification methods, the language-based approach also suffers from scalability issue. Furthermore, existing solutions either lead to hardware overhead or are not designed for vulnerable or malicious logic detection. To alleviate these challenges, we propose a new language based framework, QIF-Verilog, to evaluate the trustworthiness of a hardware system at register transfer level (RTL). This framework introduces a quantified information flow (QIF) model and extends Verilog type systems to provide more expressiveness in presenting security rules; QIF is capable of checking the security rules given by the hardware designer. Secrets are labeled by the new type and then parsed to data flow, to which a QIF model will be applied. To demonstrate our approach, we design a compiler for QIF-Verilog and perform vulnerability analysis on benchmarks from Trust-Hub and OpenCore. We show that Trojans or design faults that leak information from circuit outputs can be detected automatically, and that our method evaluates the security of the design correctly.
Gillela, Maruthi, Prenosil, Vaclav, Ginjala, Venkat Reddy.  2019.  Parallelization of Brute-Force Attack on MD5 Hash Algorithm on FPGA. 2019 32nd International Conference on VLSI Design and 2019 18th International Conference on Embedded Systems (VLSID). :88—93.
FPGA implementation of MD5 hash algorithm is faster than its software counterpart, but a pre-image brute-force attack on MD5 hash still needs 2ˆ(128) iterations theoretically. This work attempts to improve the speed of the brute-force attack on the MD5 algorithm using hardware implementation. A full 64-stage pipelining is done for MD5 hash generation and three architectures are presented for guess password generation. A 32/34/26-instance parallelization of MD5 hash generator and password generator pair is done to search for a password that was hashed using the MD5 algorithm. Total performance of about 6G trials/second has been achieved using a single Virtex-7 FPGA device.
Das, Rakesh, Chattopadhyay, Anupam, Rahaman, Hafizur.  2019.  Optimizing Quantum Circuits for Modular Exponentiation. 2019 32nd International Conference on VLSI Design and 2019 18th International Conference on Embedded Systems (VLSID). :407–412.

Today's rapid progress in the physical implementation of quantum computers demands scalable synthesis methods to map practical logic designs to quantum architectures. There exist many quantum algorithms which use classical functions with superposition of states. Motivated by recent trends, in this paper, we show the design of quantum circuit to perform modular exponentiation functions using two different approaches. In the design phase, first we generate quantum circuit from a verilog implementation of exponentiation functions using synthesis tools and then apply two different Quantum Error Correction techniques. Finally the circuit is further optimized using the Linear Nearest Neighbor (LNN) Property. We demonstrate the effectiveness of our approach by generating a set of networks for the reversible modular exponentiation function for a set of input values. At the end of the work, we have summarized the obtained results, where a cost analysis over our developed approaches has been made. Experimental results show that depending on the choice of different QECC methods the performance figures can vary by up to 11%, 10%, 8% in T-count, number of qubits, number of gates respectively.

E.V., Jaideep Varier, V., Prabakar, Balamurugan, Karthigha.  2019.  Design of Generic Verification Procedure for IIC Protocol in UVM. 2019 3rd International Conference on Electronics, Communication and Aerospace Technology (ICECA). :1146-1150.

With the growth of technology, designs became more complex and may contain bugs. This makes verification an indispensable part in product development. UVM describe a standard method for verification of designs which is reusable and portable. This paper verifies IIC bus protocol using Universal Verification Methodology. IIC controller is designed in Verilog using Vivado. It have APB interface and its function and code coverage is carried out in Mentor graphic Questasim 10.4e. This work achieved 83.87% code coverage and 91.11% functional coverage.

Guo, X., Dutta, R. G., He, J., Jin, Y..  2017.  PCH framework for IP runtime security verification. 2017 Asian Hardware Oriented Security and Trust Symposium (AsianHOST). :79–84.

Untrusted third-party vendors and manufacturers have raised security concerns in hardware supply chain. Among all existing solutions, formal verification methods provide powerful solutions in detection malicious behaviors at the pre-silicon stage. However, little work have been done towards built-in hardware runtime verification at the post-silicon stage. In this paper, a runtime formal verification framework is proposed to evaluate the trust of hardware during its execution. This framework combines the symbolic execution and SAT solving methods to validate the user defined properties. The proposed framework has been demonstrated on an FPGA platform using an SoC design with untrusted IPs. The experimentation results show that the proposed approach can provide high-level security assurance for hardware at runtime.

Kwon, H., Harris, W., Esmaeilzadeh, H..  2017.  Proving Flow Security of Sequential Logic via Automatically-Synthesized Relational Invariants. 2017 IEEE 30th Computer Security Foundations Symposium (CSF). :420–435.

Due to the proliferation of reprogrammable hardware, core designs built from modules drawn from a variety of sources execute with direct access to critical system resources. Expressing guarantees that such modules satisfy, in particular the dynamic conditions under which they release information about their unbounded streams of inputs, and automatically proving that they satisfy such guarantees, is an open and critical problem.,,To address these challenges, we propose a domain-specific language, named STREAMS, for expressing information-flow policies with declassification over unbounded input streams. We also introduce a novel algorithm, named SIMAREL, that given a core design C and STREAMS policy P, automatically proves or falsifies that C satisfies P. The key technical insight behind the design of SIMAREL is a novel algorithm for efficiently synthesizing relational invariants over pairs of circuit executions.,,We expressed expected behavior of cores designed independently for research and production as STREAMS policies and used SIMAREL to check if each core satisfies its policy. SIMAREL proved that half of the cores satisfied expected behavior, but found unexpected information leaks in six open-source designs: an Ethernet controller, a flash memory controller, an SD-card storage manager, a robotics controller, a digital-signal processing (DSP) module, and a debugging interface.