Convergence of Software Assurance Methodologies and Trustworthy Semiconductor Design and Manufacture (SA+TS)
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.
January 15, 2013 (Tuesday)
|07:30 AM||Continental breakfast|
|08:30 AM||Welcome and Overview of the Workshop
Senior Government Official (TBD)
|09:00 AM||Plenary Session 1: Overview of Semiconductor Design and Manufacture (with an eye toward the future)
Semiconductor Manufacture Tools & Processes and Potential Vulnerabilities (20 mins )— Kevin Kemp, Freescale
Semiconductor Design Tools & Processes and Potential Vulnerabilities (20 mins )— Juan Rey, Mentor Graphics
Top-to-bottom integrative design & verification (20 mins) — Carl Seger, Intel
|11:00 AM||Plenary Session 2: Overview of Software Assurance Methodologies
Thinking about attacks / minimizing trusted base (20 mins)—A. Appel, Princeton
CompCert as a software tool chain (20 minutes)—D. Pichardie, INRIA/Harvard
Specifying the HW/SW interface (20 minutes)—P. Sewell, Cambridge
|12:30 AM||Working Lunch
Reality of hardware vulnerability—F. Kiamlev, U. Delaware
|01:30 PM||Breakout sessions
(3 groups of 12-15 with mix of specialty and industry/academic; facilitated discussion on specified questions)
|05:00 PM||Preliminary Breakout reports
(5 min each; bring forward one or two issues/ideas for consideration by all)
Semiconductor Research Corporation
Program Associate, Computing Community Consortium, Computing Research Association
National Science Foundation
Semiconductor Research Corporation
Advanced Micro Devices
University of Washington
The Computing Community Consortium (CCC) covers travel expenses for all participants who desire it. Participants will be asked to make their own travel arrangements in advance, including purchasing airline tickets and making hotel reservations at the workshop hotel (see above). Following the symposium, CCC will circulate a reimbursement form that participants will need to complete and submit, along with copies of receipts for amounts exceeding $75.
In general, standard Federal travel policies apply: CCC will reimburse for non-refundable economy airfare on U.S. Flag carriers; per diem amounts will be enforced; and no alcohol will be covered.
Additional questions about the reimbursement policy should be directed to Kenneth Hines, Program Associate, CCC (khines [at] cra.org).