  Logic locking "hides" the functionality of a digital circuit to protect it
from counterfeiting, piracy, and malicious design modifications. The original
design is transformed into a "locked" design such that the circuit reveals its
correct functionality only when it is "unlocked" with a secret sequence of
bits--the key bit-string. However, strong attacks, especially the SAT attack
that uses a SAT solver to recover the key bitstring, have been profoundly
effective at breaking the locked circuit and recovering the circuit
functionality.
  We lift logic locking to Higher Order Logic Locking (HOLL) by hiding a
higher-order relation, instead of a key of independent values, challenging the
attacker to discover this key relation to recreate the circuit functionality.
Our technique uses program synthesis to construct the locked design and
synthesize a corresponding key relation. HOLL has low overhead and existing
attacks for logic locking do not apply as the entity to be recovered is no more
a value. To evaluate our proposal, we propose a new attack (SynthAttack) that
uses an inductive synthesis algorithm guided by an operational circuit as an
input-output oracle to recover the hidden functionality. SynthAttack is
inspired by the SAT attack, and similar to the SAT attack, it is verifiably
correct, i.e., if the correct functionality is revealed, a verification check
guarantees the same. Our empirical analysis shows that SynthAttack can break
HOLL for small circuits and small key relations, but it is ineffective for
real-life designs.
