A Formal Approach to Accountability in Heterogeneous Systems-on-Chip

Systems-on-chip (SoCs) are increasingly being composed of designs provided by different organizations. When such an SoC miscomputes or performs below expectation in-field, it is unclear which of the on-chip components caused the failure. The customer would like to use SoCs that provide the property of accountability, wherein the failure-causing component, and consequently its designing organization, can be unambiguously detected. Since it is a matter of trust, the various parties involved desire formal guarantees regarding any accountability solution. The solution must find the guilty component(s) in the event of a chip failure. Additionally, the solution must not falsely implicate any component that functioned correctly. This article formally describes the property of accountability, a formal methodology of constructing an accountability solution, and a formal game-theory based methodology to reason about and prove the viability of a proposed solution. We explore the entire space of solutions, and characterize the attack surface and methods to provide accountability for each setting. We show non-intuitive results in this article where seemingly simple solutions actually provide very powerful theoretical guarantees in terms of accountability.