Ensuring that a computer chip or other semiconductor-based component does exactly what it the customer wants it to do, and nothing else, is becoming more challenging. Feature sizes continue to shrink and are measured in nanometers, circuits are more complex, and design and manufacture involves a supply chain typically comprising many businesses worldwide. Threats range from improper performance or early failure to allowing access to those with malicious intent.

Semiconductor design and manufacture depends on a “pipeline of tools,” with each tool outputting something that is closer to describing what is actually produced and sold. One form of supply-chain attack involves corrupting one or more stages of this tools pipeline, so that the output of the pipeline exhibits undesirable functionality.

The programming languages community has, over the last two decades, addressed closely related problems with solutions such as “proof carrying code” and “certifying compilation” that derive from formal methods. Work in “compiler correctness” also is relevant. By analogy, semiconductor supply-chain attack might be frustrated if both the artifact and an analysis are transmitted between successive pipeline stages, with the analysis being updated by each stage. The updates would establish that properties checked by analysis in prior pipeline stages are preserved in the current pipeline stage. That is, each pipeline stage performs a kind of refinement and checks that the refinement does not invalidate properties that previous stages validated. At the final stage, an accompanying analysis would rationalize the role of each element in the output of the pipeline.

Participation in the one-and-a-half day workshop was by invitation only. The output will be a report outlining the problems and areas of research that have the potential to lead to solutions.