Hardware Security
Most semiconductor companies don’t the resources to manufacture computer chips. Advanced semiconductor chips are manufactured at one of a small number of “fabs” and several countries, India for example, do not have any on-shore fab. So, chip manufacturing is outsourced off-shore. But this raises a question of trust: how can we guarantee the security of off-shore chip fabrication?
The video above summarizes some of our prior and ongoing work in the area of hardware security. Broadly, we seek to develop defenses against hardware Trojans attacks and semiconductor IP theft.
Split Manufacturing: In our USENIX Security’13 paper (winner of the Best Student Paper Award) on split manufacturing — in this work, we proposed to partition a chip into two or more sub-components, each fabricated at a separate foundry. No one foundry sees the entire design, hindering its ability to thieve the chip’s IP or maliciously modify the chip. While the idea is both intuitive and appealing, our work was the first to propose a formal, quantitative metric for split manufacturing that we refer to as k-security. The k-security metric has subsequently been used in several follow on papers, for instance in our ICCAD’17 paper with NYU Abu Dhabi colleagues, we established new information-theoretic metrics for the security of split manufacturing against so-called proximity attacks, and leveraged these metrics to reduce the overheads of split manufacturing.
Logic Obfuscation: Another promising solution to the problem of IP piracy is IC camouflaging (and a related technique, logic locking); the idea is to obfuscate the Boolean functionality of a subset of gates in the IC so as to deter or prevent reverse engineering. In my NDSS’15 paper, we proposed the SAT attack, an extremely powerful and comprehensive attack on the then state-of-the-art IC camouflaging scheme. Built on a fresh, complexity- theoretic characterization of the attacker’s problem, our attack was able to reverse engineer in minutes camouflaged netlists that prior work had claimed would take hundreds of years to reverse. Using the same complexity-theoretic mindset, I demonstrated at ICCAD’17 a new model-checking attack against camouflaged sequential circuits. Subsequent to our SAT attack, there has been a flurry of work on devising “SAT attack resilient” defenses. However, in testament to the power of our attacks, all proposed defenses have been defeated and no general, low-cost, provably secure defense exists to this day. Indeed, the SAT attack has become a de-facto standard to evaluate the security of any new camouflaging or logic locking scheme. In recognition of its long-term impact, the SAT attack paper was recently selected as one of seven Top Picks in Hardware and Embedded Systems Security from amongst hardware security papers published between 2012-2017.
Verifiable ASICS: A third major contribution to the area of hardware security is our work, in collaboration with Michael Walfish from NYU and abhi shelat from Northeastern, on verifiable ASICs at Oakland’16 that received the Distinguished Student Paper Award. Our is the first provably secure defense against hardware Trojans. Prior work in this area has typically offered only heuristic defense strategies or has made assumptions on the design of the Trojan, for example, that Trojans introduce measurable power and/or delay penalties, or are triggered in certain ways. In contrast, the verifiable ASICs defense does not make any such assumptions; instead, we seek to detect, in the field, any Trojan that modifies the IC’s input/output functionality. We do so by leveraging powerful protocols developed by cryptographers for verifiable outsourced computing; the problem of checking that a function computed by a third-party untrusted server is correct. We have subsequently used the machinery of interactive proofs to develop verifiable hardware for matrix multiplication and deep network inference