Researcher profile

Pramod Subramanyan

Pramod Subramanyan contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 13 - UnverifiedVerification L1Unclaimed author
2works
0followers
1topics
3close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

2 published item(s)

preprint2020arXiv

Functional Analysis Attacks on Logic Locking

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).

preprint2020arXiv

Verification of Quantitative Hyperproperties Using Trace Enumeration Relations

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.