-
Analysis of Linux-PRNG (Pseudo Random Number Generator)
Authors:
Ayush Bansal,
Pramod Subramanyan,
Satyadev Nandakumar
Abstract:
The Linux pseudorandom number generator (PRNG) is a PRNG with entropy inputs and is widely used in many security-related applications and protocols. This PRNG is written as an open-source code which is subject to regular changes. It has been analysed in the works of Gutterman et al., Lacharme et al., while in the meantime, several changes have been applied to the code, to counter the attacks prese…
▽ More
The Linux pseudorandom number generator (PRNG) is a PRNG with entropy inputs and is widely used in many security-related applications and protocols. This PRNG is written as an open-source code which is subject to regular changes. It has been analysed in the works of Gutterman et al., Lacharme et al., while in the meantime, several changes have been applied to the code, to counter the attacks presented since then. Our work describes the Linux PRNG of kernel versions 5.3 and upwards. We discuss the PRNG architecture briefly and in detail about the entropy mixing function.
Our goal is to study the entropy mixing function and analyse it over two properties, namely, injectivity and length of the longest chain. For this purpose, we will be using SAT solving and model counting over targetted formulas involving multiple states of the Linux entropy store.
△ Less
Submitted 6 December, 2023;
originally announced December 2023.
-
Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
Authors:
Shubham Sahai,
Rohit Sinha,
Pramod Subramanyan
Abstract:
Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number…
▽ More
Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number of different traces. In this paper, we introduce a technique for verification of quantitative hyperproperties based on the notion of trace enumeration relations. These relations allow us to reduce the problem of trace-counting into one of model-counting of formulas in first-order logic. We also introduce a set of inference rules for machine-checked reasoning about the number of satisfying solutions to first-order formulas (aka model counting). Putting these two components together enables semi-automated verification of quantitative hyperproperties on infinite state systems. We use our methodology to prove confidentiality of access patterns in Path ORAMs of unbounded size, soundness of a simple interactive zero-knowledge proof protocol as well as other applications of quantitative hyperproperties studied in past work.
△ Less
Submitted 14 May, 2020; v1 submitted 10 May, 2020;
originally announced May 2020.
-
Functional Analysis Attacks on Logic Locking
Authors:
Deepak Sirone,
Pramod Subramanyan
Abstract:
Logic locking refers to a set of techniques that can protect integrated circuits (ICs) from counterfeiting, piracy and malicious functionality changes by an untrusted foundry. It achieves these goals by introducing new inputs, called key inputs, and additional logic to an IC such that the circuit produces the correct output only when the key inputs are set to specific values. The correct values of…
▽ More
Logic locking refers to a set of techniques that can protect integrated circuits (ICs) from counterfeiting, piracy and malicious functionality changes by an untrusted foundry. It achieves these goals by introducing new inputs, called key inputs, and additional logic to an IC such that the circuit produces the correct output only when the key inputs are set to specific values. The correct values of the key inputs are kept secret from the untrusted foundry and programmed after manufacturing and before distribution, rendering piracy, counterfeiting and malicious design changes infeasible. The security of logic locking relies on the assumption that the untrusted foundry cannot infer the correct values of the key inputs by analysis of the circuit.
This paper proposes Functional Analysis attacks on Logic Locking algorithms (abbreviated as FALL attacks). FALL attacks have two stages. Their first stage is dependent on the locking algorithm and involves analyzing structural and functional properties of locked circuits to identify a list of potential locking keys. The second stage is algorithm agnostic and introduces a powerful addition to SAT-based attacks called key confirmation. Key confirmation can identify the correct key from a list of alternatives and works even on circuits that are resilient to the SAT attack. In comparison to past work, the FALL attack is more practical as it can often succeed (90% of successful attempts in our experiments) by only analyzing the locked netlist, without requiring oracle access to an unlocked circuit. Our experimental evaluation shows that FALL attacks are able to defeat 65 out of 80 (81%) circuits locked using Stripped-Functionality Logic Locking (SFLL-HD).
△ Less
Submitted 10 January, 2020; v1 submitted 29 November, 2018;
originally announced November 2018.
-
Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification
Authors:
Bo-Yuan Huang,
Hongce Zhang,
Pramod Subramanyan,
Yakir Vizel,
Aarti Gupta,
Sharad Malik
Abstract:
Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to the pre-accelerator era, when the ISA played an important role in verification by enabling a clean separation of concerns between software and hardware, verification of these "accelerator-rich" SoCs presents new challenges…
▽ More
Modern Systems-on-Chip (SoC) designs are increasingly heterogeneous and contain specialized semi-programmable accelerators in addition to programmable processors. In contrast to the pre-accelerator era, when the ISA played an important role in verification by enabling a clean separation of concerns between software and hardware, verification of these "accelerator-rich" SoCs presents new challenges. From the perspective of hardware designers, there is a lack of a common framework for the formal functional specification of accelerator behavior. From the perspective of software developers, there exists no unified framework for reasoning about software/hardware interactions of programs that interact with accelerators. This paper addresses these challenges by providing a formal specification and high-level abstraction for accelerator functional behavior. It formalizes the concept of an Instruction Level Abstraction (ILA), developed informally in our previous work, and shows its application in modeling and verification of accelerators. This formal ILA extends the familiar notion of instructions to accelerators and provides a uniform, modular, and hierarchical abstraction for modeling software-visible behavior of both accelerators and programmable processors. We demonstrate the applicability of the ILA through several case studies of accelerators (for image processing, machine learning, and cryptography), and a general-purpose processor (RISC-V). We show how the ILA model facilitates equivalence checking between two ILAs, and between an ILA and its hardware finite-state machine (FSM) implementation. Further, this equivalence checking supports accelerator upgrades using the notion of ILA compatibility, similar to processor upgrades using ISA compatibility.
△ Less
Submitted 14 June, 2018; v1 submitted 3 January, 2018;
originally announced January 2018.
