"A key result of this work as applied to existing hardware will be whether it is possible to assign less-than-complete trust to any of the black-box components

"A key result of this work as applied to existing hardware will be whether it is possible to assign less-than-complete trust to any of the black-box components in an SoC, or whether current HW design practices are incompatible with building secure, correct systems." Having been exploring this research area for a while I fear it is the latter and there is no clean formal model that will apply to real hardware as currently construed.